Half-Positional Objectives Recognized by Deterministic Büchi Automata (Extended Abstract)

1 Introduction

Graph Games and Reactive Synthesis. We study zerosum turn-based games on graphs [Fijalkow et al., 2023] confronting two players, P1 and P2. They interact by moving a pebble in turns through the edges of a graph, ad infinitum. Each vertex belongs to a player, and the owner of the current vertex decides where to go next. Edges of the graph are labeled with colors, and this interaction thus produces an infinite sequence of colors. The objective of the game is specified by a subset of infinite sequences of colors, and P1 wins if the produced sequence is in this set. We are interested in finding a winning strategy for P1, i.e., a function indicating how P1 should move in any situation, guaranteeing the achievement of the objective, whatever the strategy of P2.

∗Extended abstract of the eponymous paper from the proceedings of CONCUR 2022. This work has been supported by the ANR Project MAVeriQ (ANR-20-CE25-0012) and by the Fonds de la Recherche Scientifique - FNRS under Grant n° T.0188.23 (PDR ControlleRS). Mickael Randour is an F.R.S.-FNRS Research Associate and a member of the TRAIL Institute. Pierre Vandenhove is an F.R.S.-FNRS Research Fellow.

This game-theoretic model is particularly fitted to study the reactive synthesis problem [Bloem et al., 2018], which aims at the automated construction of a provably-correct controller for a system (P1) trying to satisfy a specification (the objective) while interacting continuously with an uncontrollable environment (P2). This comes down to finding a winning strategy for P1 in the derived game.

In general, in a graph game, a strategy may need memory in order to be winning. This means that only observing the current graph vertex may not yield sufficient information to make an optimal decision; additional information about the past of the interaction is also required. For instance, if there are two colors a and b, and the objective of P1 is to see twice the color a in a row, memory is needed to win in some game graphs, such as the one in Figure 1. From vertex v, P1 has a choice among ab and ba, and it is possible to win by playing any infinite word starting with baab. However, a strategy without memory (called positional) from v can only achieve the infinite words baba . . . or abab . . ., both losing.

b

Figure 1: Memory is needed to see a twice in a row from v.

Some objectives do not need memory, no matter the game graph. This is for instance the case of the B¨uchi objective [Fijalkow et al., 2023]: if the goal is to see a color infinitely often and there is a winning strategy for P1 in some game graph, then there is also a positional winning strategy for P1. This is a beneficial property to obtain a controller for the system that is as simple as possible to implement.

Half-Positionality. We intend to understand for which objectives positional (also called memoryless) strategies suffice for P1 to play optimally (i.e., to win whenever it is possible) - we call these objectives half-positional. We distinguish half-positionality from bipositionality (or memorylessdeterminacy), which refers to objectives for which positional strategies suffice to play optimally for both players.

Many natural objectives have been shown to be bipositional over games on finite and sometimes infinite graphs: e.g., discounted sum [Shapley, 1953], mean-payoff [Ehrenfeucht and Mycielski, 1979], parity [Emerson and Jutla, 1991], total payoff [Gimbert and Zielonka, 2004], energy [Bouyer et al., 2008], or average-energy games [Bouyer et al., 2018]. Bipositionality can be established using general criteria and characterizations, over games on both finite graphs [Gimbert and Zielonka, 2004; Gimbert and Zielonka, 2005; Aminof and Rubin, 2017] and infinite graphs [Colcombet and Niwi´nski, 2006]. Yet, there exist many objectives and combinations thereof for which one player, but not both, has positional optimal strategies (Rabin conditions [Klarlund and Kozen, 1991; Klarlund, 1994], mean-payoff parity [Chatterjee et al., 2005], energy parity [Chatterjee and Doyen, 2012]. . . ), and to which these results do not apply.

Various attempts have been made to understand common underlying properties of half-positional objectives and provide sufficient conditions [Kopczy´nski, 2006; Kopczy´nski, 2007; Kopczy´nski, 2008; Bianco et al., 2011]. These sufficient conditions are not general enough to prove halfpositionality of some very simple objectives, even in the well-studied class of ω-regular objectives [Bianco et al., 2011, Lemma 13]. An interesting characterization uses universal graphs [Ohlmann, 2023]; although it brings insight into the structure of half-positional objectives, showing halfpositionality through the use of universal graphs is not always straightforward, and has not yet been applied in a systematic way to ω-regular objectives. The proof of our characterization makes use of this novel tool.

