The Tractability of Model-checking for LTL: The Good, the Bad, and the Ugly Fragments

DOI10.1016/j.entcs.2009.02.041zbMath1347.68217MaRDI QIDQ4982126

Michael Bauland, Thomas Schneider, Ilka Schnoor, Heribert Vollmer, Martin Mundhenk, Henning Schnoor

Publication date: 23 March 2015

Published in: Electronic Notes in Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.entcs.2009.02.041

zbMATH Keywords

computational complexity; model checking; linear temporal logic

Mathematics Subject Classification ID

68Q25: Analysis of algorithms and problem complexity

68Q60: Specification and verification (program logics, model checking, etc.)

68Q17: Computational difficulty of problems (lower bounds, completeness, difficulty of approximation, etc.)

03B44: Temporal logic

Related Items

The Tractability of Model-checking for LTL: The Good, the Bad, and the Ugly Fragments, On the applicability of Post's lattice, The complexity of satisfiability for fragments of hybrid logic. I., Generalized modal satisfiability, Weak Kripke Structures and LTL, The Complexity of Satisfiability for Fragments of Hybrid Logic—Part I

Cites Work

• Unnamed Item
• Optimal satisfiability for propositional calculi and constraint satisfaction problems.
• Past is for free: On the complexity of verifying linear temporal properties with past
• Enumerating All Solutions for Constraint Satisfaction Problems
• The complexity of propositional linear temporal logics
• Satisfiability problems for propositional calculi
• Log Space Recognition and Translation of Parenthesis Languages
• The Tractability of Model-checking for LTL: The Good, the Bad, and the Ugly Fragments
• Generalized Modal Satisfiability
• Logic for Programming, Artificial Intelligence, and Reasoning
• The Complexity of Generalized Satisfiability for Linear Temporal Logic
• The Two-Valued Iterative Systems of Mathematical Logic. (AM-5)