The Memory of $\omega$-Regular and $\mathrm{BC}({𝚺}_2^0)$ Objectives

The simplest strategies are those that assign in advance an outgoing edge to each vertex owned by Eve, and always play along this edge, disregarding all the other features of the play. All the information required to implement such a strategy appears in the game graph itself. Objectives for which such strategies are sufficient to play optimally are called positional (or memoryless). Understanding positionality has been the object of a long line of research. The landmark results of Gimbert and Zielonka [22] and Colcombet and Niwinski [18] gave a good understanding of which objectives are bi-positional, i.e. positional for both players.

More recently, Ohlmann proposed to use universal graphs as a tool for studying positionality (taking Eve’s point of view) [27]. This led to many advances in the study of positionality [2, 28], and most notably, a characterisation of positional $\omega$-regular objectives by Casares and Ohlmann [10], together with a polynomial time decision procedure (and some other important corollaries, more discussion below).

However, in many scenarios, playing optimally requires distinguishing different plays that end in the same vertex. A seminal result of Büchi and Landweber [7] states that in finite games where the objective is an $\omega$-regular language, the winner has a winning strategy that can be implemented by a finite automaton processing the edges of the game; this result was later extended to infinite game graphs by Gurevich and Harrington [23]. Here, the states of the automaton are interpreted as memory states of the strategy, and a natural measure of the complexity of a strategy is the number of such states. More precisely, the memory of an objective $W$ is the minimal $k$ such that whenever Eve wins a game with objective $W$, she has a winning strategy with $k$ states of memory. For $\omega$-regular objectives, this is always finite [7, 23], while the case of positionality discussed above corresponds to memory $k=1$.

Characterising the memory of objectives has been a recurrent research subject since the 1990s. Notable results include the characterisation for Muller objectives by Dziembowski, Jurdziński, and Walukiewicz [19], or for closed objectives by Colcombet, Fijalkow and Horn [16]. However, these are all rather restricted classes of $\omega$-regular objectives. The problem of deciding the memory of $\omega$-regular objectives has been raised in many occasions (see for instance [24, Sect. 9.2], [4, Sect. 4], [17, Conclusions], or [3]), but prior to this work, even computing the memory of open $\omega$-regular objectives (sometimes called regular reachability objectives) was not known to be decidable.

In the special case where the automata implementing strategies are only allowed to read the colours on the edges of the game graph, we speak of chromatic memory. In his PhD thesis, Kopczyński showed that, for prefix-independent $\omega$-regular objectives and over finite game graphs, the chromatic memory can be computed in exponential time [24, Theorem 8.14]. Recently, it was shown that computing the chromatic memory of some restricted subclasses of $\omega$-regular objectives is in fact NP-complete: for Muller objectives [8] and for topologically open or closed objectives [3]. However, the chromatic and the unconstrained memory of objectives may differ, even exponentially [8, 9].

The driving question in Kopczyński’s PhD thesis [24] is whether prefix-independent positional objectives are closed under union, which has become known as Kopczyński’s conjecture. Recently, Kozachinskiy [25] disproved this conjecture, but only for positionality over finite game graphs, and using non-$\omega$-regular objectives. In fact, the conjecture is now known to hold for $\omega$-regular objectives [10] and ${𝚺}_2^0$ objectives [28]. Casares and Ohlmann proposed a generalisation of this conjecture from positional objectives to objectives requiring memory [12, Conjecture 7.1] (see also [24, Proposition 8.11]):

Using the characterisation of [19], it is not hard to verify that the conjecture holds for Muller objectives.

The results in this work apply not only to $\omega$-regular languages, but to the broader class of $\mathrm{BC}({𝚺}_2^0)$ languages. These are boolean combinations of languages in ${𝚺}_2^0$ (countable unions of closed languages), or equivalently, recognised by deterministic parity automata with infinitely many states [31, Sect. 5]. This class includes typical non-$\omega$-regular examples such as energy or mean-payoff objectives (and therefore also their boolean combinations with $\omega$-regular ones) but also broader classes such as unambiguous $\omega$-petri nets [20] and deterministic $\omega$-Turing machines (Turing machines with a Muller condition).

