arXiv subjects

Stéphane Le Roux

Publications and source records attributed to Stéphane Le Roux.

At least 19 recordsLinked to original sources

arXiv2026

Positional Determinacy with Colored Vertices: a 1-to-2-Player Lift

Positional determinacy of vertex-colored parity games was proved in the 1990s, which directly implies positional determinacy of edge-colored parity games. In 2006, it was shown that if a prefix-independent color-based objective ensures that every edge-colored two-player turn-based game is positionally determined, this objective is equivalent to a parity objective. We prove a similar result for vertex-colored games, namely that the following are equivalent for any prefix-independent objective $W$ over a finite set of colors: - $W$ is positionally determined on all vertex-colored one-player games. - $W$ is positionally determined on all vertex-colored two-player games. - $W$ is equivalent to a parity objective on ordrerd pairs of colors. We prove that finiteness of the color set is required for our equivalence to hold. Beyond this $1$-to-$2$-player lift, the technique that we develop to handle the pairs of colors establishes a promising 2-way correspondence between edge-colored games and vertex-colored games.

cs.GT↗

arXiv2025

An Automata-Based Method to Formalize Psychological Theories -- The Case Study of Lazarus and Folkman's Stress Theory

Formal models are important for theory-building, enhancing the precision of predictions and promoting collaboration. Researchers have argued that there is a lack of formal models in psychology. We present an automata-based method to formalize psychological theories, i.e. to transform verbal theories into formal models. This approach leverages the tools of theoretical computer science for formal theory development, for verification, comparison, collaboration, and modularity. We exemplify our method on Lazarus and Folkman's theory of stress, showcasing a step-by-step modeling of the theory.

cs.FL↗

arXiv2023

From Local To Global Optimality in Concurrent Parity Games

We study two-player games on finite graphs. Turn-based games have many nice properties, but concurrent games are harder to tame: e.g. turn-based stochastic parity games have positional optimal strategies, whereas even basic concurrent reachability games may fail to have optimal strategies. We study concurrent stochastic parity games, and identify a local structural condition that, when satisfied at each state, guarantees existence of positional optimal strategies for both players.

cs.GT↗

arXiv2023

Sub-game optimal strategies in concurrent games with prefix-independent objectives

We investigate concurrent two-player win/lose stochastic games on finite graphs with prefix-independent objectives. We characterize subgame optimal strategies and use this characterization to show various memory transfer results: 1) For a given (prefix-independent) objective, if every game that has a subgame almost-surely winning strategy also has a positional one, then every game that has a subgame optimal strategy also has a positional one; 2) Assume that the (prefix-independent) objective has a neutral color. If every turn-based game that has a subgame almost-surely winning strategy also has a positional one, then every game that has a finite-choice (notion to be defined) subgame optimal strategy also has a positional one. We collect or design examples to show that our results are tight in several ways. We also apply our results to Büchi, co-Büchi, parity, mean-payoff objectives, thus yielding simpler statements.

cs.GT↗

arXiv2022

Playing (Almost-)Optimally in Concurrent Büchi and co-Büchi Games

We study two-player concurrent stochastic games on finite graphs, with Büchi and co-Büchi objectives. The goal of the first player is to maximize the probability of satisfying the given objective. Following Martin's determinacy theorem for Blackwell games, we know that such games have a value. Natural questions are then: does there exist an optimal strategy, that is, a strategy achieving the value of the game? what is the memory required for playing (almost-)optimally? The situation is rather simple to describe for turn-based games, where positional pure strategies suffice to play optimally in games with parity objectives. Concurrency makes the situation intricate and heterogeneous. For most ω-regular objectives, there do indeed not exist optimal strategies in general. For some objectives (that we will mention), infinite memory might also be required for playing optimally or almost-optimally. We also provide characterizations of local interactions of the players to ensure positionality of (almost-)optimal strategies for Büchi and co-Büchi objectives. This characterization relies on properties of game forms underpinning the formalism for defining local interactions of the two players. These well-behaved game forms are like elementary bricks which, when they behave well in isolation, can be assembled in graph games and ensure the good property for the whole game.

cs.GT↗

arXiv2022

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

