# Main research axes

What we spend our time on.

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

- Book

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

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

- FSTTCSThe True Colors of Memory: A Tour of Chromatic-Memory Strategies in Zero-Sum Games on Graphs (Invited Talk)
*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

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

- TACASMinimal Critical Subsystems for Discrete-Time Markov Models
*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

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

- FMSDA game-based abstraction-refinement framework for Markov decision processes
*Formal Methods Syst. Des.*, 2010 - HSCCIMPaCT: A Parallelized Software Tool for IMDP Construction and Controller Synthesis with Convergence Guarantees
*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

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

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

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

- AAAIReinforcement Learning of Risk-Constrained Policies in Markov Decision Processes
*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

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

- PLOS ONEControl strategies for COVID-19 epidemic with vaccination, shield immunity and quarantine: A metric temporal logic approach
*PLOS ONE*, Mar 2021 - Sci. Rep.
- arXiv