Beyond ωBS-regular Languages: ωT-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 S1S+U.