The Complexity of Generalized Satisfiability for Linear Temporal Logic

In a seminal paper from 1985, Sistla and Clarke showed that satisfiability for Linear Temporal Logic (LTL) is either NP-complete or PSPACE-complete, depending on the set of temporal operators used. If, in contrast, the set of propositional operators is restricted, the complexity may decrease. This paper undertakes a systematic study of satisfiability for LTL formulae over restricted sets of propositional and temporal operators. Since every propositional operator corresponds to a Boolean function, there exist infinitely many propositional operators. In order to systematically cover all possible sets of them, we use Post's lattice. With its help, we determine the computational complexity of LTL satisfiability for all combinations of temporal operators and all but two classes of propositional functions. Each of these infinitely many problems is shown to be either PSPACE-complete, NP-complete, or in P.

• Publication year

  2007

• Venue

  Electron. Colloquium Comput. Complex.

• Publication date

  2007-03-24

• Fields of study

  Mathematics, Computer Science

• Identifiers
  DOI 10.2168/LMCS-5(1:1)2009arXiv 0812.4848
• External record

  Open on Semantic Scholar

• Source metadata

  Semantic Scholar

• No claims are published for this paper.

• No concepts are published for this paper.

• The Road: Reinventing Education

  2008cited by this paper
• Generalized modal satisfiability

  2006cited by this paper
• A Trichotomy in the Complexity of Propositional Circumscription

  2005influential reference
• The Complexity of Problems Defined by Boolean Circuits

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

  2005influential reference
• SIGACT news complexity theory column 48

  2005cited by this paper
• An algebraic approach to the complexity of propositional circumscription

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

  2002influential reference
• Generalized satisfiability problems

  2001cited by this paper
• Optimal satisfiability for propositional calculi and constraint satisfaction problems

  2000cited by this paper
• Execution and Proof in a Horn-Clause Temporal Logic

  2000cited by this paper
• The Complexity of Poor Man's Logic

  1999cited by this paper
• The Complexity of Propositional Linear Temporal Logics in Simple Cases

  1998cited by this paper
• Theories of computability

  1997cited by this paper
• The Effect of Bounding the Number of Primitive Propositions and the Depth of Nesting on the Complexity of Modal Logic

  1995cited by this paper
• The Computational Complexity of Satisfiability of Temporal Horn Formulas in Propositional Linear-Time Temporal Logic

  1993cited by this paper
• On the limits of efficient temporal decidability

  1990cited by this paper
• Temporal Logic of Programs

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

  1982cited by this paper
• Satisfiability problems for propositional calculi

  1979cited by this paper
• The Polynomial-Time Hierarchy

  1976cited by this paper
• The complexity of theorem-proving procedures

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

  1942cited by this paper
• Under Consideration for Publication in Formal Aspects of Computing Specification of Communicating Processes: Temporal Logic versus Refusals-based Refinement

  year unknowncited by this paper

• Modal Fragments

  2026cites this paper
• The difficulty of predicting behavior on stochastic local search algorithms

  2025cites this paper
• Containment of Conjunctive LTL Queries

  2025cites this paper
• When Symmetry Yields NP-Hardness: Affine ML-SAT on S5 Frames

  2025cites this paper
• Synchronous Team Semantics for Temporal Logics

  2024cites this paper
• Modal context restriction for multiagent BDI logics

  2021cites 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
• From LTL to unambiguous Büchi automata via disambiguation of alternating automata

  2019cites this paper
• Backdoors for Linear Temporal Logic

  2018cites this paper
• LTL on Finite and Process Traces: Complexity Results and a Practical Reasoner

  2018cites this paper
• Fe b 20 16 Strong Backdoors for Linear Temporal Logic

  2018cites this paper
• Automatic Trace Generation for Signal Temporal Logic

  2018influential citation
• The Complexity of Linear-Time Temporal Logic Model Repair

  2017cites this paper
• Structured Object-Oriented Formal Language and Method

  2017influential citation
• Temporal Logics in Computer Science: Finite-State Systems

  2016cites this paper
• The Complexity of LTL on Finite Traces: Hard and Easy Fragments

  2016cites this paper
• Strong Backdoors for Linear Temporal Logic

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

  2015cites this paper
• Conformance for DecSerFlow Constraints

  2014cites this paper
• Bounded variability of metric temporal logic

  2013cites this paper
• The Complexity of Clausal Fragments of LTL

  2013cites this paper
• Towards a notion of unsatisfiable and unrealizable cores for LTL

  2012cites this paper
• Parameterized Complexity of Weighted Satisfiability Problems: Decision, Enumeration, Counting

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

  2012influential citation
• Lewis Dichotomies in Many-Valued Logics

  2012cites this paper
• A Cookbook for Temporal Conceptual Data Modelling with Description Logics

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

  2011cites this paper
• Generalized Satisfiability for the Description Logic ALC

  2011influential citation
• Generalized Satisfiability for the Description Logic ALC - (Extended Abstract)

  2011cites this paper
• Complexity of logic-based argumentation in Post's framework

  2011cites this paper
• Dynamic Logics of Evidence-Based Beliefs

  2011cites this paper
• Granularity and Concurrent Separation Logic

  2011cites this paper
• Dichotomies in Many-Valued Logics

  2011cites this paper
• Weak Kripke Structures and LTL

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

  2011cites this paper
• The Complexity of Model Checking for Boolean Formulas

  2010cites this paper
• Complexity Classifications for Propositional Abduction in Post's Framework

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

  2010cites this paper
• Analytic Tableaux for Simple Type Theory and its First-Order Fragment

  2010cites this paper
• Verifying Executable Object-Oriented Specifications with Separation Logic

  2010cites this paper
• Model checking finite paths and trees

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

  2010cites this paper
• The Complexity of Satisfiability for Sub-Boolean Fragments of ALC

  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
• The Complexity of Circumscriptive Inference in Post’s Lattice

  2009cites this paper
• Complexity of Propositional Abduction for Restricted Sets of Boolean Functions

  2009cites this paper
• On Relaxing Metric Information in Linear Temporal Logic

  2009cites this paper
• L O ] 5 M ay 2 00 8 The Tractability of Model-Checking for LTL : The Good , the Bad , and the Ugly Fragments ⋆

  2008cites this paper
• The Complexity of Satisfiability for Fragments of CTL and CTL*

  2008cites 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

  2008influential citation
• Generalized modal satisfiability

  2006cites this paper