Eve-positional languages: putting order into Büchi automata

TL;DR

The paper introduces ordered Büchi automata as a precise formalism for Eve-positional ω-regular languages, establishing that these languages are exactly the ordered Büchi languages. It connects this framework to ε-complete parity automata, providing a polynomial translation from ε-complete non-deterministic parity automata to ordered Büchi automata and proving the missing implication in prior work. A general determinization procedure from ordered Büchi automata to deterministic parity automata is presented, with a factorial state bound $\sum_{i=1}^{n-1} i!$, and optimality is shown in cases of sufficiently complete alphabets via a flower-game argument. Collectively, these results give structural insights into Eve-positional languages, enable practical determinization, and sharpen the understanding of the complexity landscape for Eve-positional ω-regular languages.

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 characterizations of Eve-positionallity of $ω$-regular languages. For this, they introduce the notion $\varepsilon$-complete parity automaton and show (among other results) that an $ω$-regular language is Eve-positional if and only if it can be recognized by some $\varepsilon$-completion of a deterministic parity automaton. Colcombet and Idir extended on their work, and obtained a more direct semantic characterization of Eve-positionality. We introduce a new formalism that characterizes the Eve-positional languages, consisting in 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 automaton recognizing such languages, with size blow-up at most factorial. We also show that this construction is, in a suitable sense, optimal.

Figures (9)

• Figure 1: An ordered Büchi automaton recognizing the words with infinitely often a factor $aa$ and only finitely often $bb$.
• Figure 2: An ordered Büchi automaton recognizing the words infinitely many $b$'s, or a factor $bb$ and infinitely many $a$'s.
• Figure 3: The following tiles describe the Rabin language of pairs $(\{d\}, \{a,c\})$ and $(\{b\},\{d\})$.
• Figure 4: If $(vv')^\omega \in L$, necessarily one of the following holds for some state $q\in Q$. In the third and fourth cases, one of the two transitions is necessarily Büchi, but we do not require to make a case disjunction.
• Figure 5: We compute the function $\leader$ from the given "record" $s$ in brown. This defines the set $P$.

Theorems & Definitions (44)

• Theorem 1: 3.1 and 3.2 in CO24Positional
• Remark 2
• Theorem 3: local-posi
• Definition 4: Casares, Ohlmann
• Lemma 4
• Lemma 4: existence of the skeleton
• Theorem 4
• Proposition 4
• Proposition 4
• Theorem 4