Publications | Mickael Randour

See also my Google scholar or my dblp page. Publications are grouped by type (journals, conferences, etc) and authors are usually listed alphabetically in my field.

I have (co-)authored 1 book, 12 journal articles, and 31 conference papers, including 5 invited contributions.

Books

2023

Book

Games on Graphs

Nathanaël Fijalkow, Nathalie Bertrand, Patricia Bouyer-Decitre, Romain Brenguier, Arnaud Carayol, John Fearnley, Hugo Gimbert, Florian Horn, Rasmus Ibsen-Jensen, Nicolas Markey, Benjamin Monmege, Petr Novotný, Mickael Randour, Ocan Sankur, Sylvain Schmitz, Olivier Serre, and Mateusz Skomra

2023

Abs arXiv Bib

@book{DBLP:journals/corr/abs-2305-10546,
  author = {Fijalkow, Nathana{\"{e}}l and Bertrand, Nathalie and Bouyer{-}Decitre, Patricia and Brenguier, Romain and Carayol, Arnaud and Fearnley, John and Gimbert, Hugo and Horn, Florian and Ibsen{-}Jensen, Rasmus and Markey, Nicolas and Monmege, Benjamin and Novotn{\'{y}}, Petr and Randour, Mickael and Sankur, Ocan and Schmitz, Sylvain and Serre, Olivier and Skomra, Mateusz},
  title = {Games on Graphs},
  journal = {CoRR},
  volume = {abs/2305.10546},
  year = {2023},
  url = {https://doi.org/10.48550/arXiv.2305.10546},
  doi = {10.48550/ARXIV.2305.10546},
  eprinttype = {arXiv},
  eprint = {2305.10546},
  timestamp = {Thu, 25 May 2023 01:00:00 +0200},
  biburl = {https://dblp.org/rec/journals/corr/abs-2305-10546.bib},
  bibsource = {dblp computer science bibliography, https://dblp.org},
}

Peer-reviewed journals

2024

LMCS
Half-Positional Objectives Recognized by Deterministic Büchi Automata

Patricia Bouyer, Antonio Casares, Mickael Randour, and Pierre Vandenhove

Logical Methods in Computer Science, 2024

Abs arXiv Bib

In two-player zero-sum games on graphs, the protagonist tries to achieve an objective while the antagonist aims to prevent it. Objectives for which both players do not need to use memory to play optimally are well-understood and characterized both in finite and infinite graphs. Less is known about the larger class of half-positional objectives, i.e., those for which the protagonist does not need memory (but for which the antagonist might). In particular, no characterization of half-positionality is known for the central class of ω-regular objectives. Here, we characterize objectives recognizable by deterministic Büchi automata (a class of ω-regular objectives) that are half-positional, both over finite and infinite graphs. This characterization yields a polynomial-time algorithm to decide half-positionality of an objective recognized by a given deterministic Büchi automaton.
@article{half_pos_LMCS, author = {Bouyer, Patricia and Casares, Antonio and Randour, Mickael and Vandenhove, Pierre}, title = {Half-Positional Objectives Recognized by Deterministic B{\"{u}}chi Automata}, journal = {Logical Methods in Computer Science}, year = {2024}, volume = {20}, number = {3}, }
Inf. Comput.
Different Strokes in Randomised Strategies: Revisiting Kuhn’s Theorem Under Finite-Memory Assumptions

James C. A. Main, and Mickael Randour

Information and Computation, 2024

Abs arXiv Bib

Two-player (antagonistic) games on (possibly stochastic) graphs are a prevalent model in theoretical computer science, notably as a framework for reactive synthesis. Optimal strategies may require randomisation when dealing with inherently probabilistic goals, balancing multiple objectives, or in contexts of partial information. There is no unique way to define randomised strategies. For instance, one can use so-called mixed strategies or behavioural ones. In the most general settings, these two classes do not share the same expressiveness. A seminal result in game theory - Kuhn’s theorem - asserts their equivalence in games of perfect recall. This result crucially relies on the possibility for strategies to use infinite memory, i.e., unlimited knowledge of all past observations. However, computer systems are finite in practice. Hence it is pertinent to restrict our attention to finite-memory strategies, defined as automata with outputs. Randomisation can be implemented in these in different ways: the initialisation, outputs or transitions can be randomised or deterministic respectively. Depending on which aspects are randomised, the expressiveness of the corresponding class of finite-memory strategies differs. In this work, we study two-player turn-based stochastic games and provide a complete taxonomy of the classes of finite-memory strategies obtained by varying which of the three aforementioned components are randomised. Our taxonomy holds both in settings of perfect and imperfect information, and in games with more than two players.
@article{kuhn_IandC, author = {Main, James C. A. and Randour, Mickael}, title = {Different Strokes in Randomised Strategies: Revisiting Kuhn's Theorem Under Finite-Memory Assumptions}, journal = {Information and Computation}, year = {2024}, }

2023

LMCS
Arena-Independent Finite-Memory Determinacy in Stochastic Games

Patricia Bouyer, Youssouf Oualhadj, Mickael Randour, and Pierre Vandenhove

Logical Methods in Computer Science, 2023

Abs arXiv Bib

We study stochastic zero-sum games on graphs, which are prevalent tools to model decision-making in presence of an antagonistic opponent in a random environment. In this setting, an important question is the one of strategy complexity: what kinds of strategies are sufficient or required to play optimally (e.g., randomization or memory requirements)? Our contributions further the understanding of arena-independent finite-memory (AIFM) determinacy, i.e., the study of objectives for which memory is needed, but in a way that only depends on limited parameters of the game graphs. First, we show that objectives for which pure AIFM strategies suffice to play optimally also admit pure AIFM subgame perfect strategies. Second, we show that we can reduce the study of objectives for which pure AIFM strategies suffice in two-player stochastic games to the easier study of one-player stochastic games (i.e., Markov decision processes). Third, we characterize the sufficiency of AIFM strategies through two intuitive properties of objectives. This work extends a line of research started on deterministic games to stochastic ones.
@article{DBLP:journals/lmcs/BouyerORV23, author = {Bouyer, Patricia and Oualhadj, Youssouf and Randour, Mickael and Vandenhove, Pierre}, title = {Arena-Independent Finite-Memory Determinacy in Stochastic Games}, journal = {Logical Methods in Computer Science}, volume = {19}, number = {4}, year = {2023}, url = {https://doi.org/10.46298/lmcs-19(4:18)2023}, doi = {10.46298/LMCS-19(4:18)2023}, timestamp = {Tue, 23 Jan 2024 00:00:00 +0100}, biburl = {https://dblp.org/rec/journals/lmcs/BouyerORV23.bib}, bibsource = {dblp computer science bibliography, https://dblp.org}, }
TheoretiCS
Characterizing Omega-Regularity through Finite-Memory Determinacy of Games on Infinite Graphs

Patricia Bouyer, Mickael Randour, and Pierre Vandenhove

TheoretiCS, 2023

Abs arXiv Bib

We consider zero-sum games on infinite graphs, with objectives specified as sets of infinite words over some alphabet of colors. A well-studied class of objectives is the one of ω-regular objectives, due to its relation to many natural problems in theoretical computer science. We focus on the strategy complexity question: given an objective, how much memory does each player require to play as well as possible? A classical result is that finite-memory strategies suffice for both players when the objective is ω-regular. We show a reciprocal of that statement: when both players can play optimally with a chromatic finite-memory structure (i.e., whose updates can only observe colors) in all infinite game graphs, then the objective must be ω-regular. This provides a game-theoretic characterization of ω-regular objectives, and this characterization can help in obtaining memory bounds. Moreover, a by-product of our characterization is a new one-to-two-player lift: to show that chromatic finite-memory structures suffice to play optimally in two-player games on infinite graphs, it suffices to show it in the simpler case of one-player games on infinite graphs. We illustrate our results with the family of discounted-sum objectives, for which ω-regularity depends on the value of some parameters.
@article{DBLP:journals/theoretics/BouyerRV23, author = {Bouyer, Patricia and Randour, Mickael and Vandenhove, Pierre}, title = {Characterizing Omega-Regularity through Finite-Memory Determinacy of Games on Infinite Graphs}, journal = {TheoretiCS}, volume = {2}, year = {2023}, url = {https://doi.org/10.46298/theoretics.23.1}, doi = {10.46298/THEORETICS.23.1}, timestamp = {Sat, 30 Sep 2023 01:00:00 +0200}, biburl = {https://dblp.org/rec/journals/theoretics/BouyerRV23.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }

2022

Inf. Comput.
Decisiveness of stochastic systems and its application to hybrid models

Patricia Bouyer, Thomas Brihaye, Mickael Randour, Cédric Rivière, and Pierre Vandenhove

Information and Computation, 2022

Abs arXiv Bib

In [ABM07], Abdulla et al. introduced the concept of decisiveness, an interesting tool for lifting good properties of finite Markov chains to denumerable ones. Later, this concept was extended to more general stochastic transition systems (STSs), allowing the design of various verification algorithms for large classes of (infinite) STSs. We further improve the understanding and utility of decisiveness in two ways. First, we provide a general criterion for proving decisiveness of general STSs. This criterion, which is very natural but whose proof is rather technical, (strictly) generalizes all known criteria from the literature. Second, we focus on stochastic hybrid systems (SHSs), a stochastic extension of hybrid systems. We establish the decisiveness of a large class of SHSs and, under a few classical hypotheses from mathematical logic, we show how to decide reachability problems in this class, even though they are undecidable for general SHSs. This provides a decidable stochastic extension of o-minimal hybrid systems. [ABM07] Parosh A. Abdulla, Noomene Ben Henda, and Richard Mayr. 2007. Decisive Markov Chains. Log. Methods Comput. Sci. 3, 4 (2007).
@article{DBLP:journals/iandc/BouyerBRRV22, author = {Bouyer, Patricia and Brihaye, Thomas and Randour, Mickael and Rivi{\`{e}}re, C{\'{e}}dric and Vandenhove, Pierre}, title = {Decisiveness of stochastic systems and its application to hybrid models}, journal = {Information and Computation}, volume = {289}, number = {Part}, pages = {104861}, year = {2022}, url = {https://doi.org/10.1016/j.ic.2021.104861}, doi = {10.1016/J.IC.2021.104861}, timestamp = {Sun, 12 Feb 2023 00:00:00 +0100}, biburl = {https://dblp.org/rec/journals/iandc/BouyerBRRV22.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
LMCS
Games Where You Can Play Optimally with Arena-Independent Finite Memory

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

Logical Methods in Computer Science, 2022

Abs arXiv Bib

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).
@article{DBLP:journals/lmcs/BouyerRORV22, author = {Bouyer, Patricia and Roux, Stéphane Le and Oualhadj, Youssouf and Randour, Mickael and Vandenhove, Pierre}, title = {Games Where You Can Play Optimally with Arena-Independent Finite Memory}, journal = {Logical Methods in Computer Science}, volume = {18}, number = {1}, year = {2022}, url = {https://doi.org/10.46298/lmcs-18(1:11)2022}, doi = {10.46298/LMCS-18(1:11)2022}, timestamp = {Tue, 31 Jan 2023 00:00:00 +0100}, biburl = {https://dblp.org/rec/journals/lmcs/BouyerRORV22.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }

2020

LMCS
Life is Random, Time is Not: Markov Decision Processes with Window Objectives

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

Logical Methods in Computer Science, 2020

Abs arXiv Bib

The window mechanism was introduced by Chatterjee et al. 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 because it enables reasoning about such time bounds in system specifications, but also thanks to the increased tractability that it usually yields. In this work, we extend the window framework to stochastic environments by considering Markov decision processes. A fundamental problem in this context is the threshold probability problem: given an objective it aims to synthesize strategies that guarantee satisfying runs with a given probability. We solve it 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.
@article{DBLP:journals/lmcs/BrihayeDOR20, 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}, journal = {Logical Methods in Computer Science}, volume = {16}, number = {4}, year = {2020}, url = {https://lmcs.episciences.org/6975}, timestamp = {Wed, 16 Dec 2020 00:00:00 +0100}, biburl = {https://dblp.org/rec/journals/lmcs/BrihayeDOR20.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }

2018

Acta Informatica
Average-energy games

Patricia Bouyer, Nicolas Markey, Mickael Randour, Kim G. Larsen, and Simon Laursen

Acta Informatica, 2018

Abs arXiv Bib

Two-player quantitative zero-sum games provide a natural framework to synthesize controllers with performance guarantees for reactive systems within an uncontrollable environment. Classical settings include mean-payoff games, where the objective is to optimize the long-run average gain per action, and energy games, where the system has to avoid running out of energy. We study average-energy games, where the goal is to optimize the long-run average of the accumulated energy. We show that this objective arises naturally in several applications, and that it yields interesting connections with previous concepts in the literature. We prove that deciding the winner in such games is in NP ∩ coNP and at least as hard as solving mean-payoff games, and we establish that memoryless strategies suffice to win. We also consider the case where the system has to minimize the average-energy while maintaining the accumulated energy within predefined bounds at all times: this corresponds to operating with a finite-capacity storage for energy. We give results for one-player and two-player games, and establish complexity bounds and memory requirements.
@article{DBLP:journals/acta/BouyerMRLL18, author = {Bouyer, Patricia and Markey, Nicolas and Randour, Mickael and Larsen, Kim G. and Laursen, Simon}, title = {Average-energy games}, journal = {Acta Informatica}, volume = {55}, number = {2}, pages = {91--127}, year = {2018}, url = {https://doi.org/10.1007/s00236-016-0274-1}, doi = {10.1007/S00236-016-0274-1}, timestamp = {Tue, 07 May 2024 01:00:00 +0200}, biburl = {https://dblp.org/rec/journals/acta/BouyerMRLL18.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }

2017

FMSD
Percentile queries in multi-dimensional Markov decision processes

Mickael Randour, Jean-François Raskin, and Ocan Sankur

Formal Methods in System Design, 2017

Abs arXiv Bib

Markov decision processes (MDPs) with multi-dimensional weights are useful to analyze systems with multiple objectives that may be conflicting and require the analysis of trade-offs. We study the complexity of percentile queries in such MDPs and give algorithms to synthesize strategies that enforce such constraints. Given a multi-dimensional weighted MDP and a quantitative payoff function f, thresholds v_i (one per dimension), and probability thresholds α_i, we show how to compute a single strategy to enforce that for all dimensions i, the probability of outcomes ρ satisfying f_i(ρ)≥v_i is at least α_i. We consider classical quantitative payoffs from the literature (sup, inf, lim sup, lim inf, mean-payoff, truncated sum, discounted sum). Our work extends to the quantitative case the multi-objective model checking problem studied by Etessami et al. in unweighted MDPs.
@article{DBLP:journals/fmsd/RandourRS17, author = {Randour, Mickael and Raskin, Jean{-}Fran{\c{c}}ois and Sankur, Ocan}, title = {Percentile queries in multi-dimensional Markov decision processes}, journal = {Formal Methods in System Design}, volume = {50}, number = {2-3}, pages = {207--248}, year = {2017}, url = {https://doi.org/10.1007/s10703-016-0262-7}, doi = {10.1007/S10703-016-0262-7}, timestamp = {Fri, 13 Mar 2020 00:00:00 +0100}, biburl = {https://dblp.org/rec/journals/fmsd/RandourRS17.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
Inf. Comput.
Meet your expectations with guarantees: Beyond worst-case synthesis in quantitative games

Véronique Bruyère, Emmanuel Filiot, Mickael Randour, and Jean-François Raskin

Information and Computation, 2017

Abs arXiv Bib

We extend the quantitative synthesis framework by going beyond the worst-case. On the one hand, classical analysis of two-player games involves an adversary (modeling the environment of the system) which is purely antagonistic and asks for strict guarantees. On the other hand, stochastic models like Markov decision processes represent situations where the system is faced to a purely randomized environment: the aim is then to optimize the expected payoff, with no guarantee on individual outcomes. We introduce the beyond worst-case synthesis problem, which is to construct strategies that guarantee some quantitative requirement in the worst-case while providing an higher expected value against a particular stochastic model of the environment given as input. This problem is relevant to produce system controllers that provide nice expected performance in the everyday situation while ensuring a strict (but relaxed) performance threshold even in the event of very bad (while unlikely) circumstances. We study the beyond worst-case synthesis problem for two important quantitative settings: the mean-payoff and the shortest path. In both cases, we show how to decide the existence of finite-memory strategies satisfying the problem and how to synthesize one if one exists. We establish algorithms and we study complexity bounds and memory requirements.
@article{DBLP:journals/iandc/BruyereFRR17, author = {Bruyère, Véronique and Filiot, Emmanuel and Randour, Mickael and Raskin, Jean{-}Fran{\c{c}}ois}, title = {Meet your expectations with guarantees: Beyond worst-case synthesis in quantitative games}, journal = {Information and Computation}, volume = {254}, pages = {259--295}, year = {2017}, url = {https://doi.org/10.1016/j.ic.2016.10.011}, doi = {10.1016/J.IC.2016.10.011}, timestamp = {Sat, 05 Sep 2020 01:00:00 +0200}, biburl = {https://dblp.org/rec/journals/iandc/BruyereFRR17.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }

2015

Inf. Comput.
Looking at mean-payoff and total-payoff through windows

Krishnendu Chatterjee, Laurent Doyen, Mickael Randour, and Jean-François Raskin

Information and Computation, 2015

Abs arXiv Bib

We consider two-player games played on weighted directed graphs with mean-payoff and total-payoff objectives, two classical quantitative objectives. While for single-dimensional games the complexity and memory bounds for both objectives coincide, we show that in contrast to multi-dimensional mean-payoff games that are known to be coNP-complete, multi-dimensional total-payoff games are undecidable. We introduce conservative approximations of these objectives, where the payoff is considered over a local finite window sliding along a play, instead of the whole play. For single dimension, we show that (i) if the window size is polynomial, deciding the winner takes polynomial time, and (ii) the existence of a bounded window can be decided in NP ∩ coNP, and is at least as hard as solving mean-payoff games. For multiple dimensions, we show that (i) the problem with fixed window size is EXPTIME-complete, and (ii) there is no primitive-recursive algorithm to decide the existence of a bounded window.
@article{DBLP:journals/iandc/Chatterjee0RR15, author = {Chatterjee, Krishnendu and Doyen, Laurent and Randour, Mickael and Raskin, Jean{-}Fran{\c{c}}ois}, title = {Looking at mean-payoff and total-payoff through windows}, journal = {Information and Computation}, volume = {242}, pages = {25--52}, year = {2015}, url = {https://doi.org/10.1016/j.ic.2015.03.010}, doi = {10.1016/J.IC.2015.03.010}, timestamp = {Fri, 12 Feb 2021 00:00:00 +0100}, biburl = {https://dblp.org/rec/journals/iandc/Chatterjee0RR15.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }

2014

Acta Informatica
Strategy synthesis for multi-dimensional quantitative objectives

Krishnendu Chatterjee, Mickael Randour, and Jean-François Raskin

Acta Informatica, 2014

Abs arXiv Bib

Multi-dimensional mean-payoff and energy games provide the mathematical foundation for the quantitative study of reactive systems, and play a central role in the emerging quantitative theory of verification and synthesis. In this work, we study the strategy synthesis problem for games with such multi-dimensional objectives along with a parity condition, a canonical way to express ω-regular conditions. While in general, the winning strategies in such games may require infinite memory, for synthesis the most relevant problem is the construction of a finite-memory winning strategy (if one exists). Our main contributions are as follows. First, we show a tight exponential bound (matching upper and lower bounds) on the memory required for finite-memory winning strategies in both multi-dimensional mean-payoff and energy games along with parity objectives. This significantly improves the triple exponential upper bound for multi energy games (without parity) that could be derived from results in literature for games on VASS (vector addition systems with states). Second, we present an optimal symbolic and incremental algorithm to compute a finite-memory winning strategy (if one exists) in such games. Finally, we give a complete characterization of when finite memory of strategies can be traded off for randomness. In particular, we show that for one-dimension mean-payoff parity games, randomized memoryless strategies are as powerful as their pure finite-memory counterparts.
@article{DBLP:journals/acta/ChatterjeeRR14, author = {Chatterjee, Krishnendu and Randour, Mickael and Raskin, Jean{-}Fran{\c{c}}ois}, title = {Strategy synthesis for multi-dimensional quantitative objectives}, journal = {Acta Informatica}, volume = {51}, number = {3-4}, pages = {129--163}, year = {2014}, url = {https://doi.org/10.1007/s00236-013-0182-6}, doi = {10.1007/S00236-013-0182-6}, timestamp = {Sun, 21 Jun 2020 01:00:00 +0200}, biburl = {https://dblp.org/rec/journals/acta/ChatterjeeRR14.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }

International peer-reviewed conferences

2023

FSTTCS

Reachability Games and Friends: A Journey Through the Lens of Memory and Complexity

Thomas Brihaye, Aline Goeminne, James C. A. Main, and Mickael Randour

In 43rd IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, FSTTCS 2023, December 18-20, 2023, IIIT Hyderabad, Telangana, India , 2023

Invited paper Abs Bib PDF

Keynote lecture at FSTTCS’23.

Reachability objectives are arguably the most basic ones in the theory of games on graphs (and beyond). But far from being bland, they constitute the cornerstone of this field. Reachability is everywhere, as are the tools we use to reason about it. In this invited contribution, we take the reader on a journey through a zoo of models that have reachability objectives at their core. Our goal is to illustrate how model complexity impacts the complexity of strategies needed to play optimally in the corresponding games and computational complexity.

@inproceedings{DBLP:conf/fsttcs/BrihayeGMR23,
  author = {Brihaye, Thomas and Goeminne, Aline and Main, James C. A. and Randour, Mickael},
  editor = {Bouyer, Patricia and Srinivasan, Srikanth},
  title = {Reachability Games and Friends: {A} Journey Through the Lens of Memory
                    and Complexity},
  booktitle = {43rd {IARCS} Annual Conference on Foundations of Software Technology
                    and Theoretical Computer Science, {FSTTCS} 2023, December 18-20, 2023,
                    {IIIT} Hyderabad, Telangana, India},
  series = {LIPIcs},
  volume = {284},
  pages = {1:1--1:26},
  publisher = {Schloss Dagstuhl - Leibniz-Zentrum f{\"{u}}r Informatik},
  year = {2023},
  url = {https://doi.org/10.4230/LIPIcs.FSTTCS.2023.1},
  doi = {10.4230/LIPICS.FSTTCS.2023.1},
  timestamp = {Wed, 13 Dec 2023 14:08:06 +0100},
  biburl = {https://dblp.org/rec/conf/fsttcs/BrihayeGMR23.bib},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}

ICALP
How to Play Optimally for Regular Objectives?

Patricia Bouyer, Nathanaël Fijalkow, Mickael Randour, and Pierre Vandenhove

In 50th International Colloquium on Automata, Languages, and Programming, ICALP 2023, July 10-14, 2023, Paderborn, Germany , 2023

Abs arXiv Bib

This paper studies two-player zero-sum games played on graphs and makes contributions toward the following question: given an objective, how much memory is required to play optimally for that objective? We study regular objectives, where the goal of one of the two players is that eventually the sequence of colors along the play belongs to some regular language of finite words. We obtain different characterizations of the chromatic memory requirements for such objectives for both players, from which we derive complexity-theoretic statements: deciding whether there exist small memory structures sufficient to play optimally is NP-complete for both players. Some of our characterization results apply to a more general class of objectives: topologically closed and topologically open sets.
@inproceedings{DBLP:conf/icalp/BouyerFRV23, author = {Bouyer, Patricia and Fijalkow, Nathana{\"{e}}l and Randour, Mickael and Vandenhove, Pierre}, editor = {Etessami, Kousha and Feige, Uriel and Puppis, Gabriele}, title = {How to Play Optimally for Regular Objectives?}, booktitle = {50th International Colloquium on Automata, Languages, and Programming, {ICALP} 2023, July 10-14, 2023, Paderborn, Germany}, series = {LIPIcs}, volume = {261}, pages = {118:1--118:18}, publisher = {Schloss Dagstuhl - Leibniz-Zentrum f{\"{u}}r Informatik}, year = {2023}, url = {https://doi.org/10.4230/LIPIcs.ICALP.2023.118}, doi = {10.4230/LIPICS.ICALP.2023.118}, timestamp = {Sat, 30 Sep 2023 01:00:00 +0200}, biburl = {https://dblp.org/rec/conf/icalp/BouyerFRV23.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
IJCAI
Half-Positional Objectives Recognized by Deterministic Büchi Automata (Extended Abstract)

Patricia Bouyer, Antonio Casares, Mickael Randour, and Pierre Vandenhove

In Proceedings of the Thirty-Second International Joint Conference on Artificial Intelligence, IJCAI 2023, 19th-25th August 2023, Macao, SAR, China , 2023

Invited paper Abs Bib PDF

IJCAI’23 – Sister Conferences Best Papers Track.

In two-player zero-sum games on graphs, the protagonist tries to achieve an objective while the antagonist aims to prevent it. Objectives for which both players do not need to use memory to play optimally are well-understood and characterized both in finite and infinite graphs. Less is known about the larger class of half-positional objectives, i.e., those for which the protagonist does not need memory (but for which the antagonist might). In particular, no characterization of half-positionality is known for the central class of ω-regular objectives. Here, we characterize objectives recognizable by deterministic Büchi automata (a class of ω-regular objectives) that are half-positional, both over finite and infinite graphs. This characterization yields a polynomial-time algorithm to decide half-positionality of an objective recognized by a given deterministic Büchi automaton.
@inproceedings{DBLP:conf/ijcai/BouyerCRV23, author = {Bouyer, Patricia and Casares, Antonio and Randour, Mickael and Vandenhove, Pierre}, title = {Half-Positional Objectives Recognized by Deterministic B{\"{u}}chi Automata (Extended Abstract)}, booktitle = {Proceedings of the Thirty-Second International Joint Conference on Artificial Intelligence, {IJCAI} 2023, 19th-25th August 2023, Macao, SAR, China}, pages = {6420--6425}, publisher = {ijcai.org}, year = {2023}, url = {https://doi.org/10.24963/ijcai.2023/713}, doi = {10.24963/IJCAI.2023/713}, timestamp = {Mon, 28 Aug 2023 17:23:07 +0200}, biburl = {https://dblp.org/rec/conf/ijcai/BouyerCRV23.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }

2022

CONCUR
Half-Positional Objectives Recognized by Deterministic Büchi Automata

Patricia Bouyer, Antonio Casares, Mickael Randour, and Pierre Vandenhove

In 33rd International Conference on Concurrency Theory, CONCUR 2022, September 12-16, 2022, Warsaw, Poland , 2022

Abs arXiv Bib

In two-player games on graphs, the simplest possible strategies are those that can be implemented without any memory. These are called positional strategies. In this paper, we characterize objectives recognizable by deterministic Büchi automata (a subclass of omega-regular objectives) that are half-positional, that is, for which the protagonist can always play optimally using positional strategies (both over finite and infinite graphs). Our characterization consists of three natural conditions linked to the language-theoretic notion of right congruence. Furthermore, this characterization yields a polynomial-time algorithm to decide half-positionality of an objective recognized by a given deterministic Büchi automaton.
@inproceedings{DBLP:conf/concur/BouyerCRV22, author = {Bouyer, Patricia and Casares, Antonio and Randour, Mickael and Vandenhove, Pierre}, editor = {Klin, Bartek and Lasota, Slawomir and Muscholl, Anca}, title = {Half-Positional Objectives Recognized by Deterministic B{\"{u}}chi Automata}, booktitle = {33rd International Conference on Concurrency Theory, {CONCUR} 2022, September 12-16, 2022, Warsaw, Poland}, series = {LIPIcs}, volume = {243}, pages = {20:1--20:18}, publisher = {Schloss Dagstuhl - Leibniz-Zentrum f{\"{u}}r Informatik}, year = {2022}, url = {https://doi.org/10.4230/LIPIcs.CONCUR.2022.20}, doi = {10.4230/LIPICS.CONCUR.2022.20}, timestamp = {Sun, 12 Feb 2023 00:00:00 +0100}, biburl = {https://dblp.org/rec/conf/concur/BouyerCRV22.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
CONCUR
Different Strokes in Randomised Strategies: Revisiting Kuhn’s Theorem Under Finite-Memory Assumptions

James C. A. Main, and Mickael Randour

In 33rd International Conference on Concurrency Theory, CONCUR 2022, September 12-16, 2022, Warsaw, Poland , 2022

Abs arXiv Bib

Two-player (antagonistic) games on (possibly stochastic) graphs are a prevalent model in theoretical computer science, notably as a framework for reactive synthesis. Optimal strategies may require randomisation when dealing with inherently probabilistic goals, balancing multiple objectives, or in contexts of partial information. There is no unique way to define randomised strategies. For instance, one can use so-called mixed strategies or behavioural ones. In the most general settings, these two classes do not share the same expressiveness. A seminal result in game theory - Kuhn’s theorem - asserts their equivalence in games of perfect recall. This result crucially relies on the possibility for strategies to use infinite memory, i.e., unlimited knowledge of all past observations. However, computer systems are finite in practice. Hence it is pertinent to restrict our attention to finite-memory strategies, defined as automata with outputs. Randomisation can be implemented in these in different ways: the initialisation, outputs or transitions can be randomised or deterministic respectively. Depending on which aspects are randomised, the expressiveness of the corresponding class of finite-memory strategies differs. In this work, we study two-player turn-based stochastic games and provide a complete taxonomy of the classes of finite-memory strategies obtained by varying which of the three aforementioned components are randomised. Our taxonomy holds both in settings of perfect and imperfect information, and in games with more than two players.
@inproceedings{DBLP:conf/concur/MainR22, author = {Main, James C. A. and Randour, Mickael}, editor = {Klin, Bartek and Lasota, Slawomir and Muscholl, Anca}, title = {Different Strokes in Randomised Strategies: Revisiting Kuhn's Theorem Under Finite-Memory Assumptions}, booktitle = {33rd International Conference on Concurrency Theory, {CONCUR} 2022, September 12-16, 2022, Warsaw, Poland}, series = {LIPIcs}, volume = {243}, pages = {22:1--22:18}, publisher = {Schloss Dagstuhl - Leibniz-Zentrum f{\"{u}}r Informatik}, year = {2022}, url = {https://doi.org/10.4230/LIPIcs.CONCUR.2022.22}, doi = {10.4230/LIPICS.CONCUR.2022.22}, timestamp = {Mon, 26 Sep 2022 01:00:00 +0200}, biburl = {https://dblp.org/rec/conf/concur/MainR22.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
FORMATS
Timed Games with Bounded Window Parity Objectives

James C. A. Main, Mickael Randour, and Jeremy Sproston

In Formal Modeling and Analysis of Timed Systems - 20th International Conference, FORMATS 2022, Warsaw, Poland, September 13-15, 2022, Proceedings , 2022

Abs arXiv Bib

The window mechanism, introduced by Chatterjee et al. for mean-payoff and total-payoff objectives in two-player turn-based games on graphs, refines long-term objectives with time bounds. This mechanism has proven useful in a variety of settings, and most recently in timed systems. In the timed setting, the so-called fixed timed window parity objectives have been studied. A fixed timed window parity objective is defined with respect to some time bound and requires that, at all times, we witness a time frame, i.e., a window, of size less than the fixed bound in which the smallest priority is even. In this work, we focus on the bounded timed window parity objective. Such an objective is satisfied if there exists some bound for which the fixed objective is satisfied. The satisfaction of bounded objectives is robust to modeling choices such as constants appearing in constraints, unlike fixed objectives, for which the choice of constants may affect the satisfaction for a given bound. We show that verification of bounded timed window objectives in timed automata can be performed in polynomial space, and that timed games with these objectives can be solved in exponential time, even for multi-objective extensions. This matches the complexity classes of the fixed case. We also provide a comparison of the different variants of window parity objectives.
@inproceedings{DBLP:conf/formats/MainRS22, author = {Main, James C. A. and Randour, Mickael and Sproston, Jeremy}, editor = {Bogomolov, Sergiy and Parker, David}, title = {Timed Games with Bounded Window Parity Objectives}, booktitle = {Formal Modeling and Analysis of Timed Systems - 20th International Conference, {FORMATS} 2022, Warsaw, Poland, September 13-15, 2022, Proceedings}, series = {Lecture Notes in Computer Science}, volume = {13465}, pages = {165--182}, publisher = {Springer}, year = {2022}, url = {https://doi.org/10.1007/978-3-031-15839-1\_10}, doi = {10.1007/978-3-031-15839-1\_10}, timestamp = {Mon, 24 Oct 2022 20:51:03 +0200}, biburl = {https://dblp.org/rec/conf/formats/MainRS22.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
FSTTCS
The True Colors of Memory: A Tour of Chromatic-Memory Strategies in Zero-Sum Games on Graphs (Invited Talk)

Patricia Bouyer, Mickael Randour, and Pierre Vandenhove

In 42nd IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, FSTTCS 2022, December 18-20, 2022, IIT Madras, Chennai, India , 2022

Invited paper Abs Bib PDF

Keynote lecture at FSTTCS’22.

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
@inproceedings{DBLP:conf/fsttcs/BouyerRV22, author = {Bouyer, Patricia and Randour, Mickael and Vandenhove, Pierre}, editor = {Dawar, Anuj and Guruswami, Venkatesan}, title = {The True Colors of Memory: {A} Tour of Chromatic-Memory Strategies in Zero-Sum Games on Graphs (Invited Talk)}, booktitle = {42nd {IARCS} Annual Conference on Foundations of Software Technology and Theoretical Computer Science, {FSTTCS} 2022, December 18-20, 2022, {IIT} Madras, Chennai, India}, series = {LIPIcs}, volume = {250}, pages = {3:1--3:18}, publisher = {Schloss Dagstuhl - Leibniz-Zentrum f{\"{u}}r Informatik}, year = {2022}, url = {https://doi.org/10.4230/LIPIcs.FSTTCS.2022.3}, doi = {10.4230/LIPICS.FSTTCS.2022.3}, timestamp = {Tue, 21 Mar 2023 00:00:00 +0100}, biburl = {https://dblp.org/rec/conf/fsttcs/BouyerRV22.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
STACS
Characterizing Omega-Regularity Through Finite-Memory Determinacy of Games on Infinite Graphs

Patricia Bouyer, Mickael Randour, and Pierre Vandenhove

In 39th International Symposium on Theoretical Aspects of Computer Science, STACS 2022, March 15-18, 2022, Marseille, France (Virtual Conference) , 2022

Abs arXiv Bib

We consider zero-sum games on infinite graphs, with objectives specified as sets of infinite words over some alphabet of colors. A well-studied class of objectives is the one of ω-regular objectives, due to its relation to many natural problems in theoretical computer science. We focus on the strategy complexity question: given an objective, how much memory does each player require to play as well as possible? A classical result is that finite-memory strategies suffice for both players when the objective is ω-regular. We show a reciprocal of that statement: when both players can play optimally with a chromatic finite-memory structure (i.e., whose updates can only observe colors) in all infinite game graphs, then the objective must be ω-regular. This provides a game-theoretic characterization of ω-regular objectives, and this characterization can help in obtaining memory bounds. Moreover, a by-product of our characterization is a new one-to-two-player lift: to show that chromatic finite-memory structures suffice to play optimally in two-player games on infinite graphs, it suffices to show it in the simpler case of one-player games on infinite graphs. We illustrate our results with the family of discounted-sum objectives, for which ω-regularity depends on the value of some parameters.
@inproceedings{DBLP:conf/stacs/BouyerRV22, author = {Bouyer, Patricia and Randour, Mickael and Vandenhove, Pierre}, editor = {Berenbrink, Petra and Monmege, Benjamin}, title = {Characterizing Omega-Regularity Through Finite-Memory Determinacy of Games on Infinite Graphs}, booktitle = {39th International Symposium on Theoretical Aspects of Computer Science, {STACS} 2022, March 15-18, 2022, Marseille, France (Virtual Conference)}, series = {LIPIcs}, volume = {219}, pages = {16:1--16:16}, publisher = {Schloss Dagstuhl - Leibniz-Zentrum f{\"{u}}r Informatik}, year = {2022}, url = {https://doi.org/10.4230/LIPIcs.STACS.2022.16}, doi = {10.4230/LIPICS.STACS.2022.16}, timestamp = {Sun, 12 Feb 2023 00:00:00 +0100}, biburl = {https://dblp.org/rec/conf/stacs/BouyerRV22.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }

2021

CONCUR
Time Flies When Looking out of the Window: Timed Games with Window Parity Objectives

James C. A. Main, Mickael Randour, and Jeremy Sproston

In 32nd International Conference on Concurrency Theory, CONCUR 2021, August 24-27, 2021, Virtual Conference , 2021

Abs arXiv Bib

The window mechanism was introduced by Chatterjee et al. to reinforce mean-payoff and total-payoff objectives with time bounds in two-player turn-based games on graphs. It has since proved useful in a variety of settings, including parity objectives in games and both mean-payoff and parity objectives in Markov decision processes. We study window parity objectives in timed automata and timed games: given a bound on the window size, a path satisfies such an objective if, in all states along the path, we see a sufficiently small window in which the smallest priority is even. We show that checking that all time-divergent paths of a timed automaton satisfy such a window parity objective can be done in polynomial space, and that the corresponding timed games can be solved in exponential time. This matches the complexity class of timed parity games, while adding the ability to reason about time bounds. We also consider multi-dimensional objectives and show that the complexity class does not increase. To the best of our knowledge, this is the first study of the window mechanism in a real-time setting.
@inproceedings{DBLP:conf/concur/MainRS21, author = {Main, James C. A. and Randour, Mickael and Sproston, Jeremy}, editor = {Haddad, Serge and Varacca, Daniele}, title = {Time Flies When Looking out of the Window: Timed Games with Window Parity Objectives}, booktitle = {32nd International Conference on Concurrency Theory, {CONCUR} 2021, August 24-27, 2021, Virtual Conference}, series = {LIPIcs}, volume = {203}, pages = {25:1--25:16}, publisher = {Schloss Dagstuhl - Leibniz-Zentrum f{\"{u}}r Informatik}, year = {2021}, url = {https://doi.org/10.4230/LIPIcs.CONCUR.2021.25}, doi = {10.4230/LIPICS.CONCUR.2021.25}, timestamp = {Fri, 13 Aug 2021 16:29:32 +0200}, biburl = {https://dblp.org/rec/conf/concur/MainRS21.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
CONCUR
Arena-Independent Finite-Memory Determinacy in Stochastic Games

Patricia Bouyer, Youssouf Oualhadj, Mickael Randour, and Pierre Vandenhove

In 32nd International Conference on Concurrency Theory, CONCUR 2021, August 24-27, 2021, Virtual Conference , 2021

Abs arXiv Bib

We study stochastic zero-sum games on graphs, which are prevalent tools to model decision-making in presence of an antagonistic opponent in a random environment. In this setting, an important question is the one of strategy complexity: what kinds of strategies are sufficient or required to play optimally (e.g., randomization or memory requirements)? Our contributions further the understanding of arena-independent finite-memory (AIFM) determinacy, i.e., the study of objectives for which memory is needed, but in a way that only depends on limited parameters of the game graphs. First, we show that objectives for which pure AIFM strategies suffice to play optimally also admit pure AIFM subgame perfect strategies. Second, we show that we can reduce the study of objectives for which pure AIFM strategies suffice in two-player stochastic games to the easier study of one-player stochastic games (i.e., Markov decision processes). Third, we characterize the sufficiency of AIFM strategies through two intuitive properties of objectives. This work extends a line of research started on deterministic games to stochastic ones.
@inproceedings{DBLP:conf/concur/BouyerORV21, author = {Bouyer, Patricia and Oualhadj, Youssouf and Randour, Mickael and Vandenhove, Pierre}, editor = {Haddad, Serge and Varacca, Daniele}, title = {Arena-Independent Finite-Memory Determinacy in Stochastic Games}, booktitle = {32nd International Conference on Concurrency Theory, {CONCUR} 2021, August 24-27, 2021, Virtual Conference}, series = {LIPIcs}, volume = {203}, pages = {26:1--26:18}, publisher = {Schloss Dagstuhl - Leibniz-Zentrum f{\"{u}}r Informatik}, year = {2021}, url = {https://doi.org/10.4230/LIPIcs.CONCUR.2021.26}, doi = {10.4230/LIPICS.CONCUR.2021.26}, timestamp = {Sun, 12 Feb 2023 00:00:00 +0100}, biburl = {https://dblp.org/rec/conf/concur/BouyerORV21.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }

2020

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

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

In 31st International Conference on Concurrency Theory, CONCUR 2020, September 1-4, 2020, Vienna, Austria (Virtual Conference) , 2020

Abs arXiv Bib

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).
@inproceedings{DBLP:conf/concur/Bouyer0ORV20, author = {Bouyer, Patricia and Roux, St{\'{e}}phane Le and Oualhadj, Youssouf and Randour, Mickael and Vandenhove, Pierre}, editor = {Konnov, Igor and Kov{\'{a}}cs, Laura}, title = {Games Where You Can Play Optimally with Arena-Independent Finite Memory}, booktitle = {31st International Conference on Concurrency Theory, {CONCUR} 2020, September 1-4, 2020, Vienna, Austria (Virtual Conference)}, series = {LIPIcs}, volume = {171}, pages = {24:1--24:22}, publisher = {Schloss Dagstuhl - Leibniz-Zentrum f{\"{u}}r Informatik}, year = {2020}, url = {https://doi.org/10.4230/LIPIcs.CONCUR.2020.24}, doi = {10.4230/LIPICS.CONCUR.2020.24}, timestamp = {Mon, 21 Dec 2020 13:23:22 +0100}, biburl = {https://dblp.org/rec/conf/concur/Bouyer0ORV20.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
TACAS
Simple Strategies in Multi-Objective MDPs

Florent Delgrange, Joost-Pieter Katoen, Tim Quatmann, and Mickael Randour

In Tools and Algorithms for the Construction and Analysis of Systems - 26th International Conference, TACAS 2020, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2020, Dublin, Ireland, April 25-30, 2020, Proceedings, Part I , 2020

Abs arXiv Bib

We consider the verification of multiple expected reward objectives at once on Markov decision processes (MDPs). This enables a trade-off analysis among multiple objectives by obtaining the Pareto front. We focus on strategies that are easy to employ and implement. That is, strategies that are pure (no randomization) and have bounded memory. We show that checking whether a point is achievable by a pure stationary strategy is NP-complete, even for two objectives, and we provide an MILP encoding to solve the corresponding problem. The bounded memory case can be reduced to the stationary one by a product construction. Experimental results using Storm and Gurobi show the feasibility of our algorithms.
@inproceedings{DBLP:conf/tacas/DelgrangeKQR20, author = {Delgrange, Florent and Katoen, Joost{-}Pieter and Quatmann, Tim and Randour, Mickael}, editor = {Biere, Armin and Parker, David}, title = {Simple Strategies in Multi-Objective MDPs}, booktitle = {Tools and Algorithms for the Construction and Analysis of Systems - 26th International Conference, {TACAS} 2020, Held as Part of the European Joint Conferences on Theory and Practice of Software, {ETAPS} 2020, Dublin, Ireland, April 25-30, 2020, Proceedings, Part {I}}, series = {Lecture Notes in Computer Science}, volume = {12078}, pages = {346--364}, publisher = {Springer}, year = {2020}, url = {https://doi.org/10.1007/978-3-030-45190-5\_19}, doi = {10.1007/978-3-030-45190-5\_19}, timestamp = {Fri, 14 May 2021 08:34:17 +0200}, biburl = {https://dblp.org/rec/conf/tacas/DelgrangeKQR20.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
GandALF
Decisiveness of Stochastic Systems and its Application to Hybrid Models

Patricia Bouyer, Thomas Brihaye, Mickael Randour, Cédric Rivière, and Pierre Vandenhove

In Proceedings 11th International Symposium on Games, Automata, Logics, and Formal Verification, GandALF 2020, Brussels, Belgium, September 21-22, 2020 , 2020

Abs arXiv Bib

In [ABM07], Abdulla et al. introduced the concept of decisiveness, an interesting tool for lifting good properties of finite Markov chains to denumerable ones. Later, this concept was extended to more general stochastic transition systems (STSs), allowing the design of various verification algorithms for large classes of (infinite) STSs. We further improve the understanding and utility of decisiveness in two ways. First, we provide a general criterion for proving decisiveness of general STSs. This criterion, which is very natural but whose proof is rather technical, (strictly) generalizes all known criteria from the literature. Second, we focus on stochastic hybrid systems (SHSs), a stochastic extension of hybrid systems. We establish the decisiveness of a large class of SHSs and, under a few classical hypotheses from mathematical logic, we show how to decide reachability problems in this class, even though they are undecidable for general SHSs. This provides a decidable stochastic extension of o-minimal hybrid systems. [ABM07] Parosh A. Abdulla, Noomene Ben Henda, and Richard Mayr. 2007. Decisive Markov Chains. Log. Methods Comput. Sci. 3, 4 (2007).
@inproceedings{DBLP:journals/corr/abs-2001-04347, author = {Bouyer, Patricia and Brihaye, Thomas and Randour, Mickael and Rivi{\`{e}}re, C{\'{e}}dric and Vandenhove, Pierre}, editor = {Raskin, Jean{-}Fran{\c{c}}ois and Bresolin, Davide}, title = {Decisiveness of Stochastic Systems and its Application to Hybrid Models}, booktitle = {Proceedings 11th International Symposium on Games, Automata, Logics, and Formal Verification, GandALF 2020, Brussels, Belgium, September 21-22, 2020}, series = {{EPTCS}}, volume = {326}, pages = {149--165}, year = {2020}, url = {https://doi.org/10.4204/EPTCS.326.10}, doi = {10.4204/EPTCS.326.10}, timestamp = {Sun, 12 Feb 2023 00:00:00 +0100}, biburl = {https://dblp.org/rec/journals/corr/abs-2001-04347.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }

2019

CONCUR
Life Is Random, Time Is Not: Markov Decision Processes with Window Objectives

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

In 30th International Conference on Concurrency Theory, CONCUR 2019, August 27-30, 2019, Amsterdam, the Netherlands , 2019

Best paper Abs arXiv Bib

Best paper award at CONCUR 2019.

The window mechanism was introduced by Chatterjee et al. 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 because it enables reasoning about such time bounds in system specifications, but also thanks to the increased tractability that it usually yields. In this work, we extend the window framework to stochastic environments by considering Markov decision processes. A fundamental problem in this context is the threshold probability problem: given an objective it aims to synthesize strategies that guarantee satisfying runs with a given probability. We solve it 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.
@inproceedings{DBLP:conf/concur/BrihayeDOR19, author = {Brihaye, Thomas and Delgrange, Florent and Oualhadj, Youssouf and Randour, Mickael}, editor = {Fokkink, Wan J. and van Glabbeek, Rob}, title = {Life Is Random, Time Is Not: Markov Decision Processes with Window Objectives}, booktitle = {30th International Conference on Concurrency Theory, {CONCUR} 2019, August 27-30, 2019, Amsterdam, the Netherlands}, series = {LIPIcs}, volume = {140}, pages = {8:1--8:18}, publisher = {Schloss Dagstuhl - Leibniz-Zentrum f{\"{u}}r Informatik}, year = {2019}, url = {https://doi.org/10.4230/LIPIcs.CONCUR.2019.8}, doi = {10.4230/LIPICS.CONCUR.2019.8}, timestamp = {Sun, 02 Oct 2022 01:00:00 +0200}, biburl = {https://dblp.org/rec/conf/concur/BrihayeDOR19.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
CONCUR
Energy Mean-Payoff Games

Véronique Bruyère, Quentin Hautem, Mickael Randour, and Jean-François Raskin

In 30th International Conference on Concurrency Theory, CONCUR 2019, August 27-30, 2019, Amsterdam, the Netherlands , 2019

Abs arXiv Bib

In this paper, we study one-player and two-player energy mean-payoff games. Energy mean-payoff games are games of infinite duration played on a finite graph with edges labeled by 2-dimensional weight vectors. The objective of the first player (the protagonist) is to satisfy an energy objective on the first dimension and a mean-payoff objective on the second dimension. We show that optimal strategies for the first player may require infinite memory while optimal strategies for the second player (the antagonist) do not require memory. In the one-player case (where only the first player has choices), the problem of deciding who is the winner can be solved in polynomial time while for the two-player case we show co-NP membership and we give effective constructions for the infinite-memory optimal strategies of the protagonist.
@inproceedings{DBLP:conf/concur/BruyereHRR19, author = {Bruy{\`{e}}re, V{\'{e}}ronique and Hautem, Quentin and Randour, Mickael and Raskin, Jean{-}Fran{\c{c}}ois}, editor = {Fokkink, Wan J. and van Glabbeek, Rob}, title = {Energy Mean-Payoff Games}, booktitle = {30th International Conference on Concurrency Theory, {CONCUR} 2019, August 27-30, 2019, Amsterdam, the Netherlands}, series = {LIPIcs}, volume = {140}, pages = {21:1--21:17}, publisher = {Schloss Dagstuhl - Leibniz-Zentrum f{\"{u}}r Informatik}, year = {2019}, url = {https://doi.org/10.4230/LIPIcs.CONCUR.2019.21}, doi = {10.4230/LIPICS.CONCUR.2019.21}, timestamp = {Fri, 30 Aug 2019 01:00:00 +0200}, biburl = {https://dblp.org/rec/conf/concur/BruyereHRR19.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }

2018

FSTTCS
Extending Finite-Memory Determinacy by Boolean Combination of Winning Conditions

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

In 38th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, FSTTCS 2018, December 11-13, 2018, Ahmedabad, India , 2018

Abs arXiv Bib

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.
@inproceedings{DBLP:conf/fsttcs/0001PR18, author = {Roux, St{\'{e}}phane Le and Pauly, Arno and Randour, Mickael}, editor = {Ganguly, Sumit and Pandya, Paritosh K.}, 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, December 11-13, 2018, Ahmedabad, India}, series = {LIPIcs}, volume = {122}, pages = {38:1--38:20}, publisher = {Schloss Dagstuhl - Leibniz-Zentrum f{\"{u}}r Informatik}, year = {2018}, url = {https://doi.org/10.4230/LIPIcs.FSTTCS.2018.38}, doi = {10.4230/LIPICS.FSTTCS.2018.38}, timestamp = {Tue, 11 Feb 2020 15:52:14 +0100}, biburl = {https://dblp.org/rec/conf/fsttcs/0001PR18.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
GandALF
Multi-weighted Markov Decision Processes with Reachability Objectives

Patricia Bouyer, Mauricio González, Nicolas Markey, and Mickael Randour

In Proceedings Ninth International Symposium on Games, Automata, Logics, and Formal Verification, GandALF 2018, Saarbrücken, Germany, 26-28th September 2018 , 2018

Abs arXiv Bib

In this paper, we are interested in the synthesis of schedulers in double-weighted Markov decision processes, which satisfy both a percentile constraint over a weighted reachability condition, and a quantitative constraint on the expected value of a random variable defined using a weighted reachability condition. This problem is inspired by the modelization of an electric-vehicle charging problem. We study the cartography of the problem, when one parameter varies, and show how a partial cartography can be obtained via two sequences of opimization problems. We discuss completeness and feasability of the method.
@inproceedings{DBLP:journals/corr/abs-1809-03107, author = {Bouyer, Patricia and Gonz{\'{a}}lez, Mauricio and Markey, Nicolas and Randour, Mickael}, editor = {Orlandini, Andrea and Zimmermann, Martin}, title = {Multi-weighted Markov Decision Processes with Reachability Objectives}, booktitle = {Proceedings Ninth International Symposium on Games, Automata, Logics, and Formal Verification, GandALF 2018, Saarbr{\"{u}}cken, Germany, 26-28th September 2018}, series = {{EPTCS}}, volume = {277}, pages = {250--264}, year = {2018}, url = {https://doi.org/10.4204/EPTCS.277.18}, doi = {10.4204/EPTCS.277.18}, timestamp = {Wed, 07 Dec 2022 23:00:49 +0100}, biburl = {https://dblp.org/rec/journals/corr/abs-1809-03107.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }

2017

FoSSaCS
Bounding Average-Energy Games

Patricia Bouyer, Piotr Hofman, Nicolas Markey, Mickael Randour, and Martin Zimmermann

In Foundations of Software Science and Computation Structures - 20th International Conference, FoSSaCS 2017, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2017, Uppsala, Sweden, April 22-29, 2017, Proceedings , 2017

Abs arXiv Bib

We consider average-energy games, where the goal is to minimize the long-run average of the accumulated energy. While several results have been obtained on these games recently, decidability of average-energy games with a lower-bound constraint on the energy level (but no upper bound) remained open; in particular, so far there was no known upper bound on the memory that is required for winning strategies. By reducing average-energy games with lower-bounded energy to infinite-state mean-payoff games and analyzing the density of low-energy configurations, we show an almost tight doubly-exponential upper bound on the necessary memory, and that the winner of average-energy games with lower-bounded energy can be determined in doubly-exponential time. We also prove EXPSPACE-hardness of this problem. Finally, we consider multi-dimensional extensions of all types of average-energy games: without bounds, with only a lower bound, and with both a lower and an upper bound on the energy. We show that the fully-bounded version is the only case to remain decidable in multiple dimensions.
@inproceedings{DBLP:conf/fossacs/BouyerHMR017, author = {Bouyer, Patricia and Hofman, Piotr and Markey, Nicolas and Randour, Mickael and Zimmermann, Martin}, editor = {Esparza, Javier and Murawski, Andrzej S.}, title = {Bounding Average-Energy Games}, booktitle = {Foundations of Software Science and Computation Structures - 20th International Conference, {FoSSaCS} 2017, Held as Part of the European Joint Conferences on Theory and Practice of Software, {ETAPS} 2017, Uppsala, Sweden, April 22-29, 2017, Proceedings}, series = {Lecture Notes in Computer Science}, volume = {10203}, pages = {179--195}, year = {2017}, url = {https://doi.org/10.1007/978-3-662-54458-7\_11}, doi = {10.1007/978-3-662-54458-7\_11}, timestamp = {Tue, 14 May 2019 10:00:55 +0200}, biburl = {https://dblp.org/rec/conf/fossacs/BouyerHMR017.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
ICALP
Threshold Constraints with Guarantees for Parity Objectives in Markov Decision Processes

Raphaël Berthon, Mickael Randour, and Jean-François Raskin

In 44th International Colloquium on Automata, Languages, and Programming, ICALP 2017, July 10-14, 2017, Warsaw, Poland , 2017

Abs arXiv Bib

The beyond worst-case synthesis problem was introduced recently by Bruyère et al. [BFRR14]: it aims at building system controllers that provide strict worst-case performance guarantees against an antagonistic environment while ensuring higher expected performance against a stochastic model of the environment. Our work extends the framework of [BFRR14] and follow-up papers, which focused on quantitative objectives, by addressing the case of ω-regular conditions encoded as parity objectives, a natural way to represent functional requirements of systems. We build strategies that satisfy a main parity objective on all plays, while ensuring a secondary one with sufficient probability. This setting raises new challenges in comparison to quantitative objectives, as one cannot easily mix different strategies without endangering the functional properties of the system. We establish that, for all variants of this problem, deciding the existence of a strategy lies in NP∩coNP, the same complexity class as classical parity games. Hence, our framework provides additional modeling power while staying in the same complexity class. [BFRR14] Véronique Bruyère, Emmanuel Filiot, Mickael Randour, and Jean-François Raskin. Meet your expectations with guarantees: Beyond worst-case synthesis in quantitative games. In Ernst W. Mayr and Natacha Portier, editors, 31st International Symposium on Theoretical Aspects of Computer Science, STACS 2014, March 5-8, 2014, Lyon, France, volume 25 of LIPIcs, pages 199-213. Schloss Dagstuhl - Leibniz - Zentrum fuer Informatik, 2014.
@inproceedings{DBLP:conf/icalp/BerthonRR17, author = {Berthon, Rapha{\"{e}}l and Randour, Mickael and Raskin, Jean{-}Fran{\c{c}}ois}, editor = {Chatzigiannakis, Ioannis and Indyk, Piotr and Kuhn, Fabian and Muscholl, Anca}, title = {Threshold Constraints with Guarantees for Parity Objectives in Markov Decision Processes}, booktitle = {44th International Colloquium on Automata, Languages, and Programming, {ICALP} 2017, July 10-14, 2017, Warsaw, Poland}, series = {LIPIcs}, volume = {80}, pages = {121:1--121:15}, publisher = {Schloss Dagstuhl - Leibniz-Zentrum f{\"{u}}r Informatik}, year = {2017}, url = {https://doi.org/10.4230/LIPIcs.ICALP.2017.121}, doi = {10.4230/LIPICS.ICALP.2017.121}, timestamp = {Mon, 26 Jun 2023 01:00:00 +0200}, biburl = {https://dblp.org/rec/conf/icalp/BerthonRR17.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }

2016

ICALP
Reachability in Networks of Register Protocols under Stochastic Schedulers

Patricia Bouyer, Nicolas Markey, Mickael Randour, Arnaud Sangnier, and Daniel Stan

In 43rd International Colloquium on Automata, Languages, and Programming, ICALP 2016, July 11-15, 2016, Rome, Italy , 2016

Abs arXiv Bib

We study the almost-sure reachability problem in a distributed system obtained as the asynchronous composition of N copies (called processes) of the same automaton (called protocol), that can communicate via a shared register with finite domain. The automaton has two types of transitions: write-transitions update the value of the register, while read-transitions move to a new state depending on the content of the register. Non-determinism is resolved by a stochastic scheduler. Given a protocol, we focus on almost-sure reachability of a target state by one of the processes. The answer to this problem naturally depends on the number N of processes. However, we prove that our setting has a cut-off property: the answer to the almost-sure reachability problem is constant when N is large enough; we then develop an EXPSPACE algorithm deciding whether this constant answer is positive or negative.
@inproceedings{DBLP:conf/icalp/BouyerMRSS16, author = {Bouyer, Patricia and Markey, Nicolas and Randour, Mickael and Sangnier, Arnaud and Stan, Daniel}, editor = {Chatzigiannakis, Ioannis and Mitzenmacher, Michael and Rabani, Yuval and Sangiorgi, Davide}, title = {Reachability in Networks of Register Protocols under Stochastic Schedulers}, booktitle = {43rd International Colloquium on Automata, Languages, and Programming, {ICALP} 2016, July 11-15, 2016, Rome, Italy}, series = {LIPIcs}, volume = {55}, pages = {106:1--106:14}, publisher = {Schloss Dagstuhl - Leibniz-Zentrum f{\"{u}}r Informatik}, year = {2016}, url = {https://doi.org/10.4230/LIPIcs.ICALP.2016.106}, doi = {10.4230/LIPICS.ICALP.2016.106}, timestamp = {Thu, 14 Oct 2021 01:00:00 +0200}, biburl = {https://dblp.org/rec/conf/icalp/BouyerMRSS16.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }

LATA

Non-Zero Sum Games for Reactive Synthesis

Romain Brenguier, Lorenzo Clemente, Paul Hunter, Guillermo A. Pérez, Mickael Randour, Jean-François Raskin, Ocan Sankur, and Mathieu Sassolas

In Language and Automata Theory and Applications - 10th International Conference, LATA 2016, Prague, Czech Republic, March 14-18, 2016, Proceedings , 2016

Invited paper Abs arXiv Bib

Keynote lecture at LATA’16.

In this invited contribution, we summarize new solution concepts useful for the synthesis of reactive systems that we have introduced in several recent publications. These solution concepts are developed in the context of non-zero sum games played on graphs. They are part of the contributions obtained in the inVEST project funded by the European Research Council.

@inproceedings{DBLP:conf/lata/BrenguierCHPRRS16,
  author = {Brenguier, Romain and Clemente, Lorenzo and Hunter, Paul and P{\'{e}}rez, Guillermo A. and Randour, Mickael and Raskin, Jean{-}Fran{\c{c}}ois and Sankur, Ocan and Sassolas, Mathieu},
  editor = {Dediu, Adrian{-}Horia and Janousek, Jan and Mart{\'{\i}}n{-}Vide, Carlos and Truthe, Bianca},
  title = {Non-Zero Sum Games for Reactive Synthesis},
  booktitle = {Language and Automata Theory and Applications - 10th International
                    Conference, {LATA} 2016, Prague, Czech Republic, March 14-18, 2016,
                    Proceedings},
  series = {Lecture Notes in Computer Science},
  volume = {9618},
  pages = {3--23},
  publisher = {Springer},
  year = {2016},
  url = {https://doi.org/10.1007/978-3-319-30000-9\_1},
  doi = {10.1007/978-3-319-30000-9\_1},
  timestamp = {Thu, 08 Apr 2021 01:00:00 +0200},
  biburl = {https://dblp.org/rec/conf/lata/BrenguierCHPRRS16.bib},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}

GandALF
Window parity games: an alternative approach toward parity games with time bounds

Véronique Bruyère, Quentin Hautem, and Mickael Randour

In Proceedings of the Seventh International Symposium on Games, Automata, Logics and Formal Verification, GandALF 2016, Catania, Italy, 14-16 September 2016 , 2016

Abs arXiv Bib

Classical objectives in two-player zero-sum games played on graphs often deal with limit behaviors of infinite plays: e.g., mean-payoff and total-payoff in the quantitative setting, or parity in the qualitative one (a canonical way to encode omega-regular properties). Those objectives offer powerful abstraction mechanisms and often yield nice properties such as memoryless determinacy. However, their very nature provides no guarantee on time bounds within which something good can be witnessed. In this work, we consider two approaches toward inclusion of time bounds in parity games. The first one, parity-response games, is based on the notion of finitary parity games [CHH09] and parity games with costs [FZ14,WZ16]. The second one, window parity games, is inspired by window mean-payoff games [CDRR15]. We compare the two approaches and show that while they prove to be equivalent in some contexts, window parity games offer a more tractable alternative when the time bound is given as a parameter (P-c. vs. PSPACE-C.). In particular, it provides a conservative approximation of parity games computable in polynomial time. Furthermore, we extend both approaches to the multi-dimension setting. We give the full picture for both types of games with regard to complexity and memory bounds. [CHH09] K. Chatterjee, T.A. Henzinger, F. Horn (2009): Finitary winning in omega-regular games. ACM Trans. Comput. Log. 11(1). [FZ14] N. Fijalkow, M. Zimmermann (2014): Parity and Streett Games with Costs. LMCS 10(2). [WZ16] A. Weinert, M. Zimmermann (2016): Easy to Win, Hard to Master: Optimal Strategies in Parity Games with Costs. Proc. of CSL, LIPIcs 62, pp. 31:1-31:17, Schloss Dagstuhl - LZI. [CDRR15] K. Chatterjee, L. Doyen, M. Randour, J.-F. Raskin (2015): Looking at mean-payoff and total-payoff through windows. Information and Computation 242, pp. 25-52.
@inproceedings{DBLP:journals/corr/BruyereHR16, author = {Bruy{\`{e}}re, V{\'{e}}ronique and Hautem, Quentin and Randour, Mickael}, editor = {Cantone, Domenico and Delzanno, Giorgio}, title = {Window parity games: an alternative approach toward parity games with time bounds}, booktitle = {Proceedings of the Seventh International Symposium on Games, Automata, Logics and Formal Verification, GandALF 2016, Catania, Italy, 14-16 September 2016}, series = {{EPTCS}}, volume = {226}, pages = {135--148}, year = {2016}, url = {https://doi.org/10.4204/EPTCS.226.10}, doi = {10.4204/EPTCS.226.10}, timestamp = {Wed, 12 Sep 2018 01:05:14 +0200}, biburl = {https://dblp.org/rec/journals/corr/BruyereHR16.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
GAMES
Reconciling Rationality and Stochasticity: Rich Behavioral Models in Two-Player Games

Mickael Randour

In GAMES 2016, the 5th World Congress of the Game Theory Society , 2016

Abs arXiv Bib

Two traditional paradigms are often used to describe the behavior of agents in multi-agent complex systems. In the first one, agents are considered to be fully rational and systems are seen as multi-player games. In the second one, agents are considered to be fully stochastic processes and the system itself is seen as a large stochastic process. From the standpoint of a particular agent - having to choose a strategy, the choice of the paradigm is crucial: the most adequate strategy depends on the assumptions made on the other agents. In this paper, we focus on two-player games and their application to the automated synthesis of reliable controllers for reactive systems - a field at the crossroads between computer science and mathematics. In this setting, the reactive system to control is a player, and its environment is its opponent, usually assumed to be fully antagonistic or fully stochastic. We illustrate several recent developments aiming to breach this narrow taxonomy by providing formal concepts and mathematical frameworks to reason about richer behavioral models. The interest of such models is not limited to reactive system synthesis but extends to other application fields of game theory. The goal of our contribution is to give a high-level presentation of key concepts and applications, aimed at a broad audience. To achieve this goal, we illustrate those rich behavioral models on a classical challenge of the everyday life: planning a journey in an uncertain environment.
@inproceedings{randourGAMES, author = {Randour, Mickael}, title = {Reconciling Rationality and Stochasticity: Rich Behavioral Models in Two-Player Games}, booktitle = {GAMES 2016, the 5th World Congress of the Game Theory Society}, year = {2016}, }

2015

CAV
Percentile Queries in Multi-dimensional Markov Decision Processes

Mickael Randour, Jean-François Raskin, and Ocan Sankur

In Computer Aided Verification - 27th International Conference, CAV 2015, San Francisco, CA, USA, July 18-24, 2015, Proceedings, Part I , 2015

Abs arXiv Bib

Markov decision processes (MDPs) with multi-dimensional weights are useful to analyze systems with multiple objectives that may be conflicting and require the analysis of trade-offs. We study the complexity of percentile queries in such MDPs and give algorithms to synthesize strategies that enforce such constraints. Given a multi-dimensional weighted MDP and a quantitative payoff function f, thresholds v_i (one per dimension), and probability thresholds α_i, we show how to compute a single strategy to enforce that for all dimensions i, the probability of outcomes ρ satisfying f_i(ρ)≥v_i is at least α_i. We consider classical quantitative payoffs from the literature (sup, inf, lim sup, lim inf, mean-payoff, truncated sum, discounted sum). Our work extends to the quantitative case the multi-objective model checking problem studied by Etessami et al. in unweighted MDPs.
@inproceedings{DBLP:conf/cav/RandourRS15, author = {Randour, Mickael and Raskin, Jean{-}Fran{\c{c}}ois and Sankur, Ocan}, editor = {Kroening, Daniel and Pasareanu, Corina S.}, title = {Percentile Queries in Multi-dimensional Markov Decision Processes}, booktitle = {Computer Aided Verification - 27th International Conference, {CAV} 2015, San Francisco, CA, USA, July 18-24, 2015, Proceedings, Part {I}}, series = {Lecture Notes in Computer Science}, volume = {9206}, pages = {123--139}, publisher = {Springer}, year = {2015}, url = {https://doi.org/10.1007/978-3-319-21690-4\_8}, doi = {10.1007/978-3-319-21690-4\_8}, timestamp = {Fri, 27 Mar 2020 08:45:57 +0100}, biburl = {https://dblp.org/rec/conf/cav/RandourRS15.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }

VMCAI

Variations on the Stochastic Shortest Path Problem

Mickael Randour, Jean-François Raskin, and Ocan Sankur

In Verification, Model Checking, and Abstract Interpretation - 16th International Conference, VMCAI 2015, Mumbai, India, January 12-14, 2015. Proceedings , 2015

Invited paper Abs arXiv Bib

Keynote lecture at VMCAI’15.

In this invited contribution, we revisit the stochastic shortest path problem, and show how recent results allow one to improve over the classical solutions: we present algorithms to synthesize strategies with multiple guarantees on the distribution of the length of paths reaching a given target, rather than simply minimizing its expected value. The concepts and algorithms that we propose here are applications of more general results that have been obtained recently for Markov decision processes and that are described in a series of recent papers.

@inproceedings{DBLP:conf/vmcai/RandourRS15,
  author = {Randour, Mickael and Raskin, Jean{-}Fran{\c{c}}ois and Sankur, Ocan},
  editor = {D'Souza, Deepak and Lal, Akash and Larsen, Kim Guldstrand},
  title = {Variations on the Stochastic Shortest Path Problem},
  booktitle = {Verification, Model Checking, and Abstract Interpretation - 16th International
                    Conference, {VMCAI} 2015, Mumbai, India, January 12-14, 2015. Proceedings},
  series = {Lecture Notes in Computer Science},
  volume = {8931},
  pages = {1--18},
  publisher = {Springer},
  year = {2015},
  url = {https://doi.org/10.1007/978-3-662-46081-8\_1},
  doi = {10.1007/978-3-662-46081-8\_1},
  timestamp = {Tue, 07 May 2024 20:11:13 +0200},
  biburl = {https://dblp.org/rec/conf/vmcai/RandourRS15.bib},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}

GandALF
Average-energy games

Patricia Bouyer, Nicolas Markey, Mickael Randour, Kim Guldstrand Larsen, and Simon Laursen

In Proceedings Sixth International Symposium on Games, Automata, Logics and Formal Verification, GandALF 2015, Genoa, Italy, 21-22nd September 2015 , 2015

Abs arXiv Bib

Two-player quantitative zero-sum games provide a natural framework to synthesize controllers with performance guarantees for reactive systems within an uncontrollable environment. Classical settings include mean-payoff games, where the objective is to optimize the long-run average gain per action, and energy games, where the system has to avoid running out of energy. We study average-energy games, where the goal is to optimize the long-run average of the accumulated energy. We show that this objective arises naturally in several applications, and that it yields interesting connections with previous concepts in the literature. We prove that deciding the winner in such games is in NP ∩ coNP and at least as hard as solving mean-payoff games, and we establish that memoryless strategies suffice to win. We also consider the case where the system has to minimize the average-energy while maintaining the accumulated energy within predefined bounds at all times: this corresponds to operating with a finite-capacity storage for energy. We give results for one-player and two-player games, and establish complexity bounds and memory requirements.
@inproceedings{DBLP:journals/corr/BouyerMRLL15, author = {Bouyer, Patricia and Markey, Nicolas and Randour, Mickael and Larsen, Kim Guldstrand and Laursen, Simon}, editor = {Esparza, Javier and Tronci, Enrico}, title = {Average-energy games}, booktitle = {Proceedings Sixth International Symposium on Games, Automata, Logics and Formal Verification, GandALF 2015, Genoa, Italy, 21-22nd September 2015}, series = {{EPTCS}}, volume = {193}, pages = {1--15}, year = {2015}, url = {https://doi.org/10.4204/EPTCS.193.1}, doi = {10.4204/EPTCS.193.1}, timestamp = {Tue, 07 May 2024 01:00:00 +0200}, biburl = {https://dblp.org/rec/journals/corr/BouyerMRLL15.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }

2014

STACS
Meet Your Expectations With Guarantees: Beyond Worst-Case Synthesis in Quantitative Games

Véronique Bruyère, Emmanuel Filiot, Mickael Randour, and Jean-François Raskin

In 31st International Symposium on Theoretical Aspects of Computer Science (STACS 2014), STACS 2014, March 5-8, 2014, Lyon, France , 2014

Abs arXiv Bib

We extend the quantitative synthesis framework by going beyond the worst-case. On the one hand, classical analysis of two-player games involves an adversary (modeling the environment of the system) which is purely antagonistic and asks for strict guarantees. On the other hand, stochastic models like Markov decision processes represent situations where the system is faced to a purely randomized environment: the aim is then to optimize the expected payoff, with no guarantee on individual outcomes. We introduce the beyond worst-case synthesis problem, which is to construct strategies that guarantee some quantitative requirement in the worst-case while providing an higher expected value against a particular stochastic model of the environment given as input. This problem is relevant to produce system controllers that provide nice expected performance in the everyday situation while ensuring a strict (but relaxed) performance threshold even in the event of very bad (while unlikely) circumstances. We study the beyond worst-case synthesis problem for two important quantitative settings: the mean-payoff and the shortest path. In both cases, we show how to decide the existence of finite-memory strategies satisfying the problem and how to synthesize one if one exists. We establish algorithms and we study complexity bounds and memory requirements.
@inproceedings{DBLP:conf/stacs/BruyereFRR14, author = {Bruy{\`{e}}re, V{\'{e}}ronique and Filiot, Emmanuel and Randour, Mickael and Raskin, Jean{-}Fran{\c{c}}ois}, editor = {Mayr, Ernst W. and Portier, Natacha}, title = {Meet Your Expectations With Guarantees: Beyond Worst-Case Synthesis in Quantitative Games}, booktitle = {31st International Symposium on Theoretical Aspects of Computer Science {(STACS} 2014), {STACS} 2014, March 5-8, 2014, Lyon, France}, series = {LIPIcs}, volume = {25}, pages = {199--213}, publisher = {Schloss Dagstuhl - Leibniz-Zentrum f{\"{u}}r Informatik}, year = {2014}, url = {https://doi.org/10.4230/LIPIcs.STACS.2014.199}, doi = {10.4230/LIPICS.STACS.2014.199}, timestamp = {Sat, 05 Sep 2020 01:00:00 +0200}, biburl = {https://dblp.org/rec/conf/stacs/BruyereFRR14.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
SR
Expectations or Guarantees? I Want It All! A crossroad between games and MDPs

Véronique Bruyère, Emmanuel Filiot, Mickael Randour, and Jean-François Raskin

In Proceedings 2nd International Workshop on Strategic Reasoning, SR 2014, Grenoble, France, April 5-6, 2014 , 2014

Abs arXiv Bib

When reasoning about the strategic capabilities of an agent, it is important to consider the nature of its adversaries. In the particular context of controller synthesis for quantitative specifications, the usual problem is to devise a strategy for a reactive system which yields some desired performance, taking into account the possible impact of the environment of the system. There are at least two ways to look at this environment. In the classical analysis of two-player quantitative games, the environment is purely antagonistic and the problem is to provide strict performance guarantees. In Markov decision processes, the environment is seen as purely stochastic: the aim is then to optimize the expected payoff, with no guarantee on individual outcomes. In this expository work, we report on recent results introducing the beyond worst-case synthesis problem, which is to construct strategies that guarantee some quantitative requirement in the worst-case while providing an higher expected value against a particular stochastic model of the environment given as input. This problem is relevant to produce system controllers that provide nice expected performance in the everyday situation while ensuring a strict (but relaxed) performance threshold even in the event of very bad (while unlikely) circumstances. It has been studied for both the mean-payoff and the shortest path quantitative measures.
@inproceedings{DBLP:journals/corr/BruyereFRR14, author = {Bruy{\`{e}}re, V{\'{e}}ronique and Filiot, Emmanuel and Randour, Mickael and Raskin, Jean{-}Fran{\c{c}}ois}, editor = {Mogavero, Fabio and Murano, Aniello and Vardi, Moshe Y.}, title = {Expectations or Guarantees? {I} Want It All! {A} crossroad between games and MDPs}, booktitle = {Proceedings 2nd International Workshop on Strategic Reasoning, {SR} 2014, Grenoble, France, April 5-6, 2014}, series = {{EPTCS}}, volume = {146}, pages = {1--8}, year = {2014}, url = {https://doi.org/10.4204/EPTCS.146.1}, doi = {10.4204/EPTCS.146.1}, timestamp = {Sat, 30 Sep 2023 10:08:00 +0200}, biburl = {https://dblp.org/rec/journals/corr/BruyereFRR14.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }

2013

ATVA
Looking at Mean-Payoff and Total-Payoff through Windows

Krishnendu Chatterjee, Laurent Doyen, Mickael Randour, and Jean-François Raskin

In Automated Technology for Verification and Analysis - 11th International Symposium, ATVA 2013, Hanoi, Vietnam, October 15-18, 2013. Proceedings , 2013

Abs arXiv Bib

We consider two-player games played on weighted directed graphs with mean-payoff and total-payoff objectives, two classical quantitative objectives. While for single-dimensional games the complexity and memory bounds for both objectives coincide, we show that in contrast to multi-dimensional mean-payoff games that are known to be coNP-complete, multi-dimensional total-payoff games are undecidable. We introduce conservative approximations of these objectives, where the payoff is considered over a local finite window sliding along a play, instead of the whole play. For single dimension, we show that (i) if the window size is polynomial, deciding the winner takes polynomial time, and (ii) the existence of a bounded window can be decided in NP ∩ coNP, and is at least as hard as solving mean-payoff games. For multiple dimensions, we show that (i) the problem with fixed window size is EXPTIME-complete, and (ii) there is no primitive-recursive algorithm to decide the existence of a bounded window.
@inproceedings{DBLP:conf/atva/Chatterjee0RR13, author = {Chatterjee, Krishnendu and Doyen, Laurent and Randour, Mickael and Raskin, Jean{-}Fran{\c{c}}ois}, editor = {Hung, Dang Van and Ogawa, Mizuhito}, title = {Looking at Mean-Payoff and Total-Payoff through Windows}, booktitle = {Automated Technology for Verification and Analysis - 11th International Symposium, {ATVA} 2013, Hanoi, Vietnam, October 15-18, 2013. Proceedings}, series = {Lecture Notes in Computer Science}, volume = {8172}, pages = {118--132}, publisher = {Springer}, year = {2013}, url = {https://doi.org/10.1007/978-3-319-02444-8\_10}, doi = {10.1007/978-3-319-02444-8\_10}, timestamp = {Tue, 14 May 2019 10:00:49 +0200}, biburl = {https://dblp.org/rec/conf/atva/Chatterjee0RR13.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
ECCS
Automated Synthesis of Reliable and Efficient Systems Through Game Theory: A Case Study

Mickael Randour

In Proceedings of the European Conference on Complex Systems 2012, ECCS 2012, Brussels, Belgium, September 2-7, 2012 , 2013

Abs arXiv Bib

Reactive computer systems bear inherent complexity due to continuous interactions with their environment. While this environment often proves to be uncontrollable, we still want to ensure that critical computer systems will not fail, no matter what they face. Examples are legion: railway traffic, power plants, plane navigation systems, etc. Formal verification of a system may ensure that it satisfies a given specification, but only applies to an already existing model of a system. In this work, we address the problem of synthesis: starting from a specification of the desired behavior, we show how to build a suitable system controller that will enforce this specification. In particular, we discuss recent developments of that approach for systems that must ensure Boolean behaviors (e.g., reachability, liveness) along with quantitative requirements over their execution (e.g., never drop out of fuel, ensure a suitable mean response time). We notably illustrate a powerful, practically useable algorithm for the automated synthesis of provably safe reactive systems.
@inproceedings{randourECCS, year = {2013}, isbn = {978-3-319-00394-8}, booktitle = {Proceedings of the European Conference on Complex Systems 2012, {ECCS} 2012, Brussels, Belgium, September 2-7, 2012}, series = {Springer Proceedings in Complexity}, title = {Automated {S}ynthesis of {R}eliable and {E}fficient {S}ystems {T}hrough {G}ame {T}heory: {A} {C}ase {S}tudy}, publisher = {Springer}, author = {Randour, Mickael}, pages = {731-738} }

2012

CONCUR
Strategy Synthesis for Multi-Dimensional Quantitative Objectives

Krishnendu Chatterjee, Mickael Randour, and Jean-François Raskin

In CONCUR 2012 - Concurrency Theory - 23rd International Conference, CONCUR 2012, Newcastle upon Tyne, UK, September 4-7, 2012. Proceedings , 2012

Abs arXiv Bib

Multi-dimensional mean-payoff and energy games provide the mathematical foundation for the quantitative study of reactive systems, and play a central role in the emerging quantitative theory of verification and synthesis. In this work, we study the strategy synthesis problem for games with such multi-dimensional objectives along with a parity condition, a canonical way to express ω-regular conditions. While in general, the winning strategies in such games may require infinite memory, for synthesis the most relevant problem is the construction of a finite-memory winning strategy (if one exists). Our main contributions are as follows. First, we show a tight exponential bound (matching upper and lower bounds) on the memory required for finite-memory winning strategies in both multi-dimensional mean-payoff and energy games along with parity objectives. This significantly improves the triple exponential upper bound for multi energy games (without parity) that could be derived from results in literature for games on VASS (vector addition systems with states). Second, we present an optimal symbolic and incremental algorithm to compute a finite-memory winning strategy (if one exists) in such games. Finally, we give a complete characterization of when finite memory of strategies can be traded off for randomness. In particular, we show that for one-dimension mean-payoff parity games, randomized memoryless strategies are as powerful as their pure finite-memory counterparts.
@inproceedings{DBLP:conf/concur/ChatterjeeRR12, author = {Chatterjee, Krishnendu and Randour, Mickael and Raskin, Jean{-}Fran{\c{c}}ois}, editor = {Koutny, Maciej and Ulidowski, Irek}, title = {Strategy Synthesis for Multi-Dimensional Quantitative Objectives}, booktitle = {{CONCUR} 2012 - Concurrency Theory - 23rd International Conference, {CONCUR} 2012, Newcastle upon Tyne, UK, September 4-7, 2012. Proceedings}, series = {Lecture Notes in Computer Science}, volume = {7454}, pages = {115--131}, publisher = {Springer}, year = {2012}, url = {https://doi.org/10.1007/978-3-642-32940-1\_10}, doi = {10.1007/978-3-642-32940-1\_10}, timestamp = {Tue, 14 May 2019 10:00:43 +0200}, biburl = {https://dblp.org/rec/conf/concur/ChatterjeeRR12.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }

Thesis

2014

PhD Thesis
Synthesis in Multi-Criteria Quantitative Games

Mickael Randour

Apr 2014

UMONS – Université de Mons. Supervisors: Véronique Bruyère (UMONS) et Jean-François Raskin (ULB).

Ackermann Award Bib PDF

Ackermann Award 2015: Outstanding PhD Dissertation Award for Logic in Computer Science, worldwide selection by the EACSL – European Association for Computer Science Logic.
@phdthesis{randourThesis, author = {Randour, Mickael}, title = {Synthesis in Multi-Criteria Quantitative Games}, school = {UMONS -- Université de Mons}, year = {2014}, month = apr, type = {PhD Thesis}, note = {UMONS -- Université de Mons. Supervisors: Véronique Bruyère (UMONS) et Jean-François Raskin (ULB).}, }