Logical square-driven and state-oriented generation of behavioural models

The accurate defining states in a newly designed state machine diagram can be a challenge, especially if we are not domain experts. There is an idea of the square of opposition in classical logic, which is highly informative and can support analysts when shaping states for behavioural models. We proposed an identification method employing a square-driven and state-oriented approach, ideally suited for cases where analysts struggle with understanding the investigated domain or in applications that demand rigorous adherence to formal methodologies. State identification is augmented by the encoding of state variables representing particular states and predicates along with the analysis in a logical style. We have shown a simple yet inspiring example to illustrate the entire methodology in a satisfactory manner.