Mes publications

Rapports - thèse

Mes présentations
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.
  • Réunion de fin de projet de l'ANR TickTac, Juin 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 de la présentation avec 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.

Encadrement

Un prototype Pyhton pour l'activité des alligators
Antonio Mattar et Tamazouzt Ait Eldjoudi, stagiaires de L1 (été 2022) avec Benjamin Monmege
Le jeu des alligators est une activité permettant d'introduire le lambda-calcul via la manipulation de familles d'alligators représentant les lambda-termes.
Basé sur la compréhension de cette activité et de la beta-réduction, l'objectif de ce stage était de produire un prototype Python afin de produire les familles d'alligators générées par la réduction d'un lambda-terme~donné.
Ce stage était un stage facultatif proposée aux meilleurs étudiants en L1 à AMU.

Activités administratives et tâches collectives

Élue au conseil du département informatique et interactions d'AMU
représentante des doctorants CD-CME et ATER du département
Participation aux conseils mensuel du département. Outre les questions usuelles (budget, recrutement, ...), j'ai également participé aux discussions sur l'évaluation des formations par l'HCERES du département ainsi qu'aux premières discussions sur la construction de la future maquette pour la rentrée 2024.
Membre du comité d'organisation de STACS 2022
Due au Covid, la conférence STACS 2022 à eu lieu en ligne. J'ai principalement géré les problèmes techniques pouvant survenir pendant la visio-conférence comme, par exemple, vérifier que chacun des orateurs pouvait utiliser Zoom sans problèmes.
Membre du comité d'évaluation des artéfacts de FORMATS 2023
Évaluation des artéfacts utilisés pour obtenir les résultats calculatoires publiés à FORMATS 2023 (soumission à la discrétion des auteurs des papiers acceptés comportant de tels résultats). En particulier, cette évaluation n'influe pas sur l'acceptation du papier à la conférence. Les objectifs de cette évaluation sont les suivants:
  • reporduire les résultats énoncés dans les articles;
  • trouver d'éventuelles erreurs dans l'implémentation du logiciel;
  • commenter la documentation et l'utilisabilité des artéfacts soumis.

Production logicielle

Implémentation en C++ d'un prototype pour résoudre les jeux temporisé à coût à une horloge
(Code disponible sur github)
Cet outil calcul la fonction de valeur déterministe dans un jeu tempoisé à une horloge avec un algorithme basé sur le principe de value iteration dont la terminaison est assurée par le codage du dépliage fini fourni dans notre papier CONCUR22.

Vulgarisation scientifique

Exposé invité à l'école des Cigales
(Avril 2023 - CIRM)
Partiticpation à l'école de mathématiques du printemps 2023 en donnant un exposé sur la théorie des jeux dans le cadre de la synthèse de programme (slides).
L'école mathématiques les Cigales s'adresse aux lycéennes en classe de 1ère afin d'y développer l'attractivité des mathématiques et de l'informatique auprès des jeunes filles. Pendant cinq jours, les lycéennes découvrent les mathématiques et l'informatique au travers de la résolution de problèmes mathématiques ou informatique, et de la rencontre de mathématiciennes et informaticiennes lors de conférences.

Informatique débranchée

Pendant ma scolarité à l'ENS, j'ai pu animer puis créer des séances d'activités d'informatique d'environ 1h débranché pour des classes de primaire. Ce travail a été réalisé avec Hippolyte Bourel, Santiago Bautista et Quentin Le Dilavrec.

La ville embourbée

Cette activité est une approche du problème d'arbre couvrant d'un graphe. Les élèves ont pour objectif de paver une ville (le graphe pondéré par le nombre de pavé sur les chemins) en utilisant le moins de pavés possible.

L'activité se divise en trois phases: l'introduction et le premier recouvrement du graphe, la recherche de la meilleur solution et la retranscription de la solution finale. L'introduction permet de poser le contexte de l'activité et le premier recouvrement nous permet de vérifier que les élèves ont bien compris ce qu'est un recouvrement de graphe. Une fois ce premier recouvrement effectué, les élèves, par petits groupes, cherchent la solution. Dans la majorité des cas, tous les groupes arrivent à la solution (les derniers pavés demandent quelques fois un peu d'aide extérieure). Une fois que le groupe possède leur solution, on demande à chaque élève de colorier sur leur plan personnelle la solution du groupe. Ce temps est important, il permet de remmettre tous les groupes au même niveau et de calmer les élèves après la recherche (parfois exigente).

