Logic Journal of IGPL Advance Access originally published online on November 14, 2008
Logic Journal of IGPL 2008 16(6):499-536; doi:10.1093/jigpal/jzn018
| ||||||||||||||||||||||||||||||||||||||||||||||||||||
A Sound and Complete Deductive System for CTL* Verification*
King's College, London. E-mail: dov.gabbay{at}kcl.ac.uk
New York University, Courant Institute. E-mail: amir{at}cs.nyu.edu
 |
Abstract |
|---|
The paper presents a compositional approach to the verification of CTL* properties over reactive systems. Both symbolic model-checking (SMC) and deductive verification are considered. Both methods are based on two decomposition principles. A general state formula is decomposed into basic state formulas which are CTL* formulas with no embedded path quantifiers. To deal with arbitrary basic state formulas, we introduce another reduction principle which replaces each basic path formula, i.e., path formulas whose principal operator is temporal and which contain no embedded temporal operators or path quantifiers, by a newly introduced boolean variable which is added to the system. Thus, both the algorithmic and the deductive methods are based on two statification transformations which successively replace temporal formulas by assertions which contain no path quantifiers or temporal operators. Performing these decompositions repeatedly, we remain with basic assertional formulas, i.e., formulas of the form Efp and Afp for some assertion p. In the model-checking method we present a single symbolic algorithm to verify both universal and existential basic assertional properties. In the deductive method we present a small set of proof rules and show that this set is sound and relatively complete for verifying universal and existential basic assertional properties over reactive systems. Together with two proof rules for the decompositions, we obtain a sound and relatively complete proof system for arbitrary CTL* properties. Interestingly, the deductive approach for CTL* presented here, offers a viable new approach to the deductive verification of arbitrary LTL formulas.
The paper corrects a previous preliminary version of a deductive system for CTL*, in which some of the rules were unsound. The correction is based on the introduction of a new type of temporal testers which are guaranteed to be non blocking. That is, when composed with a deadlock-free system, which is a key operation in the verification process, the resulting composed system is guaranteed to remain deadlock free.
Received for publication 23 April 2007.
*This research was supported in part by EPSRC grant GR/D 504457.