Patricia Bouyer-Decitre

Élève de l'ENS Cachan (1996-1998)[1] - [2], elle passe l'agrégation de mathématiques en 1999, puis soutient en 2002, sous la direction d'Antoine Petit[3] une thèse intitulée « Modèles et algorithmes pour la vérification des systèmes temporisés ». Elle entre ensuite au CNRS, après un postdoc à l'université d'Aalborg, où elle est successivement chargée de recherche, puis directrice de recherche à partir de 2010. Elle passe une année sabbatique en 2007 à l'université d'Oxford sur une bourse Marie Curie. Elle obtient son habilitation à diriger des recherches en 2009 à l'université Paris 7[2] avec un travail intitulé From Qualitative to Quantitative Analysis of Timed Systems[1].

Elle est directrice du Laboratoire Méthodes Formelles depuis janvier 2021. Elle a été directrice adjointe puis directrice du Laboratoire spécification et vérification. Elle préside le jury du prix de thèse Gilles Kahn de la Société informatique de France (SIF) (2016-2018). Elle est Principal Investigator (PI) du « Starting grant project » ERC EQualIS (2013-2018)[4].

En 2007 elle obtient la médaille de bronze du CNRS[5]. Le prix Presburger de l'EATCS lui est attribué en 2011[2].

Patricia Bouyer travaille en informatique théorique, sur des problèmes issus de la vérification de programmes et du model checking, en utilisant des outils d'horizons variés : les automates finis, en particulier les automates temporisés, diverses logiques comme les logiques modales et en particulier temporelles, sur des structures de graphes ; elle s'intéresse aux logiques de vérification avec stratégies, dans une formulation en théorie de jeux, avec élaboration de stratégies dans le cadre plus général d'évolutions multi-agents. Le concept d'énergie introduit dans ce contexte formalise un certain nombre de propriétés pertinentes.

Les premières recherches de Patricia Bouyer ont conduit à une caractérisation complète des propriétés de temps réel qui peuvent être vérifiées par l'analyse de l'accessibilité des automates temporisés dans le contexte d'automates de test[6].

L'un de ses résultats les plus connus concerne la caractérisation précise des classes d'automates temporisés pour lesquelles le problème du vide est décidable, publié en 2004 dans un article conjoint avec Catherine Dufourd, Emmanuel Fleury et Antoine Petit[7].

Elle a contribué, avec Antoine Petit et Denis Therien[8], à la généralisation des fondamentaux de la théorie des langages formels pour inclure la notion du temps, par une extension des théorèmes classiques de Kleene et Buchi.

Elle a travaillé sur l'expressivité, la décidabilité et la complexité des propriétés de divers fragments et extensions de la logique temporelle munies de constructions pour traiter des propriétés en fonction du temps. Elle a notamment résolu un problème longtemps ouvert concernant l'expressivité comparative de deux de ces logiques standard, publiées conjointement avec Fabrice Chevalier et Nicolas Markey[9].

Un article de synthèse sur le model checking de systèmes temps réel est paru en 2018[10].

Les automates temporisés à énergie (energy timed automata) sont un des thèmes importants des recherches de Bouyer et ses coauteurs[11]. Ces automates étendent les automates temporisés avec une variable continue d'énergie qui évolue à vitesse variable avec des mises à jour discrètes au cours de l'évolution du modèle. Les variations continues et discrètes peuvent être positives ou négatives,et même être sujettes à un certain degré d'incertitude. L'énergie accumulée peut être sujette à des bornes supérieures et inférieures, reflétant des contraintes de capacité. Dans ce contexte, le problème de l'existence de calculs (run) infini est décidable[12].

• Site officiel
• Ressources relatives à la recherche :
  • Google Scholar
  • (en) Digital Bibliography & Library Project
  • (en) Mathematics Genealogy Project
  • (en) ORCID
• Notices d'autorité :

  • VIAF
  • ISNI
  • IdRef
  • LCCN
  • Israël
  • Norvège
  • Tchéquie
  • WorldCat