Beyond omega-regular languages: omegaT-regular expressions and their automata and logic counterparts

In the last years, some extensions of ω-regular languages, namely, ωB-regular (ω-regular languages extended with boundedness), ωS-regular (ω-regular languages extended with strong unboundedness), and ωBS-regular languages (the combination of ωB- and ωS-regular ones), have been proposed in the literature. While the first two classes satisfy a generalized closure property, which states that the complement of an ωB-regular (resp., ωS-regular) language is an ωS-regular (resp., ωB-regular) one, the last class is not closed under complementation. The existence of non-ωBS-regular languages that are the complements of some ωBS-regular ones and express fairly natural asymptotic behaviors motivates the search for other significant classes of extended ω-regular languages. In this paper, we present the class of ωT-regular languages, which includes meaningful languages that are not ωBS-regular. We define this new class of languages in terms of ω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 ωT-regular languages. We also provide an encoding of ωT-regular expressions into S1S+U. Finally, we investigate a stronger variant of ωT-regular languages (ωTs-regular languages). We characterize the resulting class of languages in terms of ωTs-regular expressions, and we show how to map it into a suitable class of automata, called counter-queue automata. We conclude the paper with a comparison of the expressiveness of ωT- and ωTs-regular languages and of the corresponding automata.