Computing Reviews
Today's Issue Hot Topics Search Browse Recommended My Account Log In
Review Help
Search
Completeness and decidability results for CTL in constructive type theory
Doczkal C., Smolka G.  Journal of Automated Reasoning 56 (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 ... )
 
 
Deduction And Theorem Proving (I.2.3 )
 
 
Mechanical Verification (F.3.1 ... )
 
 
Process Management (D.4.1 )
 
 
Software/ Program Verification (D.2.4 )
 
Would you recommend this review?
yes
no
Other reviews under "Logic And Constraint Programming": Date
Probability logics: probability-based formalization of uncertain reasoning
Ognjanović Z., Rašković M., Marković Z.,  Springer International Publishing, New York, NY, 2016. 215 pp. Type: Book (978-3-319470-11-5)
Jun 5 2017
Bivalent semantics, generalized compositionality and analytic classic-like tableaux for finite-valued logics
Caleiro C., Marcos J., Volpe M.  Theoretical Computer Science 603(C): 84-110, 2015. Type: Article
Jan 13 2016
Constraint programming and decision making
Ceberio M., Kreinovich V.,  Springer Publishing Company, Incorporated, New York, NY, 2014. 200 pp. Type: Book (978-3-319042-79-4)
Nov 5 2014
more...

E-Mail This Printer-Friendly
Send Your Comments
Contact Us
Reproduction in whole or in part without permission is prohibited.   Copyright © 2000-2017 ThinkLoud, Inc.
Terms of Use
| Privacy Policy