An interval temporal logic characterization of extended -regular languages.

Some extensions of ω-regular languages have been proposed in the literature to express asymptotic properties of ω-words which are not captured by ω-regular languages. They include ωB-regular languages, that extend ω-regular languages with boundedness, ωS-regular languages, that enrich ω-regular ones with strong unboundedness, ωBS-regular languages, that combine ωB- and ωS-regular ones, and ωT-regular languages, that include meaningful languages which are not ωBS-regular. Formal definitions of extended ω-regular languages have been given in terms of both suitable classes of automata and extended ω-regular expressions, while satisfactory temporal logic counterparts are still missing. In this paper, we give a characterization of them in terms of interval temporal logics by providing an explicit encoding of expressions into formulas.