As mentioned above, Ohlmann proposed a characterisation of positionality by means of universal graphs [27]. In 2023, Casares and Ohlmann extended this characterisation to objectives with memory $\le k$ by considering partially ordered universal graphs [12]. Until now, universal graphs have been mainly used to show that certain objectives have memory $\le k$ (usually for $k=1$); this is done by constructing a universal graph for the objective. One technical novelty of this work is to exploit both directions of the characterisation, as we also rely on the existence of universal graphs to obtain decidability results.

Our characterisation is based on the notion of $k$-wise $\epsilon$-completable automata, which extends the key notion of [10] from positionality to finite memory.

In 2024, Casares and Ohlmann characterised positional $\omega$-regular objectives [10], establishing decidability of positionality in polynomial time, and settling Kopczyński’s conjecture for $\omega$-regular objectives. Although the current paper generalises the notions and some of the results from [10] to the case of memory, as well as potentially infinite automata, the proof techniques are significantly different: while [10] is based on intricate successive transformations of parity automata, ours is based on an extraction method in the infinite and manipulates ordinal numbers. Though somewhat less elementary, our proof is notably shorter, and probably easier to read.

When instantiated to the case of memory $1$, we thus extend Kopczyński’s conjecture from $\omega$-regular objectives to positional $\mathrm{BC}({𝚺}_2^0)$ objectives. This also gives an easier proof of decidability of positionality in polynomial time²²2It is explained in [10, Theorem 5.3] how decidability of positionality in polynomial time can be derived, with reasonable efforts, from Kopczyński’s conjecture. for $\omega$-regular objectives. However, some of the results of [10] are not recovered with our methods: the finite-to-infinite and 1-to-2-player lifts, as well as closure of positionality under addition of neutral letters.

A $\mathrm{SS}$-graph $G$ is given by a set of vertices $V(G)$ and a set of coloured, directed edges $E(G)\subseteq V(G)\times \mathrm{SS}\times V(G)$. We write $v\stackrel{𝑐}{\to }{v}^{\prime }$ for edges $(v,c,v^{\prime })$. A path is a sequence of edges with matching endpoints $(v_0\stackrel{c_0}{\to }{v}_1)(v_1\stackrel{c_0}{\to }{v}_2)\mathrm{\dots }$ which we write as $v_0\stackrel{c_0}{\to }{v}_1\stackrel{c_1}{\to }\mathrm{\dots }$. Paths can be empty, finite, or infinite, and have a label $c_0{c}_1\mathrm{\dots }$. Throughout the paper, graphs are implicitly assumed to be without dead-end: every vertex has an outgoing edge.

We say that a vertex $v$ in a $\mathrm{\Sigma }$-graph (resp. a $(\mathrm{\Sigma }\cup \{\epsilon \})$-graph) satisfies an objective $W\subseteq {\mathrm{\Sigma }}^{\omega }$ if the label of any infinite path from $v$ belongs to $W$ (resp. to $W^{\epsilon }$). A pointed graph is a graph with an identified initial vertex. A pointed graph satisfies an objective $W\subseteq {\mathrm{\Sigma }}^{\omega }$ if the initial vertex satisfies $W$; a non-pointed graph satisfies an objective if all its vertices do. An infinite tree is a sinkless pointed graph whose initial vertex is called the root, and with the property that every vertex admits a unique path from the root.

A morphism from a $\mathrm{\Sigma }$-graph $G$ to a $\mathrm{\Sigma }$-graph $H$ is a map $\varphi :V(G)\to V(H)$ such that for any edge $v\stackrel{𝑐}{\to }{v}^{\prime }$ in $G$, it holds that $\varphi (v)\stackrel{𝑐}{\to }\varphi (v^{\prime })$ is an edge in $H$. Morphisms between pointed graphs should moreover send the initial vertex of $G$ to the initial vertex of $H$. Morphisms need not be injective. We write $G\stackrel{}{\to }H$ when there exists a morphism $\varphi :G\to H$.

