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

DOI10.1016/J.JAL.2014.03.002zbMATH Open1328.03017arXiv1309.0829OpenAlexW3106321783MaRDI QIDQ2447179FDOQ2447179

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)

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.

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

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

zbMATH Keywords

decidabilityaxiomatizationtemporal logicstrong completenesszero-time transitions

Mathematics Subject Classification ID

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

Cites Work

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

Cited In (9)

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

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)