Propositional temporal logics: decidability and completeness
From MaRDI portal
Publication:4444910
DOI10.1093/JIGPAL/8.1.55zbMATH Open1033.03009OpenAlexW1982302236MaRDI QIDQ4444910FDOQ4444910
Authors: Orna Lichtenstein, Amir Pnueli 
Publication date: 28 January 2004
Published in: Logic Journal of the IGPL (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1093/jigpal/8.1.55
Recommendations
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)
Cited In (60)
- Probabilistic temporal logic with countably additive semantics
- SAT meets tableaux for linear temporal logic satisfiability
- Extended bounded response LTL: a new safety fragment for efficient reactive synthesis
- Gödel-Dummett linear temporal logic
- Title not available (Why is that?)
- Title not available (Why is that?)
- Temporal Assertions with Parametrized Propositions
- A general tableau method for propositional interval temporal logics: theory and implementation
- Exploring the Jungle of Intuitionistic Temporal Logics
- Propositional Projection Temporal Logic, B $\ddot{u}$ chi Automata and ω-Regular Expressions
- A survey on temporal logics for specifying and verifying real-time systems
- Title not available (Why is that?)
- Rules admissible in transitive temporal logic \(\mathrm{T}_{\mathrm{S}4}\), sufficient condition
- Axioms for real-time logics
- Dynamic topological logic of metric spaces
- Title not available (Why is that?)
- Interval vs. point temporal logic model checking. An expressiveness comparison
- Complete Proof System for QPTL
- Title not available (Why is that?)
- Temporal Verification of Fault-Tolerant Protocols
- An alternating-time temporal logic with knowledge, perfect recall and past: axiomatisation and model-checking
- One-pass and tree-shaped tableau systems for TPTL and \(\mathrm{TPTL_b+Past}\)
- Compositional reasoning using intervals and time reversal
- Cut-free sequent systems for temporal logic
- A decision procedure for combinations of propositional temporal logic and other specialized theories
- Title not available (Why is that?)
- Title not available (Why is that?)
- A sound and complete axiomatization for dynamic topological logic
- A decision procedure for propositional projection temporal logic with infinite models
- Partial cut elimination for propositional discrete linear time temporal logic
- A hierarchical completeness proof for propositional temporal logic
- 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 propositional probabilistic logic with discrete linear time for reasoning about evidence
- Completeness of a branching-time logic with possible choices
- Linear-time temporal logics with Presburger constraints: an overview
- Definability and decidability of binary predicates for time granularity
- A complete axiom system for propositional projection temporal logic with cylinder computation model
- Finite-trace linear temporal logic: coinductive completeness
- Title not available (Why is that?)
- Title not available (Why is that?)
- Embedding Linear-Time Temporal Logic into Infinitary Logic: Application to Cut-Elimination for Multi-agent Infinitary Epistemic Linear-Time Temporal Logic
- Non-deterministic semantics for dynamic topological logic
- Invariant-free clausal temporal resolution
- The intuitionistic temporal logic of dynamical systems
- A goal-directed decision procedure for hybrid PDL
- A decision procedure and complete axiomatization for projection temporal logic
- Refutation-aware Gentzen-style calculi for propositional until-free linear-time temporal logic
- Dual systems of tableaux and sequents for PLTL
- Model Theoretic Syntax and Parsing
- Complete intuitionistic temporal logics for topological dynamics
- Efficient decision procedure for propositional projection temporal logic
- Branching time? Pruning time!
- Completeness and decidability of tense logics closely related to logics above K4
- Title not available (Why is that?)
- Decidable temporal and sequential relevant logics*
- Probabilistic Temporal Logics
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Tangled modal logic for topological dynamics
This page was built for publication: Propositional temporal logics: decidability and completeness
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4444910)