Lorsque nous avons fait tourné l'activité en classe, nous avons remarqué que les élèves adhèrent très vite à l'activité, sutout grâce à la contextualisation de l'activité. Cette activité nous permet de plus de parler de réseaux informatiques et les idées principales de l'algorithme de Dijkstra appliquées sur la ville.

Documents pour l'activité: fiche professeur, une ville.
Basée sur le livre Computer Science Unplugged de Tim Bell, Ian H. Witten et Mike Fellow

Image

Cette activité Images est une première approche de la notion d'image et sa représentation. Le but de cette activité est le codage d'image monochromatique. Dans cette activité l'image codée par une suite d'entier indiquant le nombre de pixel blanc puis le nombre de pixel noir.

Après l'introduction, notament de la notion de pixel, l'activité se découpe en deux parties: décoder une image, puis coder sa propre image. La première partie permet aux élèves de bien comprendre comment fonctionne le codeage. Nous avons donné aux élèves trois exemples, cela leur permet d'avancer à leur rythme. Une fois que le premier exemple a été corrigé en classe entière, les élèves préparent la leur. Une fois cette image codée, on fait des échanges deux à deux pour que leur camarade décode leur image. On compare ensuite l'image originale à l'image décodée.

Lorsque nous avons fait tourné sur la classe, nous avons été étonnée par la connaissance de la notion de pixel des élèves. De plus la vitesse de coloriage est le plus grand frein à cette activité, et peu devenir une difficulté à cette activité. Elle nous a permis de parler du codage RVB des images en comparant cette méthode à la peinture.

Basée sur le travail de l'IREM de Clermont-Férrand.

L'île au trésor

Cette activité L'île au trésor est une activité que nous avons imaginés pour introduire la vérification formelle à des primaires. Elle se décline en trois sous-activités: la modélisation, la vérfication et l'introduction à la logique.

Le but de cette activité est de retrouver l'île sur laquelle un pirate à cacher son trésor. Pendant l'activité de la modélisation, les élèves doivent représenter les îles sous formes de graphe à partir de textes descriptifs. Ensuite, l'activité de vérification permet de choisir la bonne île correspondant à celle vérifiant toutes les phrases données aux élèves. Ces phrases décrivent des propriétés de plus en plus complexes sur les graphes des îles. Enfin, pour introduire la logique, nous proposons une activité de codage qui permet d'encoder avec les symboles de la logique les propriétés sur les graphes.

Je n'ai pas fait tournée cette activité en classe mais les travaux préliminaires sont disponible ici.

Enseignements

Au département Informatique et Intéractions d'Aix-Marseille Université
(2020 - 2023)
  • Système d'exploitation, TD/TP, Licence 2, 2021-2023
  • Architecture des ordinateurs, TD/TP, Licence 2, 2021-2023
  • Probabilité pour l'informatique, TD/TP, Master 1, 2022-2023
  • Introduction à l'informatique, TD, Licence 1, 2020-2022
  • Projet d'introduction au génie logiciel, TP, Licence 2, 2020-2022
  • Automates finis, TD/TP, Licence 2, 2020-2021
À l'ISTIC de l'université Rennes 1
(2016)
10 heures de tutorat pour les étudiants de première année des licences Informatique, Mathématiques, Électronique et MIAGE pour l'UE Algorithme et Programmation Fonctionnelle. L'objectif de ces heures était de répondre aux questions des étudiants volontaires sur la compréhension et l'écriture de programmes récursifs (sur différentes structures inductives: les entiers, les arbres, ...) en LISP.

Stages d'initiation à la recherche

Voici un résumé des stages que j'ai réalisés pendant mon cursus.

Stochastic Strategies in Quantitative or Timed Games

