Patricia Bouyer

Stéphane Le Roux

Youssouf Oualhadj

Mickael Randour

Pierre Vandenhove

Games Where You Can Play Optimally with Arena-Independent Finite Memory

Keywords: 2012 ACM Subject Classification Theory of computation → Formal languages and automata theory two-player games on graphs, finite-memory determinacy, optimal strategies .CONCUR.2020.18

come

Introduction

Controller synthesis through the game-theoretic metaphor. Two-player games on (finite) graphs are studied extensively, in particular for their application to controller synthesis for reactive systems (see, e.g., [START_REF] Grädel | Automata, Logics, and Infinite Games: A Guide to Current Research [outcome of a Dagstuhl seminar[END_REF][START_REF] Randour | Automated synthesis of reliable and efficient systems through game theory: A case study[END_REF][START_REF] Brenguier | Non-zero sum games for reactive synthesis[END_REF][START_REF] Bloem | Graph games and reactive synthesis[END_REF]). The seminal model is antagonistic (i.e., zero-sum if one chooses a quantitative view): player 1 (P 1 ) is seen as the system to control, player 2 (P 2 ) as its antagonistic environment, and the game models their interaction. Each vertex of the game graph (called arena) models a state of the system and belongs to one of the players.

Players take turns moving a pebble from state to state according to the edges, each player choosing the destination whenever the pebble is on one of his states. These choices are made according to the strategy of the player, which, in general, might use memory (bounded or not) of the past moves to prescribe the next action.

The resulting infinite sequence of states, called play, represents the execution of the system. The objective of P 1 is to enforce a given specification, often encoded as a winning condition (i.e., a set of winning plays) or as a payoff function to maximize (i.e., a quantitative performance to optimize). This paradigm focuses on the worst-case performance of the system, hence P 2 's goal is to prevent P 1 from achieving his objective.

The goal of synthesis is thus to decide if P 1 has a winning strategy, i.e., one ensuring a given winning condition or guaranteeing a given payoff threshold, against all possible strategies of P 2 , and to build such a strategy efficiently if it exists.

Winning strategies are formal blueprints for controllers to implement in applications.

Therefore, their complexity is of tremendous importance: the simpler the strategy, the easier and cheaper it will be to build the controller and maintain it. This explains why a lot of research effort is constantly put in identifying the exact complexity (in terms of memory and/or randomness) of strategies needed to play optimally (i.e., to the best of the player's ability) for each specific class of games and objectives (e.g., [START_REF] Gimbert | Games where you can play optimally without any memory[END_REF][START_REF] Chatterjee | Strategy synthesis for multi-dimensional quantitative objectives[END_REF][START_REF] Chatterjee | Looking at mean-payoff and total-payoff through windows[END_REF]42,[START_REF] Fijalkow | Trading bounds for memory in games with counters[END_REF][START_REF] Bruyère | Window parity games: an alternative approach toward parity games with time bounds[END_REF][START_REF] Aminof | First-cycle games[END_REF][START_REF] Bouyer | Bounding average-energy games[END_REF][START_REF] Le Roux | Extending finite-memory determinacy by Boolean combination of winning conditions[END_REF][START_REF] Bouyer | Average-energy games[END_REF][START_REF] Bruyère | Energy mean-payoff games[END_REF]).

Alongside the practical interest lies the theoretical puzzle: understanding the underlying mechanisms and implicit properties of games that lead to "simple" strategies being sufficient.

Given the numerous connections between games and various branches of mathematics and computer science, this fundamental question has interest in its own right.

Preference relations. There are two prominent ways to formalize a game objective in the literature. The first one, dubbed quantitative and inspired by games in economics, is to use payoff functions mapping plays to numerical values, and to see P 1 as a maximizer player. This is for example the case of mean-payoff games [START_REF] Ehrenfeucht | Positional strategies for mean payoff games[END_REF]. The second one, called qualitative, is to define a set of winning plays -called winning condition -induced by some property, as in, e.g., parity games [START_REF] Emerson | The complexity of tree automata and logics of programs[END_REF]43]. The two formalisms are strongly linked: the classical decision problem for quantitative games is to fix a payoff threshold and ask if P 1 has a strategy to guarantee it, transforming the problem into a qualitative one (where the winning plays are all those with a payoff at least equal to the threshold). To define payoff functions or winning conditions, one often uses weights, priorities, colors, etc, on states or edges of the arena.

In this work, we walk in the footsteps of Gimbert and Zielonka [START_REF] Gimbert | Games where you can play optimally without any memory[END_REF]: we associate a color to each edge of our arenas, and we adopt the abstract formalism of preference relations over infinite sequences of colors (induced by plays). This general formalism permits to encode virtually all classical game objectives, both qualitative and quantitative, and lets us reason in a well-founded framework under minimal assumptions. P. Bouyer, S. Le Roux, Y. Oualhadj, M. Randour, and P. Vandenhove 18:3 Memoryless optimal strategies. Remarkably, several canonical classes of games that have been around for decades and proved their usefulness over and over -e.g., mean-payoff [START_REF] Ehrenfeucht | Positional strategies for mean payoff games[END_REF], parity [START_REF] Emerson | The complexity of tree automata and logics of programs[END_REF]43], or energy games [12] -share a desirable property: they all admit memoryless optimal strategies for both players. That is, for every strategy σ i of P i , there is a strategy σ ML i which is at least as good (i.e., wins whenever σ i wins or ensures at least the same payoff) and that uses no memory at all. Such a memoryless strategy always picks the same edge when in the same state, regardless of what happened before in the game.

Memoryless strategies are the simplest kind of strategies one can use. Therefore, it is quite interesting that they suffice for objectives as rich as the ones we just discussed.

Following this observation, a lot of effort has been put in understanding which games admit memoryless optimal strategies, and in identifying the exact frontiers of memoryless determinacy. Let us mention, non-exhaustively, works by Gimbert and Zielonka [START_REF] Gimbert | When can you play positionally?[END_REF][START_REF] Gimbert | Games where you can play optimally without any memory[END_REF] (culminating in a complete characterization), Aminof and Rubin [START_REF] Aminof | First-cycle games[END_REF] (through the prism of first-cycle games), and Kopczyński [START_REF] Kopczyński | Half-positional determinacy of infinite games[END_REF] (half-positional determinacy). All these advances were built by identifying the common underlying mechanisms in ad hoc proofs for specific classes of games, and generalizing them to wide classes (e.g., the first-cycle games of [START_REF] Aminof | First-cycle games[END_REF] are inspired by the seminal paper of Ehrenfeucht and Mycielski on mean-payoff games [START_REF] Ehrenfeucht | Positional strategies for mean payoff games[END_REF]).

Gimbert and Zielonka's approach. Arguably, the most important result in this direction is the complete characterization of preference relations admitting memoryless optimal strategies, established in [START_REF] Gimbert | Games where you can play optimally without any memory[END_REF], fifteen years ago. By complete characterization, we mean sufficient and necessary conditions on the preference relations.

It can be stated as follows: a preference relation admits memoryless optimal strategies for both players on all arenas if and only if the relation (used by P 1 ) and its inverse (used by P 2 ) are monotone and selective. These concepts will be defined formally in Section 3, but let us give an intuition here. Roughly, a preference relation is monotone if it is stable under prefix addition: given two sequences of colors such that one is strictly preferred to the other, it is impossible to reverse this order of preference by adding the same prefix to both sequences. Selectivity is similarly defined with regard to cycle mixing: if a preference relation is selective, then, starting from two sequences of colors, it is impossible to create a third one by mixing the first two in such a way that the third one is strictly preferred to the first two.

These elegant notions coincide with the natural intuition that memoryless strategies suffice if there is no interest in behaving differently in a state depending on what happened before.

In addition to this complete characterization, Gimbert and Zielonka proved another great result, of high interest in practice [START_REF] Gimbert | Games where you can play optimally without any memory[END_REF]Corollary 7]: as a by-product of their approach, they obtain that if memoryless strategies suffice in all one-player games of P 1 and all one-player games of P 2 , they also suffice in all two-player games. Such a lifting corollary provides a neat and easy way to prove that a preference relation admits memoryless optimal strategies without proving monotony and selectivity at all: proving it in the two one-player subcases, which is generally much easier as it boils down to graph reasoning, and then lifting the result to the general two-player case through the corollary.

