Mickael Randour

I&C Journal 2024 Journal Article

Different strokes in randomised strategies: Revisiting Kuhn's theorem under finite-memory assumptions

• James C.A. Main
• Mickael Randour

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 setting, 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 concurrent 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 in games of perfect and imperfect information with perfect recall, and in games with more than two players. We also provide an adapted taxonomy for games with imperfect recall.

LAMAS&SR Workshop 2023 Workshop Paper

Different Strokes in Randomised Strategies: Revisiting Kuhn's Theorem under Finite-memory Assumptions

• James C. A. Main
• Mickael Randour

IJCAI Conference 2023 Conference Paper

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

• Patricia Bouyer
• Antonio Casares
• Mickael Randour
• Pierre Vandenhove

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.

LAMAS&SR Workshop 2022 Workshop Paper

Characterizing Omega-Regularity through Finite-Memory Determinacy of Games on Infinite Graphs

• Patricia Bouyer
• Mickael Randour
• Pierre Vandenhove

I&C Journal 2022 Journal Article

Decisiveness of stochastic systems and its application to hybrid models

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

In 2007, 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 the 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.

GandALF Workshop 2020 Workshop Paper

Decisiveness of Stochastic Systems and its Application to Hybrid Models

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

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

GandALF Workshop 2018 Workshop Paper

Multi-weighted Markov Decision Processes with Reachability Objectives

• Patricia Bouyer
• Mauricio González
• Nicolas Markey
• Mickael Randour

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.

I&C Journal 2017 Journal Article

Meet your expectations with guarantees: Beyond worst-case synthesis in quantitative games

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

Classical analysis of two-player quantitative games involves an adversary (modeling the environment of the system) which is purely antagonistic and asks for strict guarantees while Markov decision processes model systems facing 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 a higher expected value against a particular stochastic model of the environment given as input. 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.

Highlights Conference 2017 Conference Abstract

Rich behavioral models: illustration on journey planning

• Mickael Randour

I will illustrate rich behavioral models in games and Markov decision processes through applications to journey planning in an uncertain environment. The shortest path problem asks to find a path of minimal length between a source vertex and a destination vertex within a weighted graph. It can be used to model minimization of travel time between two places in a town where the environment (traffic, weather, etc) is perfectly predictable. I will first discuss how it can be generalized to more realistic stochastic environments, in which case one usually wants to minimize its expected time to destination, or to maximize its chances to reach the destination within a given time. To that end, I will use (discrete) Markov decision processes. Then, I will present recent extensions allowing to reason about richer types of travel strategies (choice of route, mean of transport, etc): strategies that take into account both the length of a journey and its cost, strategies that minimize the expected travel time while providing strong guarantees on the worst-case travel time (i. e. , when considering the environment as an opponent in a two-player game), and more. I will focus on the modeling power of the different models through natural application scenarios of the everyday life.

GandALF Workshop 2016 Workshop Paper

Window Parity Games: An Alternative Approach Toward Parity Games with Time Bounds

• Véronique Bruyère
• Quentin Hautem
• Mickael Randour

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, Schloss Dagstuhl - LZI. To appear. [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.

Highlights Conference 2016 Conference Abstract

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

• joint work with Véronique Bruyère
• Mickael Randour

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 w-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 and parity games with costs. The second one, window parity games, is inspired by window mean-payoff games. 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 vs PSPACE). 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.

GandALF Workshop 2015 Workshop Paper

Average-energy games

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

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

I&C Journal 2015 Journal Article

Looking at mean-payoff and total-payoff through windows

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

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.

Highlights Conference 2015 Conference Abstract

Percentile Queries in Multi-Dimensional Markov Decision Processes

• Mickael Randour

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. In this paper, 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 $\alpha_i$, we show how to compute a single strategy to enforce that for all dimensions $i$, the probability of outcomes $\rho$ satisfying $f_i(\rho) \geq v_i$ is at least $\alpha_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.

Highlights Conference 2014 Conference Abstract

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

• Mickael Randour

Classical analysis of two-player quantitative games involves an adversary (modeling the environment of the system) which is purely antagonistic and asks for strict guarantees while Markov decision processes model systems facing a purely randomized environment: the aim is 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. We consider mean-payoff and shortest path settings. 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. This talk is based on a joint paper with Véronique Bruyère, Emmanuel Filiot and Jean-François Raskin, published in STACS 2014 [BFRR14]. An extended version can be found on arXiv [BFRR13]. [BFRR13] V. Bruyère, E. Filiot, M. Randour, and J. -F. Raskin. Meet your expectations with guarantees: beyond worst-case synthesis in quantitative games. CoRR, abs/1309. 5439, 2013 [BFRR14] V. Bruyère, E. Filiot, M. Randour, and J. -F. Raskin. Meet your expectations with guarantees: beyond worst-case synthesis in quantitative games. In Proc. of STACS, volume 25 of LIPIcs, pages 199–213. Schloss Dagstuhl - LZI, 2014.

Highlights Conference 2013 Conference Abstract

Looking at mean-payoff and total-payoff through windows

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

We consider two-player games with mean-payoff (MP) and total-payoff (TP) objectives. In single dimension, their complexities coincide. In multi dimensions, MP games are coNP-complete. We show that TP games are undecidable. We introduce conservative approximations, considering the payoff over a local finite window sliding along a play. For single dimension, we show that (i) if the window is polynomial, deciding the winner is in P, and (ii) the existence of a bounded window can be decided in NP $\cap$ coNP, and is at least as hard as solving MP games. For multi dimensions, we show that (i) the fixed window size problem is EXP-complete, and (ii) there is no primitive-recursive algorithm to decide the existence of a bounded window.