Tableaux and Sequent Calculi for CTL and ECTL: Satisfiability Test with Certifying Proofs and Models

Abstract

Certifying proofs are automated deductive proofs obtained as outcomes of a formal verification of temporal properties, where model checking is one of the most promi- nent approaches. The satisfiability problem for the Computation Tree Logic (CTL) cannot be reduced to the CTL model checking problem. Hence model checking algo- rithms for CTL cannot be adapted for testing CTL satisfiability. However, any decision procedure of CTL satisfiability can perform model checking tasks. Our context-based tableau approach to CTL satisfiability introduces a tree-style one-pass tableau that does not require auxiliary constructions or extra-logical rules for branch pruning. As a con- sequence this method brings the classical duality between tableaux and sequent calculi in temporal logic. For any input formula, a closed tableau represents a formal sequent proof that certifies the unsatisfiability of the input, whereas an open tableau provides at least a model certifying the satisfiability of the input formula. Hence, in this framework the satisfiability test can be performed and complemented with certifying proofs and models. This is also true in relation to more expressive branching-time logic, Extended CTL (ECTL), which enriches CTL with simple fairness formulae. This paper contin- ues the development of dual systems of tableau method and sequent calculi, introduc- ing these techniques for CTL and ECTL. We prove the soundness and completeness of both methods and define algorithms for obtaining systematic tableaux which produce models and formal proofs (as certificates) depending on whether the input formulae are satisfiable or not. We also describe the implementation of this technique and provide experimental results.