Eve-positional languages: putting order into Büchi automata
Fuente:
arXiv
Guardado en:
| Autor principal: | |
|---|---|
| Formato: | Preprint |
| Publicado: |
2026
|
| Materias: | |
| Acceso en línea: | |
| Etiquetas: |
Agregar Etiqueta
Sin Etiquetas, Sea el primero en etiquetar este registro!
|
| _version_ | 1866910161368514560 |
|---|---|
| author | Idir, Olivier |
| author_facet | Idir, Olivier |
| contents | An $ω$-regular language is Eve-positional if, in all games with this language as objective, the existential player can play optimally without keeping any information from the previous moves. This notion plays a crucial role in verification, automata theory and synthesis.
Casares and Ohlmann recently gave several characterisations of Eve-positionality of $ω$-regular languages. For this, they introduce the notion of $\varepsilon$-complete parity automaton and show (among other results) that an $ω$-regular language is Eve-positional if and only if it can be recognised by some $\varepsilon$-completion of a deterministic parity automaton. Colcombet and Idir built on their work, and obtained a more direct algebraic characterisation of Eve-positionality.
We introduce a new formalism that characterises the Eve-positional languages, consisting of a restriction of non-deterministic Büchi automata. This allows us to complete a missing implication in Casares and Ohlmann's work. We then use this formalism to describe a determinization procedure for non-deterministic Büchi automata recognising such languages, with size blow-up at most factorial. We also show that this construction is state-wise optimal for languages over sufficiently complete alphabets. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2602_09896 |
| institution | arXiv |
| publishDate | 2026 |
| record_format | arxiv |
| spellingShingle | Eve-positional languages: putting order into Büchi automata Idir, Olivier Formal Languages and Automata Theory 68Q45 F.4.3 An $ω$-regular language is Eve-positional if, in all games with this language as objective, the existential player can play optimally without keeping any information from the previous moves. This notion plays a crucial role in verification, automata theory and synthesis. Casares and Ohlmann recently gave several characterisations of Eve-positionality of $ω$-regular languages. For this, they introduce the notion of $\varepsilon$-complete parity automaton and show (among other results) that an $ω$-regular language is Eve-positional if and only if it can be recognised by some $\varepsilon$-completion of a deterministic parity automaton. Colcombet and Idir built on their work, and obtained a more direct algebraic characterisation of Eve-positionality. We introduce a new formalism that characterises the Eve-positional languages, consisting of a restriction of non-deterministic Büchi automata. This allows us to complete a missing implication in Casares and Ohlmann's work. We then use this formalism to describe a determinization procedure for non-deterministic Büchi automata recognising such languages, with size blow-up at most factorial. We also show that this construction is state-wise optimal for languages over sufficiently complete alphabets. |
| title | Eve-positional languages: putting order into Büchi automata |
| topic | Formal Languages and Automata Theory 68Q45 F.4.3 |
| url | https://arxiv.org/abs/2602.09896 |