Positional $ω$-regular languages

TL;DR

This work provides a complete automata-theoretic characterisation of positional ω-regular languages in two-player graph games. The authors introduce signature automata and ε-completable automata, along with universal-graph techniques, to establish equivalences between positionality, structural automata properties, and universal constructions. They derive polynomial-time decision procedures for positionality, prove finite-to-infinite and 1-to-2-player lifts, and show closure under union with prefix-independent components, addressing longstanding conjectures. The framework also extends to bipositionality and to positionality for closed and open ω-regular objectives, including neutrality-letter and lift results, with broad implications for synthesis and verification in infinite-duration games. Overall, the paper advances a unified, constructive theory connecting ω-regular languages, automata structure, and game-theoretic strategy complexity.

Abstract

In the context of two-player games over graphs, a language $L$ is called positional if, in all games using $L$ as winning objective, the protagonist can play optimally using positional strategies, that is, strategies that do not depend on the history of the play. In this work, we describe the class of parity automata recognising positional languages, providing a complete characterisation of positionality for $ω$-regular languages. As corollaries, we establish decidability of positionality in polynomial time, finite-to-infinite and 1-to-2-players lifts, and show the closure under union of prefix-independent positional objectives, answering a conjecture by Kopczyński in the $ω$-regular case.

Figures (24)

• Figure 1: Consider the game above, where "Eve" controls both vertices $v_1$ and $v_2$. Let $W = ab(a+b)^\oo$ be the "winning condition" of the game, that is, "Eve" "wins" if the play starts by $ab$. She has two "positional strategies" $\strat_1$ and $\strat_2$ "winning" from $v_1$ and $v_2$, respectively. However, no "positional strategy" is winning from the entire "winning region" $\{v_1,v_2\}$.
• Figure 2: "Universal graph" $\UPar$ for the "parity objective" over "priorities" $[0,5]$. Vertices are ordered from left to right. Edges between two boxes $B_1 \xrightarrow{x} B_2$ represent that there are edges $v_1\xrightarrow{x} v_2$ for all $v_1\in B_1$ and all $v_2\in B_2$. Edges obtained by monotonicity are not represented: if $v\xrightarrow{x}v'$ and $v"\leq v'$, then $v\xrightarrow{x}v"$ too; for example, by reading colour $5$ from a vertex $v$ one can go to any vertex strictly on the left of $v$. Edges coloured $0$ are not depicted in the figure: they appear between every pair of vertices. The label of a box represents the forms of the names of vertices inside it.
• Figure 3: Representation of the notions of "uniformity", "congruence" and "strong congruence". We picture an automaton with three equivalence classes, each of them represented by a yellow bubble. Green-dotted transitions are "uniform" over the classes, but the relation is not a "congruence" for them. The relation is a "congruence for" blue-dashed transitions, and a "strong congruence for" red-solid transitions.
• Figure 4: On the left, a deterministic automaton recognising the "positional" language $\infOften(a) \vee (\noOcc(a) \wedge \finOften(bb))$. On the right, a representation of an "$\ee$-completion" of the automaton: we can add "$\ee$-transitions" indicated by the tree, that is: $q_2, q_3 \xrightarrow{\ee:0,1} q_1$, $q_2 \xrightarrow{\ee:1} q_3$, $q_3 \xrightarrow{\ee:1} q_2$, $q_3\xrightarrow{\ee:2,3} q_2 \xrightarrow{\ee:2,3} q_1$, and $q\xrightarrow{\ee:x}q$ for all $q$ and odd $x$. Some of these are represented on the left as dotted arrows.
• Figure 5: A game $\G$ in which "Eve" cannot "play optimally using positional strategies" if $\Res{W}$ is not totally ordered. □

Theorems & Definitions (230)

• remark 1
• remark 2
• proposition 1: Ohlmann23Univ
• lemma 1
• lemma 2
• proof
• lemma 3
• proof
• remark 3: Transition-based acceptance
• remark 4