Quirky quantifiers: optimal models and complexity of computation tree logic

DOI10.1142/S0129054118500028MaRDI QIDQ4639929zbMATH OpenOpenAlexWikidataFDO

Authors Martin Lück

Publication date 14 May 2018

Published in International Journal of Foundations of Computer Science (Search for Journal in Brave)

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

zbMATH Keywords

computational complexityCTLfragmentssatisfiabilitytemporal logic

Mathematics Subject Classification ID

Temporal logic (03B44) Analysis of algorithms and problem complexity (68Q25)

Abstract: The satisfiability problem of the branching time logic CTL is studied in terms of computational complexity. Tight upper and lower bounds are provided for each temporal operator fragment. In parallel, the minimal model size is studied with a suitable notion of minimality. Thirdly, flat CTL is investigated, i.e., formulas with very low temporal operator nesting depth. A sharp dichotomy is shown in terms of complexity and minimal models: Temporal depth one has low expressive power, while temporal depth two is equivalent to full CTL.

Recommendations

• THE COMPLEXITY OF SATISFIABILITY FOR FRAGMENTS OF CTL AND CTL⋆
• The complexity of satisfiability for fragments of CTL and \(\text{CTL}^*\)
• Quantified CTL: expressiveness and complexity
• Quantified computation tree logic
• scientific article; zbMATH DE number 1512710

Cites work

• A near-optimal method for reasoning about action
• Alternation
• Automatic verification of finite-state concurrent systems using temporal logic specifications
• Decision procedures and expressiveness in the temporal logic of branching time
• Extremal combinatorics. With applications in computer science
• Finite model theory and its applications.
• Generalized modal satisfiability
• Handbook of modal logic
• scientific article; zbMATH DE number 3129315 (Why is no real title available?)
• scientific article; zbMATH DE number 3560737 (Why is no real title available?)
• scientific article; zbMATH DE number 1142326 (Why is no real title available?)
• scientific article; zbMATH DE number 2196601 (Why is no real title available?)
• Model Checking CTL is Almost Always Inherently Sequential
• On the Lambert \(w\) function
• Propositional dynamic logic of regular programs
• Satisfiability problems for propositional calculi
• The complexity of propositional linear temporal logics
• The complexity of propositional linear temporal logics in simple cases
• THE COMPLEXITY OF SATISFIABILITY FOR FRAGMENTS OF CTL AND CTL⋆
• The complexity of theorem-proving procedures
• The Computational Complexity of Provability in Systems of Modal Propositional Logic
• The effect of bounding the number of primitive propositions and the depth of nesting on the complexity of modal logic
• The Two-Valued Iterative Systems of Mathematical Logic. (AM-5)
• “Sometimes” and “not never” revisited

Cited in

(5)

• Parameterized complexity of CTL
• Branching-Time Temporal Logics with Minimal Model Quantifiers
• Branching-depth hierarchies
• scientific article; zbMATH DE number 7577569 (Why is no real title available?)
• Minimisation of models satisfying CTL formulas

This page was built for publication: Quirky quantifiers: optimal models and complexity of computation tree logic

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