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

• Arena-Independent Finite-Memory Determinacy in Stochastic Games. Patricia Bouyer, Youssouf Oualhadj, Mickael Randour, Pierre Vandenhove. Logical Methods in Computer Science, volume 19, issue 4, pages 18:1-18:51, 2023. On arXiv (51 pages).
• Arena-independent Memory Bounds for Nash Equilibria in Reachability Games James C. A. Main. STACS'23, LIPIcs, 18 pages, Schloss Dagstuhl, 2024. Extended version on arXiv (32 pages).
• Reachability Games and Friends: A Journey through the Lens of Memory and Complexity. Thomas Brihaye, Aline Goeminne, James C. A. Main, Mickael Randour. Keynote lecture at FSTTCS’23, LIPIcs 284, 26 pages, Schloss Dagstuhl, 2023. Open access through DROPS (18 pages).
• Half-Positional Objectives Recognized by Deterministic Büchi Automata (Extended Abstract). Patricia Bouyer, Antonio Casares, Mickael Randour, Pierre Vandenhove. IJCAI’23 – Sister Conferences Best Papers Track, 2023. Extended version on arXiv (37 pages).
• How to Play Optimally for Regular Objectives? Patricia Bouyer, Nathanael Fijalkow, Mickael Randour, Pierre Vandenhove. ICALP'23, LIPIcs 261, 18 pages, Schloss Dagstuhl, 2023. Extended version on arXiv (26 pages).