The complexity of propositional linear temporal logics

DOI10.1145/3828.3837zbMath0632.68034OpenAlexW2003227046WikidataQ56619906 ScholiaQ56619906MaRDI QIDQ3769957

Publication date: 1985

Published in: Journal of the ACM (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1145/3828.3837

zbMATH Keywords

complexity NP-complete satisfiability PSPACE-complete decision procedures branching time temporal logic determination of truth propositional linear temporal logics

Mathematics Subject Classification ID

Logic in computer science (03B70) Specification and verification (program logics, model checking, etc.) (68Q60) Abstract data types; algebraic specification (68Q65)

Related Items

Extracting unsatisfiable cores for LTL via temporal resolution ⋮ A branching time logic with past operators ⋮ The complementation problem for Büchi automata with applications to temporal logic ⋮ The logic of ``initially and ``next: complete axiomatization and complexity ⋮ A note on a question of Peled and Wilke regarding stutter-invariant LTL ⋮ Spanning the spectrum from safety to liveness ⋮ Safety, liveness and fairness in temporal logic ⋮ Parameterized model checking of rendezvous systems ⋮ Belief, awareness, and limited reasoning ⋮ A decision procedure for combinations of propositional temporal logic and other specialized theories ⋮ Imperfect information in reactive modules games ⋮ Satisfiability in many-valued sentential logic is NP-complete ⋮ Checking interval properties of computations ⋮ LARS: a logic-based framework for analytic reasoning over streams ⋮ Reasoning about equilibria in game-like concurrent systems ⋮ Decentralised LTL monitoring ⋮ Tableau-based automata construction for dynamic linear time temporal logic ⋮ On the freeze quantifier in Constraint LTL: Decidability and complexity ⋮ Quantitative temporal logics over the reals: PSpace and below ⋮ An automata-theoretic approach to constraint LTL ⋮ The complexity of reasoning about knowledge and time. I: Lower bounds ⋮ Finite-trace linear temporal logic: coinductive completeness ⋮ Problems concerning fairness and temporal logic for conflict-free Petri nets ⋮ Characterizing finite Kripke structures in propositional temporal logic ⋮ Rules admissible in transitive temporal logic \(\mathrm{T}_{\mathrm{S}4}\), sufficient condition ⋮ Branching-time logics with path relativisation ⋮ Optimal bounds in parametric LTL games ⋮ Temporal BI: proof system, semantics and translations ⋮ On projective and separable properties ⋮ The ins and outs of first-order runtime verification ⋮ Verification of relational transducers for electronic commerce ⋮ Deciding safety and liveness in TPTL ⋮ The complexity of the temporal logic with ``until over general linear time ⋮ On feasible cases of checking multi-agent systems behavior. ⋮ Temporal logics over linear time domains are in PSPACE ⋮ Complexity of hybrid logics over transitive frames ⋮ Towards a notion of unsatisfiable and unrealizable cores for LTL ⋮ Reasoning about sequences of memory states ⋮ The complexity of temporal logic over the reals ⋮ \textit{Once} and \textit{for all} ⋮ An explicit transition system construction approach to LTL satisfiability checking ⋮ A first-order coalition logic for BDI-agents ⋮ Specifying and computing preferred plans ⋮ Interrupt timed automata: verification and expressiveness ⋮ Reasoning about networks with many identical finite state processes ⋮ Simple interpretations among complicated theories ⋮ Linear temporal logic symbolic model checking ⋮ Branching time logics \(\mathcal {BTL}^{\text{U,S}}_{\text{N},\text{N}^{-1}}(\mathcal {Z})_{\alpha }\) with operations \textit{Until} and \textit{Since} based on bundles of integer numbers, logical consecutions, deciding algorithms ⋮ Constraint LTL satisfiability checking without automata ⋮ Runtime verification using the temporal description logic \(\mathcal{ALC}\)-LTL revisited ⋮ TABLEAUX: A general theorem prover for modal logics ⋮ Model checking properties on reduced trace systems ⋮ Interval logics and their decision procedures. I: An interval logic ⋮ A hierarchy of temporal logics with past ⋮ Sublogics of a branching time logic of robustness ⋮ On Gabbay's temporal fixed point operator ⋮ On relative and probabilistic finite counterability ⋮ Linear temporal logic with until and next, logical consecutions ⋮ Complexity of fixed-size bit-vector logics ⋮ The complexity of counting models of linear-time temporal logic ⋮ Enhancing unsatisfiable cores for LTL with information on temporal relevance ⋮ A model checker for linear time temporal logic ⋮ Parametric linear dynamic logic ⋮ Synthesis from component libraries with costs ⋮ A unified approach for showing language inclusion and equivalence between various types of \(\omega\)-automata ⋮ Verification of qualitative \(\mathbb Z\) constraints ⋮ Nash equilibria in symmetric graph games with partial observation ⋮ An approach to infinitary temporal proof theory ⋮ The computational complexity of satisfiability of temporal Horn formulas in propositional linear-time temporal logic ⋮ Difficult configurations -- on the complexity of LTrL ⋮ Unification in linear temporal logic LTL ⋮ Generalized modal satisfiability ⋮ Model checking for fragments of the interval temporal logic HS at the low levels of the polynomial time hierarchy ⋮ Diagnosability of repairable faults ⋮ Efficient model checking for LTL with partial order snapshots ⋮ Developing bounded reasoning ⋮ Variable and clause elimination for LTL satisfiability checking ⋮ The price of universality ⋮ Minimal temporal epistemic logic ⋮ An algorithmic approach for checking closure properties of temporal logic specifications and \(\omega\)-regular languages ⋮ Before and after vacuity ⋮ Bounded linear-time temporal logic: a proof-theoretic investigation ⋮ Dual systems of tableaux and sequents for PLTL ⋮ Systems of agents controlled by logical programs: complexity of verification ⋮ Complexity and succinctness issues for linear-time hybrid logics ⋮ On relation between linear temporal logic and quantum finite automata ⋮ Product interval automata ⋮ A two-level temporal logic for evolving specifications. ⋮ A multiprocess network logic with temporal and spatial modalities ⋮ An until hierarchy and other applications of an Ehrenfeucht-Fraïssé game for temporal logic ⋮ Module checking ⋮ The complexity of propositional linear temporal logics in simple cases ⋮ Process logic with regular formulas ⋮ Global and local views of state fairness ⋮ A modal perspective on the computational complexity of attribute value grammar ⋮ A taxonomy of fairness and temporal logic problems for Petri nets ⋮ The complexity of achievement and maintenance problems in agent-based systems ⋮ \({\mathcal E}\)-connections of abstract description systems ⋮ Complete problems in the first-order predicate calculus ⋮ All finitely axiomatizable tense logics of linear time flows are coNP-complete ⋮ Efficient timed model checking for discrete-time systems ⋮ Specification and Verification of Multi-Agent Systems ⋮ Vectorial languages and linear temporal logic ⋮ Unifying models ⋮ The computational complexity of scenario-based agent verification and design ⋮ Complexity results on branching-time pushdown model checking ⋮ Some modal aspects of XPath ⋮ Size-Change Termination and Satisfiability for Linear-Time Temporal Logics ⋮ Temporal Logic and Fair Discrete Systems ⋮ Automata Theory and Model Checking ⋮ Functional Specification of Hardware via Temporal Logic ⋮ Branching Time? Pruning Time! ⋮ Undecidability of QLTL and QCTL with two variables and one monadic predicate letter ⋮ Multi-Valued Reasoning about Reactive Systems ⋮ From LTL to unambiguous Büchi automata via disambiguation of alternating automata ⋮ Social bot detection as a temporal logic model checking problem ⋮ A brief account of runtime verification ⋮ The power of first-order quantification over states in branching and linear time temporal logics ⋮ Unnamed Item ⋮ Sub-propositional Fragments of the Interval Temporal Logic of Allen’s Relations ⋮ From model checking to equilibrium checking: reactive modules for rational verification ⋮ Bounded variability of metric temporal logic ⋮ Mean-payoff games with \(\omega\)-regular specifications ⋮ A decidable timeout-based extension of linear temporal logic ⋮ Parameterized linear temporal logics meet costs: still not costlier than LTL ⋮ Robust, expressive, and quantitative linear temporal logics: pick any two for free ⋮ Suitability of the propositional temporal logic to express properties of real-time systems ⋮ A survey on temporal logics for specifying and verifying real-time systems ⋮ Cooperative concurrent games ⋮ On the complexity of linear temporal logic with team semantics ⋮ Verification of a technical system model with linear temporal logic ⋮ Branching vs. Linear Time: Semantical Perspective ⋮ The Birth of Model Checking ⋮ Some results on parametric temporal logic ⋮ Classifying the computational complexity of problems ⋮ On the Decision Problem for Two-Variable First-Order Logic ⋮ Reasoning about Conditions and Exceptions to Laws in Regulatory Conformance Checking ⋮ Unnamed Item ⋮ Interval vs. Point Temporal Logic Model Checking ⋮ Temporal aspects of the modal logic of subset spaces ⋮ Complexity and Succinctness Issues for Linear-Time Hybrid Logics ⋮ A propositional linear time logic with time flow isomorphic to \(\omega^2\) ⋮ A SURVEY ON SMALL FRAGMENTS OF FIRST-ORDER LOGIC OVER FINITE WORDS ⋮ Multi-player games with LDL goals over finite traces ⋮ Theorem proving for pointwise metric temporal logic over the naturals via translations ⋮ Team semantics for the specification and verification of hyperproperties ⋮ Using temporal logics to express search control knowledge for planning ⋮ Quirky Quantifiers: Optimal Models and Complexity of Computation Tree Logic ⋮ Epistemic GDL: a logic for representing and reasoning about imperfect information games ⋮ First-order rewritability of ontology-mediated queries in linear temporal logic ⋮ Strategic reasoning with a bounded number of resources: the quest for tractability ⋮ Deciding Robustness against Total Store Ordering ⋮ Search strategies for resolution in temporal logics ⋮ Probabilistic verification and approximation ⋮ Transformation from PLTL to automata via NFGs ⋮ The stuttering principle revisited ⋮ On the expressiveness of TPTL and MTL ⋮ Unnamed Item ⋮ A parametric analysis of the state-explosion problem in model checking ⋮ \(\text{BTL}_{2}\) and the expressive power of \(\text{ECTL}^{+}\) ⋮ The complexity of agent design problems: Determinism and history dependence ⋮ From Philosophical to Industrial Logics ⋮ Verification of concurrent programs: The automata-theoretic framework ⋮ Unnamed Item ⋮ LTL over integer periodicity constraints ⋮ Removing irrelevant information in temporal resolution proofs ⋮ Model checking Petri nets with MSVL ⋮ Temporalization of Probabilistic Propositional Logic ⋮ First-order logic with two variables and unary temporal logic ⋮ One-pass and tree-shaped tableau systems for TPTL and \(\mathrm{TPTL_b+Past}\) ⋮ A general tableau method for propositional interval temporal logics: theory and implementation ⋮ A novel approach to verifying context free properties of programs ⋮ Matching Trace Patterns with Regular Policies ⋮ Model checking for hybrid branching-time logics ⋮ Unnamed Item ⋮ A temporal negative normal form which preserves implicants and implicates ⋮ Temporal logic with recursion ⋮ Synthesis from hyperproperties ⋮ Interval Temporal Logic Model Checking: The Border Between Good and Bad HS Fragments ⋮ Weak Kripke Structures and LTL ⋮ Two Variable vs. Linear Temporal Logic in Model Checking and Games ⋮ Expressiveness of Hybrid Temporal Logic on Data Words ⋮ Unnamed Item ⋮ The Complexity of Satisfiability for Fragments of CTL and CTL⋆ ⋮ The Tractability of Model-checking for LTL: The Good, the Bad, and the Ugly Fragments ⋮ THE COMPLEXITY OF SATISFIABILITY FOR FRAGMENTS OF CTL AND CTL⋆ ⋮ Linear-time temporal logics with Presburger constraints: an overview ★ ⋮ \( \omega \)-automata ⋮ Deductive verification of simple foraging robotic behaviours ⋮ Past is for Free: on the Complexity of Verifying Linear Temporal Properties with Past ⋮ Tableaux and sequent calculi for \textsf{CTL} and \textsf{ECTL}: satisfiability test with certifying proofs and models ⋮ Complexity of monodic guarded fragments over linear and real time ⋮ Relating word and tree automata ⋮ Is your model checker on time? On the complexity of model checking for timed modal logics ⋮ Iterated Boolean games ⋮ Taming past LTL and flat counter systems ⋮ Satisfiability checking for mission-time \textsf{LTL} (MLTL) ⋮ Probabilistic Temporal Logics ⋮ Qualitative analysis of gene regulatory networks by temporal logic ⋮ Property-oriented expansion ⋮ Taming strategy logic: non-recurrent fragments ⋮ Time and Gödel: fuzzy temporal reasoning in PSPACE ⋮ Defeasible linear temporal logic ⋮ A framework for transforming specifications in reinforcement learning ⋮ Temporal stream logic modulo theories ⋮ Synchronizing words under \textsf{LTL} constraints ⋮ A space-efficient on-the-fly algorithm for real-time model checking ⋮ An algorithmic approach for checking closure properties of Ω-regular languages ⋮ Modal logics and local quantifiers: a zoo in the elementary hierarchy ⋮ Construction of deterministic transition graphs from dynamic integrity constraints ⋮ Incentive Engineering for Concurrent Games ⋮ Unnamed Item ⋮ Knowledge-based programs ⋮ A GENERAL NOTION OF UNIFORM STRATEGIES ⋮ Temporal Logic with Recursion. ⋮ One-pass Context-based Tableaux Systems for CTL and ECTL ⋮ Embedding theorems for LTL and its variants ⋮ Some Results on the Expressive Power and Complexity of LSCs ⋮ From Monadic Logic to PSL ⋮ Model Checking Almost All Paths Can Be Less Expensive Than Checking All Paths ⋮ AN NP-COMPLETE FRAGMENT OF LTL ⋮ An auxiliary logic on trees: on the tower-hardness of logics featuring reachability and submodel reasoning ⋮ An auxiliary logic on trees: on the tower-hardness of logics featuring reachability and submodel reasoning ⋮ Unnamed Item ⋮ Alternating automata: Unifying truth and validity checking for temporal logics ⋮ Tomorrow and All our Yesterdays: MTL Satisfiability over the Integers ⋮ First-Order Rewritability and Complexity of Two-Dimensional Temporal Ontology-Mediated Queries