Barozzini, DavidFrutos Escrig, David DeDella Monica, DarioMontanari, AngeloSala, Pietro2023-06-172023-06-172020-04-12Barozzini, D., Frutos Escrig, D., Della Monica, D. et al. «Beyond ω-Regular Languages: ωT-Regular Expressions and Their Automata and Logic Counterparts». Theoretical Computer Science, vol. 813, abril de 2020, pp. 270-304. DOI.org (Crossref), https://doi.org/10.1016/j.tcs.2019.12.029.0304397510.1016/j.tcs.2019.12.029https://hdl.handle.net/20.500.14352/7725"This is a pre-print of an article published in Theoretical Computer Science. The final authenticated version is available online at: https://doi.org/10.1016/j.tcs.2019.12.029”.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 (-regular languages). We characterize the resulting class of languages in terms of -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 -regular languages and of the corresponding automata.engjournal articlehttps://doi.org/10.1016/j.tcs.2019.12.029https://www.sciencedirect.com/science/article/pii/S0304397519308114open access510.6ω-regular languagesω-regular expressionsCounter automataMonadic second-order logic of one successorInformática (Informática)Lógica simbólica y matemática (Matemáticas)1203.17 Informática1102.14 Lógica Simbólica