Skip Navigation


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
This Article
Right arrow Abstract Freely available
Right arrow Full Text (PDF)
Right arrow Alert me when this article is cited
Right arrow Alert me if a correction is posted
Services
Right arrow Email this article to a friend
Right arrow Similar articles in this journal
Right arrow Alert me to new issues of the journal
Right arrow Add to My Personal Archive
Right arrow Download to citation manager
Right arrowRequest Permissions
Google Scholar
Right arrow Articles by Gabbay, D. M.
Right arrow Articles by Pnueli, A.
Right arrow Search for Related Content
Social Bookmarking
Add to CiteULike   Add to Connotea   Add to Del.icio.us  
What's this?

Vol. 16 No. 6, © The Author 2008. Published by Oxford University Press. All rights reserved. For Permissions, please email: journals.permissions@oxfordjournals.org

A Sound and Complete Deductive System for CTL* Verification*

Dov M. Gabbay

King's College, London. E-mail: dov.gabbay{at}kcl.ac.uk

Amir Pnueli

New York University, Courant Institute. E-mail: amir{at}cs.nyu.edu

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.



References

    [BBC+95]  Bjørner N, Browne IA, Chang E, Colón M, Kapur A, Manna Z, Sipma HB, Uribe TE. STeP: The Stanford Temporal Prover, User's Manual. In: Technical Report STAN-CS-TR-95-1562 (1995) November. Computer Science Department, Stanford University.

    [BCM+92]  Burch JR, Clarke EM, McMillan KL, Dill DL, Hwang J. Symbolic model checking: 1020states and beyond. In: Information and Computation (1992) 98((2)):142–170.[CrossRef][Web of Science]

    [CGH94]  Clarke EM, Grumberg O, Hamaguchi K. Another look at LTLmodel checking. In: Proc. 6th Conference on Computer Aided Verification, volume 818 of Lect. Notes in Comp. Sci.—Dill DL, ed. (1994) Springer-Verlag. 415–427.

    [Cho74]  Choueka Y. Theories of automata on {omega}-tapes: A simplified approach. In: J. Comp. Systems Sci. (1974) 8:117–141.[CrossRef]

    [EH86]  Emerson EA, Halpern JY. ‘Sometimes’ and ‘not never’ revisited: On branching time versus linear time. In: J. ACM (1986) 33:151–178.[CrossRef]

    [EL87]  Emerson EA, Lei C. Modalities for model checking: Branching time logic strikes back. In: Science of Computer Programming (1987) 8:275–306.[CrossRef][Web of Science]

    [Eme90]  Emerson EA. Temporal and modal logics. In: Handbook of theoretical computer science—van Leeuwen J, ed. (1990) volume B. Elsevier. 995–1072.

    [Gab87]  Gabbay D. The declarative past and imperative future. In: Temporal Logic in Specification, volume 398 of Lect. Notes in Comp. Sci.—Banieqbal B, Barringer H, Pnueli A, eds. (1987) Springer-Verlag. 407–448.

    [KP00]  Kesten Y, Pnueli A. Control and data abstractions: The cornerstones of practical formal verification. In: Software Tools for Technology Transfer (2000) 2((1)):328–342.[CrossRef]

    [KP02]  Kesten Y, Pnueli A. A Deductive Proof System for CTL*. In: 13th International Conference on Concurrency Theory (CONCUR02), volume 2421 of Lect. Notes in Comp. Sci. (2002) Springer-Verlag. 24–39.

    [KP05]  Kesten Y, Pnueli A. A compositional approach to CTL* verification. In: Theor. Comp. Sci. (2005) 331:397–428.[CrossRef]

    [KPR98]  Kesten Y, Pnueli A, Raviv L. Algorithmic verification of linear temporal logic specifications. In: Proc. 25th Int. Colloq. Aut. Lang. Prog. volume 1443 of Lect. Notes in Comp. Sci.—Larsen KG, Skyum S, Winskel G, eds. (1998) Springer-Verlag. 1–16.

    [KPRS06]  Kesten Y, Pnueli A, Raviv L, Shahar E. LTL model checking with strong fairness. In: Formal Methods in System Design (2006) 28((1)):57–84.[CrossRef][Web of Science]

    [Lam80]  Lamport L. ‘sometimes’ is sometimes ‘not never’: A tutorial on the temporal logic of programs. In: Proc. 7th ACM Symp. Princ. of Prog. Lang. (1980) 174–185.

    [LP85]  Lichtenstein O, Pnueli A. Checking that finite-state concurrent programs satisfy their linear specification. In: Proc. 12th ACM Symp. Princ. of Prog. Lang. (1985) 97–107.

    [LPS81]  Lehmann D, Pnueli A, Stavi J. Impartiality, justice and fairness: The ethics of concurrent termination. In: Proc. 8th Int. Colloq. Aut. Lang. Prog. volume 115 of Lect. Notes in Comp. Sci. (1981) Springer-Verlag. 264–277.

    [MP91a]  Manna Z, Pnueli A. Completing the temporal picture. In: Theor. Comp. Sci. (1991) 83((1)):97–130.[CrossRef]

    [MP91b]  Manna Z, Pnueli A. The Temporal Logic of Reactive and Concurrent Systems: Specification (1991) New York: Springer-Verlag.

    [MP95]  Manna Z, Pnueli A. Temporal Verification of Reactive Systems: Safety (1995) New York: Springer-Verlag.

    [Nam01]  Namajoshi KS. Certifying model checkers. In: Proc. 13rdIntl. Conference on Computer Aided Verification (CAV'01), volume 2102 of Lect. Notes in Comp. Sci. (2001) Springer-Verlag. 2–13.

    [PK03]  Pnueli Amir, Kesten Yonit. Models, Algebras and Logic of Engineering Software, volume 191 of NATO Science Series: Computer and Systems Science (2003) IOS Press. 109–132. chapter Algorithmic and Deductive Verification Methods for CTLS*.

    [PPZ01]  Peled D, Pnueli A, Zuck L. From falsification to verification. In: Proc. 21st Conference on Foundations of Software Technology and Theroretical Computer Science (FSTTCS'01), volume 2245 of Lect. Notes in Comp. Sci. (2001) Springer-Verlag. 292–304.

    [PR88]  Pnueli A, Rosner R. A framework for the synthesis of reactive modules. In: Proc. Intl. Conf. on Concurrency: Concurrency 88, volume 335 of Lect. Notes in Comp. Sci.—Vogt FH, ed. (1988) Springer-Verlag. 4–17.

    [Rey01]  Reynolds M. An axiomatization of full computation tree logic. In: J. Symb. Logic (2001) 66((3)):1011–1057.[CrossRef]

    [SdRG89]  Stomp FA, de Roever W-P, Gerth RT. The µ-calculus as an assertion language for fairness arguments. In: Inf. and Comp. (1989) 82:278–322.[CrossRef]

    [Spr00]  Sprenger C. On the Verification of CTL* (2000) Properties of Infinite-State Reactive Systems. PhD thesis, Swiss Federal Institute of Technology, Lausanne.

    [SUM99]  Sipma HB, Uribe TE, Manna Z. Deductive model checking. In: Formal Methods in System Design (1999) 15((1)):49–74.[CrossRef][Web of Science]

    [Var91]  Vardi MY. Verification of concurrent programs – the automata-theoretic framework. In: Annals of Pure Applied Logic (1991) 51:79–98.[CrossRef]


Add to CiteULike CiteULike   Add to Connotea Connotea   Add to Del.icio.us Del.icio.us    What's this?



This Article
Right arrow Abstract Freely available
Right arrow Full Text (PDF)
Right arrow Alert me when this article is cited
Right arrow Alert me if a correction is posted
Services
Right arrow Email this article to a friend
Right arrow Similar articles in this journal
Right arrow Alert me to new issues of the journal
Right arrow Add to My Personal Archive
Right arrow Download to citation manager
Right arrowRequest Permissions
Google Scholar
Right arrow Articles by Gabbay, D. M.
Right arrow Articles by Pnueli, A.
Right arrow Search for Related Content
Social Bookmarking
Add to CiteULike   Add to Connotea   Add to Del.icio.us  
What's this?