The complexity of propositional linear temporal logics

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

Mathematics Subject Classification ID

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

Cited In (only showing first 100 items - show all)

Synthesis from component libraries with costs
A unified approach for showing language inclusion and equivalence between various types of \(\omega\)-automata
The computational complexity of scenario-based agent verification and design
A general tableau method for propositional interval temporal logics: theory and implementation
\( \omega \)-automata
Reasoning about Conditions and Exceptions to Laws in Regulatory Conformance Checking
Complexity of monodic guarded fragments over linear and real time
Complete problems in the first-order predicate calculus
Model checking for fragments of the interval temporal logic HS at the low levels of the polynomial time hierarchy
LARS: a logic-based framework for analytic reasoning over streams
Complexity and Succinctness Issues for Linear-Time Hybrid Logics
Deciding Robustness against Total Store Ordering
The stuttering principle revisited
A Paraconsistent Linear-time Temporal Logic
An until hierarchy and other applications of an Ehrenfeucht-Fraïssé game for temporal logic
\(\text{BTL}_{2}\) and the expressive power of \(\text{ECTL}^{+}\)
Tableau-based automata construction for dynamic linear time temporal logic
Verification of concurrent programs: The automata-theoretic framework
Automata Theory and Model Checking
On the freeze quantifier in Constraint LTL: Decidability and complexity
Efficient model checking for LTL with partial order snapshots
Developing bounded reasoning
Difficult configurations -- on the complexity of LTrL
On projective and separable properties
Is your model checker on time? On the complexity of model checking for timed modal logics
Tableaux and sequent calculi for \textsf{CTL} and \textsf{ECTL}: satisfiability test with certifying proofs and models
A space-efficient on-the-fly algorithm for real-time model checking
Theorem proving for pointwise metric temporal logic over the naturals via translations
Interval Temporal Logic Model Checking: The Border Between Good and Bad HS Fragments
Probabilistic verification and approximation
All finitely axiomatizable tense logics of linear time flows are coNP-complete
A propositional linear time logic with time flow isomorphic to \(\omega^2\)
Variable and clause elimination for LTL satisfiability 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
A taxonomy of fairness and temporal logic problems for Petri nets
Complexity of hybrid logics over transitive frames
Systems of agents controlled by logical programs: complexity of verification
A modal perspective on the computational complexity of attribute value grammar
From model checking to equilibrium checking: reactive modules for rational verification
Strategic reasoning with a bounded number of resources: the quest for tractability
Problems concerning fairness and temporal logic for conflict-free Petri nets
Some results on parametric temporal logic
The price of universality
Complexity of finite-variable fragments of propositional temporal and modal logics of computation
Complexity and succinctness issues for linear-time hybrid logics
Quantitative temporal logics over the reals: PSpace and below
Simple interpretations among complicated theories
On relation between linear temporal logic and quantum finite automata
On feasible cases of checking multi-agent systems behavior.
Interval vs. Point Temporal Logic Model Checking
LTL over integer periodicity constraints
Some modal aspects of XPath
Global and local views of state fairness
Interval logics and their decision procedures. I: An interval logic
Imperfect information in reactive modules games
Parametric linear dynamic logic
The complexity of achievement and maintenance problems in agent-based systems
The Complexity of Satisfiability for Fragments of CTL and CTL⋆
On Gabbay's temporal fixed point operator
Nash equilibria in symmetric graph games with partial observation
Optimal bounds in parametric LTL games
AN NP-COMPLETE FRAGMENT OF LTL
Unification in linear temporal logic LTL
A multiprocess network logic with temporal and spatial modalities
Deciding safety and liveness in TPTL
Extracting unsatisfiable cores for LTL via temporal resolution
The Birth of Model Checking
Linear temporal logic with until and next, logical consecutions
Bounded linear-time temporal logic: a proof-theoretic investigation
On the Decision Problem for Two-Variable First-Order Logic
Temporal BI: proof system, semantics and translations
Towards a notion of unsatisfiable and unrealizable cores for LTL
Iterated Boolean games
Interrupt timed automata: verification and expressiveness
Constraint LTL satisfiability checking without automata
Enhancing unsatisfiable cores for LTL with information on temporal relevance
Generalized modal satisfiability
Rules admissible in transitive temporal logic \(\mathrm{T}_{\mathrm{S}4}\), sufficient condition
The complexity of temporal logic over the reals
Efficient timed model checking for discrete-time systems
Temporal logics over linear time domains are in PSPACE
Reasoning about networks with many identical finite state processes
The Tractability of Model-checking for LTL: The Good, the Bad, and the Ugly Fragments
An automata-theoretic approach to constraint LTL
Characterizing finite Kripke structures in propositional temporal logic
Reasoning about sequences of memory states
Title not available (Why is that?)
Belief, awareness, and limited reasoning
Module checking
Verification of qualitative \(\mathbb Z\) constraints
An approach to infinitary temporal proof theory
A note on a question of Peled and Wilke regarding stutter-invariant LTL
The logic of ``initially and ``next: complete axiomatization and complexity
\({\mathcal E}\)-connections of abstract description systems
The ins and outs of first-order runtime verification
A hierarchy of temporal logics with past
\textit{Once} and \textit{for all}
Verification of relational transducers for electronic commerce
Satisfiability in many-valued sentential logic is NP-complete
The complexity of the temporal logic with ``until over general linear time

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

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