The rise of memory. The need to model complex specifications has shifted research toward games where multiple (quantitative and qualitative) objectives co-exist and interact, requiring the analysis of interplay and trade-offs between several objectives. Hence, a lot of effort is put in studying games where objectives are actually conjunctions of objectives, or even richer Boolean combinations. See for example [START_REF] Chatterjee | Generalized parity games[END_REF] for combinations of parity, [START_REF] Chatterjee | Energy parity games[END_REF][START_REF] Chatterjee | Strategy synthesis for multi-dimensional quantitative objectives[END_REF][START_REF] Jurdzinski | Fixed-dimensional energy games are in pseudo-polynomial time[END_REF] for combinations of energy and parity, [42] for combinations of mean-payoff, [START_REF] Bouyer | Average-energy games[END_REF][START_REF] Bouyer | Bounding average-energy games[END_REF] Games Where You Can Play Optimally with Arena-Independent Finite Memory of energy and average-energy, [START_REF] Bruyère | Energy mean-payoff games[END_REF] for combinations of energy and mean-payoff, [START_REF] Chatterjee | Looking at mean-payoff and total-payoff through windows[END_REF] for combinations of total-payoff, or [START_REF] Chatterjee | Looking at mean-payoff and total-payoff through windows[END_REF][START_REF] Bruyère | Window parity games: an alternative approach toward parity games with time bounds[END_REF][START_REF] Brihaye | Life is random, time is not: Markov decision processes with window objectives[END_REF] for combinations of window objectives. When considering such rich objectives, memoryless strategies usually do not suffice, and one has to use an amount of memory that can quickly become an obstacle to implementation (e.g., exponential memory) or that can prevent it completely (infinite memory). Establishing precise memory bounds for such general combinations of objectives is tricky and sometimes counterintuitive. For example, while energy games and mean-payoff games are inter-reducible in the single-objective setting, exponential-memory strategies are both sufficient and necessary for conjunctions of energy objectives [START_REF] Chatterjee | Strategy synthesis for multi-dimensional quantitative objectives[END_REF][START_REF] Jurdzinski | Fixed-dimensional energy games are in pseudo-polynomial time[END_REF] while infinite-memory strategies are required for conjunctions of mean-payoff ones [42].

A natural question arises: which preference relations do admit finite-memory optimal strategies? Surprisingly, whether an equivalent to Gimbert and Zielonka's characterization could be obtained for finite memory or not has remained an open question up to now. It is worth noticing that such an equivalent could be of tremendous help in practice, especially if a lifting corollary also holds: see for example [START_REF] Bouyer | Average-energy games[END_REF][START_REF] Bouyer | Bounding average-energy games[END_REF][START_REF] Bruyère | Energy mean-payoff games[END_REF], where proving that finite-memory strategies suffice in one-player games was fairly easy, in contrast to the high complexity of the two-player case -a lifting corollary could grant the two-player case for free! Having said that, one has to hope that the following corollary can be established: "if finite-memory strategies suffice in all one-player games of P 1 and all one-player games of P 2 , they also suffice in all two-player games." Unfortunately, this hope is but a delusion.

Lifting corollary: a counterexample. Consider games where the colors are integers, and the objective of P 1 is to create a play such that (a) the running sum of weights grows up to infinity (e.g., consider its lim inf to define it properly), or (b) this running sum of weights takes value zero infinitely often. As this defines a qualitative objective, the corresponding preference relation induces only two equivalence classes: winning and losing plays. The inverse relation, used by P 2 , is trivial to obtain. It is fairly easy to prove that P 1 always has finite-memory optimal strategies in his one-player games (i.e., games where P 2 has no choice), and so does P 2 in his one-player games. Now, consider the very simple two-player game depicted in Figure 1. Player P 1 (circle) has an infinite-memory strategy to win: keeping track of the running sum of weights (which is unbounded, hence the need for infinite memory) and looping in s 1 up to the point where this sum hits zero, then going to s 2 . This strategy ensures victory because either P 2 always goes back to s 1 , in which case (b) is satisfied; or P 2 eventually loops forever on s 2 , in which case (a) is satisfied. It remains to argue that P 1 has no finite-memory winning strategy in this game. This can be done using a standard argument: whatever the amount of memory used by P 1 , P 2 may loop in s 2 long enough as to exceed the bound up to which P 1 can track the sum accurately; thus dooming P 1 to fail to reset the sum to zero in s 1 infinitely often.

This modest example proves that Gimbert and Zielonka's approach cannot work in full generality in the finite-memory case, and for good reasons. Informally, in this case, the corollary breaks down because of (the absence of some sort of) monotony. In the case of P. Bouyer, S. Le Roux, Y. Oualhadj, M. Randour, and P. Vandenhove 18:5 memoryless strategies, as in [START_REF] Gimbert | Games where you can play optimally without any memory[END_REF], P 1 is already doomed in one-player games in the absence of monotony: two prefixes to distinguish -in order to play optimally -can be hardcoded as different paths leading to the same state in a game arena, as if they were chosen by P 2 in a two-player game. In the case of finite-memory strategies, however, the situation is different.

In one-player games, the number of such paths that can be hardcoded in an arena is always bounded, hence finite memory might suffice to react, i.e., to keep track of which prefix is the current one and how to behave accordingly. However, in two-player games, P 2 might create an infinite number of prefixes to distinguish (using a cycle), thus requiring P 1 to use infinite memory to be able to do so. This is exactly what happens in the example above: in any one-player game, the largest sum that P 1 has to track is bounded, whereas P 2 can make this sum as large as he wants in two-player games.

Our approach. We generalize Gimbert and Zielonka's results -characterization and lifting corollary -to the case of arena-independent finite memory. That is, we encompass all situations where the memory needed by the two players is solely dependent on the preference relation (e.g., colors, dimensions of weight vectors), and not on the game arena (i.e., number of edges/states). Let us take some examples.

All memoryless-determined relations -studied in [START_REF] Gimbert | Games where you can play optimally without any memory[END_REF] -use arena-independent memory: the memory required, none, is the same for all arenas.

Combinations of parity objectives use arena-independent memory [START_REF] Chatterjee | Generalized parity games[END_REF]: the memory only depends on the number of objectives and the number of priorities -both parameters of the preference relation, not on the size of the arena.

Lower-and upper-bounded energy objectives also use arena-independent memory (see, e.g., [START_REF] Bouyer | Infinite runs in weighted timed automata with energy constraints[END_REF][START_REF] Bouyer | Average-energy games[END_REF][START_REF] Bouyer | Bounding average-energy games[END_REF]): the memory only depends on the bounds and the weights -parameters of the preference relation, not on the size of the arena.

On the contrary, combinations of lower-bounded energy objectives (with no upper bound) require arena-dependent memory [START_REF] Chatterjee | Strategy synthesis for multi-dimensional quantitative objectives[END_REF][START_REF] Jurdzinski | Fixed-dimensional energy games are in pseudo-polynomial time[END_REF]: it depends on the size of the arena in addition to the weights used in it. Such a setting falls outside the scope of our results. This informal concept of arena-independent memory is transparent in our work: in all our results, we use memory skeletons -essentially Mealy machines without a next-action function (Section 2) -that suffice for all arenas, and that are at the basis of the strategies we build. A quick look at our main concepts (Section 3) and results (Section 4) suffices to grasp the formalism behind this intuition. This restriction to arena-independent memory is natural given the counterexample to a general approach presented above. It is also important to note that it is not as restrictive as it may seem, as hinted by the examples above: we are not restricted to constant memory but to memory only depending on the parameters of the preference relation (or equivalently, objective), and not of the arena. This framework thus already encompasses many objectives from the literature -e.g., [START_REF] Ehrenfeucht | Positional strategies for mean payoff games[END_REF][START_REF] Emerson | The complexity of tree automata and logics of programs[END_REF]43,12,[START_REF] Bouyer | Average-energy games[END_REF]21,[START_REF] Chatterjee | Generalized parity games[END_REF][START_REF] Bruyère | Window parity games: an alternative approach toward parity games with time bounds[END_REF][START_REF] Chatterjee | Looking at mean-payoff and total-payoff through windows[END_REF][START_REF] Bouyer | Infinite runs in weighted timed automata with energy constraints[END_REF][START_REF] Bouyer | Average-energy games[END_REF][START_REF] Bouyer | Bounding average-energy games[END_REF], as well as possible extensions. More details in Appendix A.

The arena-independent case, which we solve here, is an exact equivalent to Gimbert and Zielonka's results in the finite-memory case: the memoryless case is de facto arena-independent.

Therefore, this paper strictly generalizes [START_REF] Gimbert | Games where you can play optimally without any memory[END_REF] by allowing to study any arena-independent memory skeleton instead of the unique trivial one corresponding to memoryless strategies.

Outline of our contributions. Informally, our characterization can be stated as follows:

given a preference relation and a memory skeleton M, both players have optimal finitememory strategies based on skeleton M in all games if and only if the relation and its inverse These last two concepts are keys to our approach. Intuitively, they correspond to Gimbert and Zielonka's monotony and selectivity, modulo a memory skeleton. Recall that monotony and selectivity are related to stability of the preference relation with regard to prefix addition and cycle mixing, respectively. Our more general concepts of M-monotony and M-selectivity serve the same purpose, but they only compare sequences of colors that are deemed equivalent by the memory skeleton. For the sake of illustration, take selectivity: it implies that one has no interest in mixing different cycles of the game arena. For its generalization, the memory skeleton is taken into account: M-selectivity implies that one has no interest in mixing cycles of the game arena that are read as cycles on the same memory state in the skeleton M.

