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 sonesU.

Beyond $omega BS$-regular Languages: $omegaT$-regular Expressions and Counter-Check Automata

Della Monica, Dario;Angelo Montanari;Pietro Sala
2017-01-01

Abstract

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 sonesU.
File in questo prodotto:
File Dimensione Formato  
gandalf17_editor.pdf

accesso aperto

Tipologia: Versione Editoriale (PDF)
Licenza: Creative commons
Dimensione 405 kB
Formato Adobe PDF
405 kB Adobe PDF Visualizza/Apri

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/11390/1201762
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 1
  • ???jsp.display-item.citation.isi??? 1
social impact