A propositional linear time logic with time flow isomorphic to ^2

DOI10.1016/J.JAL.2014.03.002MaRDI QIDQ2447179zbMATH OpenOpenAlexFDO

Authors Bojan Marinković, Zoran Ognjanović, Dragan Doder, Aleksandar Perović

Publication date 24 April 2014

Published in Journal of Applied Logic (Search for Journal in Brave)

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

zbMATH Keywords

axiomatizationdecidabilitystrong completenesstemporal logiczero-time transitions

Mathematics Subject Classification ID

Decidability of theories and sets of sentences (03B25) Temporal logic (03B44)

Abstract: Primarily guided with the idea to express zero-time transitions by means of temporal propositional language, we have developed a temporal logic where the time flow is isomorphic to ordinal $omeg{a}^2$ (concatenation of $omega$ copies of $omega$). If we think of $omeg{a}^2$ as lexicographically ordered $omegaimesomega$, then any particular zero-time transition can be represented by states whose indices are all elements of some $nimesomega$. In order to express non-infinitesimal transitions, we have introduced a new unary temporal operator $[omega]$ ($omega$-jump), whose effect on the time flow is the same as the effect of $alphamapstoalpha+omega$ in $omeg{a}^2$. In terms of lexicographically ordered $omegaimesomega$, $[omega]phi$ is satisfied in $<i,j>$-th time instant iff $phi$ is satisfied in $<i+1,0>$-th time instant. Moreover, in order to formally capture the natural semantics of the until operator $mathttU$, we have introduced a local variant $mathttu$ of the until operator. More precisely, $phi,mathttupsi$ is satisfied in $<i,j>$-th time instant iff $psi$ is satisfied in $<i,j+k>$-th time instant for some nonnegative integer $k$, and $phi$ is satisfied in $<i,j+l>$-th time instant for all $0leqslantl<k$. As in many of our previous publications, the leitmotif is the usage of infinitary inference rules in order to achieve the strong completeness.

Recommendations

• The axiomatization of propositional linear time temporal logic
• scientific article; zbMATH DE number 1361487
• The complexity of propositional linear temporal logics
• scientific article; zbMATH DE number 1499103
• A propositional dense time logic
• From linear temporal logic properties to rewrite propositions
• The temporal logic of linear time frames with inductions axiom
• A Paraconsistent Linear-time Temporal Logic
• scientific article; zbMATH DE number 1696880
• A complete axiomatic characterization of first-order temporal logic of linear time

Cites work

• A decidable propositional dynamic logic with explicit probabilities
• A logic for reasoning about time and reliability
• An axiomatization of full computation tree logic
• Axioms for tense logic. I: 'Since' and 'until'
• Dealing with zero-time transitions in axiom systems.
• Decidability for branching time
• Decision procedures and expressiveness in the temporal logic of branching time
• Discrete Linear-time Probabilistic Logics: Completeness, Decidability and Complexity
• scientific article; zbMATH DE number 3129315 (Why is no real title available?)
• scientific article; zbMATH DE number 747023 (Why is no real title available?)
• scientific article; zbMATH DE number 3494394 (Why is no real title available?)
• scientific article; zbMATH DE number 1028831 (Why is no real title available?)
• scientific article; zbMATH DE number 1142326 (Why is no real title available?)
• scientific article; zbMATH DE number 5790393 (Why is no real title available?)
• Logic and time
• REASONING ABOUT TRANSFINITE SEQUENCES
• Reasoning with time and chance
• The complexity of linear-time temporal logic over the class of ordinals
• The complexity of propositional linear temporal logics
• The temporal logic of branching time
• Using branching time temporal logic to synthesize synchronization skeletons

Cited in

(9)

• An epistemic probabilistic logic with conditional probabilities
• On Topologically Relevant Fragments of the Logic of Linear Flows of Time
• Logics with Probability Operators
• Probabilistic Temporal Logics
• Reasoning About Degrees of Confirmation
• A temporal logic for micro- and macro-step-based real-time systems: foundations and applications
• Probability logics for reasoning about quantum observations
• Incomplete Information and Justifications
• Probabilistic temporal logic with countably additive semantics

This page was built for publication: A propositional linear time logic with time flow isomorphic to \(\omega^2\)

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