A game is given by a pointed $(\mathrm{\Sigma }\cup \{\epsilon \})$-graph $G$ together with an objective $W\subseteq {\mathrm{\Sigma }}^{\omega }$, and a partition of the vertex set $V(G)=V_{\text{Eve}}\bigsqcup V_{\text{Adam}}$ into the vertices controlled by Eve and those controlled by Adam. A strategy⁴⁴4We follow the terminology from [12]. The classical notion of a strategy as a function $f:E{(G)}^{\ast }\to V(G)$ can be recovered by considering the graph with vertices $E{(G)}^{\ast }$, and edges $\rho \stackrel{𝑒}{\to }\rho e$. (for Eve) is a pointed graph together with a morphism $\pi$ towards $G$, satisfying that for every edge $v\stackrel{𝑐}{\to }{v}^{\prime }$ in the game, where $v\in V_{\text{Adam}}$, and for all $u\in {\pi }^{-1}(v)$, there is an edge $u\stackrel{𝑐}{\to }{u}^{\prime }$ such that $u^{\prime }\in {\pi }^{-1}(v^{\prime })$. A strategy is winning if it satisfies the objective $W$ of the game. We say that Eve wins if there exists a winning strategy.

A finite-memory strategy⁵⁵5It is common to define a memory structure as an automaton reading the edges of a game graph. This notion can be recovered by taking $k$ as the states of the automaton. is a strategy with vertices $V(G)\times k$ and projection $\pi (v,m)=v$, with the additional requirement that for every edge $(v,m)\stackrel{𝜀}{\to }(v^{\prime },m^{\prime })$, it holds that $m=m^{\prime }$. We say that $k$ is the memory of the strategy, and numbers $1,\mathrm{\dots },k$ are called memory states. Informally, the requirement above says that when reading an $\epsilon$-transition in the game, we are not allowed to change the memory state; this is called $\epsilon$-memory in [12] (to which we refer for more discussion), but since it is the main kind of memory in this paper, we will simply call it the memory.

A finite-memory strategy is called chromatic if there is a map $\chi :k\times (\mathrm{\Sigma }\cup \{\epsilon \})\to k$ such that for every edge $(v,m)\stackrel{𝑐}{\to }(v^{\prime },m^{\prime })$ in the strategy, it holds that $m^{\prime }=\chi (m,c)$. We say that $\chi$ is the chromatic update. Note that necessarily, we have $\chi (m,\epsilon )=m$ for every memory state $m$.

The (chromatic) memory of an objective $W$ is the minimal $k$ such that for every game with objective $W$, if Eve has a winning strategy, she has a winning (chromatic) strategy with memory $\le k$.

A $k$-blowup $ℬ$ of an automaton $𝒜$ is any automaton with $V(ℬ)\subseteq V(𝒜)\times \{1,\mathrm{\dots },k\}$, with initial state in $\{q_0\}\times k$ and such that for each transition $q\stackrel{a:y}{\to }{q}^{\prime }$ in $𝒜$ and each $m\in k$, there is a transition $(q,m)\stackrel{a:y}{\to }(q^{\prime },\mathrm{\_})$. We also allow for extra transitions in $ℬ$. Note that in this case $L(𝒜)\subseteq L(ℬ)$.

A $k$-automaton is just an automaton whose states are a subset of $Q\times k$, for some set $Q$; for instance, $k$-blowups are $k$-automata. Equivalently, these are automata with a partition of their states in $k$ subsets. For a state $(q,m)$ in a $k$-automaton, $m$ is called its memory state. A $k$-automaton is called chromatic if there is a map $\chi :\{1,\mathrm{\dots },k\}\times (\mathrm{\Sigma }\cup \{\epsilon \})\to \{1,\mathrm{\dots },k\}$ such that for all transition $(q,m)\stackrel{a:y}{\to }(q^{\prime },m^{\prime })$ it holds that $m^{\prime }=\chi (m,c)$.

