Key words about my research: formal verification, synthesis, timed systems, games, quantitative models, probabilistic models

My publications

International conferences

Reports- thesis

My recent talks
Synthesis of Robust Optimal Real-Time Systems
(slides)
Weighted Timed Games (WTG for short) are the most widely used model to describe controller synthesis problems involving real-time issues. The synthesized strategies rely on a perfect measure of time elapse, which is not realistic in practice. In order to produce strategies tolerant to timing imprecisions, we rely on a notion of robustness first introduced for timed automata. More precisely, WTGs are two-player zero-sum games played in a timed automaton equipped with integer weights in which one of the players, that we call Min, wants to reach a target location while minimising the cumulated weight. In this work, we equip the underlying timed automaton with a semantics depending on some parameter (representing the maximal possible perturbation) in which the opponent of Min can in addition perturb delays chosen by Min.

The robust value problem can then be stated as follows: given some threshold, determine whether there exists a positive perturbation and a strategy for Min ensuring to reach the target, with an accumulated weight below the threshold, whatever the opponent does.

We provide the first decidability result for the robust value problem. More precisely, we show that we can compute the robust value function, in a parametric way, for the class of divergent WT (this class has been introduced previously to obtain decidability of the (classical) value problem in WTGs). To this end, we show that the robust value is the fixpoint of some operators, as is classically done for value iteration algorithms. We then combine in a very careful way two representations: piecewise affine functions introduced in Alur et. al. (2004) to analyse WTGs, and shrunk BDMs considered in Sankur et. al. (2011) to analyse robustness in timed automata. The crux of our result consists in showing that using this representation, the operator of value iteration can be computed for infinitesimally small perturbations.

Last, we also study qualitative decision problems and close an open problem on robust reachability, showing it is EXPTIME-complete for general WTGs.

This is joint work with Benjamin Monmege and Pierre-Alain Reynier.
Counterfactual Causality for Reachability and Safety based on Distance Functions
(slides)
Investigations of causality in operational systems aim at providing human-understandable explanations of why a system behaves as it does. There is, in particular, a demand to explain what went wrong on a given counterexample execution that shows that a system does not satisfy a given specification. To this end, this paper investigates a notion of counterfactual causality in transition systems based on Stalnaker's and Lewis' semantics of counterfactuals in terms of most similar possible worlds and introduces a novel corresponding notion of counterfactual causality in two-player games. Using distance functions between paths in transition systems to capture the similarity of executions, this notion defines whether reaching a certain set of states is a cause for the fact that a given execution of a system; satisfies an undesirable reachability or safety property. Similarly, using distance functions between memoryless strategies in reachability and safety games, it is defined whether reaching a set of states is a cause for the fact that a given strategy for the player under investigation is losing.

The contribution is two-fold:
In transition systems, it is shown that counterfactual causality can be checked in polynomial time for three prominent distance functions between paths.
In two-player games, the introduced notion of counterfactual causality is shown to be checkable in polynomial time for two natural distance functions between memoryless strategies. Further, a notion of explanation that can be extracted from a counterfactual cause and that pinpoints changes to be made to the given strategy in order to transform it into a winning strategy is defined. For the two distance functions under consideration, the problem to decide whether such an explanation imposes only minimal necessary changes to the given strategy with respect to the used distance function turns out to be coNP-complete and not to be solvable in polynomial time if P is not equal to NP, respectively.

This is joint work with Jakob Priribauer and Christel Baier.
Weighted Timed Games: Decidability, Randomisation and Robustness
(slides, poster)
Weighted timed games are two-player zero-sum games played in a timed automaton equipped with integer weights. We consider optimal reachability objectives, in which one of the players, whom we call Min, wants to reach a target location while minimising the cumulated weight. While knowing if Min has a (deterministic) strategy to guarantee a value lower than a given threshold is known to be undecidable (with two or more clocks), several conditions, one of them being the divergence or one-clock WTGs with only non-negative weights, have been given to recover decidability. We, first, extend this list by considering arbitrary weights by showing that the value function can be computed in exponential time (if weights are encoded in unary).