For decades, two-player (antagonistic) games on graphs have been a framework of choice for many important problems in theoretical computer science. A notorious one is controller synthesis, which can be rephrased through the game-theoretic metaphor as the quest for a winning strategy of the system in a game against its antagonistic environment. Depending on the specification, optimal strategies might be simple or quite complex, for example having to use (possibly infinite) memory. Hence, research strives to understand which settings allow for simple strategies. In 2005, Gimbert and Zielonka provided a complete characterization of preference relations (a formal framework to model specifications and game objectives) that admit memoryless optimal strategies for both players. In the last fifteen years however, practical applications have driven the community toward games with complex or multiple objectives, where memory -- finite or infinite -- is almost always required. Despite much effort, the exact frontiers of the class of preference relations that admit finite-memory optimal strategies still elude us. In this work, we establish a complete characterization of preference relations that admit optimal strategies using arena-independent finite memory, generalizing the work of Gimbert and Zielonka to the finite-memory case. We also prove an equivalent to their celebrated corollary of great practical interest: if both players have optimal (arena-independent-)finite-memory strategies in all one-player games, then it is also the case in all two-player games. Finally, we pinpoint the boundaries of our results with regard to the literature: our work completely covers the case of arena-independent memory (e.g., multiple parity objectives, lower- and upper-bounded energy objectives), and paves the way to the arena-dependent case (e.g., multiple lower-bounded energy objectives).

cs.GT↗

arXiv2021

Optimal strategies in concurrent reachability games

We study two-player reachability games on finite graphs. At each state the interaction between the players is concurrent and there is a stochastic Nature. Players also play stochastically. The literature tells us that 1) Player B, who wants to avoid the target state, has a positional strategy that maximizes the probability to win (uniformly from every state) and 2) from every state, for every ε > 0, Player A has a strategy that maximizes up to ε the probability to win. Our work is two-fold. First, we present a double-fixed-point procedure that says from which state Player A has a strategy that maximizes (exactly) the probability to win. This is computable if Nature's probability distributions are rational. We call these states maximizable. Moreover, we show that for every ε > 0, Player A has a positional strategy that maximizes the probability to win, exactly from maximizable states and up to ε from sub-maximizable states. Second, we consider three-state games with one main state, one target, and one bin. We characterize the local interactions at the main state that guarantee the existence of an optimal Player A strategy. In this case there is a positional one. It turns out that in many-state games, these local interactions also guarantee the existence of a uniform optimal Player A strategy. In a way, these games are well-behaved by design of their elementary bricks, the local interactions. It is decidable whether a local interaction has this desirable property.

cs.GT↗

arXiv2021

Finite-memory strategies in two-player infinite games

We study infinite two-player win/lose games $(A,B,W)$ where $A,B$ are finite and $W \subseteq (A \times B)^ω$. At each round Player 1 and Player 2 concurrently choose one action in $A$ and $B$, respectively. Player 1 wins iff the generated sequence is in $W$. Each history $h \in (A \times B)^*$ induces a game $(A,B,W_h)$ with $W_h := \{ρ\in (A \times B)^ω\mid h ρ\in W\}$. We show the following: if $W$ is in $Δ^0_2$ (for the usual topology), if the inclusion relation induces a well partial order on the $W_h$'s, and if Player 1 has a winning strategy, then she has a finite-memory winning strategy. Our proof relies on inductive descriptions of set complexity, such as the Hausdorff difference hierarchy of the open sets. Examples in $Σ^0_2$ and $Π^0_2$ show some tightness of our result. Our result can be translated to games on finite graphs: e.g. finite-memory determinacy of multi-energy games is a direct corollary, whereas it does not follow from recent general results on finite memory strategies.

cs.GT↗

arXiv2021

From local to global determinacy in concurrent graph games

