Model Checking: How is everything connected

Introduction

This is the final blog in our series on Model Checking. Since we now have knowledge of typical modelling techniques (mainly Kripke structures) and property specification (using LTL and CTL), we are ready to understand how to check the correctness of properties in a given model.

Verification of LTL Formulas

Intersection of Büchi Automata

For two Büchi automata \(B\) and \(B’\), we can build a Büchi automaton for the intersection of their \(\omega\)-languages. The construction is similar to that of finite automata, where the resulting automaton’s states are pairs of states from both automata. This is also similar to the synchronous product of Kripke structures discussed in the previous blog.

The algorithm is defined as follows:

1. Input: Two Büchi automata \(B = (Q, \Sigma, \delta, Q_0, F)\) and \(B’ = (Q’, \Sigma, \delta’, Q’_0, F’)\).
2. Construct a new Büchi automaton \(B_{\cap}\) whose state space is \(Q \times Q’\).
3. The initial states are all pairs \((q, q’)\) where \(q \in Q_0\) and \(q’ \in Q’_0\).
4. The transition relation is defined synchronously: \((q, q’) \xrightarrow{a} (r, r’)\) if \(q \xrightarrow{a} r\) in \(B\) and \(q’ \xrightarrow{a} r’\) in \(B’\).
5. The set of accepting states is \(F \times F’\).
6. Return the Büchi automaton \(B_{\cap}\).

Emptiness Problem on Büchi Automata

Checking whether a Büchi automaton can produce any \(\omega\)-word at all is often called the emptiness problem. This is an efficient algorithm that traverses the automaton and checks for the existence of a lasso with at least one accepting state in its cycle. A lasso is a path from an initial state to a state that is reachable from itself.

The algorithm for checking whether a Büchi automaton is empty is given by:

1. Input: A Büchi automaton \(B = (Q, \Sigma, \delta, Q_0, F)\).
2. Compute the set of states reachable from the initial states \(Q_0\).
3. Compute the strongly connected components (SCCs) of the reachable subgraph.
4. Check whether there exists an SCC that contains at least one accepting state from \(F\) and at least one cycle.
5. If such an SCC exists, return non-empty.
6. Otherwise, return empty.

LTL Model Checking

In the previous blog, we discussed the transformation of both LTL formulae and Kripke structures into Büchi automata. These transformations form the core of LTL model checking. Let us assume that we have the automata \(B_M\) for the model and \(B_{\varphi}\) for the LTL formula \(\varphi\).

Checking the property on the model is equivalent to proving that the language of all possible paths generated by the model is a subset of the language generated by the formula. In other words, every execution of the model satisfies the property:

\[ L(B_M) \subseteq L(B_{\varphi}) \]

This can be rewritten as:

\[ L(B_M) \cap \overline{L(B_{\varphi})} = \emptyset \]

Using this formulation, the LTL model checking algorithm can be defined as follows:

1. Input: A Kripke structure \(M\) and an LTL formula \(\varphi\).
2. Build the Büchi automaton \(B_M\) for the model \(M\).
3. Build the Büchi automaton \(B_{\varphi}\) for the LTL formula \(\varphi\).
4. Construct the complement \(\overline{B_{\varphi}}\) (using Safra’s construction, later optimized by Piterman).
5. Build the intersection of \(B_M\) and \(\overline{B_{\varphi}}\).
6. Check whether the resulting Büchi automaton generates any word.
7. Return whether \(B_M \cap \overline{B_{\varphi}}\) is empty.

However, the construction in step 4 is expensive and often infeasible for large models, as it has a worst-case complexity of \(2^{O(n \log n)}\). For this reason, practical model checkers avoid explicit complementation.

Instead, we build the Büchi automaton for the negated formula \(\lnot \varphi\), leading to a more efficient algorithm:

1. Input: A Kripke structure \(M\) and an LTL formula \(\varphi\).
2. Build the Büchi automaton \(B_M\) for the model \(M\).
3. Build the Büchi automaton \(B_{\lnot \varphi}\) for the LTL formula \(\lnot \varphi\).
4. Build the intersection of \(B_M\) and \(B_{\lnot \varphi}\).
5. Check whether the resulting Büchi automaton generates any word.
6. Return whether \(B_M \cap B_{\lnot \varphi}\) is empty.

Verification of CTL Formulas

Unlike LTL, CTL model checking is performed directly on the Kripke structure without translating formulas into automata. CTL formulas are evaluated using graph-based algorithms that rely on fixpoint computations, strongly connected components, and backward reachability. The following two algorithms are examples for CTL Model Checking, where the output are all the states on which the formula holds. Checking if a Kripke structure satisfies a CTL property is then checking if an initial state is in the set of the returned states.

EG Operator

The formula \(EG \, \varphi\) holds in a state if there exists a path starting from that state such that \(\varphi\) holds globally along the entire path.

1. Compute the set of states that satisfy \(\varphi\).
2. Restrict the Kripke structure to these states.
3. Compute the strongly connected components of the restricted graph.
4. Mark states that belong to SCCs containing a cycle.
5. Return all states that can reach such SCCs.

EU Operator

The formula \(\varphi \, EU \, \psi\) holds in a state if there exists a path where \(\psi\) eventually holds and \(\varphi\) holds at all preceding states.

1. Initialize a set with all states that satisfy \(\psi\).
2. Iteratively add states that satisfy \(\varphi\) and have a transition to a state already in the set.
3. Repeat until a fixpoint is reached.
4. Return the resulting set of states.

Conclusion

Model checking provides a powerful and fully automated technique for verifying complex systems, especially in security-critical and safety-critical domains. By rigorously exploring all possible executions, it can uncover subtle errors that are difficult to detect through testing alone.

Understanding the theoretical foundations behind model checking, including automata theory and temporal logic, allows practitioners to better appreciate its strengths, limitations, and practical optimizations. This knowledge is essential for effectively applying model checking to real-world systems.