16 Search Results for "Le Roux, Stéphane"


Document
From Local to Global Optimality in Concurrent Parity Games

Authors: Benjamin Bordais, Patricia Bouyer, and Stéphane Le Roux

Published in: LIPIcs, Volume 288, 32nd EACSL Annual Conference on Computer Science Logic (CSL 2024)


Abstract
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.

Cite as

Benjamin Bordais, Patricia Bouyer, and Stéphane Le Roux. From Local to Global Optimality in Concurrent Parity Games. In 32nd EACSL Annual Conference on Computer Science Logic (CSL 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 288, pp. 18:1-18:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)


Copy BibTex To Clipboard

@InProceedings{bordais_et_al:LIPIcs.CSL.2024.18,
  author =	{Bordais, Benjamin and Bouyer, Patricia and Le Roux, St\'{e}phane},
  title =	{{From Local to Global Optimality in Concurrent Parity Games}},
  booktitle =	{32nd EACSL Annual Conference on Computer Science Logic (CSL 2024)},
  pages =	{18:1--18:21},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-310-2},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{288},
  editor =	{Murano, Aniello and Silva, Alexandra},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2024.18},
  URN =		{urn:nbn:de:0030-drops-196612},
  doi =		{10.4230/LIPIcs.CSL.2024.18},
  annote =	{Keywords: Game forms, stochastic games, parity games, Blackwell/Martin values}
}
Document
Invited Talk
The True Colors of Memory: A Tour of Chromatic-Memory Strategies in Zero-Sum Games on Graphs (Invited Talk)

Authors: Patricia Bouyer, Mickael Randour, and Pierre Vandenhove

Published in: LIPIcs, Volume 250, 42nd IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2022)


Abstract
Two-player turn-based zero-sum games on (finite or infinite) graphs are a central framework in theoretical computer science - notably as a tool for controller synthesis, but also due to their connection with logic and automata theory. A crucial challenge in the field is to understand how complex strategies need to be to play optimally, given a type of game and a winning objective. In this invited contribution, we give a tour of recent advances aiming to characterize games where finite-memory strategies suffice (i.e., using a limited amount of information about the past). We mostly focus on so-called chromatic memory, which is limited to using colors - the basic building blocks of objectives - seen along a play to update itself. Chromatic memory has the advantage of being usable in different game graphs, and the corresponding class of strategies turns out to be of great interest to both the practical and the theoretical sides.

Cite as

Patricia Bouyer, Mickael Randour, and Pierre Vandenhove. The True Colors of Memory: A Tour of Chromatic-Memory Strategies in Zero-Sum Games on Graphs (Invited Talk). In 42nd IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 250, pp. 3:1-3:18, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2022)


Copy BibTex To Clipboard

@InProceedings{bouyer_et_al:LIPIcs.FSTTCS.2022.3,
  author =	{Bouyer, Patricia and Randour, Mickael and Vandenhove, Pierre},
  title =	{{The True Colors of Memory: A Tour of Chromatic-Memory Strategies in Zero-Sum Games on Graphs}},
  booktitle =	{42nd IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2022)},
  pages =	{3:1--3:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-261-7},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{250},
  editor =	{Dawar, Anuj and Guruswami, Venkatesan},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2022.3},
  URN =		{urn:nbn:de:0030-drops-173957},
  doi =		{10.4230/LIPIcs.FSTTCS.2022.3},
  annote =	{Keywords: two-player games on graphs, finite-memory strategies, chromatic memory, parity automata, \omega-regularity}
}
Document
Playing (Almost-)Optimally in Concurrent Büchi and Co-Büchi Games

Authors: Benjamin Bordais, Patricia Bouyer, and Stéphane Le Roux

Published in: LIPIcs, Volume 250, 42nd IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2022)


Abstract
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.

Cite as

Benjamin Bordais, Patricia Bouyer, and Stéphane Le Roux. Playing (Almost-)Optimally in Concurrent Büchi and Co-Büchi Games. In 42nd IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 250, pp. 33:1-33:18, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2022)


Copy BibTex To Clipboard