De janvier 2020 à juillet 2020, j'ai effectué un stage de recherche à Aix-Marseille Université sous la direction de Pierre-Alain Reynier et Benjamin Monmege. Lors de ce stage, je travaille sur un problème issu de la théorie des jeux. L'objectif est d'étudier un compromis entre la mémoire et les probabilités utilisées dans les stratégies de jeux quantitatifs ou temporisés à coût. Voici mon rapport bibliographique (en anglais) et les slides de la présentation (en anglais), ainsi que mon rapport de stage (en anglais) et les slides de la présentation.

Selective Monitoring

De mai 2018 à août 2018, j'ai effectué un stage d'initiation à la recherche à l'université d'Oxford sous la direction de Stefan Kiefer. Lors de ce stage, j'ai travaillé sur un problème de monitoring sur des automates probabilistes. L'objectif était de trouver une stratégie d'observation de notre automate minimisant l'information observée mais décidant, dès que possible, la présence ou non d'erreurs. Puis nous avons essayer de classifier ce problème. Voici mon rapport (en anglais) et les slides de la présentation (en anglais).

Ce stage a été également l'occasion d'assiter à la conférence FLOC 2018 en
tant que bénévole. J'ai alors pu découvrir une conférence (du côté de l'organisation et du côté de l'auditeur). Cette expérience a été très enrichissante et a été l'occasion, pour moi, de rencontrer des chercheurs de la communauté. Je remercie Stefan Kiefer de son accueil, son temps, nos interractions ainsi que les opportunités qu'il m'a offert (notamment avec la conférence FLOC).

Model checking rail networks

De septembre 2017 à avril 2018, nous effectuons un stage (sous forme de projet), en trinôme avec Benjamin Bordais et Thomas Mari, à hauteur d'une demi-journée par semaine dans l'équipe SUMO sous la supervision de Ocan Sankur, de Loïc Hélouët et de Nathalie Bertrand. Pendant ce stage, nous cherchons à modéliser et à verifier les régulations dans les réseaux ferroviaires urbains. Pour ce faire, nous utilisons des modèles probalisitics (DTMC et MDP) afin de modéliser les retards aléatoires dans nos rése  aux de métros. L'objectif de ce stage est d'évaluer les performances d'une politique de régulation donnée, et/ou de construire (extraire) de nouvelles politiques de régulation optimales.

Lors du premier semestre nous avons effectué une étude bibliograohique sur le sujet: les modèles et la vérification avec des MDP et des DTMC, la modélisation de réseaux ferroviaires afin d'en étudier le retard et les outils PRISM et Storm. Voici le rapport (en anglais) pour cette première partie du travail ainsi que les slides de notre présentation (en anglais). Le second semestre est consacré à la recherche afin d'atteindre nos objectifs de modélisation d'un réseau ferroviaires simple avec une politique de régulation pour réguler les retards. Voici le rapport (en anglais) pour cette deuxième partie du travail ainsi que les slides de notre présentation (en anglais). Ce travail a été conclut par la publication de notre travail à RSSRail 2019 (article).

Ce stage est pour moi très interressant tant au niveau scientifique (par le domaine et les méthodes de travail que nous apprenons à mettre en place) que humainement. En effet, il a été l'occasion de rencontré plusieurs personnes impliquées dans cette communauté et prêtent à partager leur savoir, ce qui a été très attractif. Je remercie nos encadrants Ocan Sankur, Loïc Hélouët et Nathalie Bertrand pour leur acceil, leur temps et nos interractions qui continues de beaucoup m'appris.


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

De mi-mai à mi-juillet 2017, j'ai effectué un stage d'initiation à la recherche à l'Inria Rhône-Alpes à Grenoble sous la direction d'Hubert Garavel. Pendant ce stage, j'ai étudié les outils permettant la vérification des systèmes probabilistes. Notre objectif était d'obtenir une base de donnée pour ces outils contenant des informations sur leurs caractéristiques: les auteurs, leur version et status, les modèles et logiques supportées, ainsi que des modèles publiés à titre d'exemple. Lorsque ces données ont été récoltées, nous avons organiser sur une page web les informations sur les outils. De plus, nous avons écrit un script permettant d'avoir une première approximation des caractéristiques de nos modèles afin de commencer à les classer. Ce travail a aboutit sur la rédaction d'un rapport et d'une soutenance. Je remercie Hubert Garavel et l'équipe Inria Convecs pour leur acceuil, leur temps et nos interractions qui m'ont beaucoup apportées.