Beyond $omega BS$-regular Languages: $omegaT$-regular Expressions and Counter-Check Automata

In the last years, various extensions of $omega$-regular languages have been proposed in the literature, including $omega{B}$-regular ($omega$-regular languages extended with boundedness), $omega{S}$-regular ($omega$-regular languages extended with strict unboundedness), and $omega{BS}$-regular languages (the combination of $omega{B}$- and $omega{S}$-regular ones). While the first two classes satisfy a generalized closure property, namely, the complement of an $omega{B}$-regular (resp., $omega{S}$-regular) language is an $omega{S}$-regular (resp., $omega{B}$-regular) one, the last class is not closed under complementation. The existence of non-$omega{BS}$-regular languages that are the complements of some $omega{BS}$-regular ones and express fairly natural properties of reactive systems motivates the search for other well-behaved classes of extended $omega$-regular languages. In this paper, we introduce the class of $omega{T}$-regular languages, that includes meaningful languages which are not $omega{BS}$-regular. We first define it in terms of $omega{T}$-regular expressions. Then, we introduce a new class of automata (counter-check automata) and we prove that (i) their emptiness problem is decidable in PTIME and (ii) they are expressive enough to capture $omega{T}$-regular languages (whether or not $omega{T}$-regular languages are expressively complete with respect to counter-check automata is still an open problem). Finally, we provide an encoding of $omega{T}$-regular expressions into sonesU.