@InProceedings{bordais_et_al:LIPIcs.FSTTCS.2022.33,
  author =	{Bordais, Benjamin and Bouyer, Patricia and Le Roux, St\'{e}phane},
  title =	{{Playing (Almost-)Optimally in Concurrent B\"{u}chi and Co-B\"{u}chi Games}},
  booktitle =	{42nd IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2022)},
  pages =	{33:1--33:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-261-7},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{250},
  editor =	{Dawar, Anuj and Guruswami, Venkatesan},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2022.33},
  URN =		{urn:nbn:de:0030-drops-174258},
  doi =		{10.4230/LIPIcs.FSTTCS.2022.33},
  annote =	{Keywords: Concurrent Games, Optimal Strategies, B\"{u}chi Objective, co-B\"{u}chi Objective}
}
Document
Finite-Memory Strategies in Two-Player Infinite Games

Authors: Patricia Bouyer, Stéphane Le Roux, and Nathan Thomasset

Published in: LIPIcs, Volume 216, 30th EACSL Annual Conference on Computer Science Logic (CSL 2022)


Abstract
We study infinite two-player win/lose games (A,B,W) where A,B are finite and W ⊆ (A×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 ∈ (A×B)^* induces a game (A,B,W_h) with W_h : = {ρ ∈ (A×B)^ω ∣ h ρ ∈ W}. We show the following: if W is in Δ⁰₂ (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 Σ⁰₂ and Π⁰₂ 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.

Cite as

Patricia Bouyer, Stéphane Le Roux, and Nathan Thomasset. Finite-Memory Strategies in Two-Player Infinite Games. In 30th EACSL Annual Conference on Computer Science Logic (CSL 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 216, pp. 8:1-8:16, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2022)


Copy BibTex To Clipboard

@InProceedings{bouyer_et_al:LIPIcs.CSL.2022.8,
  author =	{Bouyer, Patricia and Le Roux, St\'{e}phane and Thomasset, Nathan},
  title =	{{Finite-Memory Strategies in Two-Player Infinite Games}},
  booktitle =	{30th EACSL Annual Conference on Computer Science Logic (CSL 2022)},
  pages =	{8:1--8:16},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-218-1},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{216},
  editor =	{Manea, Florin and Simpson, Alex},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2022.8},
  URN =		{urn:nbn:de:0030-drops-157285},
  doi =		{10.4230/LIPIcs.CSL.2022.8},
  annote =	{Keywords: Two-player win/lose games, Infinite trees, Finite-memory winning strategies, Well partial orders, Hausdorff difference hierarchy}
}
Document
Optimal Strategies in Concurrent Reachability Games

Authors: Benjamin Bordais, Patricia Bouyer, and Stéphane Le Roux

Published in: LIPIcs, Volume 216, 30th EACSL Annual Conference on Computer Science Logic (CSL 2022)


Abstract
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 𝖡, 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 𝖠 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 𝖠 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 𝖠 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 𝖠 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 𝖠 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.

Cite as

Benjamin Bordais, Patricia Bouyer, and Stéphane Le Roux. Optimal Strategies in Concurrent Reachability Games. In 30th EACSL Annual Conference on Computer Science Logic (CSL 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 216, pp. 7:1-7:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)


Copy BibTex To Clipboard

@InProceedings{bordais_et_al:LIPIcs.CSL.2022.7,
  author =	{Bordais, Benjamin and Bouyer, Patricia and Le Roux, St\'{e}phane},
  title =	{{Optimal Strategies in Concurrent Reachability Games}},
  booktitle =	{30th EACSL Annual Conference on Computer Science Logic (CSL 2022)},
  pages =	{7:1--7:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-218-1},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{216},
  editor =	{Manea, Florin and Simpson, Alex},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2022.7},
  URN =		{urn:nbn:de:0030-drops-157278},
  doi =		{10.4230/LIPIcs.CSL.2022.7},
  annote =	{Keywords: Concurrent reachability games, Game forms, Optimal strategies}
}
Document
From Local to Global Determinacy in Concurrent Graph Games

Authors: Benjamin Bordais, Patricia Bouyer, and Stéphane Le Roux

Published in: LIPIcs, Volume 213, 41st IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2021)


Abstract
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 largest class with this property. To this end, we introduce the notion of local interaction at a state of a graph game: it is a 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 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).

Cite as

Benjamin Bordais, Patricia Bouyer, and Stéphane Le Roux. From Local to Global Determinacy in Concurrent Graph Games. In 41st IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 213, pp. 41:1-41:14, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2021)