In general, finite concurrent two-player reachability games are only determined in a weak sense: the supremum probability to win can be approached via stochastic strategies, but cannot be realized. We introduce a class of concurrent games that are determined in a much stronger sense, and in a way, it is the larger class with this property. To this end, we introduce the notion of \emph{local interaction} at a state of a graph game: it is a \emph{game form} whose outcomes (i.e. a table whose entries) are the next states, which depend on the concurrent actions of the players. By definition, a game form is \emph{determined} iff it always yields games that are determined via deterministic strategies when used as a local interaction in a Nature-free, one-shot reachability game. We show that if all the local interactions of a graph game with Borel objective are determined game forms, the game itself is determined: if Nature does not play, one player has a winning strategy; if Nature plays, both players have deterministic strategies that maximize the probability to win. This constitutes a clear-cut separation: either a game form behaves poorly already when used alone with basic objectives, or it behaves well even when used together with other well-behaved game forms and complex objectives. Existing results for positional and finite-memory determinacy in turn-based games are extended this way to concurrent games with determined local interactions (CG-DLI).

cs.GT↗

arXiv2020

Time-aware uniformization of winning strategies

Two-player win/lose games of infinite duration are involved in several disciplines including computer science and logic. If such a game has deterministic winning strategies, one may ask how simple such strategies can get. The answer may help with actual implementation, or to win despite imperfect information, or to conceal sensitive information especially if the game is repeated. Given a concurrent two-player win/lose game of infinite duration, this article considers equivalence relations over histories of played actions. A classical restriction used here is that equivalent histories have equal length, hence \emph{time awareness}. A sufficient condition is given such that if a player has winning strategies, she has one that prescribes the same action at equivalent histories, hence \emph{uniformization}. The proof is fairly constructive and preserves finiteness of strategy memory, and counterexamples show relative tightness of the result. Several corollaries follow for games with states and colors.

cs.GT↗

arXiv2018

Connected Choice and the Brouwer Fixed Point Theorem

We study the computational content of the Brouwer Fixed Point Theorem in the Weihrauch lattice. Connected choice is the operation that finds a point in a non-empty connected closed set given by negative information. One of our main results is that for any fixed dimension the Brouwer Fixed Point Theorem of that dimension is computably equivalent to connected choice of the Euclidean unit cube of the same dimension. Another main result is that connected choice is complete for dimension greater than or equal to two in the sense that it is computably equivalent to Weak Kőnig's Lemma. While we can present two independent proofs for dimension three and upwards that are either based on a simple geometric construction or a combinatorial argument, the proof for dimension two is based on a more involved inverse limit construction. The connected choice operation in dimension one is known to be equivalent to the Intermediate Value Theorem; we prove that this problem is not idempotent in contrast to the case of dimension two and upwards. We also prove that Lipschitz continuity with Lipschitz constants strictly larger than one does not simplify finding fixed points. Finally, we prove that finding a connectedness component of a closed subset of the Euclidean unit cube of any dimension greater or equal to one is equivalent to Weak Kőnig's Lemma. In order to describe these results, we introduce a representation of closed subsets of the unit cube by trees of rational complexes.

math.LO↗

arXiv2018

Extending finite-memory determinacy by Boolean combination of winning conditions

We study finite-memory (FM) determinacy in games on finite graphs, a central question for applications in controller synthesis, as FM strategies correspond to implementable controllers. We establish general conditions under which FM strategies suffice to play optimally, even in a broad multi-objective setting. We show that our framework encompasses important classes of games from the literature, and permits to go further, using a unified approach. While such an approach cannot match ad-hoc proofs with regard to tightness of memory bounds, it has two advantages: first, it gives a widely-applicable criterion for FM determinacy; second, it helps to understand the cornerstones of FM determinacy, which are often hidden but common in proofs for specific (combinations of) winning conditions.

cs.GT↗

arXiv2017

On the existence of weak subgame perfect equilibria

We study multi-player turn-based games played on (potentially infinite) directed graphs. An outcome is assigned to every play of the game. Each player has a preference relation on the set of outcomes which allows him to compare plays. We focus on the recently introduced notion of weak subgame perfect equilibrium (weak SPE). This is a variant of the classical notion of SPE, where players who deviate can only use strategies deviating from their initial strategy in a finite number of histories. Having an SPE in a game implies having a weak SPE but the contrary is generally false. We propose general conditions on the structure of the game graph and on the preference relations of the players that guarantee the existence of a weak SPE, that additionally is finite-memory. From this general result, we derive two large classes of games for which there always exists a weak SPE: (i) the games with a finite-range outcome function, and (ii) the games with a finite underlying graph and a prefix-independent outcome function. For the second class, we identify conditions on the preference relations that guarantee memoryless strategies for the weak SPE.

