Model Checking¶
Model checking is a technique to establish the set of states in Kripke structure that satisfy a given temporal formula. More formally, provided a Kripke structure \(K=(S,S_0,R,L)\) and a temporal formula \(\varphi\), model checking aims to identify \(S' \subseteq S\) such that
for all \(s_i \in S'\).
Model checking problem for CTL*, CTL and LTL is decidable even though the time complexity of the algorithm is logics dependent: the complexities of the CTL, LTL and CTL* decision procedures are \(O(|\varphi| * (|S|+|R|))\), \(O(2^{O(|\varphi|)} * (|S|+|R|))\) and \(O(2^{O(|\varphi|)} * (|S|+|R|))\), respectively.
Fair Model Checking¶
A fair Kripke structure is a Kripke structure \((S, S_0, R, L)\) added with a set of fair states \(F \subseteq S\). A fair path for it is an infinite path that passes through all the fair states infinitely often.
Fair model checking only considers fair paths. A fair state is a path from which at least one fair path originates.