18 citations · 100 across the 28 of their papers we have counts for
36 papers
Proceedings Seventeenth International Symposium on Games, Automata, Logics, and Formal Verification
Giorgio Bacci, Mickaël Randour
This volume contains the proceedings of GandALF 2026, the Seventeenth International Symposium on Games, Automata, Logics, and Formal Verification. The symposium was held in Aalborg…
Simplicity Lies in the Eye of the Beholder: A Strategic Perspective on Controllers in Reactive Synthesis
Mickael Randour
In the game-theoretic approach to controller synthesis, we model the interaction between a system to be controlled and its environment as a game between these entities, and we seek…
Taming Infinity one Chunk at a Time: Concisely Represented Strategies in One-Counter MDPs
Michal Ajdarów, James C. A. Main, Petr Novotný +1
Markov decision processes (MDPs) are a canonical model to reason about decision making within a stochastic environment. We study a fundamental class of infinite MDPs: one-counter M…
Mixing Any Cocktail with Limited Ingredients: On the Structure of Payoff Sets in Multi-Objective POMDPs and its Impact on Randomised Strategies
James C. A. Main, Mickael Randour
We consider multi-dimensional payoff functions in partially observable Markov decision processes. We study the structure of the set of expected payoff vectors of all strategies (po…
Games on Graphs: From Logic and Automata to Algorithms
Nathanaël Fijalkow, C. Aiswarya, Guy Avni +22
The objective of this book is to give a comprehensive presentation of the research field concerned with infinite duration games on graphs. Historically, these game models appeared…
How to Play Optimally for Regular Objectives?
Patricia Bouyer, Nathanaël Fijalkow, Mickael Randour +1
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 optimal…
Timed Games with Bounded Window Parity Objectives
James C. A. Main, Mickael Randour, Jeremy Sproston
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 b…
Half-Positional Objectives Recognized by Deterministic Büchi Automata
Patricia Bouyer, Antonio Casares, Mickael Randour +1
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 char…
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 strate…
Characterizing Omega-Regularity through Finite-Memory Determinacy of Games on Infinite Graphs
Patricia Bouyer, Mickael Randour, Pierre Vandenhove
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 $ω…
Time Flies When Looking out of the Window: Timed Games with Window Parity Objectives
James C. A. Main, Mickael Randour, Jeremy Sproston
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 sinc…
Arena-Independent Finite-Memory Determinacy in Stochastic Games
Patricia Bouyer, Youssouf Oualhadj, Mickael Randour +1
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, a…
Decisiveness of Stochastic Systems and its Application to Hybrid Models (Full Version)
Patricia Bouyer, Thomas Brihaye, Mickael Randour +2
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…
Decisiveness of Stochastic Systems and its Application to Hybrid Models
Patricia Bouyer, Thomas Brihaye, Mickael Randour +2
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…
Games Where You Can Play Optimally with Arena-Independent Finite Memory
Patricia Bouyer, Stéphane Le Roux, Youssouf Oualhadj +2
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 sy…
Simple Strategies in Multi-Objective MDPs (Technical Report)
Florent Delgrange, Joost-Pieter Katoen, Tim Quatmann +1
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 obta…
Energy mean-payoff games
Véronique Bruyère, Quentin Hautem, Mickael Randour +1
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…
Life is Random, Time is Not: Markov Decision Processes with Window Objectives
Thomas Brihaye, Florent Delgrange, Youssouf Oualhadj +1
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 acceptab…
Multi-weighted Markov Decision Processes with Reachability Objectives
Patricia Bouyer, Mauricio González, Nicolas Markey +1
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 reachabilit…
Extending finite-memory determinacy by Boolean combination of winning conditions
Stéphane Le Roux, Arno Pauly, Mickael Randour
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 control…
Threshold Constraints with Guarantees for Parity Objectives in Markov Decision Processes
Raphaël Berthon, Mickael Randour, Jean-François Raskin
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 guaran…
Bounding Average-energy Games
Patricia Bouyer, Piotr Hofman, Nicolas Markey +2
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, de…
Window Parity Games: An Alternative Approach Toward Parity Games with Time Bounds (Full Version)
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…
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…