cs.GT↗

arXiv2017

Dynamics and Coalitions in Sequential Games

We consider N-player non-zero sum games played on finite trees (i.e., sequential games), in which the players have the right to repeatedly update their respective strategies (for instance, to improve the outcome wrt to the current strategy profile). This generates a dynamics in the game which may eventually stabilise to a Nash Equilibrium (as with Kukushkin's lazy improvement), and we argue that it is interesting to study the conditions that guarantee such a dynamics to terminate. We build on the works of Le Roux and Pauly who have studied extensively one such dynamics, namely the Lazy Improvement Dynamics. We extend these works by first defining a turn-based dynamics, proving that it terminates on subgame perfect equilibria, and showing that several variants do not terminate. Second, we define a variant of Kukushkin's lazy improvement where the players may now form coalitions to change strategies. We show how properties of the players' preferences on the outcomes affect the termination of this dynamics, and we thereby characterise classes of games where it always terminates (in particular two-player games).

cs.GT↗

arXiv2017

An Existence Theorem of Nash Equilibrium in Coq and Isabelle

Nash equilibrium (NE) is a central concept in game theory. Here we prove formally a published theorem on existence of an NE in two proof assistants, Coq and Isabelle: starting from a game with finitely many outcomes, one may derive a game by rewriting each of these outcomes with either of two basic outcomes, namely that Player 1 wins or that Player 2 wins. If all ways of deriving such a win/lose game lead to a game where one player has a winning strategy, the original game also has a Nash equilibrium. This article makes three other contributions: first, while the original proof invoked linear extension of strict partial orders, here we avoid it by generalizing the relevant definition. Second, we notice that the theorem also implies the existence of a secure equilibrium, a stronger version of NE that was introduced for model checking. Third, we also notice that the constructive proof of the theorem computes secure equilibria for non-zero-sum priority games (generalizing parity games) in quasi-polynomial time.

cs.GT↗

arXiv2017

A semi-potential for finite and infinite sequential games

We consider a dynamical approach to game in extensive forms. By restricting the convertibility relation over strategy profiles, we obtain a semi-potential (in the sense of Kukushkin), and we show that in finite games the corresponding restriction of better-response dynamics will converge to a Nash equilibrium in quadratic (finite) time. Convergence happens on a per-player basis, and even in the presence of players with cyclic preferences, the players with acyclic preferences will stabilize. Thus, we obtain a candidate notion for rationality in the presence of irrational agents. Moreover, the restriction of convertibility can be justified by a conservative updating of beliefs about the other players strategies. For infinite games in extensive form we can retain convergence to a Nash equilibrium (in some sense), if the preferences are given by continuous payoff functions; or obtain a transfinite convergence if the outcome sets of the game are $Δ^0_2$-sets.

cs.GT↗

arXiv2016

Extending Finite Memory Determinacy to Multiplayer Games

We show that under some general conditions the finite memory determinacy of a class of two-player win/lose games played on finite graphs implies the existence of a Nash equilibrium built from finite memory strategies for the corresponding class of multi-player multi-outcome games. This generalizes a previous result by Brihaye, De Pril and Schewe. We provide a number of example that separate the various criteria we explore. Our proofs are generally constructive, that is, provide upper bounds for the memory required, as well as algorithms to compute the relevant Nash equilibria.

cs.GT↗

arXiv2016

Minkowski games

We introduce and study Minkowski games. These are two player games, where the players take turns to chose positions in $\mathbb{R}^d$ based on some rules. Variants include boundedness games, where one player wants to keep the positions bounded, and the other wants to escape to infinity; as well as safety games, where one player wants to stay within a prescribed set, while the other wants to leave it. We provide some general characterizations of which player can win such games, and explore the computational complexity of the associated decision problems. A natural representation of boundedness games yields coNP-completeness, whereas the safety games are undecidable.

cs.GT↗