Publication details

Saarland University Computer Science

Completeness and Decidability Results for CTL in Constructive Type Theory

Christian Doczkal, Gert Smolka

Journal of Automated Reasoning 56(3):343-365, 2016

We prove completeness and decidability results for the temporal logic CTL in Coq/Ssreflect. Our main result is a constructive proof that for every formula one can obtain either a finite model satisfying the formula or a proof in a Hilbert system certifying the unsatisfiability of the formula. The small model property of CTL and completeness of the Hilbert system follow as corollaries. Our proofs mostly refine the mathematical proofs given by Emerson and Halpern. One important deviation is our use of an inductive semantics for CTL to avoid reasoning about infinite paths. On finite models the inductive semantics agrees constructively with the standard path semantics. The proof amounts to the verification of a simple model checking algorithm. For general models, the agreement between the inductive semantics and the path semantics requires excluded middle and dependent choice.

Coq Development

This is an extended and revised version of the ITP 2014 paper.

Download PDF        Show BibTeX               

Login to edit

Webmaster, Wed Sep 16 10:47:00 2009