A Propositional Linear Time Logic with Time Flow Isomorphic to \omega^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 $\omega^2$ (concatenation of $\omega$ copies of $\omega$). If we think of $\omega^2$ as lexicographically ordered $\omega\times \omega$, then any particular zero-time transition can be represented by states whose indices are all elements of some $\{n\}\times\omega$. 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 $\alpha\mapsto \alpha+\omega$ in $\omega^2$. In terms of lexicographically ordered $\omega\times \omega$, $[\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 $\mathtt U$, we have introduced a local variant $\mathtt u$ of the until operator. More precisely, $\phi\,\mathtt u \psi$ 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 $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.