English

Eve-positional languages: putting order into B\"uchi automata

Formal Languages and Automata Theory 2026-04-27 v2

Abstract

An ω\omega-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 ω\omega-regular languages. For this, they introduce the notion of ε\varepsilon-complete parity automaton and show (among other results) that an ω\omega-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\"uchi 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\"uchi 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.

Cite

@article{arxiv.2602.09896,
  title  = {Eve-positional languages: putting order into B\"uchi automata},
  author = {Olivier Idir},
  journal= {arXiv preprint arXiv:2602.09896},
  year   = {2026}
}

Comments

Fixed some major typos, upgraded proofs

R2 v1 2026-07-01T10:29:54.773Z