Authors: Marinković, Bojan 
Ognjanović, Zoran 
Doder, Dragan
Perović, Aleksandar
Title: A propositional linear time logic with time flow isomorphic to ω2
Journal: Journal of Applied Logic
Volume: 12
First page: 208
Last page: 229
Issue Date: 1-Jan-2014
Rank: M22
ISSN: 1570-8683
DOI: 10.1016/j.jal.2014.03.002
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 ω2 (concatenation of ω copies of ω). If we think of ω2 as lexicographically ordered ω×ω, then any particular zero-time transition can be represented by states whose indices are all elements of some {n}×ω. In order to express non-infinitesimal transitions, we have introduced a new unary temporal operator [ω] (ω-jump), whose effect on the time flow is the same as the effect of α→α+ω in ω2. In terms of lexicographically ordered ω×ω , [ω]φ is satisfied in 〈i,j〉-th time instant iff φ is satisfied in 〈i+1,0〉-th time instant. Moreover, in order to formally capture the natural semantics of the until operator U, we have introduced a local variant u of the until operator. More precisely, φuψ is satisfied in 〈i,j〉-th time instant iff ψ is satisfied in 〈i,j+k〉-th time instant for some nonnegative integer k, and φ is satisfied in 〈i,j+l〉-th time instant for all 0≤lt≤k. As in many of our previous publications, the leitmotif is the usage of infinitary inference rules in order to achieve the strong completeness.
Keywords: Axiomatization | Decidability | Strong completeness | Temporal logic | Zero time transitions
Publisher: Elsevier

Show full item record


checked on Jun 12, 2024

Page view(s)

checked on May 10, 2024

Google ScholarTM




Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.