Furthermore, multiple questions concerning halfpositionality remain open [Kopczy´nski, 2008]. For instance, it is still unclear how to decide half-positionality, even for ω-regular objectives in general. A result in this direction is given by Kopczy´nski [Kopczy´nski, 2007], who showed that half-positionality over finite graphs is decidable in exponential time for a subclass of the ω-regular objectives (incomparable to the one considered in this article). It is unknown whether this is doable in polynomial time, and no algorithm is known for half-positionality over infinite graphs.

Half-Positionality in RL. Reinforcement learning (RL) shares goals similar to synthesis, in that a strategy achieving some specification must be built. While it is common that synthesis considers strategies with memory, half-positionality of the objective is typically a requirement to apply RL algorithms, as decisions are usually taken simply based on the current state of the game [Sutton and Barto, 2018]. Given an objective and a graph, two steps can be taken to apply RL algorithms [Hahn et al., 2022a]: (i) inject sufficient information in the graph to guarantee that positional strategies suffice, and (ii) label vertices/edges with rewards such that strategies winning for the objective correspond to optimal strategies w.r.t. RL. Half-positional objectives correspond to the objectives for which no information must be added in step (i). Given step (i) (on which we focus in this article), note that step (ii) is not always straightforward [Hahn et al., 2022b].

Omega-Regular Objectives and Deterministic B¨uchi Automata. A central class of objectives, whose halfpositionality is not yet completely understood, is the class of ω-regular objectives. There are multiple equivalent definitions for them: they are the objectives defined, e.g., by ω-regular expressions, by non-deterministic B¨uchi automata [McNaughton, 1966], and by deterministic parity automata [Mostowski, 1984]. These objectives coincide with the class of objectives defined by monadic second-order formulas [B¨uchi, 1962], and they encompass linear-time temporal logic (LTL) specifications [Pnueli, 1977]. Part of their interest is due to the landmark result that finite-state machines are sufficient to implement optimal strategies in ω-regular games [B¨uchi and Landweber, 1969; Gurevich and Harrington, 1982], implying the decidability of related problems.

Here, we focus on the subclass of ω-regular objectives recognized by deterministic B¨uchi automata (DBA), that we call DBA-recognizable. The winner of a game with a DBArecognizable objective can be decided in polynomial time in the size of the graph and the DBA by solving a B¨uchi game on their product [Bloem et al., 2018], but this does not yield the smallest possible strategies in general.

Contributions. Our main contribution is a characterization (Theorem 1) of half-positionality for DBA-recognizable objectives through a conjunction of three easy-to-check conditions, presented in Section 3.

A few examples of simple DBA-recognizable objectives not encompassed by previous half-positionality criteria [Kopczy´nski, 2006; Bianco et al., 2011] are, e.g., reaching a color twice [Bianco et al., 2011, Lemma 13] and weak parity [Thomas, 2008]. We also refer to Example 3, which is half-positional but not bipositional, and whose halfpositionality is straightforward using our characterization.

Various corollaries with practical and theoretical interest follow from our characterization. In particular, we obtain a painless path to show that given a DBA, the half-positionality (over both finite and infinite graphs) of the objective it recognizes is decidable in time O(k · n4 ), where k is the number of colors and n is the number of states of the DBA.

For additional technical discussions, examples, and complete proofs, we direct the interested reader to the conference version of this paper [Bouyer et al., 2022a].

Other Related Works. We have discussed relevant literature on half-positionality and bipositionality. A more general quest is to understand memory requirements when positional strategies are not powerful enough: e.g., [Le Roux et al., 2018; Bouyer et al., 2022c].

Memory requirements have been precisely characterized for some classes of ω-regular objectives (not encompassing DBA-recognizable objectives), such as Muller conditions [Dziembowski et al., 1997; Zielonka, 1998; Casares, 2022; Casares et al., 2022] and general safety and reachability objectives [Colcombet et al., 2014; Bouyer et al., 2023a].

