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

TL;DR
This paper introduces a new formalism for Eve-positional languages, enabling a determinization procedure for non-deterministic Büchi automata recognizing these languages, with optimal size blow-up.
Contribution
It provides a novel formalism characterizing Eve-positional languages and a determinization method with factorial size blow-up, completing prior theoretical frameworks.
Findings
New formalism for Eve-positional languages based on restricted nondeterministic Büchi automata.
Determinization procedure with at most factorial size blow-up.
Construction is state-wise optimal for sufficiently complete alphabets.
Abstract
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 -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 -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…
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
