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 | 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 ω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
SCOPUSTM
Citations
15
checked on Nov 7, 2024
Page view(s)
23
checked on Nov 8, 2024
Google ScholarTM
Check
Altmetric
Altmetric
Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.