2 Preliminaries

Letter C refers to a finite non-empty set of colors. Given a set A, we write respectively A∗ , A+, and Aω for the set of finite, non-empty finite, and infinite sequences of elements of A. We denote by ε the empty word.

Arenas. We consider two players P1 and P2. An arena is a tuple A = (V, V1, V2,E) such that V is a non-empty set of vertices (of any cardinality), E ⊆ V × C × V is a set of colored edges, and V is the disjoint union of V1 and V2. Vertices in V1 are controlled by P1 and vertices in V2 are controlled by P2. We assume arenas to be nonblocking: for all v ∈ V , there exists some (v, c, v′ ) ∈ E. For v0 ∈ V , a play of A from v0 is an infinite sequence of edges π = (v0, c1, v1)(v1, c2, v2)(v2, c3, v3) . . . ∈ Eω . A history is a finite prefix of a play. For convenience, we define an empty path λv for every v ∈ V . If γ = (v0, c1, v1) . . . (vn-1, cn, vn) is a non-empty history, we define last(γ) = vn. For an empty path λv, we define last(λv) = v. For i ∈ {1, 2}, we denote by Histsi(A) the set of histories γ of A such that last(γ) ∈ Vi.

Strategies. Let i ∈ {1, 2}. A strategy of Pi on A is a function σi : Histsi(A) → E such that for all γ ∈ Histsi(A), the first component of σi(γ) coincides with last(γ). Given a strategy σi of Pi, we say that a play π = e1e2 . . . is consistent with σi if for all finite prefixes γ = e1 . . . en of π such that last(γ) ∈ Vi, σi(γ) = en+1. A strategy σi is positional if its outputs only depend on the current vertex and not on the whole history, i.e., if there exists a function f : Vi →E such that for γ ∈ Histsi(A), σi(γ) = f(last(γ)).

Objectives. An objective is a set W ⊆ C ω . An infinite word w ∈ C ω is winning if w ∈ W, and losing if w /∈ W. A game is a tuple (A,W) of an arena A and an objective W.

Optimality and Half-Positionality. Let A = (V, V1, V2,E) be an arena, (A,W) be a game, and v ∈ V . A strategy σ1 of P1 is winning from v if all plays consistent with σ1 induce a sequence of colors in W. A strategy of P1 is optimal for P1 in (A,W) if it is winning from all the vertices from which P1 has a winning strategy. We stress that this notion of optimality requires a single strategy to be winning from all the winning vertices (a property sometimes called uniformity).

An objective W is half-positional if for all arenas A, there exists an optimal strategy of P1 that is positional.

Deterministic Automata. A deterministic B¨uchi automaton (DBA) is a tuple B = (Q, C, qinit, δ, α) where Q is a finite set of states, qinit ∈ Q is an initial state, δ : Q×C → Q is an update function, and α ⊆ Q×C is a set of B¨uchi transitions. 1 We denote by δ∗ the natural extension of δ to finite words.

A word c1c2 . . . ∈ C ω is in the language of a DBA B if, when read from qinit following δ, it sees infinitely many B¨uchi transitions. The language of a DBA is denoted L(B). An objective W is DBA-recognizable if there exists a DBA B such that W = L(B).

Example 1. We give two examples of DBA in Figure 2. The language of the one on the left is the set of infinite words seeing a infinitely often; for the one on the right, it is the set of words seeing a infinitely often, or aa at some point.

Remark 1. The language of a DBA is always an ω-regular language. However, unlike their nondeterministic counterparts, DBA recognize only a proper subset of the ω-regular languages [Wagner, 1979].

1 We use transition-based acceptance conditions, and it is technically important in our approach.

Right Congruence and Prefix Preorder. Let W ⊆ C ω be an objective. For a finite word w ∈ C ∗ , we write w-1W = {w′ ∈ C ω | ww′ ∈ W} for the set of winning continuations of w. We define the right congruence ∼W ⊆ C ∗ × C ∗ of W as w1 ∼W w2 if w-1 1 W = w-1 2 W (meaning that w1 and w2 have the same winning continuations). It is an equivalence relation. When the context is clear, we simply write ∼. For w ∈ C ∗ , we denote by [w] ⊆ C ∗ its equivalence class of ∼.