Let $𝒜$ be an automaton with alphabet $\mathrm{\Sigma }$ and index $d$, and let $S$ be a $d$-graph. We define their cascade product $𝒜⋉S$ to be the $(\mathrm{\Sigma }\cup \left\{\epsilon \right\})$-graph with vertices $V(𝒜)\times V(S)$ and edges

If $S$ is a pointed graph with intial vertex $s_0$, then $𝒜⋉S$ is pointed with initial vertex $(q_0,s_0)$. It is easy to check that we then have the following lemma.

A $k$-automaton $𝒜$ with index $d$ is called $k$-wise $\epsilon$-complete if for each even $x\in d$, for each memory state $m$ and each ordered pair of states $(q,m),(q^{\prime },m)$:

Intuitively, having an edge $(q,m)\stackrel{\epsilon :x}{\to }(q^{\prime },m)$ means that “$(q,m)$ is much better than $(q^{\prime },m)$”, as one may freely go from $(q,m)$ to $(q^{\prime },m)$ and even see a good priority on the way. Similarly, $(q^{\prime },m)\stackrel{\epsilon :x+1}{\to }(q,m)$ means that “$(q^{\prime },m)$ is not much worse than $(q,m)$”.

It is also useful to consider how the definition instantiates when applied to both ordered pairs $⟨(q,m),(q^{\prime },m)⟩$ and $⟨(q^{\prime },m),(q,m)⟩$. Since automata exclude accepting runs which are ultimately comprised of $\epsilon$-transitions, we cannot have $(q,m)\stackrel{\epsilon :x}{\leftrightarrow }(q^{\prime },m)$, and therefore $\epsilon$-completability rewrites as: For each $x$, each memory state $m$ and each unordered pair $(q,m),(q^{\prime },m)$ of states,

Hence an alternative, maybe more useful view (this is the point of view adopted in [10]) is that, up to applying some adequate closure properties, a $k$-wise $\epsilon$-complete automaton is endowed with the following structure: for each even priority $x$ and each memory state $m$, the states with memory state $m$ are totally preordered by the relation $\stackrel{x+1}{\to }$, and the relation $\stackrel{𝑥}{\to }$ is the strict version of this preorder. Moreover, for $x^{\prime }>x$, the $x^{\prime }$-preorder is a refinement of the $x$-preorder.

A $k$-automaton $𝒜$ is called $k$-wise $\epsilon$-completable if one may add $\epsilon$-transitions to it so as to turn it into a $k$-wise $\epsilon$-complete automaton ${𝒜}^{\epsilon }$ satisfying $L({𝒜}^{\epsilon })=L(𝒜)$. We simply say “$\epsilon$-complete” (resp. “$\epsilon$-completable”) as a shorthand for “1-wise $\epsilon$-complete” (resp. “1-wise” $\epsilon$-completable).

The following theorem, a key result in [12] where it is called the structuration lemma, will also be crucial to this work. Recall that we see well-founded pointed graphs as automata with only $0$-transitions, and we apply the terms $k$-blowup and $\epsilon$-completable to them accordingly.

Given an objective $W$ and a cardinal $\kappa$, we say that a graph $U$ is $(\kappa ,W)$-universal if for any infinite tree $T$ of cardinality satisfying $W$, there is a morphism $\varphi :T\to U$ such that $\varphi (t_0)$ satifies $W$ in $U$, where $t_0$ is the root of $T$. We may now rephrase the main theorem of [12] in terms of $\epsilon$-complete universal graphs.

We now give an explicit definition of a $(\kappa ,{\mathrm{Parity}}_d)$-universal graph $S_d^{\kappa }$ which is $\epsilon$-complete. These ideas date back to the works of Streett and Emerson, who coined the name signatures [30], and were made more explicit by Walukiewicz [33]. Vertices are tuples of ordinals , indexed by odd priorities in $d$ and ordered lexicographically (with the smaller indices being the most significant). For a tuple $s$ and index $y$, we let be the tuple obtained from $s$ by restricting to coordinates with index . Edges are given by

