Decidability of quantifed propositional branching time logics

Abstract

We extend the branching temporal logics CTL and CTL* with quantified propositions and consider various semantic interpretations for the quantification. The use of quantificiation greatly increases the expressive power of the logics allowing us to represent, for example, tree-automata. We also show that some interpretations of quantification allow us to represent non-propositional properties of Kripke frames, such as the branching degree of trees. However this expressive power may also make the satisfiability problem for the logic undecidable. We give a proof of one such case, and also examine decidability in the less expressive semantics.