Quantified CTL: expressiveness and complexity

DOI10.2168/LMCS-10(4:17)2014MaRDI QIDQ2938770zbMATH OpenFDO

Authors François Laroussinie, Nicolas Markey

Publication date 15 January 2015

Published in Logical Methods in Computer Science (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1411.4332

zbMATH Keywords

expressivenessmodel checkingtemporal logicstree automata

Mathematics Subject Classification ID

Temporal logic (03B44) Computational difficulty of problems (lower bounds, completeness, difficulty of approximation, etc.) (68Q17) Specification and verification (program logics, model checking, etc.) (68Q60)

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).

Recommendations

• Quantified CTL: expressiveness and model checking (extended abstract)
• On the expressiveness of QCTL
• Quantified computation tree logic
• From quantified CTL to QBF
• \(\mathsf{QCTL}\) model-checking with \(\mathsf{QBF}\) solvers

Cited in

(33)

• On the expressivity and complexity of quantitative branching-time temporal logics
• Quantified computation tree logic
• Second-order propositional modal logic: expressiveness and completeness results
• Cycle detection in computation tree logic
• The power of first-order quantification over states in branching and linear time temporal logics
• Quantified CTL: expressiveness and model checking (extended abstract)
• On the complexity of \(\mathsf{ATL}\) and \(\mathsf{ATL}^*\) module checking
• A Tableau for Bundled CTL
• On the Expressive Power of QLTL
• Counting CTL
• On the expressiveness of QCTL
• Quirky quantifiers: optimal models and complexity of computation tree logic
• scientific article; zbMATH DE number 7438567 (Why is no real title available?)
• Undecidability of QLTL and QCTL with two variables and one monadic predicate letter
• Quantifying Bounds in Strategy Logic
• On temporal and separation logics
• scientific article; zbMATH DE number 7577569 (Why is no real title available?)
• Good-for-Game QPTL: An Alternating Hodges Semantics
• On Composing Finite Forests with Modal Logics
• An auxiliary logic on trees: on the tower-hardness of logics featuring reachability and submodel reasoning
• An auxiliary logic on trees: on the tower-hardness of logics featuring reachability and submodel reasoning
• To be announced
• Reasoning about Quality and Fuzziness of Strategic Behaviors
• From quantified CTL to QBF
• On the expressive power of the normal form for branching-time temporal logics
• Module checking of pushdown multi-agent systems
• QLTL model-checking
• Formal verification and synthesis of mechanisms for social choice
• Finitely defined preference and preference indiscernibility in ATL with strategy contexts
• Arbitrary-arity tree automata for QCTL
• Verification of multi-agent systems with public actions against strategy logic
• \(\mathsf{QCTL}\) model-checking with \(\mathsf{QBF}\) solvers
• Augmenting ATL with strategy contexts

This page was built for publication: Quantified CTL: expressiveness and complexity

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2938770)