Computing Reviews
Today's Issue Hot Topics Search Browse Recommended My Account Log In
Review Help
Completeness and decidability results for CTL in constructive type theory
Doczkal C., Smolka G. Journal of Automated Reasoning56 (3):343-365,2016.Type:Article
Date Reviewed: Jul 15 2016

The following sentence from the rather demanding introduction to this quite demanding paper reveals common ground between us users of formal methods and the expert authors of this paper: “Given the practical importance of CTL [computation tree logic] and the complexity of the proofs of the metatheoretic results for CTL, we think that the metatheory of CTL is an interesting and rewarding candidate for formalization.” As a user of model-checking methods of verifying the correctness of safety-critical systems and software, I can vouch for the “practical importance” of CTL [1] in the safety assurance of rapid transit and several other real-life applications. Formalization seems the only means of overcoming the complexity of proofs--such that the proofs are believable by us users (and indeed by the proofs’ originators).

Stated sketchily, CTL models time via a tree structure comprising logical, possibly infinite, paths. Ordinary Boolean connectives, such as “and,” “or,” and “not,” are each prefixed with a pair of quantifiers/qualifiers such as AX: AllPaths/NeXtState [1]. The paper’s “main result” is a constructive proof that every CTL formula has either a finite model that satisfies it, or there is an axiom-based proof of the formula’s unsatisfiability. The paper reflects heavy use of the Coq proof assistant [2], and focuses on constructive logic. It is very interesting that if constructive constraints, namely the law of the excluded middle and a choice axiom, are loosened, then all models are sound.

This well-researched, substantive, and original paper is aimed at experts in applied proof theory and the foundations of formal methods. I’m very happy to have read it, as it confirmed for me the solidity of formal methods, especially those based on constructive logic.

Reviewer:  George Hacken Review #: CR144588 (1611-0831)
1) Huth, M.; Ryan, M. Logic in computer science (2nd ed.). Cambridge University Press, Cambridge, UK, 2004.
2) Chlipala, A. Certified programming with dependent types. MIT Press, Cambridge, MA, 2013.
Bookmark and Share
  Featured Reviewer  
Logic And Constraint Programming (F.4.1 ... )
Mechanical Verification (F.3.1 ... )
Deduction And Theorem Proving (I.2.3 )
Process Management (D.4.1 )
Software/ Program Verification (D.2.4 )
Would you recommend this review?
Other reviews under "Logic And Constraint Programming": Date
Negation by default and unstratifiable logic programs
Bidoit N., Froidevaux C. Theoretical Computer Science 78(1): 85-112, 1991. Type: Article
Feb 1 1992
Programming in three-valued logic
Delahaye J. (ed), Thibau V. Theoretical Computer Science 78(1): 189-216, 1991. Type: Article
Jan 1 1992
Essentials of logic programming
Hogger C., Oxford University Press, Inc., New York, NY, 1990. Type: Book (9780198538325)
Sep 1 1992

E-Mail This Printer-Friendly
Send Your Comments
Contact Us
Reproduction in whole or in part without permission is prohibited.   Copyright 1999-2024 ThinkLoud®
Terms of Use
| Privacy Policy