Main research axes

What we spend our time on.


complexity.jpg

Controller representations and complexity

In the game-theoretic approach toward controller synthesis, we model the interaction between a system to control and its environment as (some variation of) game between these entities, and we are looking for an appropriate (e.g., winning or optimal) strategy of the system. This strategy then constitutes a formal blueprint for a real-world controller for the system (Randour, 2013; Clarke et al., 2018).

The general consensus is that simple (e.g., using limited memory) strategies are better: corresponding controllers will be easier to conceive and understand, and cheaper to produce and maintain. Yet, the traditional formal model used to represent strategies is some sort of finite automaton (Fijalkow et al., 2023), which is usually far from what we expect in practice. In particular, our theoretical measures of strategy complexity are somewhat disconnected from what can be considered as complex or not in implemented controllers. Hence, we challenge the key concept of strategy and how to assess their complexity, and we study alternative strategy models (e.g., augmented automata, decision trees, RNNs) over the complete span from theoretical power to proper applicability. My FNRS project ControlleRS is dedicated to this research program.

References

  1. 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
  2. Book
    Handbook of Model Checking
    Edmund M. Clarke, Thomas A. Henzinger, Helmut Veith, and Roderick Bloem
    2018
  3. 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 RandourOcan Sankur, Sylvain Schmitz, Olivier Serre, and Mateusz Skomra
    2023

dice.jpg

Randomness in strategies

Optimal strategies may require randomization (i.e., the ability to take probabilistic decisions) when dealing with inherently probabilistic goals, balancing multiple objectives, or in contexts of partial information. There are multiple ways to augment strategies (and related strategy representation models) with randomness. We study the expressive power of these different types of randomness: we notably establish a complete taxonomy for finite-memory strategies, valid up to multi-player games of imperfect information, in (Main & Randour, 2022).

References

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

HDD.jpg

Memory bounds

The vast majority of simple objectives (which encode specifications) in two-player (stochastic) games admit memoryless optimal strategies. That is, controllers for the system only need to look at the current state to act optimally, regardless of what happened in the past. This usually does not hold when considering more complex objectives, such as, e.g., conjunctions of simple objectives, which are needed to accurately model the richness of real-world situations. An important research area is therefore devoted to understanding for which objectives we need memory and how much. We notably characterize the objectives for which arena-independent memory suffices, in a variety of settings (Bouyer et al., 2022; Bouyer et al., 2023; Bouyer et al., 2023; Bouyer et al., 2022), or provide tight bounds for specific types of objectives (Bouyer et al., 2022).

References

  1. FSTTCS
    The True Colors of Memory: A Tour of Chromatic-Memory Strategies in Zero-Sum Games on Graphs (Invited Talk)
    Patricia BouyerMickael 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
  2. TheoretiCS
    Characterizing Omega-Regularity through Finite-Memory Determinacy of Games on Infinite Graphs
    Patricia BouyerMickael Randour, and Pierre Vandenhove
    TheoretiCS, 2023
  3. LMCS
    Arena-Independent Finite-Memory Determinacy in Stochastic Games
    Logical Methods in Computer Science, 2023
  4. LMCS
    Games Where You Can Play Optimally with Arena-Independent Finite Memory
    Patricia Bouyer, Stéphane Le Roux, Youssouf OualhadjMickael Randour, and Pierre Vandenhove
    Logical Methods in Computer Science, 2022
  5. CONCUR
    Half-Positional Objectives Recognized by Deterministic Büchi Automata
    In 33rd International Conference on Concurrency Theory, CONCUR 2022, September 12-16, 2022, Warsaw, Poland , 2022

refine.jpg

Refinement mechanisms in synthesis

Programming is an inherently iterative process: when was the last time you coded a feature that worked right away without any debugging? Yet, we often assume that synthesis must be a push-a-button-once process where either you get a perfect controller from the get-go, or you are guaranteed there is no suitable one. But what happens if your specification is ill-defined and needs to be amended, or if your system needs to be patched to permit the existence of a suitable controller? This is what we are working on: techniques to help when synthesis fails. In particular, we are studying appropriate notions of counter-examples à la (Wimmer et al., 2012) to understand where a system fails and how to fix it, hence enabling synthesis through iterative refinements.

References

  1. TACAS
    Minimal Critical Subsystems for Discrete-Time Markov Models
    Ralf Wimmer, Nils Jansen, Erika Ábrahám, Bernd Becker, and Joost-Pieter Katoen
    In Tools and Algorithms for the Construction and Analysis of Systems - 18th International Conference, TACAS 2012, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2012, Tallinn, Estonia, March 24 - April 1, 2012. Proceedings , 2012

abstraction.jpg

Abstractions

Abstraction is at the core of formal methods: we analyze complex systems by looking at simplified versions of them. Yet, it is often the case that the first formal model we work with is not abstract enough, and that we need to keep abstracting even further to enable effective model checking or synthesis. It may be necessary because the model under study is simply too large for practical purposes, or possesses complex features that are difficult to handle with classical techniques (e.g., continuous state spaces). Hence, several axes described on this page involve dealing with abstractions as a key mechanism. We notably use it to provide faster algorithms for classical problems (à la (Kattenbelt et al., 2010)), or to enable guarantee-driven reasoning in continuous models (à la (Wooding & Lavaei, 2024)).

