ControlleRS | Mickael Randour

Project highlights

FNRS Research Project.
Project leader: Mickael Randour.
Duration: January 2023 to December 2026. Budget ~270.000 euros.
Postdoctoral positions are available: contact me! Here is a non-exhaustive list of possible topics:
- multi-criteria approaches in formal methods,
- machine learning and AI,
- synthesis in stochastic systems,
- tool development,
- industrial applications.

Project summary

We live in the days of ubiquitous computing: we are surrounded by reactive (computer) systems that continuously interact with their environment through user input, sensors, etc. Their correctness is often critical, either for safety reasons (e.g., ABS for cars) or due to constraints of mass production (e.g., smartphones). Unfortunately, their development is difficult and prone to errors. Formal verification and synthesis have proved to be success stories of computer science, aiming at the automated construction of provably-safe system controllers. Many techniques take roots in the game-theoretic framework, modeling the interaction between the system and its environment as a competitive game.

One crucial change over the last decade is the evolution from Boolean to quantitative specifications, giving birth to models describing performance of systems. Recent research focuses on taking into account the interplay between different quantitative (or qualitative) aspects and the resulting trade-offs. Such trade-offs may occur between different resources (e.g., decreasing response time requires additional computing power and energy consumption) but also between different behavioral models (e.g., average-case vs. worst-case performance). Those interactions are at the core of practical scenarios and require developers to decide how to balance the different aspects. My research group is at the forefront of research on many-sided synthesis, which supports such multi-objective reasoning.

The goal of ControlleRS is to challenge the key concept of strategy, currently based on automata-like finite-state machines acting as blueprints for implementable controllers. I aim to broaden the theoretical understanding and the practical usefulness of this abstract concept through the systematic study of alternative strategy models over the complete span from theoretical power to proper applicability. This endeavor promises fundamental advances toward truly implementable many-sided synthesis.

Publications supported by the project: 5

Peer-reviewed journals

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}, }

International peer-reviewed conferences

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}
}

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} }
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} }
STACS
Arena-Independent Memory Bounds for Nash Equilibria in Reachability Games

James C. A. Main

In 41st International Symposium on Theoretical Aspects of Computer Science, STACS 2024, March 12-14, 2024, Clermont-Ferrand, France , 2024

Abs arXiv Bib

We study the memory requirements of Nash equilibria in turn-based multiplayer games on possibly infinite graphs with reachability, shortest path and Büchi objectives. We present constructions for finite-memory Nash equilibria in these games that apply to arbitrary game graphs, bypassing the finite-arena requirement that is central in existing approaches. We show that, for these three types of games, from any Nash equilibrium, we can derive another Nash equilibrium where all strategies are finite-memory such that the same players accomplish their objective, without increasing their cost for shortest path games. Furthermore, we provide memory bounds that are independent of the size of the game graph for reachability and shortest path games. These bounds depend only on the number of players. To the best of our knowledge, we provide the first results pertaining to finite-memory constrained Nash equilibria in infinite arenas and the first arena-independent memory bounds for Nash equilibria.
@inproceedings{DBLP:conf/stacs/Main24, author = {Main, James C. A.}, editor = {Beyersdorff, Olaf and Kant{\'{e}}, Mamadou Moustapha and Kupferman, Orna and Lokshtanov, Daniel}, title = {Arena-Independent Memory Bounds for Nash Equilibria in Reachability Games}, booktitle = {41st International Symposium on Theoretical Aspects of Computer Science, {STACS} 2024, March 12-14, 2024, Clermont-Ferrand, France}, series = {LIPIcs}, volume = {289}, pages = {50:1--50:18}, publisher = {Schloss Dagstuhl - Leibniz-Zentrum f{\"{u}}r Informatik}, year = {2024}, url = {https://doi.org/10.4230/LIPIcs.STACS.2024.50}, doi = {10.4230/LIPICS.STACS.2024.50}, timestamp = {Mon, 11 Mar 2024 20:24:54 +0100}, biburl = {https://dblp.org/rec/conf/stacs/Main24.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }