Temporal Logic Model Checking as Automated Theorem Proving

Abstract

Model checking is an automatic technique for the verification of temporal properties of a system. In this technique, a system is represented as a labelled graph and the specification as a temporal logic formula. The core of temporal logic model checking is the reachability problem, which is not expressible in first-order logic (FOL); as a result, model checking of finite/infinite state systems without the use of iteration or abstraction is considered beyond the realm of automated FOL theorem provers. In this thesis, we focus on formulating the temporal logic model checking problem as a FOL theorem proving problem and use automated tools, such as SAT/SMT solvers to directly model check a system without the need for a fixed-point calculation or abstraction.

We present CTL-Live: a fragment of computational tree logic whose model checking for (infinite) Kripke structures is reducible to FOL validity checking. CTL-Live includes the CTL connectives that are often used to express liveness properties. We also derive decidability results about CTL-Live model checking by examining decidable subsets of FOL. We evaluate our reduction technique for CTL-Live model checking. Our case studies show that state-of-the-art SMT solvers are capable of verifying CTL-Live properties of infinite systems; moreover, the verification of an infinite state model can sometimes complete more quickly than verifying a finite version of the model. We prove the maximality of CTL-Live: we show that CTL-Live is the largest fragment of CTL whose model checking is reducible to FOL validity checking.

The maximality of CTL-Live implies that model checking safety properties requires a logic more expressive than FOL; as a result, we examine FOL plus transitive closure (FOLTC). We can reduce model checking of a more expressive fragment of CTL, which we call CTL\EG, to validity checking in FOLTC. CTL\EG is more expressive than CTL-Live and yet less expressive than CTL. By adding a finiteness restriction, we can reduce model checking of all of CTL with fairness constraints (CTLFC) formulas to validity checking in FOLTC. The finiteness restriction requires that the system under-study must have a finite number of states, but it does not require this number to be known. Reduction of CTLFC to FOLTC allows us to use the Alloy Analyzer for model checking. Our case studies show that the Alloy Analyzer can analyze CTLFC formulas up to the same scopes that Alloy models are analyzed.