An axiomatization of full Computation Tree Logic

1 September 2001

journal article
Published by Cambridge University Press (CUP) in The Journal of Symbolic Logic

Vol. 66 (3) , 1011-1057
https://doi.org/10.2307/2695091

Abstract

We give a sound and complete axiomatization for the full computation tree logic. CTL*, of R-generable models. This solves a long standing open problem in branching time temporal logic.

Keywords

This publication has 8 references indexed in Scilit:

Non-definability of the class of complete bundled trees
Logic Journal of the IGPL, 1999
Ockhamist Computational Logic: Past-Sensitive Necessitation in CTL
Journal of Logic and Computation, 1993
R-generability, and definability in branching time logics
Information Processing Letters, 1992
A finite axiomatization of the set of strongly valid Ockhamist formulas
Journal of Philosophical Logic, 1985
Deciding full branching time logic
Information and Control, 1984
An Irreflexivity Lemma with Applications to Axiomatizations of Conditions on Tense Frames
Published by Springer Nature ,1981
Decidability for branching time
Studia Logica, 1980
Testing and generating infinite sequences by a finite automaton
Information and Control, 1966