The complexity of propositional linear temporal logics in simple cases

DOI10.1006/inco.2001.3094zbMath1009.68072OpenAlexW2026379532MaRDI QIDQ1854521

Philippe Schnoebelen, Stéphane P. Demri

Publication date: 14 January 2003

Published in: Information and Computation (Search for Journal in Brave)

Full work available at URL: https://semanticscholar.org/paper/0c8c9dd55fe6f91bb106107dbf1109544bf5312d

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Computational difficulty of problems (lower bounds, completeness, difficulty of approximation, etc.) (68Q17) Temporal logic (03B44)

Related Items

Extracting unsatisfiable cores for LTL via temporal resolution ⋮ Parametrised Complexity of Satisfiability in Temporal Logic ⋮ Complexity of finite-variable fragments of propositional temporal and modal logics of computation ⋮ Algorithms for monitoring real-time properties ⋮ LARS: a logic-based framework for analytic reasoning over streams ⋮ From model checking to equilibrium checking: reactive modules for rational verification ⋮ Bounded variability of metric temporal logic ⋮ A Cookbook for Temporal Conceptual Data Modelling with Description Logics ⋮ Temporal BI: proof system, semantics and translations ⋮ Computational complexity of the word problem in modal and Heyting algebras with a small number of generators ⋮ Taming strategy logic: non-recurrent fragments ⋮ Defeasible linear temporal logic ⋮ Two-Variable Separation Logic and Its Inner Circle ⋮ On the complexity of linear temporal logic with team semantics ⋮ On the expressivity and complexity of quantitative branching-time temporal logics ⋮ Complexity and Succinctness Issues for Linear-Time Hybrid Logics ⋮ Backdoors for linear temporal logic ⋮ Quirky Quantifiers: Optimal Models and Complexity of Computation Tree Logic ⋮ Strategic reasoning with a bounded number of resources: the quest for tractability ⋮ Alternating-time temporal logics with linear past ⋮ Embedding theorems for LTL and its variants ⋮ On regular temporal logics with past ⋮ A parametric analysis of the state-explosion problem in model checking ⋮ \(\text{BTL}_{2}\) and the expressive power of \(\text{ECTL}^{+}\) ⋮ AN NP-COMPLETE FRAGMENT OF LTL ⋮ Weak Kripke Structures and LTL ⋮ Bounded linear-time temporal logic: a proof-theoretic investigation ⋮ Past is for Free: on the Complexity of Verifying Linear Temporal Properties with Past ⋮ Complexity and succinctness issues for linear-time hybrid logics ⋮ Mu-calculus path checking ⋮ Tomorrow and All our Yesterdays: MTL Satisfiability over the Integers

Uses Software

• SPIN

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• The logic of ``initially and ``next: complete axiomatization and complexity
• The propositional dynamic logic of deterministic, well-structured programs
• Hierarchical verification of asynchronous circuits using temporal logic
• Characterizing finite Kripke structures in propositional temporal logic
• On the size of refutation Kripke models for some linear modal and tense logics
• The computational complexity of satisfiability of temporal Horn formulas in propositional linear-time temporal logic
• Space-bounded reducibility among combinatorial problems
• Cut-free sequent and tableau systems for propositional Diodorean modal logics
• The complexity of concept languages
• Modalities for model checking: Branching time logic strikes back
• Specification in CTL + past for verification in CTL.
• The effect of bounding the number of primitive propositions and the depth of nesting on the complexity of modal logic
• Recurring Dominoes: Making the Highly Undecidable Highly Understandable
• Temporal logic can be more expressive
• The complexity of propositional linear temporal logics
• Log Space Recognition and Translation of Parenthesis Languages
• Flat fragments of CTL and CTL: separating the expressive and distinguishing powers
• An algebraic study of Diodorean modal systems
• The complexity of theorem-proving procedures