Mes publications

Reports- thesis

My presentations
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.
Robustness in Weighted Timed Games
(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.
  • End of project meeting of ANR TickTac, June 2023
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, teaser, 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

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.

Administrative activities and collective tasks

Elected to the council of the Department of Computer Science and Interactions of AMU
representative of the department’s PhD students  and ATER
Participation in monthly departmental councils. In addition to the usual questions (budget, recruitment, etc.), I also participated in discussions on the evaluation by HCERES of the department's training as well as in the first discussions on the construction of the future model of trainings for the start of the 2024 university year.
Member of organisation comitee of STACS 2022
Due to Covid, the STACS 2022 conference took place online. I mainly managed technical problems that could arise during the videoconference, such as, for example, checking that each of the speakers could use Zoom without problems.
Member of Artefacts Evaluation comitee of FORMATS 2023
Evaluation of the artefacts used to obtain the computational results published at FORMATS 2023 (submission at the discretion of the authors of accepted papers containing such results). In particular, this evaluation does not influence the acceptance of the paper at the conference. The objectives of this evaluation are:
  • reproduce the results stated in the articles;
  • find possible errors in the software implementation;
  • comment on the documentation and usability of the submitted artefacts.

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.

Scientific mediation

Invited presentation at the Cigales school
(April 2023 - CIRM)
Participation in the spring 2023 mathematics school by giving a presentation on game theory as part of the program synthesis (slides, in French).
The Cigales Mathematics School is aimed at girls in 2nd year of high school to develop the attractiveness of mathematics and computer science among young girls. For five days, high school girl students discover mathematics and computer science by solving mathematical or computer science problems and meeting mathematicians and computer women scientists during conferences.
Creation of an unplugged activity on formal verification with Santiago Bautista and Quentin Le Dilavrec
(2019-2020 - ENS Rennes)
Preparation of an activity for primary school pupils to introduce formal verification. The activity's objective is to find treasure hidden by pirates using text descriptions of several possible islands. This activity is divided into three sub-activities (which can be carried out independently):
  • modelling: produce a graph for each of the possible islands from a textual description of each of the islands;
  • verification: find the island where the treasure is hidden using the textual information from the pirate who hid the treasure;
  • introduction to logic: encode/decode the pirate's textual indications.
The material produced during this work is available here.
Animation of unplugged activities around computer science in primary classes with Hippolyte Bourel
(2016 - 2017 - ENS Rennes)
Presentation of computer science concepts to primary school students without using computers. On this occasion, we presented two activities:
  • The mired city activity based on the book Computer Science Unplugged of Tim Bell, Ian H. Witten and Mike Fellow. It introduces the spanning tree problem of a graph. The students aim to pave a city in such a way that one can always reach a house via a paved path (weights in the graph of the city are given by the number of paving stones on the paths) using as few paving stones as possible.
    Documents (in French) for the activity; sheet teacher, a city.;
  • The Picture activity based on the work of IREM de Clermont-Férrand. It introduces the coding of a monochromatic image in a computer with the notion of pixel and sequence of pixels. In this activity, the picture is coded by a series of integers indicating the number of white pixels and then the number of black pixels. Students draw a given coded picture before producing their own coded pictures.

Teaching

At the Computer Science and Interactions department of AMU
(2020 - 2023)
  • Operating systems, tutorials - practical sessions, 2nd year of Bachelor, 2021-2023
  • Architecture of computers, tutorials - practical sessions, 2nd year of Bachelor, 2021-2023
  • Probabilities for computer science, tutorials - practical sessions, 1st year of Master, 2022-2023
  • Introduction to computer science, tutorials, 1st year of Bachelor, 2020-2022
  • Projet: introduction to software engineering, practical sessions, 2nd year of Bachelor, 2020-2022
  • Finite automata, tutorials - practical sessions, 2nd year of Bachelor, 2020-2021
At ISTIC in Rennes 1 University
(2016)
10 hours of tutoring for first-year students of Computer Science, Mathematics, Electronics and MIAGE degrees for the Algorithm and Functional Programming course. The objective of these hours was to answer questions from volunteer students on understanding and writing recursive programs (on different inductive structures: integers, trees, etc.) in LISP.

Research interships

Stochastic Strategies in Quantitative or Timed Games

From January 2020 to July 2020, I did a research internship at Aix-Marseille University under the supervision of Pierre-Alain Reynier and Benjamin Monmege. During this internship, I worked on a problem stemming from game theory. The objective is to study a compromise between memory and the probabilities used in the strategies of quantitative or timed games at cost. Here are my bibliographic report and the slides of the presentation, as well as my internship report and the slides of the presentation.

Selective Monitoring

From May 2018 to August 2018, I did an introductory research internship at the University of Oxford under the supervision of Stefan Kiefer. During this internship, I worked on a monitoring problem on probabilistic automatons. The objective was to find a strategy for minimizing the observations on our automation but deciding, as soon as possible, the presence or absence of errors. Then we tried to classify this problem. Here is my report and the slides of the presentation.

This internship was also the opportunity to attend the FLOC 2018 conference as a volunteer. I was then able to discover a conference (on the side of the organization and the side of the auditor). This experience was very enriching and was the opportunity for me to meet researchers from the community. I would like to thank Stefan Kiefer for his welcome, his time, our interactions as well as the opportunities he offered me (especially with the FLOC conference).

Model checking rail networks

With Benjamin Bordais and Thomas Mari, we make an intership (research project) during our first year of master degree.  Ocan Sankur, Loïc Hélouët and Nathalie Bertrand welcom us in their team, SUMO (IRISA/Inria Rennes) a half of a day per week. In this project, we work modelisation, verification and regulation of urban train networks. To do so, we use probabilistic models (DTMC, MDP) to reflect the unpredictable delays of metros. The objective is to evaluate the performances of given regulation policies, or to design new optimal regulation policies.

During the first semester, we create a bibliography. So, we have read some research articles about verification with MDP or DTMC, dalays of rail networks modelisation PRISM, Storm tools. This work was concluded by a report and a presentation (here our slides). During the second semester, we will reach our goals.

This project interested me both for the scientific topic and for the human aspect. It allows me to meet exciting people and improve my knowledge about interesting subjects. I want to thanks our supervisors Nathalie Bertrand, Loïc Hélouët and Ocan Sankur for their time, their accomodation and their help all along this year.

Panorama des modèles et outils de vérification pour les systèmes probabilistes

In summer 2017, I made a resaerch intership in Grenoble (Inria Rhône-Alpes) supervized by Hubert Garavel. I Have study the verification tools for the probabilistic systems. Our goal was build a tools databases with their caracterisitcs: authors, versions, models and logic used, published examples. Datas are stocked and organised on this webpage. Moreover, I wrote a script (caracteristics based) to sort data. This work has concluded by a report (in French) and a presentation (in French). I want to
thinks Hubert Garavel and Convecs Inria team for their welcom, their tims and our discussion all along this intership.