The Complexity of Satisfiability for Fragments of CTL and CTL*

The satisfiability problems for and are known to be EXPTIME-complete, resp. 2EXPTIME-complete (Fischer and Ladner (1979), Vardi and Stockmeyer (1985)). For fragments that use less temporal or propositional operators, the complexity may decrease. This paper undertakes a systematic study of satisfiability for -and -formulae over restricted sets of propositional and temporal operators. We show that restricting the temporal operators yields satisfiability problems complete for 2EXPTIME, EXPTIME, PSPACE, and NP. Restricting the propositional operators either does not change the complexity (as determined by the temporal operators), or yields very low complexity like NC1, TC0, or NLOGTIME.

• Publication year

  2008

• Venue

  International Journal of Foundations of Computer Science

• Publication date

  2008-12-01

• Fields of study

  Mathematics, Computer Science

• Identifiers
  DOI 10.1142/S0129054109006954
• External record

  Open on Semantic Scholar

• Source metadata

  Semantic Scholar

• No claims are published for this paper.

• No concepts are published for this paper.

• Introduction to Circuit Complexity: A Uniform Approach

  2010cited by this paper
• The Complexity of Generalized Satisfiability for Linear Temporal Logic

  2007cited by this paper
• SIGACT news complexity theory column 48

  2005cited by this paper
• The Complexity of the Boolean Formula Value Problem

  2005cited by this paper
• Past is for free: on the complexity of verifying linear temporal properties with past

  2002cited by this paper
• Sometimes and Not Never Re-revisited: On Branching Versus Linear Time

  1998cited by this paper
• Gap-Languages and Log-Time Complexity Classes

  1997cited by this paper
• Theories of computability

  1997cited by this paper
• About the Expressive Power of CTL Combinators

  1995cited by this paper
• Handbook of Theoretical Computer Science, Vol. B: Formal Models and Semantics

  1994cited by this paper
• Temporal and Modal Logic

  1991cited by this paper
• Automatic verification of finite-state concurrent systems using temporal logic specifications

  1986cited by this paper
• Improved upper and lower bounds for modal logics of programs

  1985cited by this paper
• "Sometimes" and "not never" revisited: on branching versus linear time (preliminary report)

  1983cited by this paper
• The complexity of propositional linear temporal logics

  1982cited by this paper
• Satisfiability problems for propositional calculi

  1979cited by this paper
• Propositional Dynamic Logic of Regular Programs

  1979cited by this paper
• The Computational Complexity of Provability in Systems of Modal Propositional Logic

  1977influential reference
• Propositional modal logic of programs

  1977influential reference
• The complexity of theorem-proving procedures

  1971cited by this paper
• The two-valued iterative systems of mathematical logic

  1942cited by this paper

• Modal Fragments

  2026cites this paper
• Robust Alternating-Time Temporal Logic

  2023cites this paper
• Uncertainty-Based Knowing How Logic

  2023cites this paper
• A Deontic Logic of Knowingly Complying

  2023cites this paper
• Computing Sufficient and Necessary Conditions in CTL: A Forgetting Approach

  2022cites this paper
• Complexity Assessments for Decidable Fragments of Set Theory. I: A Taxonomy for the Boolean Case

  2021cites this paper
• Adaptive On-the-Fly Changes in Distributed Processing Pipelines

  2021cites this paper
• Intention as Commitment toward Time

  2020cites this paper
• Branching-time logic ECTL# and its tree-style one-pass tableau: Extending fairness expressibility of ECTL+

  2020cites this paper
• An Auxiliary Logic on Trees: on the Tower-Hardness of Logics Featuring Reachability and Submodel Reasoning

  2020cites this paper
• On Sufficient and Necessary Conditions in Bounded CTL

  2020cites this paper
• Parameterized complexity of abduction in Schaefer's framework

  2020cites this paper
• Parameterised Complexity of Abduction in Schaefer's Framework

  2019cites this paper
• Parameterised Complexity for Abduction

  2019cites this paper
• Model Checking: The Interval Way

  2019cites this paper
• Parameterized complexity of decision problems in non-classical logics

  2018cites this paper
• Extending Fairness Expressibility of ECTL+: A Tree-Style One-Pass Tableau Approach

  2018cites this paper
• Parametrised Complexity of Satisfiability in Temporal Logic

  2017cites this paper
• Detecting Decidable Classes of Finitely Ground Logic Programs with Function Symbols

  2017influential citation
• Online, library-based visual formal specification monitoring system for monitoring log-files with visible and hidden data

  2016cites this paper
• A decidable weakening of Compass Logic based on cone-shaped cardinal directions

  2015cites this paper
• Quirky Quantifiers: Optimal Models and Complexity of Computation Tree Logic

  2015cites this paper
• Early detection of evolving system failures and temporal conflicts using parameterized formal specifications and bounded constraint-solving

  2015cites this paper
• The model checking fingerprints of CTL operators

  2015cites this paper
• Parallel Computational Tree Logic

  2015cites this paper
• LTL Fragments are Hard for Standard Parameterisations

  2015cites this paper
• A Team Based Variant of CTL

  2015cites this paper
• Lightweight Description Logics and Branching Time: A Troublesome Marriage

  2014cites this paper
• Subsumption Checking in Conjunctive Coalgebraic Fixpoint Logics

  2014cites this paper
• Detecting decidable classes of finitely ground logic programs with function symbols

  2013cites this paper
• COMPUTATIONAL ASPECTS OF DEPENDENCE LOGIC

  2012cites this paper
• The Complexity of Circumscriptive Inference in Post’s Lattice

  2012cites this paper
• Computational Aspects of Dependence Logic

  2012cites this paper
• On the Complexity of Modal Logic Variants and their Fragments

  2011cites this paper
• On the Complexity of Modal Logic Variants and their Fragments

  2011cites this paper
• The Complexity of Satisfiability for Fragments of Hybrid Logic---Part II

  2010cites this paper
• On the applicability of Post's lattice

  2010cites this paper
• 20. Theorietag der GI-Fachgruppe "Automaten und Formale Sprachen''

  2010cites this paper
• Complexity Results for Modal Dependence Logic

  2010cites this paper
• Dependence and Independence in Logic

  2010cites this paper
• Decidability of interval temporal logics

  2010cites this paper
• The Complexity of Reasoning for Fragments of Autoepistemic Logic

  2010cites this paper
• The Complexity of Satisfiability for Fragments of Hybrid Logic-Part I

  2009cites this paper
• Model Checking CTL is Almost Always Inherently Sequential

  2009cites this paper
• A Decidable Spatial Logic with Cone-Shaped Cardinal Directions

  2009cites this paper
• The complexity of propositional implication

  2008cites this paper
• The tractability of model checking for LTL: The good, the bad, and the ugly fragments

  2008cites this paper