Intuitionistic linear temporal logics

DOI10.1145/3365833zbMATH Open1433.03047arXiv1912.12893OpenAlexW2994676117WikidataQ126542510 ScholiaQ126542510MaRDI QIDQ5216145FDOQ5216145

Authors: Philippe Balbiani, Joseph Boudou, Martín Diéguez, David Fernández-Duque 

Publication date: 14 February 2020

Published in: ACM Transactions on Computational Logic (Search for Journal in Brave)

Abstract: We consider intuitionistic variants of linear temporal logic with `next', `until' and `release' based on expanding posets: partial orders equipped with an order-preserving transition function. This class of structures gives rise to a logic which we denote $iltl$, and by imposing additional constraints we obtain the logics $itlb$ of persistent posets and $itlht$ of here-and-there temporal logic, both of which have been considered in the literature. We prove that $iltl$ has the effective finite model property and hence is decidable, while $itlb$ does not have the finite model property. We also introduce notions of bounded bisimulations for these logics and use them to show that the `until' and `release' operators are not definable in terms of each other, even over the class of persistent posets.

Full work available at URL: https://arxiv.org/abs/1912.12893

Recommendations

• Bisimulations for intuitionistic temporal logics
• A decidable intuitionistic temporal logic
• An intuitionistic axiomatization of `eventually'
• Complete intuitionistic temporal logics for topological dynamics
• Combining linear-time temporal logic with constructiveness and paraconsistency

zbMATH Keywords

intuitionistic logictheory of computationtemporal logicbisimulationmathematics of computing

Mathematics Subject Classification ID

Substructural logics (including relevance, entailment, linear logic, Lambek calculus, BCK and BCI logics) (03B47) Subsystems of classical logic (including intuitionistic logic) (03B20) Decidability of theories and sets of sentences (03B25) Temporal logic (03B44)

Cited In (26)

• Unification in linear temporal logic LTL
• Logical Consecutions in Intransitive Temporal Linear Logic of Finite Intervals
• Exploring the Jungle of Intuitionistic Temporal Logics
• Polymodal logic of the class of inductive linear time frames
• A Paraconsistent Linear-time Temporal Logic
• Algebraic Methodology and Software Technology
• Logical consecutions in discrete linear temporal logic
• An algebraic study of tense logics with linear time
• Linear, branching time and joint closure semantics for temporal logic
• On the finite model property of weak intuitionistic tense logic
• The temporal logic of linear time frames with inductions axiom
• Linear and affine logics with temporal, spatial and epistemic operators
• Cyclic Proofs for Linear Temporal Logic
• Computer Science Logic
• The intuitionistic temporal logic of dynamical systems
• Interval Temporal Logic Semantics of Box Algebra
• A strongly complete axiomatization of intuitionistic temporal logic
• A decidable intuitionistic temporal logic
• Time and Gödel: fuzzy temporal reasoning in PSPACE
• Bisimulations for intuitionistic temporal logics
• An intuitionistic axiomatization of `eventually'
• Gödel-Dummett linear temporal logic
• Complete intuitionistic temporal logics for topological dynamics
• Ill-founded proof systems for intuitionistic linear-time temporal logic
• Intuitionistic linear-time \(\mu\)-calculus
• Undecidability of QLTL and QCTL with two variables and one monadic predicate letter

This page was built for publication: Intuitionistic linear temporal logics

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