Jeudi 01 octobre 2026, 14:00 à 15:00

salle des séminaires du département d'informatique

Olivier Idir

(IRIF Université Paris Cité)

An ω-regular language is exist-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 characterizations of exist-positionality of ω-regular languages. For this, they introduce the notion ε-complete parity automaton and show (among other results) that an ω-regular language is exist-positional if and only if it can be recognized by some ε-completion of a deterministic parity automaton. In this joint work with Thomas Colcombet, we provide a new simple combinatorial characterization of exist-positionality for ω-regular conditions. We also propose a new convenient formalism to describe these languages, using Büchi automata with totally ordered states. This allows in term to describe a determinisation procedure transforming an ε-complete parity automaton with n states into an equivalent deterministic parity automaton of size at most n!. This construction is, in a suitable sense, optimal.