and $\epsilon$-edges are given by $s\stackrel{𝜀}{\to }{s}^{\prime }$ if and only if $s\ge s^{\prime }$.

We will work extensively with such tuples, as well as their prefixes and suffixes. For readability, we also use subscripts to indicate which (odd) coordinates are concerned, for instance will be our notation for tuples of ordinals indexed with odd priorities , and similarly for $s_{>x}$. Concatenation of tuples is written like for words, therefore denotes a tuple indexed by all odd priorities (i.e. an vertex of $S_{\kappa }^d$). We treat and $s_{>x}$ as different variables, which we may quantify independently.

Take a tree $T$ of size which satisfies $W$. We should show that $T\to U$. Since $ℬ$ is deterministic, we can define a labelling $\rho :V(T)\to V(ℬ)$ by mapping $t_0$ to $q_0$ and $t\mapsto q$ if the run of $ℬ$ on the finite word labelling the path $t_0\stackrel{}{\to }t$ ends in $q$. Then, any infinite path from $t_0$ in $T$ is mapped to a run in $ℬ$ that is accepting (since $T$ satisfies $W$). Therefore the tree $T^{\prime }$ obtained by taking $T$ and replacing edge-labels by the priorities appearing in their $\rho$-images satisfies ${\mathrm{Parity}}_d$ and has size , so there is a morphism $\mu :T\to S$. It is a direct check that $(\rho ,\mu ):V(T)\to V(ℬ)\times V(S)=V(U)$ indeed defines a morphism. $\mathrm{⊲}$

Showing that $U$ is $k$-wise $\epsilon$-complete is slightly trickier.

Well-foundedness of $U$ follows directly from Lemma 2. Let us write $B_1,\mathrm{\dots },B_k$ for the $k$ parts of ${ℬ}^{\epsilon }$; the $k$ parts of $U$ will be $B_1\times V(S),\mathrm{\dots },B_k\times V(S)$. If applicable, chromaticity is a direct check. Let $(b,s),(b^{\prime },s^{\prime })\in V(U)$ be in the same part, i.e. $b,b^{\prime }\in B_i$ for some $i$. Let $x_0$ be the minimal even priority such that $b\stackrel{\epsilon :x_0}{\to }{b}^{\prime }$ in ${ℬ}^{\epsilon }$ (if such an $x$ does not exist then $x_0=d+2$). Then let $y_0$ be the minimal odd priority such that $s_{\le y_0}^{\prime }>s_{\le y_0}$ (as previously, if $s=s^{\prime }$ then we let $y_0=d+1$). We distinguish two cases.

1. (1)

   If . Then we have $b\stackrel{\epsilon :x_0}{\to }{b}^{\prime }$ in ${ℬ}^{\epsilon }$ and which gives $s\stackrel{x_0}{\to }{s}^{\prime }$ in $S$. Thus we get $(b,s)\stackrel{𝜀}{\to }(b^{\prime },s^{\prime })$ in $U$.

2. (2)

   If . Then $s_{\le y_0}^{\prime }>s_{\le y_0}$, which gives $s^{\prime }\stackrel{y_0}{\to }s$ in $S$. Since ${ℬ}^{\epsilon }$ is $k$-wise $\epsilon$-complete and by definition of $x_0$, we also have $b^{\prime }\stackrel{\epsilon :y_0}{\to }b$ in ${ℬ}^{\epsilon }$, therefore $(b^{\prime },s^{\prime })\stackrel{𝜀}{\to }(b,s)$ in $U$.

We conclude that either $(b,s)\stackrel{𝜀}{\to }(b^{\prime },s^{\prime })$ or $(b^{\prime },s^{\prime })\stackrel{𝜀}{\to }(b,s)$, as required. $\mathrm{⊲}$