When ∼ has finitely many equivalence classes, we can associate a natural deterministic "automaton structure" S∼ = (Q∼, C, ˜ qinit, δ∼) to ∼ such that Q∼ is the set of equivalence classes of ∼, ˜ qinit = [ε], and δ∼([w], c) = [wc] [Staiger, 1983]. The transition function δ∼ is well-defined since if w1 ∼ w2, then for all c ∈ C, w1c ∼ w2c. We call S∼ the prefix-classifier of W.

We define the prefix preorder ⪯W of W: for w1,w2 ∈ C ∗ , we write w1 ⪯W w2 if w-1 1 W ⊆ w-1 2 W. Intuitively, w1 ⪯W w2 means that a game starting with w2 is always preferable to a game starting with w1 for P1, as there are more ways to win after w2. When the context is clear, we simply write ⪯. It is a (partial) preorder. Notice that ∼ is equal to ⪯∩⪰. We also define the strict preorder ≺ = ⪯\∼.

Given a DBA B = (Q, C, qinit, δ, α) recognizing the objective W, observe that for w,w′ ∈ C ∗ such that δ∗ (qinit,w) = δ∗ (qinit,w′ ), we have w ∼ w′ . In this case, equivalence relation ∼ has at most |Q| equivalence classes. For q ∈ Q, we write abusively q-1W for the objective recognized by the DBA (Q, C, q, δ, α). Objective q-1W equals w-1W for any word w ∈ C ∗ such that δ∗ (qinit,w) = q. We extend the equivalence relation ∼ and preorder ⪯ to elements of Q.

3 Half-Positionality Characterization

Conditions. We first establish concepts at the core of our upcoming characterization.

Definition 1 (Progress-consistency). An objective W is progress-consistent if for all w1 ∈ C ∗ and w2 ∈ C + such that w1 ≺ w1w2, we have w1(w2)ω ∈ W.

Intuitively, this means that whenever a word w2 can be used to make progress after seeing a word w1 (in the sense of getting to a position in which more continuations are winning), then repeating this word has to be winning.

Example 2 (Non-progress-consistent objective). Let C = {a, b}. We consider the objective W = C ∗aaC ω recognized by the DBA with three states in Figure 3. This objective contains the words seeing, at some point, twice the color a in a row. This objective was discussed in the introduction and shown not to be half-positional. In particular, it is not progress-consistent: we have ε ≺ ba, but (ba)ω /∈ W.

Example 3 (Progress-consistent objective). We go back to a slightly different example by adding two B¨uchi transitions:

see the DBA in Figure 2 (right). This DBA recognizes the objective W asking to see a infinitely often, or a twice in a row at some point. The equivalence classes of ∼W are q-1 init W = W, q-1 a W = aC ω ∪W and q-1 aa W = C ω . This objective is progress-consistent: any word reaching qaa is accepted when repeated infinitely often, and any word w such that δ∗ (qinit, w) = qa necessarily contains at least one a, and thus is accepted when repeated infinitely often.

Objective W is half-positional; it will be readily shown with Theorem 1. Half-positionality of W cannot be shown using previous half-positionality [Kopczy´nski, 2006; Bianco et al., 2011] or bipositionality criteria (it is not bipositional). Definition 2 (Recognizability by the prefix-classifier). For an objective W ⊆ C ω and its prefix-classifier S∼ = (Q∼, C, ˜ qinit, δ∼), being recognized by a DBA built on top of the prefix-classifier requires that there exists α∼ ⊆ Q∼ × C such that W is recognized by DBA (Q∼, C, ˜ qinit, δ∼, α∼).

In the case of languages of finite words, a straightforward adaptation of the right congruence recovers the known Myhill-Nerode congruence. This equivalence relation characterizes the regular languages (a language is regular if and only if its congruence has finitely many equivalence classes), and the prefix-classifier is exactly the smallest deterministic finite automaton recognizing a language - this is the celebrated Myhill-Nerode theorem [Nerode, 1958].

