The complexity of propositional linear temporal logics in simple cases. (Extended abstract)

DOI10.1007/BFB0028549MaRDI QIDQ4381382zbMATH OpenFDO

Authors Stéphane Demri, Philippe Schnoebelen

Publication date 19 August 1999

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/BFB0028549

zbMATH Keywords

complexitylinear-time temporal logicmodel checkingsatisfiability

Mathematics Subject Classification ID

Modal logic (including the logic of norms) (03B45) Complexity of computation (including implicit computational complexity) (03D15) Analysis of algorithms and problem complexity (68Q25) Specification and verification (program logics, model checking, etc.) (68Q60)

Review text

The authors investigate the standard linear-time propositional temporal logic (PLTL). They recall the known PSPACE-completeness of satisfiability (SAT) and model checking (MC) and study the complexity of these problems for some fragments of PLTL. They show several polynomial-time (p.t.) reductions which allow to conclude: (1) when the number of propositions is fixed, SAT can be p.t. reduced to MC, (2) if the temporal operators \(F\) (sometimes) and \(X\) (next) are allowed, then \(n\) propositional variables can be encoded into one, (3) and into two if \(U\) (until) is allowed. When arbitrarily many propositions are allowed, (4) temporal height can be reduced to 2 if \(F\) is allowed, and (5) MC for logics with \(X\) can be transformed into MC without \(X\). When a formula \(\phi\) has temporal height at most 1, (6) the fact whether \(S\models \phi\) only depends on \(O(| \phi|)\) places in \(S\). The paper also gives new, simpler, proofs of PSPACE-hardness of SAT and MC for \(L(X,F)\) and \(L(U)\) by showing a straightforward reduction from the QBF problem (quantified boolean formulas). For the entire collection see [Zbl 0885.68008].

Recommendations

• The complexity of propositional linear temporal logics in simple cases
• The complexity of propositional linear temporal logics
• The Complexity of Generalized Satisfiability for Linear Temporal Logic
• The Complexity of Generalized Satisfiability for Linear Temporal Logic

Cited in

(12)

• The computational complexity of satisfiability of temporal Horn formulas in propositional linear-time temporal logic
• A polynomial space construction of tree-like models for logics with local chains of modal connectives
• Specification in CTL + past for verification in CTL.
• The complexity of propositional linear temporal logics in simple cases
• Is your model checker on time? On the complexity of model checking for timed modal logics
• Implicates and reduction techniques for temporal logics
• The complexity of dual models problem of propositional linear temporal logics
• The complexity of propositional linear temporal logics
• Verification of PLTL formulae by means of monotone disjunctive normal forms
• scientific article; zbMATH DE number 1950255 (Why is no real title available?)
• Propositional temporal proving with reductions to a SAT problem
• Simple interpretations among complicated theories

This page was built for publication: The complexity of propositional linear temporal logics in simple cases. (Extended abstract)

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