Let us give a quick breakdown of our paper. Due to space constraints, we only provide an intuitive overview of our results and technical approach in this conference version: formal details and proofs, along with additional results, can be found in the full article [START_REF] Bouyer | Games where you can play optimally with arena-independent finite memory[END_REF].

In Section 2, we introduce some basic notions, including the memory skeletons, and we establish several technical results. We also discuss optimal strategies and Nash equilibria.

In Section 3, we introduce M-monotony and M-selectivity, cornerstones of our work. We also present two essential tools: prefix-covers and cyclic-covers of arenas. Section 4 states formally our characterization (Theorem 9), as well as the corresponding lifting corollary (Corollary 10), from one-player to two-player games. We show an example of application in Section 5. Finally, we give an overview of the technical highlights of our approach in Section 6 -its details are broken down in several intermediate results in our full paper [START_REF] Bouyer | Games where you can play optimally with arena-independent finite memory[END_REF].

In a nutshell, the proof of the characterization (Theorem 9) is split in two. We first establish that (the sufficiency of) finite memory based on M implies M-monotony and M-selectivity of the preference relation. The crux is to build game arenas based on automata recognizing the languages involved in the two concepts, and to use the existence of finitememory optimal strategies in these arenas to prove that M-monotony and M-selectivity hold.

To prove the converse implication, we proceed in two steps, first establishing the existence of memoryless optimal strategies in "covered" arenas, and then building on it to obtain the existence of finite-memory optimal strategies in general arenas. The main technical tools we use are Nash equilibria and the aforementioned notions of prefix-covers and cyclic-covers.

Alongside the technical details, we analyze our characterization in Appendix A: we highlight some limitations and interesting features, compare our techniques with Gimbert and Zielonka's, discuss our place in the research landscape, and sketch directions for future work.

Let us just stress already that our result -relating a memory skeleton M and preference relations for which this skeleton suffices -cannot be obtained by simply considering product arenas and invoking Gimbert and Zielonka's result on memoryless determinacy [START_REF] Gimbert | Games where you can play optimally without any memory[END_REF]. While, of course, memoryless strategies on product arenas correspond to memoryfull strategies on original arenas (as we will formally establish in Lemma 1), invoking [START_REF] Gimbert | Games where you can play optimally without any memory[END_REF] requires to be able to quantify on all arenas, not only product arenas. Filling this gap is exactly the goal of this paper, and it is made possible through the new concepts we sketched above.

Preliminaries

We only give here the notions and results necessary to understand this overview. Necessary notions and results -some of them interesting in their own right -to understand the technical details of the approach are found in the full paper [START_REF] Bouyer | Games where you can play optimally with arena-independent finite memory[END_REF].

Automata and languages of colors. Let C be an arbitrary set of colors. We assume knowledge of non-deterministic finite-state automata (NFA), which recognize regular languages.

For any finite subset B ⊆ C, we denote by Reg(B) the set of all regular languages over B.

Let

R(C) = B ⊆ C, |B|<∞ Reg(B)
, that is, all the regular languages built over C.

Let K ⊆ C * be a language of finite words. We write Prefs(K) for the set of all prefixes of words in K. We define the set of infinite words

[K] = {w = c 1 . . . ∈ C ω | ∀ n ≥ 1, c 1 . . . c n ∈
Prefs(K)}, which contains all infinite words for which every finite prefix is a prefix of a word in K. Intuitively, if K is regular, [K] is the language of infinite words that correspond to infinite paths that can always branch and reach a final state, on an automaton for K. Given a finite word w ∈ C * and a language K ⊆ C * , we write wK for their concatenation, i.e., the

language wK = {w = ww | w ∈ K} ⊆ C * .
Arenas. We consider two players: player 1 (P 1 ) and player 2 (P 2 ). An arena is a tuple i.e., e = (in(e), col(e), out(e)). We assume all arenas to be non-blocking, i.e., for all s ∈ S,

