Quantified CTL: Expressiveness and Complexity

Abstract

While it was defined long ago, the extension of CTL with quantification over atomic propositions has never been studied extensively. Considering two different semantics (depending whether propositional quantification refers to the Kripke structure or to its unwinding tree), we study its expressiveness (showing in particular that QCTL coincides with Monadic Second-Order Logic for both semantics) and characterise the complexity of its model-checking and satisfiability problems, depending on the number of nested propositional quantifiers (showing that the structure semantics populates the polynomial hierarchy while the tree semantics populates the exponential hierarchy).

Cited by in corpus (11)

• The Hierarchy of Hyperlogics
• Strategy Logic with Imperfect Information
• Satisfiability of ATL with strategy contexts
• ATLsc with partial observation
• To Be Announced
• On the Complexity of ATL and ATL* Module Checking
• QCTL model-checking with QBF solvers
• Timed Systems through the Lens of Logic
• Why Does Propositional Quantification Make Modal and Temporal Logics on Trees Robustly Hard?
• On the Expressive Power of the Normal Form for Branching-Time Temporal Logics
• Modal Logics with Composition on Finite Forests: Expressivity and Complexity (Extra Material)