Copy BibTex To Clipboard

@InProceedings{bordais_et_al:LIPIcs.FSTTCS.2021.41,
  author =	{Bordais, Benjamin and Bouyer, Patricia and Le Roux, St\'{e}phane},
  title =	{{From Local to Global Determinacy in Concurrent Graph Games}},
  booktitle =	{41st IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2021)},
  pages =	{41:1--41:14},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-215-0},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{213},
  editor =	{Boja\'{n}czyk, Miko{\l}aj and Chekuri, Chandra},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2021.41},
  URN =		{urn:nbn:de:0030-drops-155522},
  doi =		{10.4230/LIPIcs.FSTTCS.2021.41},
  annote =	{Keywords: Concurrent games, Game forms, Local interaction}
}
Document
Games Where You Can Play Optimally with Arena-Independent Finite Memory

Authors: Patricia Bouyer, Stéphane Le Roux, Youssouf Oualhadj, Mickael Randour, and Pierre Vandenhove

Published in: LIPIcs, Volume 171, 31st International Conference on Concurrency Theory (CONCUR 2020)


Abstract
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 [Hugo Gimbert and Wieslaw Zielonka, 2005] 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).

Cite as

Patricia Bouyer, Stéphane Le Roux, Youssouf Oualhadj, Mickael Randour, and Pierre Vandenhove. Games Where You Can Play Optimally with Arena-Independent Finite Memory. In 31st International Conference on Concurrency Theory (CONCUR 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 171, pp. 24:1-24:22, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2020)


Copy BibTex To Clipboard