Next, in such weighted timed games (like in untimed weighted games in the presence of negative weights), Min may need finite memory to play (close to) optimally. This is thus tempting to try to emulate this finite memory with other strategic capabilities. In particular, we allow the players to use stochastic decisions, both in the choice of transitions and timing delays. We give, for the first time, a definition of the expected value in weighted timed games, overcoming several theoretical challenges. We then show that, in divergent weighted timed games, the stochastic value is indeed equal to the classical (deterministic) value, thus proving that Min can guarantee the same value while only using stochastic choices and no memory.

Finally, even stochastic strategies, almost optimal strategies are not implementable since they use infinite precision of clocks in the choice of the delay or in the knowledge about the configurations. Robustness is a known process to encode the imprecision of delays in strategies: robustness allows to Max player (the opponent of Min) to lightly modify the delay chosen by Min. In the literature, two robust semantics exist: conservative semantic checks a guard after the perturbation, and excessive semantic checks a guard before. As for deterministic strategies, it was known that if Min has a (robust) strategy to guarantee a value lower than a given threshold is known to be undecidable. By adapting the process of value iteration introduced by Alur, we compute the (robust) value in acyclic WTG under conservative and excessive semantics.

This is joint work with Benjamin Monmege and Pierre-Alain Reynier.
Decidability of One-Clock Weighted Timed Games with Arbitrary Weights
(slides)
Weighted Timed Games (WTG for short) are the most widely used model to describe controller synthesis problems involving real-time issues. Unfortunately, they are notoriously difficult, and undecidable in general. As a consequence, one-clock WTGs have attracted a lot of attention, especially because they are known to be decidable when only non-negative weights are allowed. However, when arbitrary weights are considered, despite several recent works, their decidability status was still unknown. In this paper, we solve this problem positively and show that the value function can be computed in exponential time (if weights are encoded in unary).

This is joint work with Benjamin Monmege and Pierre-Alain Reynier.
Playing stochastically in Weighted Timed Games to Emulate Memory
(slides, video of the full presentation with Benjamin Monmege, poster)
Weighted timed games are two-player zero-sum games played in a timed automaton equipped with integer weights. We consider optimal reachability objectives, in which one of the players, that we call Min, wants to reach a target location while minimising the cumulated weight. While knowing if Min has a strategy to guarantee a value lower than a given threshold is known to be undecidable (with two or more clocks), several conditions, one of them being the divergence, have been given to recover decidability. In such weighted timed games (like in untimed weighted games in the presence of negative weights), Min may need finite memory to play (close to) optimally. This is thus tempting to try to emulate this finite memory with other strategic capabilities. In this work, we allow the players to use stochastic decisions, both in the choice of transitions and of timing delays. We give for the first time a definition of the expected value in weighted timed games, overcoming several theoretical challenges. We then show that, in divergent weighted timed games, the stochastic value is indeed equal to the classical (deterministic) value, thus proving that Min can guarantee the same value while only using stochastic choices, and no memory.

This is joint work with Benjamin Monmege and Pierre-Alain Reynier.

Students supervision

Fast termination in timed workflow nets
Jaladhi Joshi (IIT Bombay), intern in second year of the B.Tech. (undergraduate) training of IIT Bombay (summer 2024) with Piotr Hofman.
For a long time, workflows have been modeled by Petri nets having interesting properties such as fast termination, that is to say that all executions are universally linearly bounded in the size of the network. The objective of this internship was to introduce a modeling of these workflows using timed Petri nets and then to study the impact of this extension on the fast termination property in this class of networks.
A Python prototype for the activity about alligators
Antonio Mattar et Tamazouzt Ait Eldjoudi, intern in first year of bachelor (summer 2022) with Benjamin Monmege
The alligator game (description in french) is an activity that introduces lambda calculus through the manipulation of families of alligators representing lambda terms.
Based on the understanding of this activity and the beta-reduction mechanism, this internship aimed to produce a Python prototype to generate alligator families obtained along the beta-reduction of a given lambda term.
This internship was optional for the best L1 students at AMU.

Software project

Implementation in C++ of a prototype to solve one-clock weighted timed games
(Code available on github)
This tool computes the deterministic value function in a one-clock weighted timed game with an algorithm based on the principle of value iteration whose termination is guaranteed by the coding of the finished unfolding provided in our CONCUR22 paper.