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$\mathrm{.}Intermsoflexicographicallyordered$\omega\times \omega$,$[\omega] \phi$issatisfiedin$\ < i,j\ >$-th time instant iff $\varphi$ is satisfied in $<i+1,0>$-th time instant. Moreover, in order to formally capture the natural semantics of the until operator $\mathtt U$,wehaveintroducedalocalvariant$\mathtt u$ of the until operator. More precisely, $\varphi \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 $\varphi$ is satisfied in $<i,j+l>$-th time instant for all $0⩽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.