The complexity of propositional linear temporal logics in simple cases

DOI10.1006/INCO.2001.3094MaRDI QIDQ1854521zbMATH OpenOpenAlexFDO

Authors Philippe Schnoebelen, Stéphane 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

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

Recommendations

• scientific article; zbMATH DE number 1136071
• The tractability of model-checking for LTL: the good, the bad, and the ugly fragments
• The complexity of propositional linear temporal logics
• Past is for free: on the complexity of verifying linear temporal properties with past
• The Complexity of Generalized Satisfiability for Linear Temporal Logic

Cites work

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

Cited in

(40)

• Parametrised complexity of satisfiability in temporal logic
• Backdoors for linear temporal logic
• AN NP-COMPLETE FRAGMENT OF LTL
• Extracting unsatisfiable cores for LTL via temporal resolution
• Bounded linear-time temporal logic: a proof-theoretic investigation
• Temporal BI: proof system, semantics and translations
• On regular temporal logics with past
• On the satisfiability of indexed linear temporal logics
• Embedding theorems for LTL and its variants
• The complexity of counting models of linear-time temporal logic
• LARS: a logic-based framework for analytic reasoning over streams
• Weak Kripke structures and LTL
• Complexity and Succinctness Issues for Linear-Time Hybrid Logics
• Alternating-time temporal logics with linear past
• \(\text{BTL}_{2}\) and the expressive power of \(\text{ECTL}^{+}\)
• Defeasible linear temporal logic
• Tomorrow and All our Yesterdays: MTL Satisfiability over the Integers
• A Cookbook for Temporal Conceptual Data Modelling with Description Logics
• On the complexity of linear temporal logic with team semantics
• Past is for free: on the complexity of verifying linear temporal properties with past
• A parametric analysis of the state-explosion problem in model checking
• Two-Variable Separation Logic and Its Inner Circle
• The tractability of model checking for LTL: the good, the bad, and the ugly fragments
• The complexity of dual models problem of propositional linear temporal logics
• Taming strategy logic: non-recurrent fragments
• Past is for free: On the complexity of verifying linear temporal properties with past
• The tractability of model-checking for LTL: the good, the bad, and the ugly fragments
• From model checking to equilibrium checking: reactive modules for rational verification
• Strategic reasoning with a bounded number of resources: the quest for tractability
• scientific article; zbMATH DE number 1950255 (Why is no real title available?)
• Complexity and succinctness issues for linear-time hybrid logics
• Mu-calculus path checking
• Complexity of finite-variable fragments of propositional temporal and modal logics of computation
• Quirky quantifiers: optimal models and complexity of computation tree logic
• Computational complexity of the word problem in modal and Heyting algebras with a small number of generators
• Bounded variability of metric temporal logic
• scientific article; zbMATH DE number 2196601 (Why is no real title available?)
• The computational complexity of satisfiability of temporal Horn formulas in propositional linear-time temporal logic
• Algorithms for monitoring real-time properties
• On the expressivity and complexity of quantitative branching-time temporal logics

Describes a project that uses

Uses Software

• SPIN

This page was built for publication: The complexity of propositional linear temporal logics in simple cases

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1854521)