Model Checking: How to model my system?

Introduction

As the goal of this series is to learn how model checking works and how it helps us check the correctness of models, our first step is to define the model of our system. This clearly requires a full understanding of the system and its components.

In general, one would like to see the model in front of their eyes to check if it satisfies the system’s properties and requirements. On the other hand, one would not like to exaggerate the description of the system to the point where it becomes more complex than our brain can process. This is why, in general, one defines independent components without their actual interaction with the other components. Then, using our brain delegate, the computer, we can connect those interacting components into one big model.

In this blog, we will investigate the data structures used in modelling and the possible “combination techniques” which allow the generation of our model from the smaller interactive components.

Kripke structures

Kripke structures are transition systems in the form of directed graphs which allow the modelling of a system using states and propositions. Formally, for a given set of propositions (i.e. Boolean variables), a Kripke structure is defined as a tuple of:

• A set of states S
• A set of initial states I
• A set of edges, called transitions R. Each transition is a directed edge going from one state to another.
• A labelling function L, i.e. a mapping from states to proposition sets. The labelling of a state characterizes it by the fact that every proposition in the labelling is true and every other is false. For example, for a set of propositions {a, b, c}, at the state s labelled by L(s) = {a}, only the proposition a holds; b and c do not.

To understand this structure more, we can directly start with an example. An elevator in a building with 3 floors (including the ground floor) can be working or out of service, and can be at one of the floors 1, 2, or 3. With this information, we can define the set of propositions:

AP = {w, f1, f2, f3}

where w represents the proposition “Elevator is working” and each fi represents the proposition “Elevator is at floor i”. With that, one can model the elevator with the following Kripke structure.

The model defines 6 states, s1 to s6. We directly wrote the labelling of each state (the corresponding proposition set) within the state in the given diagram.

We suppose that the elevator is initially working without knowing its current position. This is why we defined the states s1, s2, and s3 as initial states. The states s4 to s6 represent the out-of-service elevator states which can happen at any floor. We suppose, in our case, that the failure is permanent, i.e. it cannot cure by itself once it happens. This is the reason we only have a loop for the elevator at these states, as they can only stay at the same floor and can never become working again.

A path produced by a Kripke structure is an infinite list of states, starting with an initial state and only moving to one of the states to which it is connected. In our example, the path s2, s3, s3, s2, s3, s3, s1, s4, s4, s4… is produced by the given Kripke structure. This is, however, not the case for the path s1, s2, s3, s1, s4, s4… because we cannot move from s3 to s1 directly.

An execution is the infinite list of labels of a path. For example, for s1, s2, s3, s1, s4, s4…, we have the execution {w,f1}{w,f2}{w,f3}{w,f1}{f1}{f1}{f1}…

Transition systems

A (labelled) transition system (LTS) is very similar to a Kripke structure except for one big point of difference: an LTS defines the properties/actions of the model on its transitions, while a Kripke structure defines them on the states. Again, an LTS is defined as a tuple of:

• A set of states S
• A set of initial states
• A set of actions A
• A set of edges, called transitions R. Each transition is a directed edge going from one state to another and is labelled with an action. There are special edges connected directly to the initial states and are only labelled with guards which are the conditions that the graph must satisfy if it starts at that state.

An LTS concentrates more on the dynamics of the system, i.e. how, when, and under which conditions it actually changes, instead of what should hold at each state.

To model our previous example as an LTS, we define the set of actions A = {goto1, goto2, goto3, oos} (oos stands for out-of-service) and initial s1, and define it as follows:

A path produced by an LTS is, again, a valid infinite list of states. An execution is an infinite list of actions that is valid in our LTS. For example, s1, s2, s3, s2, s3, s2, s3… is a path produced by our example LTS. The execution [goto1][goto2][goto1]… is not valid in our LTS as s1, our initial state, cannot execute the action goto1.

Program Graphs

Although program graphs are harder to define, they are in general the most intuitive ones to use when you model your system. This is especially the case when you have parallel subsystems interacting with each other, yet able to run some of their subtasks independently.

Imagine having three independent elevators that can work. Modelling this system is a challenge, as each state must contain information on all elevators at the same time. Let’s do some computation:

Each elevator can be in one of 6 states (as in the example Kripke structure), which means that their combination will have 6*6*6 = 216 states! You can see that looking at such a Kripke structure and probably looking for a mistake you made while modelling could be hell, especially given the fact that this resulting Kripke structure will have 468 transitions.

This is where program graphs can simplify this for us. A program graph is defined, again, as a tuple consisting of:

• A set of integer variables V, each with a given number range. For example, a variable x defined within the interval [0, 5] is a valid variable that can be used in the program graph. Boolean variables are then a special case of the integer variables where the range is [0,1].
• A set of states S, each having its own name.
• A labelling L for the states S which is a bijection from S to [1, |S|]. This allows a new variable S in V which defines the state at which the program graph currently is.
• A set of labelled transitions R. A transition is, as in the other definitions, a directed edge from one state to another. The label of the transition, however, is of the form φ/α. φ is the set of guards of the transition. Each guard is a Boolean expression that only allows the transition to be activated when it evaluates to true. α is a set of actions. An action is an assignment of one expression to a variable. However, an action cannot change the variable S (which changes the state of that program graph).

A system is in general a set of program graphs that can interact with each other. For example, having three elevators can be defined as this set of three program graphs with variables {Elevator1, Elevator2, Elevator3, working1, working2, working3} where Elevator_i can take values from {1,2,3} corresponding to the state of the graph (the value is in the graph labelled under the state’s name) and working_i are Boolean variables to indicate if Elevator_i is working.

As the program graphs do not interact, each graph does not use variables of the other graphs. However, this is not always the case. For instance, if elevator 1 works only when elevator 2 is out-of-service, the special edge to elevator2_i will have guard working2 == 1 AND working1 == 0.

Summary

In this post, we explored how to model systems as a first step toward understanding model checking. We discussed the need to represent a system clearly—capturing its behavior without unnecessary complexity.

We introduced three main modelling structures:

1. Kripke structures – model systems through states and propositions that describe what holds true at each point.
2. Transition systems – focus on actions and how the system changes over time.
3. Program graphs – use variables, guards, and actions to describe complex or interacting subsystems.

Together, these approaches form the base of how we represent and analyze systems before applying model checking to verify their correctness.

Resources and Further Reading

To explore more about the concepts discussed in this post — such as Kripke structures, transition systems, and program graphs — the following resources provide clear definitions, examples, and formal details:

• Kripke Structure (Wikipedia) – A concise explanation of Kripke structures and their use in temporal logic and model checking.
• Labelled Transition System – Overview of transition systems, their components, and relation to system behaviour modelling.
• Program Graphs – Describes how program graphs are used to represent the control flow and state of concurrent systems.
• Model Checking – General overview of model checking as a verification technique and its connection to system modelling.

For a broader theoretical background and to connect these concepts together, the following references are recommended:

• Principles of Model Checking – Christel Baier and Joost-Pieter Katoen, MIT Press, 2008.
• Model Checking – Edmund M. Clarke, Orna Grumberg, and Doron A. Peled, MIT Press, 1999.
• Christel Baier and Joost-Pieter Katoen, Principles of Model Checking, MIT Press, 2008.
  Comprehensive coverage of the theoretical foundations of model checking, including Kripke structures, LTS, temporal logics, and program graph semantics.
• Edmund M. Clarke, Orna Grumberg, and Doron A. Peled, Model Checking, MIT Press, 1999.
  A classic text introducing the principles of model construction, verification techniques, and the practical side of state-space exploration.
• Koushik Sen and Gábor Holzmann, Model Checking: From Tools to Theory, Communications of the ACM, Vol. 56, No. 11, 2013.
  An accessible article linking theoretical model checking to its use in real-world software and concurrent systems.
• Gerard J. Holzmann, The SPIN Model Checker: Primer and Reference Manual, Addison-Wesley, 2004.
  A practical introduction to modelling concurrent systems using labelled transition systems and program graphs, with hands-on examples.
• M. Ben-Ari, Mathematical Logic for Computer Science, Springer, 2012.
  Explains the logical foundations of system modelling and verification, with examples of Kripke structures and temporal logic semantics.

These materials expand on the definitions, formalisms, and examples introduced in this blog, providing a deeper understanding of how system models are defined and verified.