Objectives are languages of infinite words, for which the situation is not so clear-cut. In particular, an ω-regular objective may not always be recognized by its prefix-classifier along with a natural acceptance condition [Maler and Staiger, 1997; Angluin and Fisman, 2021]. We show an example below for the B¨uchi acceptance condition.

Example 4 (Not recognizable by the prefix-classifier). Let C = {a, b}. Consider the objective W recognized by the DBA in Figure 4: it asks to see both a and b infinitely often. There is only one equivalence class for ∼: the winning continuations of all finite words coincide (and are actually equal to W). Therefore, its prefix-classifier S∼ has only one state; however, any DBA recognizing this objective needs at least two states. This objective is not half-positional, as witnessed by the arena in Figure 4 (right): P1 has a winning strategy from v, but it needs to take infinitely often both a and b.

Characterization. Our characterization consists of the conjunction of three conditions. The first one requires that the prefix preorder is total, and the other two correspond to the two definitions above.

Theorem 1. Let W ⊆ C ω be a DBA-recognizable objective. Objective W is half-positional if and only if

• its prefix preorder ⪯ is a total preorder,
• it is progress-consistent, and
• it is recognized by a DBA built on top of its prefixclassifier.

Figure 4: Left: DBA recognizing the objective of Example 4. Right: arena in which positional strategies do not suffice for P1 to play optimally for this objective.

This characterization is valuable to prove (and disprove) half-positionality of DBA-recognizable objectives. Examples 2 and 4 are not half-positional, and each of them falsifies exactly one of the three conditions from the statement. On the other hand, Example 3 is half-positional. We have discussed its progress-consistency, and it is also straightforward to verify that its prefix preorder is total ([ε] ≺ [a] ≺ [aa]) and that it is recognizable by a DBA built on top of its prefix-classifier (as shown with the DBA in Figure 2, right).

The first two conditions are necessary for half-positionality of all objectives. Being recognized by a DBA built on top of the prefix-classifier is necessary for half-positionality of DBA-recognizable objectives, but not for arbitrary objectives in general, including objectives recognized by other standard classes of automata over infinite words. The first condition turns out to be equivalent to earlier properties used to study bipositionality and half-positionality [Gimbert and Zielonka, 2005; Bianco et al., 2011]. The third condition has been studied multiple times in the language-theoretic literature, both for itself and for minimization and learning algorithms [Staiger, 1983; Le Sa¨ec, 1990; Maler and Staiger, 1997; Angluin and Fisman, 2021]. As an example, all deterministic weak automata (a restriction on DBA) satisfy it [Staiger, 1983; Angluin and Fisman, 2021].

We state two notable consequences of Theorem 1.

Lifting Result. We showed that half-positionality of DBArecognizable objectives can be reduced to half-positionality over the restricted class of finite, one-player arenas. A oneplayer arena of P1 is an arena in which P1 controls all vertices (i.e., V2 = ∅). Results reducing strategy complexity in two-player arenas to the easier question of strategy complexity in one-player arenas are sometimes called oneto-two-player lifts and appear in multiple places in the literature [Gimbert and Zielonka, 2005; Bouyer et al., 2022b; Kozachinskiy, 2022; Bouyer et al., 2023b].

Proposition 1 (One-to-two-player and finite-to-infinite lift). Let W ⊆ C ω be a DBA-recognizable objective. If objective W is half-positional over the class of finite one-player arenas, then it is half-positional (over all arenas of any cardinality).

Decidability of Half-Positionality. Given a DBAB, deciding if L(B) is half-positional can be done in polynomial time. Proposition 2. Given a DBA B = (Q, C, qinit, δ, α), the halfpositionality of L(B) can be decided in time O(|C| · |Q|4 ).

The algorithm checks every condition separately. It reduces each one to the inclusion of multiple pairs of languages recognized by DBA (language containment queries). Such a problem is standard: given two DBA B (with states Q) and B′ (with states Q′ ) on the same set C of colors, the inclusion L(B) ⊆ L(B′ ) can be decided in time O(|C| · |Q| · |Q′ |).