A Propositional Linear Time Logic with Time Flow Isomorphic to ω^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$ (concatenation of $ω$ copies of $ω$). If we think of $ω^2$ as lexicographically ordered $ω\times ω$, then any particular zero-time transition can be represented by states whose indices are all elements of some $\{n\}\timesω$. 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 $α\mapsto α+ω$ in $ω^2$. In terms of lexicographically ordered $ω\times ω$, $[ω] ϕ$ 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 $\mathtt U$, we have introduced a local variant $\mathtt u$ of the until operator. More precisely, $ϕ\,\mathtt 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\leqslant l<k$. As in many of our previous publications, the leitmotif is the usage of infinitary inference rules in order to achieve the strong completeness.