Decidability of Quantifed Propositional Branching Time Logics

摘要

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.