The complexity of propositional linear temporal logics

1985/07/01 by A. P. Sistla, A. Prasad Sistla, E. M. Clarke · 28 citations
Computer Science · #Logic, Reasoning, and Knowledge #Advanced Algebra and Logic #Logic, programming, and type systems

paper · pdf · doi:10.1145/3828.3837

Abstract

The complexity of satisfiability and determination of truth in a particular finite structure are considered for different propositional linear temporal logics. It is shown that these problems are NP-complete for the logic with F and are PSPACE-complete for the logics with F, X, with U, with U, S, X operators and for the extended logic with regular operators given by Wolper.

Cited by

• “Sometimes” and “not never” revisited
• Reasoning about systems with many processes
• Linear Temporal Logic and Propositional Schemata, Back and Forth (extended version)
• LTL Fragments are Hard for Standard Parameterisations
• Revisiting Timed Logics with Automata Modalities
• Monitorability of ω-regular languages
• A Decidable Timeout based Extension of Propositional Linear Temporal Logic
• Modalities for model checking: branching time logic strikes back
• Timed Automata Approach for Motion Planning Using Metric Interval Temporal Logic
• Parametric Linear Dynamic Logic (full version)
• Parikh Images of Regular Languages: Complexity and Applications
• Temporal Conjunctive Query Answering in the Extended DL-Lite Family
• An Epistemic Strategy Logic
• Automatic verification of finite-state concurrent systems using temporal logic specifications
• Model checking: the interval way
• A Simple Probabilistic Extension of Modal Mu-calculus
• Timeline-based planning: Expressiveness and Complexity
• Algorithmic metatheorems for decidable LTL model checking over infinite systems
• The Complexity of Admissibility in Omega-Regular Games
• On the complexity of Temporal Equilibrium Logic
• Verifying Stochastic Hybrid Systems with Temporal Logic Specifications via Model Reduction
• A Metric for Linear Temporal Logic
• Parameterized Linear Temporal Logics Meet Costs: Still not Costlier than LTL (full version)
• On the Complexity of Verifying Regular Properties on Flat Counter\n Systems
• Parameterized model checking of rendezvous systems. [europepmc]
• Synthesis from hyperproperties. [europepmc]
• Modelling and verification of reconfigurable multi-agent systems. [europepmc]
• Formal Modelling and Runtime Verification of Autonomous Grasping for Active Debris Removal. [europepmc]

Related

• The Complexity of Temporal Logic over the Reals
• Complexity of Safety and coSafety Fragments of Linear Temporal Logic
• Computational Complexity of Standpoint LTL
• Linear Temporal Logic and Propositional Schemata, Back and Forth (extended version)
• The Tractability of Model-Checking for LTL: The Good, the Bad, and the Ugly Fragments