Propositional temporal logics: decidability and completeness
From MaRDI portal
Publication:4444910
DOI10.1093/jigpal/8.1.55zbMath1033.03009OpenAlexW1982302236MaRDI QIDQ4444910
Orna Lichtenstein, Amir Pnueli
Publication date: 28 January 2004
Published in: Logic Journal of IGPL (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1093/jigpal/8.1.55
completenessaxiomatic systempast operatorspropositional temporal logictableau-based decision proceduredeductive proof systemspecification and verification of reactive systems
Specification and verification (program logics, model checking, etc.) (68Q60) Decidability of theories and sets of sentences (03B25) Temporal logic (03B44)
Related Items (31)
An alternating-time temporal logic with knowledge, perfect recall and past: axiomatisation and model-checking ⋮ Branching Time? Pruning Time! ⋮ A sound and complete axiomatization for Dynamic Topological Logic ⋮ Invariant-free clausal temporal resolution ⋮ Finite-trace linear temporal logic: coinductive completeness ⋮ Rules admissible in transitive temporal logic \(\mathrm{T}_{\mathrm{S}4}\), sufficient condition ⋮ A propositional probabilistic logic with discrete linear time for reasoning about evidence ⋮ COMPLETE INTUITIONISTIC TEMPORAL LOGICS FOR TOPOLOGICAL DYNAMICS ⋮ A survey on temporal logics for specifying and verifying real-time systems ⋮ Exploring the Jungle of Intuitionistic Temporal Logics ⋮ Refutation-aware Gentzen-style calculi for propositional until-free linear-time temporal logic ⋮ Unnamed Item ⋮ Interval vs. Point Temporal Logic 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 ⋮ Dynamic topological logic of metric spaces ⋮ Cut-free sequent systems for temporal logic ⋮ A decision procedure and complete axiomatization for projection temporal logic ⋮ Non-finite axiomatizability of dynamic topological logic ⋮ Compositional reasoning using intervals and time reversal ⋮ Model Theoretic Syntax and Parsing ⋮ The intuitionistic temporal logic of dynamical systems ⋮ 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 ⋮ Non-deterministic semantics for dynamic topological logic ⋮ Temporal Verification of Fault-Tolerant Protocols ⋮ Embedding Linear-Time Temporal Logic into Infinitary Logic: Application to Cut-Elimination for Multi-agent Infinitary Epistemic Linear-Time Temporal Logic ⋮ Tangled modal logic for topological dynamics ⋮ Linear-time temporal logics with Presburger constraints: an overview ★ ⋮ Dual systems of tableaux and sequents for PLTL ⋮ A goal-directed decision procedure for hybrid PDL ⋮ Probabilistic Temporal Logics
This page was built for publication: Propositional temporal logics: decidability and completeness
