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

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ω2 (concatenation of ω copies of ω  ). If we think of ω2ω2 as lexicographically ordered ω×ωω×ω, then any particular zero-time transition can be represented by states whose indices are all elements of some {n}×ω{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ω2. In terms of lexicographically ordered ω×ωω×ω, [ω]ϕ[ω]ϕ is satisfied in 〈i,j〉〈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〉〈i,j〉-th time instant iff ψ   is satisfied in 〈i,j+k〉〈i,j+k〉-th time instant for some nonnegative integer k, and ϕ   is satisfied in 〈i,j+l〉〈i,j+l〉-th time instant for all 0≤l