References

  1. FMSD
    A game-based abstraction-refinement framework for Markov decision processes
    Mark Kattenbelt, Marta Z. Kwiatkowska, Gethin Norman, and David Parker
    Formal Methods Syst. Des., 2010
  2. HSCC
    IMPaCT: A Parallelized Software Tool for IMDP Construction and Controller Synthesis with Convergence Guarantees
    Ben Wooding, and Abolfazl Lavaei
    In Proceedings of the 27th ACM International Conference on Hybrid Systems: Computation and Control, HSCC 2024, Hong Kong SAR, China, May 14-16, 2024 , 2024

multi.jpg

Many-sided synthesis

Historically, game-theoretic models have been focused on single-objective scenarios, where the goal of the system is either to ensure satisfaction of a qualitative property (e.g., avoiding unsafe states) or to optimize a given payoff function (e.g., minimize the energy consumption). Richer models are needed to accurately model many real-world situations: 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). Our group develops numerous techniques and tools dedicated to such multi-objective reasoning, e.g., (Brihaye et al., 2020; Randour et al., 2017; Bruyère et al., 2017). My FNRS project ManySynth was dedicated to this research program. See also my chapter on the subject in (Fijalkow et al., 2023).

References

  1. 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 RandourOcan Sankur, Sylvain Schmitz, Olivier Serre, and Mateusz Skomra
    2023
  2. 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
  3. FMSD
    Percentile queries in multi-dimensional Markov decision processes
    Mickael RandourJean-François Raskin, and Ocan Sankur
    Formal Methods in System Design, 2017
  4. Inf. Comput.
    Meet your expectations with guarantees: Beyond worst-case synthesis in quantitative games
    Information and Computation, 2017

hourglass.jpg

Continuous and timed systems

A key decision in modeling real-world systems is how we handle time: either as a sequence of discrete steps with events only happening at predefined ticks or as a continuous flow where events can take place at any point. While the second model is arguably more realistic (which can be necessary for time-sensitive applications), the resulting models are usually more difficult to analyze, often leading to undecidability when combined with complex specifications. Our team focuses on developing expressive frameworks while maintaining tractability through novel concepts, both in timed automata and games (Main et al., 2022; Main et al., 2021), and in hybrid systems (Bouyer et al., 2022).

References

  1. FORMATS
    Timed Games with Bounded Window Parity Objectives
    James C. A. MainMickael 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
  2. CONCUR
    Time Flies When Looking out of the Window: Timed Games with Window Parity Objectives
    James C. A. MainMickael Randour, and Jeremy Sproston
    In 32nd International Conference on Concurrency Theory, CONCUR 2021, August 24-27, 2021, Virtual Conference , 2021
  3. Inf. Comput.
    Decisiveness of stochastic systems and its application to hybrid models
    Patricia BouyerThomas BrihayeMickael Randour, Cédric Rivière, and Pierre Vandenhove
    Information and Computation, 2022

robot.jpg

RL x FM

In a sense, there are two worlds: the world of AI and learning, which offers unparalleled efficiency but few guarantees, and the one of logic, which provides a fundamental framework to reason about safety, but usually lacks efficiency (as most formal methods problems have inherently high computational complexity and thus suffer from poor scalability). Our group participates in a blooming effort to combine the formal reasoning from logic and the power of learning (e.g., (Brázdil et al., 2020)). We develop techniques mixing reinforcement learning and exact methods for reactive synthesis, with a particular focus on the application contexts developed in the axes above, such as the expressive multi-objective framework of (Randour et al., 2017).

References

  1. FMSD
    Percentile queries in multi-dimensional Markov decision processes
    Mickael RandourJean-François Raskin, and Ocan Sankur
    Formal Methods in System Design, 2017
  2. AAAI
    Reinforcement Learning of Risk-Constrained Policies in Markov Decision Processes
    Tomás Brázdil, Krishnendu Chatterjee, Petr Novotný, and Jiri Vahala
    In The Thirty-Fourth AAAI Conference on Artificial Intelligence, AAAI 2020, The Thirty-Second Innovative Applications of Artificial Intelligence Conference, IAAI 2020, The Tenth AAAI Symposium on Educational Advances in Artificial Intelligence, EAAI 2020, New York, NY, USA, February 7-12, 2020 , 2020

epidemic.jpg

Formal methods meet epidemic models

In collaboration with a local research group in applied probability, we are exploring how formal methods can help in reasoning about stochastic processes used in epidemic modeling. These particular stochastic processes are complex both due to their size (capturing huge populations) and their non-linear dynamics. Work in this direction has notably been inspired by the recent pandemic (Xu et al., 2021; Svoboda et al., 2022; Leys & Pérez, 2024). Our focus is on rich specifications and control, i.e., enabling reasoning about strategies in epidemic stochastic models.

References

  1. PLOS ONE
    Control strategies for COVID-19 epidemic with vaccination, shield immunity and quarantine: A metric temporal logic approach
    Zhe Xu, Bo Wu, and Ufuk Topcu
    PLOS ONE, Mar 2021
  2. Sci. Rep.
    Infection dynamics of COVID-19 virus under lockdown and reopening
    Jakub Svoboda, Josef Tkadlec, Andreas Pavlogiannis, Krishnendu Chatterjee, and Martin A Nowak
    Scientific reports, Mar 2022
  3. arXiv
    Inform: From Compartmental Models to Stochastic Bounded Counter Machines
    Tim Leys, and Guillermo A. Pérez
    CoRR, Mar 2024