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.