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

摘要

In the last years, some extensions of omega-regular languages, namely, omega B-regular (omega-regular languages extended with boundedness), omega S-regular (omega-regular languages extended with strong unboundedness), and omega BS-regular languages (the combination of omega B- and omega 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 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 asymptotic behaviors motivates the search for other significant classes of extended omega-regular languages. In this paper, we present the class of omega T-regular languages, which includes meaningful languages that are not omega BS-regular. We define this new class of languages 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. We also provide an encoding of omega T-regular expressions into S1S+U. Finally, we investigate a stronger variant of omega T-regular languages (omega T-s -regular languages). We characterize the resulting class of languages in terms of omega T-s -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 omega T- and omega T-s -regular languages and of the corresponding automata. (C) 2020 Elsevier B.V. All rights reserved.