A = (S 1 , S 2 , E) such that S = S 1 S 2 (disjoint
there exists e ∈ E such that in(e) = s. For i ∈ {1, 2}, we call an arena

A = (S 1 , S 2 , E) a P i 's one-player arena if for all s ∈ S 3-i , |{e ∈ E | in(e) = s}| = 1 -that is, P 3-i has no choice.
Let Hists(A, s) denote the histories in A from s ∈ S, i.e., finite sequences of edges ρ = e 1 . . . e n ∈ E + such that in(e 1 ) = s and for all i,

1 ≤ i < n, out(e i ) = in(e i+1 ). Let
Plays(A, s) denote the plays in A from s ∈ S, i.e., infinite sequences π = e 1 e 2 . . . ∈ E ω such that in(e 1 ) = s and for all i ≥ 1, out(e i ) = in(e i+1 ). We write Hists(A, S ) and Plays(A, S ) for unions over S ⊆ S, and write Hists(A) and Plays(A) for the unions over all states of A.

Let ρ = e 1 . . . e n ∈ Hists(A) (resp. π = e 1 e 2 . . . ∈ Plays(A)): we extend the operator in to histories (resp. plays) by identifying in(ρ) (resp. in(π)) to in(e 1 ). We proceed similarly for out and histories: out(ρ) = out(e n ). For the sake of convenience, we consider that any set Hists(A, s) contains the empty history λ s such that in(λ s ) = out(λ s ) = s. We write Hists i (A, s) and Hists i (A) for the subsets of histories ρ such that out(ρ) ∈ S i , i ∈ {1, 2}, i.e., histories whose last state belongs to P i . For any set H ⊆ Hists(A), we write col(H) for its projection to colors, i.e., col(H) = { col(ρ) | ρ ∈ H}. We do the same for sets of plays.

Memory skeletons.

A memory skeleton is a tuple M = (M, m init , α upd ) where M is a finite set of states, m init ∈ M is a fixed initial state and α upd : M × C → M is an update function.

We write α upd for the natural extension of α upd to sequences in C * . Memory skeletons are deterministic and might have an infinite number of transitions, in contrast to NFA. We define the trivial memory skeleton as

M triv = (M = {m init }, m init , α upd : {m init } × C → {m init }): it
permits to formalize memoryless strategies [START_REF] Gimbert | Games where you can play optimally without any memory[END_REF] in our framework.

Let M = (M, m init , α upd ) be a skeleton. For m, m ∈ M , we define the language L m,m = {w ∈ C * | α upd (m, w) = m } that contains all words that can be read from m to m in M.

Let M 1 = (M 1 , m 1 init , α 1 upd ) and M 2 = (M 2 , m 2 init , α 2 upd ). Their product M 1 ⊗ M 2 is the memory skeleton M = (M, m init , α upd ) where M = M 1 × M 2 , m init = (m 1 init , m 2 init ), and, for all m 1 ∈ M 1 , m 2 ∈ M 2 , c ∈ C, α upd ((m 1 , m 2 ), c) = (α 1 upd (m 1 , c), α 2 upd (m 2 , c)).
That is, the memories are updated in parallel when a color is read.

Product arenas.

Let A = (S 1 , S 2 , E) be an arena and M = (M, m init , α upd ) be a skeleton.

Their product A M is the arena (S 1 , S 2 , E ) where Games Where You Can Play Optimally with Arena-Independent Finite Memory

S 1 = S 1 × M , S 2 = S 2 × M ,
E ⊆ S × C × S , with S = S 1 S 2 , is such that ((s 1 , m 1 ), c, (s 2 , m 2 )) ∈ E if and only if (s 1 , c, s 2 ) ∈ E and α upd (m 1 , c) = m 2 .
That is, the memory is updated according to the colors of the edges in E. Though M might contain an infinite number of transitions, A M is always finite, as E is finite. Since we assume A is non-blocking, it is also the case of A M.

Strategies.

A strategy σ i for P i , i ∈ {1, 2}, on arena A = (S 1 , S 2 , E), is a function

σ i : Hists i (A) → E such that for all ρ ∈ Hists i (A), in(σ i (ρ)) = out(ρ). Let Σ i (A)
α nxt : M × S i → E such that for all m ∈ M , s ∈ S i , in(α nxt (m, s)) = s.
Given a Mealy machine Γ σi = (M, α nxt ), strategy σ i is defined as follows:

∀ s ∈ S i , σ i (λ s ) = α nxt (m init , s), ∀ ρ • e ∈ Hists i (A), e ∈ E, σ i (ρ • e) = α nxt α upd m init , col (ρ • e) , out(e) .
Let Σ FM i (A) be the finite-memory strategies of P i on A. We say that a strategy

σ i ∈ Σ FM i (A)
is based on memory skeleton M if it can be encoded as a Mealy machine Γ σi = (M, α nxt ), as above. We implicitly assume that strategies of Σ FM i (A) are built by restricting the transitions of their skeleton M to the actual subset of colors appearing in

A. A strategy σ i is memoryless if it is a function σ i : S i → E, or equivalently, if it is based on M triv .
We write Plays(A, s, σ i ) for the plays consistent with a strategy σ i of P i from a state s, i.e., plays π = e 1 e 2 . . . ∈ Plays(A, s) such that for all ρ = e 1 . . . e n , out(ρ)

∈ S i =⇒ σ i (ρ) = e n+1 .
We write Plays(A, s, σ 1 , σ 2 ) for the singleton set containing the unique play consistent with a couple of strategies for the two players. We use similar notations for histories.

Preference relations. Let be a total preorder on C ω , called preference relation. We consider antagonistic games, where the objective of P 1 is to create the best possible play with regard to whereas the objective of P 2 is the opposite. That is, P 2 uses the inverse relation -1 . This corresponds to zero-sum games when using a quantitative framework.

Given w, w ∈ C ω , we write w w if we have ¬(w w) since the preorder is total. We extend to subsets: for

W, W ⊆ C ω , W W ⇐⇒ ∀ w ∈ W, ∃ w ∈ W , w w . We also write W W ⇐⇒ ∃ w ∈ W , ∀ w ∈ W, w w . Note that W W ⇐⇒ ¬(W W ).
To compare a word w ∈ C ω with a language K ⊆ C ω , we simply identify it to {w}.

Games. A (deterministic turn-based two-player) game is a tuple G = (A, ) where A is an arena and is a preference relation. All classical objectives from the literature (both qualitative and quantitative) can be expressed in the general framework of preference relations

(see Example 3 in [6]). For i ∈ {1, 2}, a P i 's one-player game is a game G = (A, ) such that
A is a P i 's one-player arena.

Optimal strategies. Let G = (A, ) be a game on arena A = (S 1 , S 2 , E). Given a P istrategy σ i ∈ Σ i (A) and a state s ∈ S, we define

UCol (A, s, σ i ) = {w ∈ C ω | ∃ σ 3-i ∈ Σ 3-i (A), col(Plays(A, s, σ 1 , σ 2 )) w}, DCol (A, s, σ i ) = {w ∈ C ω | ∃ σ 3-i ∈ Σ 3-i (A), w col(Plays(A, s, σ 1 , σ 2 ))}.
Note that DCol (A, s, σ i ) = UCol -1 (A, s, σ i ). Intuitively, UCol and DCol represent the upward and downward closures of sequences of colors (consistent with a strategy) with respect to the preference relation.

Taking the standpoint of P 1 , we say that σ 1 ∈ Σ 1 (A) is at least as good as

σ 1 ∈ Σ 1 (A)
from s ∈ S if UCol (A, s, σ 1 ) ⊆ UCol (A, s, σ 1 ). Intuitively, σ 1 is at least as good as σ 1 if the "worst-case" plays consistent with σ 1 are at least as good as the ones consistent with σ 1 .

The UCol operator is useful to define this notion properly even in the case where there is no "worst-case" play (i.e., if the infimum used in the classical quantitative setting is not reached).

Similar notions have been used before, e.g., in [START_REF] Le | Infinite sequential Nash equilibrium[END_REF]. Symmetrically, for P 2 , we say that

σ 2 ∈ Σ 2 (A) is at least as good as σ 2 ∈ Σ 2 (A) from s ∈ S if DCol (A, s, σ 2 ) ⊆ DCol (A, s, σ 2 ).
Now, we say that σ i ∈ Σ i (A) of P i is optimal from s ∈ S, aka s-optimal, if it is at least as good as every other σ i ∈ Σ i (A) from s. We extend this notation to subsets of states in the natural way, and we say that a strategy σ i is uniformly-optimal if it is S-optimal.

Our goal is to characterize the preference relations that admit uniformly-optimal finitememory (UFM) strategies based on a given skeleton M in all arenas. We also discuss the simpler case of uniformly-optimal memoryless (UML) strategies, which corresponds to the subcase studied by Gimbert and Zielonka [START_REF] Gimbert | Games where you can play optimally without any memory[END_REF], using the trivial skeleton M triv .

In that respect, the following link is important to observe. Nash equilibria. We use Nash equilibria [START_REF] Osborne | A course in game theory[END_REF] as tools to establish the existence of optimal strategies in some of our proofs. Let G = (A, ) be a game on arena A = (S 1 , S 2 , E). Formally,

a Nash equilibrium (NE) from a state s ∈ S is a couple of strategies (σ 1 , σ 2 ) ∈ Σ 1 (A) × Σ 2 (A) such that, for all σ 1 ∈ Σ 1 (A), σ 2 ∈ Σ 2 (A), col(Plays(A, s, σ 1 , σ 2 )) col(Plays(A, s, σ 1 , σ 2 )) col(Plays(A, s, σ 1 , σ 2 )). (1)
Similarly to optimal strategies, we call an NE uniform if it is an NE from all states s ∈ S.

The connection between optimal strategies and Nash equilibria in our specific context of antagonistic games is interesting to discuss, especially with respect to Gimbert and Zielonka's original work [START_REF] Gimbert | Games where you can play optimally without any memory[END_REF]. We defer this discussion to [START_REF] Bouyer | Games where you can play optimally with arena-independent finite memory[END_REF] due to space constraints, and only provide here a brief account of the results one has to know to understand this overview. First, NE are de facto pairs of optimal strategies. Second, it is possible to mix different NE.

Lemma 2. Let G = (A, ) be a game on arena A = (S 1 , S 2 , E), and let s ∈ S be a state.

Let (σ a 1 , σ a 2 ) and (σ b 1 , σ b 2 ) ∈ Σ 1 (A) × Σ 2 (A) be two Nash equilibria from s. Then, (σ a 1 , σ b 2 )
is also a Nash equilibrium from s.

Remark 3. Lemma 2 crucially relies on the assumption (transparent in our definition of Nash equilibrium) that we consider antagonistic games, that is, P 2 uses the inverse preference relation -1 .

Concepts

Generalizing monotony and selectivity. As seen in Section 1, Gimbert and Zielonka's characterization [START_REF] Gimbert | Games where you can play optimally without any memory[END_REF] relies on monotony and selectivity of the preference relation. The main difference between their technical approach and ours is the following. In the memoryless setting, all the reasoning can be abstracted away from the underlying arena and done on sequences of colors. In the finite-memory one, however, one has to pay attention to how Much of our effort was thus spent on trying to define concepts that would preserve the elegance of monotony and selectivity while allowing us to lift the theory to the finite-memory case. As often the case, the good concepts turned out to be the most natural ones, capturing the intuitive idea that one needs monotony and selectivity modulo a memory skeleton.

C O N C U R
Definition 4 (M-monotony). Let M = (M, m init , α upd ) be a memory skeleton. A preference

relation is M-monotone if for all m ∈ M , for all K 1 , K 2 ∈ R(C), (∃ w ∈ L minit,m , [wK 1 ] [wK 2 ]) =⇒ (∀ w ∈ L minit,m , [w K 1 ] [w K 2 ]) . ( 2
)
Recall that a skeleton M has a fixed initial state m init . Intuitively, M-monotony extends Gimbert and Zielonka's monotony by comparing prefixes belonging to the same language L minit,m , that is, prefixes that are deemed equivalent by skeleton M. This property roughly captures that is stable with regard to prefix addition, for memory-equivalent prefixes.

The original monotony notion is equivalent to our M-monotony with M being the trivial skeleton M triv : that is, the memoryless case is naturally a subcase of our framework.

Definition 5 (M-selectivity). Let M = (M, m init , α upd ) be a memory skeleton. A preference

relation is M-selective if for all w ∈ C * , m = α upd (m init , w), for all K 1 , K 2 ∈ R(C) such that K 1 , K 2 ⊆ L m,m , for all K 3 ∈ R(C), [w(K 1 ∪ K 2 ) * K 3 ] [wK * 1 ] ∪ [wK * 2 ] ∪ [wK 3 ]. (3)
Similarly, M-selectivity extends Gimbert and Zielonka's selectivity by asking one to compare sequences of colors belonging to the same language L m,m , that is, sequences read as cycles on the memory skeleton. Note also that the memory state m should be consistent with the prefix w read from the initial memory state m init . This property roughly captures that is stable with regard to cycle mixing, for memory-equivalent cycles.

Again, the original selectivity notion is exactly equivalent to M triv -selectivity.

In a nutshell, M-monotony deals with prefixes up to the first cycle (on memory) and M-selectivity deals with the cycles thereafter; we will see that memory skeletons can be built in a compositional way based on these two orthogonal yet complementary tasks.

Our notions respect the natural intuition that access to additional memory should always be helpful: if a skeleton M is sufficient to classify sequences of colors in a way that guarantees M-monotony and M-selectivity, then it should also be the case for "more powerful" skeletons.

Lemma 6.

Let M and M be two memory skeletons.

If is M-monotone (resp. M- selective) then, it is also (M ⊗ M )-monotone (resp. (M ⊗ M )-selective).
Prefix-covers and cyclic-covers. While the concepts of M-monotony and M-selectivity are the primordial ones for stating the characterization, we still need two additional notions to prove it. Let us sketch the issue. To prove that monotone and selective preference relations yield UML strategies, Gimbert and Zielonka deploy an inductive argument on the number of choices in an arena. Intuitively, we want to use a similar approach for UFM strategies, but because of the unavoidable coupling between the memory skeleton and the arena (e.g., Lemma 1), the induction argument breaks, as adding one choice in the arena results in adding many in the product arena (as many as there are memory states), where the reasoning needs to take place. New insight and techniques are thus needed to patch this scheme.

To solve this issue, we decouple the two aspects. We first establish that, on arenas that inherently share the same good properties as product arenas (i.e., they already "classify" prefixes and cycles as the memory would), we can deploy the induction argument and obtain UML strategies. Then, we obtain UFM strategies on general arenas as a corollary. The crux is identifying such "good" arenas: this is done through the following notions.

Definition 7 (Prefix-covers and cyclic-covers). Let M = (M, m init , α upd ) be a memory skeleton and A = (S 1 , S 2 , E) be an arena. Let S cov ⊆ S.

We say that M is a prefix-cover of S cov in A if for all s ∈ S, there exists m s ∈ M such that, for all ρ ∈ Hists(A) such that in(ρ) ∈ S cov , out(ρ) = s and such that for all ρ proper prefix of ρ, out(ρ ) = s, we have α upd (m init , col(ρ)) = m s .

We say that M is a cyclic-cover of S cov in A if for all ρ ∈ Hists(A) such that in(ρ) ∈ S cov , if s = out(ρ) and m = α upd (m init , col(ρ)), for all ρ ∈ Hists(A) such that in(ρ

) = out(ρ ) = s, α upd (m, col(ρ )) = m.
Intuitively, M is a prefix-cover for a set of states S cov if the histories starting in S cov and visiting a given state s ∈ S for the first time are read up to the same memory state in the memory skeleton. Similarly, M is a cyclic-cover of A if the cycles of A are read as cycles in the memory skeleton, once the memory has been initialized properly.

As hinted above, the canonical example of a prefix-and cyclic-covered arena is a product arena (but many more may be in this case; it is beneficial to be general with these concepts).

Lemma 8. Let M = (M, m init , α upd ) be a memory skeleton and A = (S 1 , S 2 , E) be an arena. Then M is a prefix-and cyclic-cover for S cov = S × {m init } in A M.

Characterization

Equivalence. We now have the necessary ingredients to state our equivalence result.

Theorem 9 (Equivalence). Let be a preference relation and let M be a memory skeleton.

Then, both players have UFM strategies based on memory skeleton M in all games G = (A, )

if and only if and -1 are M-monotone and M-selective.

We state this theorem broadly and with a focus on UFM strategies. The actual results

we have for each direction of the equivalence -see [6, Section 4 and Section 5] -are a bit stronger, of wider applicability and/or more interesting, but this statement carries the take-home message of our work. It is also meant to mirror the seminal result of Gimbert and Zielonka [27, Theorem 2]: their result can be retrieved from Theorem 9 by taking the trivial memory skeleton M triv . As such, our work brings a strict generalization of Gimbert and Zielonka's results [START_REF] Gimbert | Games where you can play optimally without any memory[END_REF] to the finite-memory case.

Lifting corollary. As discussed in Section 1, the work of Gimbert and Zielonka contains not one, but two great results. Alongside the aforementioned equivalence result, Gimbert and Zielonka provide a corollary of high practical interest [27, Corollary 7]: they essentially obtain as a by-product of their approach that if memoryless strategies suffice in all one-player games of P 1 and all one-player games of P 2 , they also suffice in all two-player games.

This provides an elegant way to prove that a preference relation (equivalently, an objective) admits memoryless optimal strategies without proving monotony and selectivity at all: proving it in the two one-player subcases, which is generally much easier as it boils down to graph reasoning, and then lifting the result to the general two-player case through the corollary.

See examples of one-player vs. two-player complexity in [START_REF] Bouyer | Average-energy games[END_REF][START_REF] Bouyer | Bounding average-energy games[END_REF][START_REF] Bruyère | Energy mean-payoff games[END_REF].

Again, we are able to lift this corollary to the arena-independent finite-memory case. Then, for all two-player arenas A = (S 1 , S 2 , E), both P 1 and P 2 have UFM strategies

σ i ∈ Σ FM i (A) based on memory skeleton M = M 1 ⊗ M 2 in G = (A, ).
We highlight the two (possibly different) skeletons of the two players to maintain a compositional approach, but if the same skeleton M works in both one-player versions, it also suffices in the two-player version.

Example of application

We present an illustrative application, thereby proving the existence of UFM strategies for a specific preference relation: the conjunction of two reachability objectives, a subcase of generalized reachability games, studied extensively in [21]. Let C be an arbitrary set of colors, and T 1 , T 2 ⊆ C be two target sets of colors that have to be visited. Formally, let W ⊆ C ω be the set of words w = c 1 c 2 . . . such that ∃ i, j ∈ N, c i ∈ T 1 ∧ c j ∈ T 2 . This winning condition induces a two-level (i.e., win/lose) preference relation .

In this example, we will use Theorem 9 directly in order to provide one thorough illustration of the definitions of M-monotony and M-selectivity. However, in practice, using Corollary 10 is preferable, as it yields a much shorter proof: by exhibiting the right skeletons for P 1 and P 2 , we simply have to show that these skeletons are sufficient to play optimally on both players' one-player arenas, which amounts to graph reasoning. We assume that T1 = {t1}, T2 = {t2}. The (S × {minit})-optimal memoryless strategy is in bold.

We start by showing that this preference relation is not M triv -monotone (that is, is not monotone for [START_REF] Gimbert | Games where you can play optimally without any memory[END_REF]). Assume

c 1 ∈ T 1 \ T 2 , c 2 ∈ T 2 \ T 1 , and c 3 / ∈ T 1 ∪ T 2 . Take K 1 = c * 1 , K 2 = c * 2 . For w = c 1 , w = c 2 , we have [wK 1 ] [wK 2 ], but [w K 2 ] [w K 1 ]
. This means that the preference relation is not stable with regard to prefix addition (at least, without distinguishing different classes of prefixes). Similarly, it is not M triv -selective (take w as the empty word,

K 1 = c * 1 , K 2 = c * 2 , K 3 = c * 3 :
to win, K 1 and K 2 need to be mixed).

In Figure 2, we exhibit skeletons M p = (M p , m p init , α p upd ) and

M c = (M c , m c init , α c upd ) such that is M p -monotone
word in [w K 2 ], so [w K 1 ] [w K 2 ]. Let us now prove that is M c -selective. Let w ∈ C * , m = α c upd (m c init , w), K 1 , K 2 ∈ R(C) such that K 1 , K 2 ⊆ L m,m
, and K 3 ∈ R(C). We show that Equation ( 3) is satisfied, i.e., that If m = m c init , then w does not reach T 1 nor T 2 , and the same holds for all words of K 1 and K 2 , as Similar arguments can be laid out to show that the preference relation -1 of P 2 is M p -monotone and M triv -selective (where M triv is the trivial memory skeleton defined earlier).

[w(K 1 ∪ K 2 ) * K 3 ] [wK * 1 ] ∪ [wK * 2 ] ∪ [wK 3 ]. If all words of [w(K 1 ∪ K 2 ) * K 3 ]
K 1 , K 2 ⊆ L m c init ,m c init . Therefore, if a word of [w(K 1 ∪ K 2 ) * K 3 ]
Let M = M p ⊗ M c ⊗ M triv be the product of all the considered skeletons. Although M formally has six states, its only reachable part is isometric to skeleton M c , with m 1 ↔ m c init as initial state, m 2 ↔ m c 2 , and m 3 ↔ m c 3 : we thus do not depict it to save space.

By Lemma 6, we have that both and -1 are M-monotone and M-selective. Using Theorem 9, we obtain that both players have UFM strategies based on skeleton M in all games G = (A, ). Note that memory skeleton M is minimal (no memory skeleton with two states or less suffices for P 1 to play optimally in all arenas [21]).

We provide an example of a one-player arena A = (S 1 , S 2 = ∅, E) in Figure 2, and show that there is a UFM strategy for the preference relation based on skeleton M.

To do so, we invoke Lemma 1: we show equivalently that the product A M admits an (S × {m init })-optimal memoryless strategy for . Notice that no memoryless strategy suffices to play optimally in G = (A, ), as when starting in s 2 , P 1 should first visit s 1 before going to s 3 . Also, the (S × {m init })-optimal memoryless strategy for the product arena is only optimal if the initial state is in S × {m init }; it is for instance not optimal from state (s 2 , m 2 ).

C O N C U R 2 0 2 0 18:14 Games Where You Can Play Optimally with Arena-Independent Finite Memory

Technical sketch

Due to space constraints, we only sketch our proof schemes here: full proofs are in [START_REF] Bouyer | Games where you can play optimally with arena-independent finite memory[END_REF].

From finite memory based on M to M-monotony and M-selectivity. For the left-toright implication of Theorem 9, it suffices to consider the weaker assumption involving only one-player: we establish that if UFM strategies based on M exist in all one-player games of P 1 (resp. P 2 ), then his preference relation (resp. -1 ) is M-monotone and M-selective. To maintain a compositional approach, we consider M-monotony and M-selectivity separately.

Details are in [6, Section 4].

Let us sketch the proof for M-monotony and P 1 . We need to establish Equation (2).

We instantiate the four languages involved in it: {w}, {w }, K 1 and K 2 . We take NFA recognizing them and build an NFA N that joins them in such a way that, when N is considered as a one-player game arena, its plays correspond exactly to the languages of infinite words considered in Equation ( 2). This arena is composed of two chains emulating the two prefixes w and w and leading to a state t where P 1 has to pick a side corresponding to the two languages [K 1 ] and [K 2 ]. Now, proving the M-monotony of boils down to invoking an optimal strategy σ in the corresponding game, the crux being that σ always picks the same edge in t (i.e., the same side between subarenas corresponding to [K 1 ] and

[K 2 ]
) as both prefixes w and w are deemed equivalent by the memory skeleton M.

The proof for M-selectivity is similar. The main difference is that the "joining" state t can be visited repeatedly in this case -possibly infinitely often. This is because Equation ( 3)

is about cycles and their languages. Our proof takes that into account.

From M-monotony and M-selectivity to finite memory based on M. The right-to-left implication of Theorem 9 is more complex to establish. In this case, we want the result for two-player games, provided both preference relations are M-monotone and M-selective. The general scheme we use is an induction on the number of choices in arenas. The main issue is dealing with the memory: one additional choice in an arena results in many ones in the corresponding product arena. To circumvent this obstacle, we proceed in two steps. Details are in [6, Section 5].

We first establish the existence of UML strategies in (prefix-and cyclic-)covered arenas.

Let us focus on the induction step we use to prove this result, as an example of the techniques involved. For an arena A = (S 1 , S 2 , E), we write n A = |E| -|S| for its number of choices.

To simplify, let us say we have a skeleton M such that is M-monotone and M-selective, and that we assume that memoryless -for the two players -NE exist from all covered states in arenas with less than n choices. Then we establish that we can also build an NE in arenas with n choices, in which P 1 uses a memoryless strategy -but maybe not P 2 ! To prove this, we proceed as follows.

Let A be an arena with n A = n choices. We identify a state t in which P 1 has at least two outgoing edges. By splitting the edges in t in two sets, we obtain two corresponding subarenas A a and A b such that n Aa , n A b < n, along with the corresponding subgames. The induction hypothesis gives us two memoryless NE (from covered states) in these subgames: (σ a 1 , σ a 2 )

and (σ b 1 , σ b 2 ). The arguments can then be unfolded as follows. First, using M-monotony and M being a prefix-cover, we identify one subarena (say A a ) which is clearly at least as good as the other for P 1 . Second, we build a strategy profile (σ # 1 , σ # 2 ), that we claim to be an NE in G = (A, ), in the following way: P 1 uses strategy σ a 1 (the one from the best subarena) and P 2 reacts to P 1 's actions by playing the corresponding best-response strategy. I.e., if P. Bouyer, S. Le Roux, Y. Oualhadj, M. Randour, and P. Vandenhove 18:15 P 1 plays in A a , P 2 plays according to σ a 2 , and otherwise he plays according to σ b 2 . Third, it remains to prove the two inequalities of Equation ( 1). The rightmost one is easy, as well as the leftmost one in the subcase where the unique play π ∈ Plays(A, s, σ # 1 , σ # 2 ) does not visit state t: they can both be proved thanks to the induction hypothesis and easy construction arguments. The crux of the proof is thus in the last step: proving that the leftmost inequality holds when the play visits t. This can be achieved thanks to M-selectivity and M being a cyclic-cover, properties of the union operator in languages of prefixes, inherent properties of the preference relation, A a being the best subarena thanks M-monotony, and the induction hypothesis, in that order.

The actual induction step and its proof are more subtle -for example, we use different skeletons for monotony and selectivity and obtain the result in a compositional way; but the main intuition is carried here. The same result can be established symmetrically for P 2 , but again the resulting NE is only memoryless for P 2 . Yet, assuming both and -1 are M-monotone and M-selective, we have two half-memoryless NE that we can mix to obtain a truly memoryless NE via Lemma 2; thus proving the existence of UML strategies in covered arenas. Observe this interesting by-product of our approach: we can actually detect arenas where memory is not needed at all thanks to our concepts of prefix-and cyclic-covers.

The final result -the existence of UFM strategies based on M in all arenas -can then be obtained as a corollary, based on the link between memoryless strategies in product arenas and memoryfull ones in original arenas (Lemma 1). Another nice by-product of our approach, witnessed in Corollary 10, is that the product of individual memories from one-player games is sufficient to play optimally in two-player games, for both players. This is in stark contrast to the counter-example discussed in Section 1 and it illustrates that our characterization matches well-behaved preference relations.

Equivalence and lifting corollary. The equivalence (Theorem 9) is easily obtained by putting together its two directions. Note that we also establish a similar equivalence in the one-player case as a by-product.

Theorem 11 (One-player equivalence). Let be a preference relation and let M be a memory skeleton. Then, P 1 has UFM strategies based on memory skeleton M in all his one-player games G = (A, ) if and only if is M-monotone and M-selective.

Although this looks like a weak version of Theorem 9 at first sight, this is actually a distinct result as both sides of the equivalence are weaker: on the left side, it only handles the memory requirements for P 1 's one-player games; on the right side, it does not assume anything about the inverse preference relation -1 .

The lifting corollary, Corollary 10, is also a consequence of our approach. As we have seen, the existence of UFM strategies based on a skeleton M in one-player games suffices to yield M-monotony and M-selectivity of the corresponding preference relation. Hence if both players have UFM strategies in their one-player games, both relations satisfy these properties and we can take the other direction of Theorem 9 to ensure that UFM strategies also exist in two-player games. As explained above, this approach can actually be used compositionally.

All proofs, as well as the one-player equivalence, are presented in details in [START_REF] Bouyer | Games where you can play optimally with arena-independent finite memory[END_REF].

18:19

A Discussion

We close our paper with a discussion of the assets and limits of our approach, its applicability with regard to the current research landscape, and the directions we aim to follow in future work.

Technical overview. Naturally, our technical approach is inspired by the one of Gimbert and Zielonka for the memoryless case [START_REF] Gimbert | Games where you can play optimally without any memory[END_REF], which can actually be rediscovered through our results using a trivial memory skeleton. Two of the most important challenges we had to overcome were:

1. establishing natural concepts of monotony and selectivity modulo memory that are exactly as powerful as required to maintain a complete characterization (i.e., sufficient and necessary conditions) in the finite-memory case;

2. circumventing the seemingly unavoidable coupling between the memory skeleton and the arena in the inductive argument needed to prove the implication from M-monotony and M-selectivity to finite-memory optimal strategies -which we were able to do using our notions of prefix-covers and cyclic-covers.

All along our paper, we highlighted the similarities and discrepancies between our work and Gimbert and Zielonka's [START_REF] Gimbert | Games where you can play optimally without any memory[END_REF]. As observed through [START_REF] Bouyer | Games where you can play optimally with arena-independent finite memory[END_REF]Remark 16], our results are established using fine-grained assumptions and conclusions, in an effort to push the approach to its limits. They also preserve compositionality, splitting the reasoning for M-monotony and M-selectivity, and for the two players.

Alongside M-monotony and M-selectivity, we define two other key concepts to solve the technical issues related to the induction on product arenas: prefix-covers and cyclic-covers.

These notions are crucial tools to prove the right-to-left implication of Theorem 9.

Some advantages.

The aforementioned concepts of prefix-covers and cyclic-covers also have benefits from a practical point of view: given a preference relation and the corresponding memory skeleton M, they let us identify game arenas where memoryless strategies suffice whereas finite memory (based on M) might be necessary in general. Such arenas are the ones covered by M. Hence in practice, this approach permits to obtain UML strategies for many arenas where a coarser approach would only provide UFM ones.

Our approach yields two methods to establish that a preference relation (or equivalently a payoff function or a winning condition) admits UFM strategies. The first one, exhibiting appropriate memory skeletons and proving M-monotony and M-selectivity, is based on Theorem 9 and can be used compositionally through [START_REF] Bouyer | Games where you can play optimally with arena-independent finite memory[END_REF]Corollary 25]. The second one follows the lifting corollary, Corollary 10: one only has to study the one-player subcases then invoke this result to lift the existence of UFM strategies to the two-player case, without checking for M-monotony and M-selectivity at all. Hence this second method is often painless in practice.

Two interesting facts can be seen through Corollary 10. First, there is no blow-up in the memory required when going from one-player games to two-player games: the overall memory simply combines the memory skeletons of the two players. Second, assuming that one has an algorithm to solve 1 one-player games -say for P 1 -for a winning condition satisfying our hypotheses, this lifting corollary also induces a naive algorithm for the two-player case for free: thanks to the bounds on memory, one may enumerate the strategies of the adversary, P 2

1 I.e., decide who has a winning strategy from a given state.

-or guess one if one aims for a non-deterministic algorithm -and solve the corresponding P 1 's game(s) where the strategy of P 2 is fixed. Note that while such a simple algorithm might not be optimal, it does correspond to the approach giving the best complexity class known for the renowned family of games in NP ∩ coNP, such as, e.g., parity or mean-payoff games (e.g., [START_REF] Jurdzinski | Deciding the winner in parity games is in UP ∩ co-UP[END_REF]). These last two cases could already be dealt with thanks to Gimbert and Zielonka's result since they involve memoryless strategies, but now a similar road can be taken for any objective that admits arena-independent finite-memory optimal strategies, such as, e.g., generalized parity games.

Applicability. Let us give a quick tour of some classical (combinations of) objectivesexpressed through winning conditions, payoffs or preference relations -and assess whether our approach permits to establish the existence of UFM strategies in the corresponding games.

Note that when considering multiple (quantitative) objectives, optimal strategies usually do not exist, and one has to settle for Pareto-optimal ones (e.g., [START_REF] Delgrange | Simple strategies in multi-objective MDPs[END_REF]). However, in many cases, the (decision) problem under study is as follows: given a threshold (vector), define the winning condition as all the plays achieving at least this threshold, and check for a winning strategy. Hence multi-objective quantitative games are often de facto reduced to qualitative win-lose games for this so-called threshold problem. Observe that, given a multi-objective setting, if UFM strategies exist for all threshold problems, then finite-memory strategies suffice to realize the Pareto front (as each point of this front can be considered as a threshold). Therefore, our approach also enables reasoning about the existence of finite-memory Pareto-optimal strategies in multi-objective games.

We start our overview with some game settings that fall under the scope of our approach.

Obviously, all memoryless-determined objectives are among them, since we generalize Gimbert and Zielonka's work [START_REF] Gimbert | Games where you can play optimally without any memory[END_REF]: this includes, e.g., mean-payoff [START_REF] Ehrenfeucht | Positional strategies for mean payoff games[END_REF], parity [START_REF] Emerson | The complexity of tree automata and logics of programs[END_REF]43], energy [12] or average-energy games [START_REF] Bouyer | Average-energy games[END_REF]. As established in Section 1, our results encompass all cases where arena-independent memory suffices. Hence they permit to rediscover the existence of UFM strategies for games such as, e.g., generalized reachability [21], generalized parity [START_REF] Chatterjee | Generalized parity games[END_REF],

window parity games [START_REF] Bruyère | Window parity games: an alternative approach toward parity games with time bounds[END_REF], some variants of window mean-payoff games [START_REF] Chatterjee | Looking at mean-payoff and total-payoff through windows[END_REF], or lower-and upper-bounded (multi-dimension) energy games [START_REF] Bouyer | Infinite runs in weighted timed automata with energy constraints[END_REF][START_REF] Bouyer | Average-energy games[END_REF][START_REF] Bouyer | Bounding average-energy games[END_REF]. Our approach can also be useful to extend these known results to more general combinations, either via appropriate memory skeletons or through the lifting corollary (see an application in Section 5).

There are many games that do not fit our approach for good reasons, as they do not admit UFM strategies in general: e.g., multi-dimension mean-payoff [42], mean-payoff parity [START_REF] Chatterjee | Mean-payoff parity games[END_REF],

or energy mean-payoff games [START_REF] Bruyère | Energy mean-payoff games[END_REF]. More interesting are games for which finite-memory strategies exist, but the memory is arena-dependent. These notably include games with multi-dimension lower-bounded energy objectives and no upper bound [START_REF] Chatterjee | Strategy synthesis for multi-dimensional quantitative objectives[END_REF][START_REF] Jurdzinski | Fixed-dimensional energy games are in pseudo-polynomial time[END_REF], or other variants of window mean-payoff games [START_REF] Chatterjee | Looking at mean-payoff and total-payoff through windows[END_REF]. In such games, the players usually have to keep track of information such as, e.g., the sum of weights along an acyclic path, which is bounded for any given arena, but by a value that grows when the arena grows. Hence the need for memory that grows with the arena parameters. Our results cannot be applied directly to such cases in order to obtain the existence of finite-memory strategies for all games. An adaptation of our approach could potentially be used for subclasses of arenas where the parameters are bounded (in order to regain a skeleton working on all arenas of the class).

Critical analysis.

Let us take a step back and assess the place of our work in its larger line of research. The natural endgame is characterizing all preference relations admitting finite-C O N C U R 2 0 2 0 18:22 Games Where You Can Play Optimally with Arena-Independent Finite Memory memory optimal strategies, including those using arena-dependent memory, and pinpointing the frontiers of application of the lifting corollary -that is, under which conditions is finite-memory determinacy preserved when going from one-player to two-player games?

The road is long from Gimbert and Zielonka's characterization in the memoryless case [START_REF] Gimbert | Games where you can play optimally without any memory[END_REF] to such a general result, and this work is but a first step. We have already established that Gimbert and Zielonka's approach cannot be fully transposed for finite memory. Our focus on arena-independent memory is a way to study the frontiers of this approach while providing an extension of practical interest. While it may seem limited at first, note that our framework already encompasses arguably rich classes of games such as, e.g., generalized parity games and fully-bounded energy games. As argued in Section 1, recall that our result is in no way a simple application of [START_REF] Gimbert | Games where you can play optimally without any memory[END_REF] to product arenas.

From a practical point of view, our equivalence result has limitations as it inherently uses the memory skeleton M. At this point, our approach neither helps in finding an appropriate skeleton, nor in determining the minimal one; two highly interesting questions from a practical standpoint. Nonetheless, to advance toward answering these questions and to be able to find good skeletons automatically, one first has to understand their theoretical characteristics, which we do here as a necessary stepping stone. Focusing on applications, let us note that the equivalence result is often not the most suited tool: this is instead where the lifting corollary shines. As noted before, reasoning on one-player games (i.e., graphs) is generally much easier than in two-player games (e.g., [START_REF] Bouyer | Average-energy games[END_REF][START_REF] Bouyer | Bounding average-energy games[END_REF][START_REF] Bruyère | Energy mean-payoff games[END_REF]). Hence, a reasonably easy way to tackle practical cases is to find skeletons sufficient for P 1 and P 2 in their respective one-player games and to use our constructive result to build a skeleton that suffices for both in two-player games.

Comparison with related work. We already discussed the most important related papers [START_REF] Gimbert | When can you play positionally?[END_REF][START_REF] Gimbert | Games where you can play optimally without any memory[END_REF][START_REF] Kopczyński | Half-positional determinacy of infinite games[END_REF][START_REF] Aminof | First-cycle games[END_REF][START_REF] Martin | Borel determinacy[END_REF][START_REF] Le Roux | Extending finite-memory determinacy by Boolean combination of winning conditions[END_REF] in Section 1. Let us highlight here some works where similar approaches have been considered to establish "meta-theorems" applying to general classes of games, or works that inspire interesting directions of research. First and foremost is the determinacy theorem by Martin that guarantees determinacy (without considering the complexity of strategies) for Borel winning conditions [START_REF] Martin | Borel determinacy[END_REF].

Aminof and Rubin provide a simpler (but incomplete) approach to memoryless determinacy through the prism of first-cycle games in [START_REF] Aminof | First-cycle games[END_REF]: a similar take on finite-memory determinacy could be appealing -it could provide sufficient conditions easier to test than M-monotony and M-selectivity.

Let us discuss the work of Kopczyński. First, in [START_REF] Kopczyński | Half-positional determinacy of infinite games[END_REF], he establishes sufficient (and relaxed) conditions to ensure the existence of UML strategies for one player, in two-player games: it would be interesting to study the corresponding problem in the finite-memory case.

Indeed, in many games where infinite memory is needed, it is only the case for one of the players (e.g., [42,[START_REF] Chatterjee | Mean-payoff parity games[END_REF][START_REF] Bruyère | Energy mean-payoff games[END_REF]) and conditions à la Kopczyński could thus prove useful. Note that this is different from Theorem 11, which gives a sufficient and necessary condition but for one-player games only. Second, we recently discovered unpublished content in Kopczyński's

PhD thesis [START_REF] Kopczyński | Half-positional Determinacy of Infinite Games[END_REF]. Kopczyński distinguishes chromatic memory (which corresponds to our definition of memory skeleton), and the more powerful chaotic memory, where transitions can depend on the actual edges of the arenas, rather than simply on their colors. Chaotic memory is thus intrinsically arena-dependent. Our notion of an arena being both prefix-and cyclic-covered by a memory skeleton M is equivalent to a notion in [START_REF] Kopczyński | Half-positional Determinacy of Infinite Games[END_REF]Definition 8.12],

which defines that an arena adheres to chromatic memory M if it is possible to assign a state of M to every state of the arena such that moving along the edges updates these memory P. Bouyer, S. Le Roux, Y. Oualhadj, M. Randour, and P. Vandenhove

18:23

states in a consistent way. Our definitions of prefix-and cyclic-cover can be seen as two distinct sides of this idea of adherence, which when added up, are actually equivalent to it.

Following the same motivation as our work -the need to characterize (combinations of) objectives admitting finite-memory optimal strategies, Le Roux et al. [START_REF] Le Roux | Extending finite-memory determinacy by Boolean combination of winning conditions[END_REF] take another road:

whereas our work permits to lift results from one-player games to two-player games, they provide a lifting from the single-objective case to the multi-objective one. Their techniques, as well as the scope of their results, are somewhat orthogonal to ours. Whether both approaches can be intertwined to obtain results on more general settings remains an open question.

Our work focuses on deterministic turn-based two-player games. Sufficient conditions have been published for stochastic models but to the best of our knowledge, no complete characterization, even for the simplest case of Markov decision processes (e.g., [START_REF] Gimbert | Pure stationary optimal strategies in Markov decision processes[END_REF]). Two unpublished articles contain interesting results on stochastic games [START_REF] Gimbert | Pure and Stationary Optimal Strategies in Perfect-Information Stochastic Games with Global Preferences[END_REF][START_REF] Gimbert | Two-player perfect-information shift-invariant submixing stochastic games are half-positional[END_REF], including an extension of Gimbert and Zielonka's original work, by the same authors [START_REF] Gimbert | Pure and Stationary Optimal Strategies in Perfect-Information Stochastic Games with Global Preferences[END_REF]. Whether part of our approach can be useful to tackle the finite-memory case in this context, or in richer contexts mixing games and stochastic models (e.g., [START_REF] Bruyère | Meet your expectations with guarantees: Beyond worst-case synthesis in quantitative games[END_REF]) is a question for future research.

Some sufficient criteria, orthogonal to our approach, were studied for concurrent games in [START_REF] Le | Concurrent games and semi-random determinacy[END_REF].

Limits and future work. To close this paper, we recall three limits of our approach, and the corresponding open problems.

First, as explained throughout the paper, our results cover all cases where arenaindependent memory suffices, and are limited to these cases. We have argued that the approach cannot be fully lifted to the general case, for good reasons, as the lifting corollary breaks in some situations (Section 1). Still, we have hope to generalize our approach to some extent to the arena-dependent case, through some function associating memory skeletons to arenas, as discussed in Section 1. Obtaining a lifting corollary -under well-chosen conditions -in the arena-dependent case would be of tremendous help in practice: see for example [START_REF] Bouyer | Average-energy games[END_REF][START_REF] Bouyer | Bounding average-energy games[END_REF][START_REF] Bruyère | Energy mean-payoff games[END_REF]. Hence this is clearly the next step in our quest.

Second, our result is a characterization instantiated by a memory skeleton M. While the lifting corollary is helpful in applications, it would be fantastic to be able to find an appropriate skeleton automatically, and to be able to determine if a given skeleton is minimal (with regard to a preference relation). This paper is a first step toward these long-term objectives.

Lastly, as explained in Remark 3 and [6, Remark 24], most of our arguments carry over to the case of general Nash equilibria. That is, when considering not necessarily antagonistic games where the two players use different, not necessarily inverse, preference relations.

Whether our approach can be adapted in this case, at the price of an unavoidable blow-up of memory, is an open question worth considering. In particular, we want to study the links between our results (including the lifting from one-player to two-player games) and recent results lifting finite-memory determinacy in two-player games to the existence of finite-memory Nash equilibria in multi-player games [START_REF] Le | Extending finite-memory determinacy to multi-player games[END_REF].

C O N C U R 2 0 2 0

Figure 1

 1 Figure 1 P1 (circle) needs infinite memory to win.

  Can Play Optimally with Arena-Independent Finite Memory are M-monotone and M-selective.

  be the set of all strategies of P i on A. A finite-memory strategy σ i can be encoded as a Mealy machine, i.e., a skeleton M = (M, m init , α upd ) with transitions over a finite subset of colors B ⊆ C, enriched with a next-action function

Lemma 1 .

 1 Let G = (A, ) be a game on arena A = (S 1 , S 2 , E). Let M = (M, m init , α upd ) be a memory skeleton and let σ i ∈ Σ FM i (A) be a finite-memory strategy encoded by the Mealy machine Γ σi = (M, α nxt ). Then, σ i is a UFM strategy in G if and only if α nxt corresponds to an (S × {m init })-optimal memoryless strategy in G = (A M, ).

2 0 2 0 18 :

 18 10 Games Where You Can Play Optimally with Arena-Independent Finite Memory sequences of colors are composed and compared, to maintain consistency with regard to the memory and the game arena. This need to intertwine abstract reasoning on arbitrary sequences of colors with concrete tracking of memory updates is the key obstacle to overcome.

1 . 2 .

 12 Let be a preference relation and M 1 , M 2 be two memory skeletons.Assume that for all one-player arenas A = (S 1 , S 2 = ∅, E), P 1 has a UFM strategy σ 1 ∈ Σ FM 1 (A) based on memory skeleton M 1 in G = (A, ); for all one-player arenas A = (S 1 = ∅, S 2 , E), P 2 has a UFM strategy σ 2 ∈ Σ FM 2 (A) based on memory skeleton M 2 in G = (A, ).

Figure 2

 2 Figure 2First and second: memory skeletons M p and M c for two-target reachability games; third: arena A; fourth: product arena A M (only states reachable from S × {minit} are depicted). We assume that T1 = {t1}, T2 = {t2}. The (S × {minit})-optimal memoryless strategy is in bold.

  are losing, this equation trivially holds; we thus assume that this set contains a winning word. We therefore have to show that there is a winning word in [wK * 1 ], [wK * 2 ], or [wK 3 ]. We study the three possible values of m separately.

Randour, and P. Vandenhove 18:13

  Let us prove that is M p -monotone. Let m ∈ M p , K 1 , K 2 ∈ R(C); we want to show that Equation (2) is satisfied. We assume that there exists w ∈ L m p init ,m such that [wK 1 ] [wK 2 ]: this means that all words of [wK 1 ] are losing, and that there exists a winning word in [wK 2 ]. ] is empty, this always holds; we now assume that [K 1 ] is non-empty. We study the two possible values of m separately. If m = m p init , then w and w do not reach T 1 . If w does not reach T 2 either, as there is a winning word in [wK 2 ], then there must be a winning word in [K 2 ]. This word is still winning after prepending w to it, so there is a winning word in [w K 2 ], and [w K 1 ] [w K 2 ]. If w reaches T 2 , then [K 1 ] cannot have a word reaching T 1 . As w does not reach T 1 either, all words of [w K 1 ] are losing, so [w K 1 ] [w K 2 ]. If m = m p 2 , then w and w reach T 1 . Clearly, w cannot reach T 2 (as [wK 1 ] would be winning). This implies that [K 2 ] must contain a word reaching T 2 ; as w reaches T 1 , the concatenation of w with the word of [K 2 ] reaching T 2 means that there is a winning

	Let w ∈ L m p init ,m ; we show that we necessarily have that [w K 1 ]	[w K 2 ]. Note that if
	[K 1

and M c -selective. Note that such skeletons are obviously not unique. P. Bouyer, S. Le Roux, Y. Oualhadj, M.

18:20 Games Where You Can Play Optimally with Arena-Independent Finite Memory

  38th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, FSTTCS 2018, December 11-13, 2018, Ahmedabad, India, volume 122 of LIPIcs, pages 38:1-38:20. Schloss Dagstuhl -Leibniz-Zentrum fuer Informatik, 2018. URL: https: //doi.org/10.4230/LIPIcs.FSTTCS.2018.38, doi:10.4230/LIPIcs.FSTTCS.2018.38.

	42 Yaron Velner, Krishnendu Chatterjee, Laurent Doyen, Thomas A. Henzinger, Alexander Moshe
	Rabinovich, and Jean-François Raskin. The complexity of multi-mean-payoff and multi-energy
	games. Inf. Comput., 241:177-196, 2015. URL: https://doi.org/10.1016/j.ic.2015.03.001,
	doi:10.1016/j.ic.2015.03.001.
	43 Wieslaw Zielonka. Infinite games on finitely coloured graphs with applications to automata
	on infinite trees. Theor. Comput. Sci., 200(1-2):135-183, 1998.
	C O N C U R 2 0 2 0

Acknowledgements

We extend our warmest thanks to Mathieu Sassolas, for inspiring discussions that were essential in starting this work.

Funding Research supported by F.R.S.-FNRS under Grant n • F.4520.18 (ManySynth), F.R.S.-FNRS mobility funding for scientific missions (Y. Oualhadj in UMONS, 2018), and ENS Paris-Saclay visiting professorship (M. Randour, 2019). Mickael Randour is an F.R.