@InProceedings{bouyer_et_al:LIPIcs.CONCUR.2020.24,
  author =	{Bouyer, Patricia and Le Roux, St\'{e}phane and Oualhadj, Youssouf and Randour, Mickael and Vandenhove, Pierre},
  title =	{{Games Where You Can Play Optimally with Arena-Independent Finite Memory}},
  booktitle =	{31st International Conference on Concurrency Theory (CONCUR 2020)},
  pages =	{24:1--24:22},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-160-3},
  ISSN =	{1868-8969},
  year =	{2020},
  volume =	{171},
  editor =	{Konnov, Igor and Kov\'{a}cs, Laura},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2020.24},
  URN =		{urn:nbn:de:0030-drops-128360},
  doi =		{10.4230/LIPIcs.CONCUR.2020.24},
  annote =	{Keywords: two-player games on graphs, finite-memory determinacy, optimal strategies}
}
Document
Primitive Floats in Coq

Authors: Guillaume Bertholon, Érik Martin-Dorel, and Pierre Roux

Published in: LIPIcs, Volume 141, 10th International Conference on Interactive Theorem Proving (ITP 2019)


Abstract
Some mathematical proofs involve intensive computations, for instance: the four-color theorem, Hales' theorem on sphere packing (formerly known as the Kepler conjecture) or interval arithmetic. For numerical computations, floating-point arithmetic enjoys widespread usage thanks to its efficiency, despite the introduction of rounding errors. Formal guarantees can be obtained on floating-point algorithms based on the IEEE 754 standard, which precisely specifies floating-point arithmetic and its rounding modes, and a proof assistant such as Coq, that enjoys efficient computation capabilities. Coq offers machine integers, however floating-point arithmetic still needed to be emulated using these integers. A modified version of Coq is presented that enables using the machine floating-point operators. The main obstacles to such an implementation and its soundness are discussed. Benchmarks show potential performance gains of two orders of magnitude.

Cite as

Guillaume Bertholon, Érik Martin-Dorel, and Pierre Roux. Primitive Floats in Coq. In 10th International Conference on Interactive Theorem Proving (ITP 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 141, pp. 7:1-7:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)


Copy BibTex To Clipboard

@InProceedings{bertholon_et_al:LIPIcs.ITP.2019.7,
  author =	{Bertholon, Guillaume and Martin-Dorel, \'{E}rik and Roux, Pierre},
  title =	{{Primitive Floats in Coq}},
  booktitle =	{10th International Conference on Interactive Theorem Proving (ITP 2019)},
  pages =	{7:1--7:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-122-1},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{141},
  editor =	{Harrison, John and O'Leary, John and Tolmach, Andrew},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2019.7},
  URN =		{urn:nbn:de:0030-drops-110629},
  doi =		{10.4230/LIPIcs.ITP.2019.7},
  annote =	{Keywords: Coq formal proofs, floating-point arithmetic, reflexive tactics, Cholesky decomposition}
}
Document
Life Is Random, Time Is Not: Markov Decision Processes with Window Objectives

Authors: Thomas Brihaye, Florent Delgrange, Youssouf Oualhadj, and Mickael Randour

Published in: LIPIcs, Volume 140, 30th International Conference on Concurrency Theory (CONCUR 2019)


Abstract
The window mechanism was introduced by Chatterjee et al. [Krishnendu Chatterjee et al., 2015] to strengthen classical game objectives with time bounds. It permits to synthesize system controllers that exhibit acceptable behaviors within a configurable time frame, all along their infinite execution, in contrast to the traditional objectives that only require correctness of behaviors in the limit. The window concept has proved its interest in a variety of two-player zero-sum games, thanks to the ability to reason about such time bounds in system specifications, but also the increased tractability that it usually yields. In this work, we extend the window framework to stochastic environments by considering the fundamental threshold probability problem in Markov decision processes for window objectives. That is, given such an objective, we want to synthesize strategies that guarantee satisfying runs with a given probability. We solve this problem for the usual variants of window objectives, where either the time frame is set as a parameter, or we ask if such a time frame exists. We develop a generic approach for window-based objectives and instantiate it for the classical mean-payoff and parity objectives, already considered in games. Our work paves the way to a wide use of the window mechanism in stochastic models.

Cite as

Thomas Brihaye, Florent Delgrange, Youssouf Oualhadj, and Mickael Randour. Life Is Random, Time Is Not: Markov Decision Processes with Window Objectives. In 30th International Conference on Concurrency Theory (CONCUR 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 140, pp. 8:1-8:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)


Copy BibTex To Clipboard

@InProceedings{brihaye_et_al:LIPIcs.CONCUR.2019.8,
  author =	{Brihaye, Thomas and Delgrange, Florent and Oualhadj, Youssouf and Randour, Mickael},
  title =	{{Life Is Random, Time Is Not: Markov Decision Processes with Window Objectives}},
  booktitle =	{30th International Conference on Concurrency Theory (CONCUR 2019)},
  pages =	{8:1--8:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-121-4},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{140},
  editor =	{Fokkink, Wan and van Glabbeek, Rob},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2019.8},
  URN =		{urn:nbn:de:0030-drops-109103},
  doi =		{10.4230/LIPIcs.CONCUR.2019.8},
  annote =	{Keywords: Markov decision processes, window mean-payoff, window parity}
}
Document
The Complexity of Subgame Perfect Equilibria in Quantitative Reachability Games

Authors: Thomas Brihaye, Véronique Bruyère, Aline Goeminne, Jean-François Raskin, and Marie van den Bogaard

Published in: LIPIcs, Volume 140, 30th International Conference on Concurrency Theory (CONCUR 2019)


Abstract
We study multiplayer quantitative reachability games played on a finite directed graph, where the objective of each player is to reach his target set of vertices as quickly as possible. Instead of the well-known notion of Nash equilibrium (NE), we focus on the notion of subgame perfect equilibrium (SPE), a refinement of NE well-suited in the framework of games played on graphs. It is known that there always exists an SPE in quantitative reachability games and that the constrained existence problem is decidable. We here prove that this problem is PSPACE-complete. To obtain this result, we propose a new algorithm that iteratively builds a set of constraints characterizing the set of SPE outcomes in quantitative reachability games. This set of constraints is obtained by iterating an operator that reinforces the constraints up to obtaining a fixpoint. With this fixpoint, the set of SPE outcomes can be represented by a finite graph of size at most exponential. A careful inspection of the computation allows us to establish PSPACE membership.

Cite as

Thomas Brihaye, Véronique Bruyère, Aline Goeminne, Jean-François Raskin, and Marie van den Bogaard. The Complexity of Subgame Perfect Equilibria in Quantitative Reachability Games. In 30th International Conference on Concurrency Theory (CONCUR 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 140, pp. 13:1-13:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)


Copy BibTex To Clipboard

@InProceedings{brihaye_et_al:LIPIcs.CONCUR.2019.13,
  author =	{Brihaye, Thomas and Bruy\`{e}re, V\'{e}ronique and Goeminne, Aline and Raskin, Jean-Fran\c{c}ois and van den Bogaard, Marie},
  title =	{{The Complexity of Subgame Perfect Equilibria in Quantitative Reachability Games}},
  booktitle =	{30th International Conference on Concurrency Theory (CONCUR 2019)},
  pages =	{13:1--13:16},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-121-4},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{140},
  editor =	{Fokkink, Wan and van Glabbeek, Rob},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2019.13},
  URN =		{urn:nbn:de:0030-drops-109153},
  doi =		{10.4230/LIPIcs.CONCUR.2019.13},
  annote =	{Keywords: multiplayer non-zero-sum games played on graphs, quantitative reachability objectives, subgame perfect equilibria, constrained existence problem}
}
Document
Extending Finite-Memory Determinacy by Boolean Combination of Winning Conditions

Authors: Stéphane Le Roux, Arno Pauly, and Mickael Randour

Published in: LIPIcs, Volume 122, 38th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2018)


Abstract
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.

Cite as

Stéphane Le Roux, Arno Pauly, and Mickael Randour. Extending Finite-Memory Determinacy by Boolean Combination of Winning Conditions. In 38th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 122, pp. 38:1-38:20, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2018)


Copy BibTex To Clipboard

@InProceedings{leroux_et_al:LIPIcs.FSTTCS.2018.38,
  author =	{Le Roux, St\'{e}phane and Pauly, Arno and Randour, Mickael},
  title =	{{Extending Finite-Memory Determinacy by Boolean Combination of Winning Conditions}},
  booktitle =	{38th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2018)},
  pages =	{38:1--38:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-093-4},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{122},
  editor =	{Ganguly, Sumit and Pandya, Paritosh},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2018.38},
  URN =		{urn:nbn:de:0030-drops-99373},
  doi =		{10.4230/LIPIcs.FSTTCS.2018.38},
  annote =	{Keywords: games on graphs, finite-memory determinacy, multiple objectives}
}
Document
Concurrent Games and Semi-Random Determinacy

Authors: Stéphane Le Roux

Published in: LIPIcs, Volume 117, 43rd International Symposium on Mathematical Foundations of Computer Science (MFCS 2018)


Abstract
Consider concurrent, infinite duration, two-player win/lose games played on graphs. If the winning condition satisfies some simple requirement, the existence of Player 1 winning (finite-memory) strategies is equivalent to the existence of winning (finite-memory) strategies in finitely many derived one-player games. Several classical winning conditions satisfy this simple requirement. Under an additional requirement on the winning condition, the non-existence of Player 1 winning strategies from all vertices is equivalent to the existence of Player 2 stochastic strategies almost-sure winning from all vertices. Only few classical winning conditions satisfy this additional requirement, but a fairness variant of omega-regular languages does.

Cite as

Stéphane Le Roux. Concurrent Games and Semi-Random Determinacy. In 43rd International Symposium on Mathematical Foundations of Computer Science (MFCS 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 117, pp. 40:1-40:15, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2018)


Copy BibTex To Clipboard

@InProceedings{leroux:LIPIcs.MFCS.2018.40,
  author =	{Le Roux, St\'{e}phane},
  title =	{{Concurrent Games and Semi-Random Determinacy}},
  booktitle =	{43rd International Symposium on Mathematical Foundations of Computer Science (MFCS 2018)},
  pages =	{40:1--40:15},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-086-6},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{117},
  editor =	{Potapov, Igor and Spirakis, Paul and Worrell, James},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.MFCS.2018.40},
  URN =		{urn:nbn:de:0030-drops-96220},
  doi =		{10.4230/LIPIcs.MFCS.2018.40},
  annote =	{Keywords: Two-player win/lose, graph, infinite duration, abstract winning condition}
}
Document
Minkowski Games

Authors: Stéphane Le Roux, Arno Pauly, and Jean-François Raskin

Published in: LIPIcs, Volume 66, 34th Symposium on Theoretical Aspects of Computer Science (STACS 2017)


Abstract
We introduce and study Minkowski games. In these games, two players take turns to choose positions in R^d based on some rules. Variants include boundedness games, where one player wants to keep the positions bounded (while the other wants to escape to infinity), and safety games, where one player wants to stay within a given 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.

Cite as

Stéphane Le Roux, Arno Pauly, and Jean-François Raskin. Minkowski Games. In 34th Symposium on Theoretical Aspects of Computer Science (STACS 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 66, pp. 50:1-50:13, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2017)


Copy BibTex To Clipboard

@InProceedings{leroux_et_al:LIPIcs.STACS.2017.50,
  author =	{Le Roux, St\'{e}phane and Pauly, Arno and Raskin, Jean-Fran\c{c}ois},
  title =	{{Minkowski Games}},
  booktitle =	{34th Symposium on Theoretical Aspects of Computer Science (STACS 2017)},
  pages =	{50:1--50:13},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-028-6},
  ISSN =	{1868-8969},
  year =	{2017},
  volume =	{66},
  editor =	{Vollmer, Heribert and Vall\'{e}e, Brigitte},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.STACS.2017.50},
  URN =		{urn:nbn:de:0030-drops-69849},
  doi =		{10.4230/LIPIcs.STACS.2017.50},
  annote =	{Keywords: Control in R^d, determinacy, polytopic/arbitrary, coNP-complete, undecidable}
}
Document
Stable States of Perturbed Markov Chains

Authors: Volker Betz and Stéphane Le Roux

Published in: LIPIcs, Volume 58, 41st International Symposium on Mathematical Foundations of Computer Science (MFCS 2016)


Abstract
Given an infinitesimal perturbation of a discrete-time finite Markov chain, we seek the states that are stable despite the perturbation, i.e. the states whose weights in the stationary distributions can be bounded away from 0 as the noise fades away. Chemists, economists, and computer scientists have been studying irreducible perturbations built with monomial maps. Under these assumptions, Young proved the existence of and computed the stable states in cubic time. We fully drop these assumptions, generalize Young's technique, and show that stability is decidable as long as f in O(g) is. Furthermore, if the perturbation maps (and their multiplications) satisfy f in O(g) or g in O(f), we prove the existence of and compute the stable states and the metastable dynamics at all time scales where some states vanish. Conversely, if the big-O assumption does not hold, we build a perturbation with these maps and no stable state. Our algorithm also runs in cubic time despite the weak assumptions and the additional work. Proving its correctness relies on new or rephrased results in Markov chain theory, and on algebraic abstractions thereof.

Cite as

Volker Betz and Stéphane Le Roux. Stable States of Perturbed Markov Chains. In 41st International Symposium on Mathematical Foundations of Computer Science (MFCS 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 58, pp. 18:1-18:14, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2016)


Copy BibTex To Clipboard

@InProceedings{betz_et_al:LIPIcs.MFCS.2016.18,
  author =	{Betz, Volker and Le Roux, St\'{e}phane},
  title =	{{Stable States of Perturbed Markov Chains}},
  booktitle =	{41st International Symposium on Mathematical Foundations of Computer Science (MFCS 2016)},
  pages =	{18:1--18:14},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-016-3},
  ISSN =	{1868-8969},
  year =	{2016},
  volume =	{58},
  editor =	{Faliszewski, Piotr and Muscholl, Anca and Niedermeier, Rolf},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.MFCS.2016.18},
  URN =		{urn:nbn:de:0030-drops-64335},
  doi =		{10.4230/LIPIcs.MFCS.2016.18},
  annote =	{Keywords: evolution, metastability, tropical, shortest path, SCC, cubic time}
}
Document
Weak Subgame Perfect Equilibria and their Application to Quantitative Reachability

Authors: Thomas Brihaye, Véronique Bruyère, Noémie Meunier, and Jean-Francois Raskin

Published in: LIPIcs, Volume 41, 24th EACSL Annual Conference on Computer Science Logic (CSL 2015)


Abstract
We study n-player turn-based games played on a finite directed graph. For each play, the players have to pay a cost that they want to minimize. Instead of the well-known notion of Nash equilibrium (NE), we focus on the notion of subgame perfect equilibrium (SPE), a refinement of NE well-suited in the framework of games played on graphs. We also study natural variants of SPE, named weak (resp. very weak) SPE, where players who deviate cannot use the full class of strategies but only a subclass with a finite number of (resp. a unique) deviation step(s). Our results are threefold. Firstly, we characterize in the form of a Folk theorem the set of all plays that are the outcome of a weak SPE. Secondly, for the class of quantitative reachability games, we prove the existence of a finite-memory SPE and provide an algorithm for computing it (only existence was known with no information regarding the memory). Moreover, we show that the existence of a constrained SPE, i.e. an SPE such that each player pays a cost less than a given constant, can be decided. The proofs rely on our Folk theorem for weak SPEs (which coincide with SPEs in the case of quantitative reachability games) and on the decidability of MSO logic on infinite words. Finally with similar techniques, we provide a second general class of games for which the existence of a (constrained) weak SPE is decidable.

Cite as

Thomas Brihaye, Véronique Bruyère, Noémie Meunier, and Jean-Francois Raskin. Weak Subgame Perfect Equilibria and their Application to Quantitative Reachability. In 24th EACSL Annual Conference on Computer Science Logic (CSL 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 41, pp. 504-518, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)


Copy BibTex To Clipboard

@InProceedings{brihaye_et_al:LIPIcs.CSL.2015.504,
  author =	{Brihaye, Thomas and Bruy\`{e}re, V\'{e}ronique and Meunier, No\'{e}mie and Raskin, Jean-Francois},
  title =	{{Weak Subgame Perfect Equilibria and their Application to Quantitative Reachability}},
  booktitle =	{24th EACSL Annual Conference on Computer Science Logic (CSL 2015)},
  pages =	{504--518},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-90-3},
  ISSN =	{1868-8969},
  year =	{2015},
  volume =	{41},
  editor =	{Kreutzer, Stephan},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2015.504},
  URN =		{urn:nbn:de:0030-drops-54345},
  doi =		{10.4230/LIPIcs.CSL.2015.504},
  annote =	{Keywords: multi-player games on graphs, quantitative objectives, Nash equilibrium, subgame perfect equilibrium, quantitative reachability}
}
  • Refine by Author
  • 10 Le Roux, Stéphane
  • 7 Bouyer, Patricia
  • 4 Bordais, Benjamin
  • 4 Randour, Mickael
  • 3 Brihaye, Thomas
  • Show More...

  • Refine by Classification
  • 4 Theory of computation → Formal languages and automata theory
  • 3 Theory of computation → Solution concepts in game theory
  • 2 Software and its engineering → Formal methods
  • 2 Theory of computation
  • 2 Theory of computation → Logic and verification
  • Show More...

  • Refine by Keyword
  • 3 Game forms
  • 2 finite-memory determinacy
  • 2 two-player games on graphs
  • 1 Blackwell/Martin values
  • 1 Büchi Objective
  • Show More...

  • Refine by Type
  • 16 document

  • Refine by Publication Year
  • 4 2022
  • 3 2019
  • 2 2015
  • 2 2018
  • 1 2016
  • Show More...

Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail