Patricia Bouyer-Decitre
Pour les articles homonymes, voir Bouyer (homonymie).
| Naissance | |
|---|---|
| Nationalité | |
| Formation | |
| Activités |
| A travaillé pour |
Laboratoire Albert-Fert CNRS Délégation Île-de-France Sud (d) |
|---|---|
| Directeur de thèse |
Antoine Petit (d) |
| Site web | |
| Distinctions |
Patricia Bouyer-Decitre est une chercheuse française en informatique, née le . Elle a obtenu le prix Presburger en 2011, pour ses travaux sur les automates temporisés.
Biographie
[modifier | modifier le code]É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].
Travaux
[modifier | modifier le code]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].
Notes et références
[modifier | modifier le code]- Patricia Bouyer, « Curriculum vitæ »
- « Presburger Award 2011 », sur EATCS
- (en) « Patricia Bouyer », sur le site du Mathematics Genealogy Project.
- « BOUYER-DECITRE Patricia, CV », sur lsv.fr, (consulté le )
- « « Talents » Médaille de bronze du CNRS Palmarès 2007. Patricia Bouyer : la vérification au quotidien », sur CNRS.
- Luca Aceto, Patricia Bouyer, Augusto Burgueño et Kim G Larsen, « The power of reachability testing for timed automata », Theoretical Computer Science, vol. 300, nos 1-3, , p. 411–475 (ISSN 0304-3975, DOI 10.1016/S0304-3975(02)00334-1).
- Patricia Bouyer, Catherine Dufourd, Emmanuel Fleury et Antoine Petit, « Updatable timed automata », Theoretical Computer Science, vol. 321, nos 2-3, , p. 291–345 (ISSN 0304-3975, DOI 10.1016/j.tcs.2004.04.003).
- Patricia Bouyer, Antoine Petit et Denis Thérien, « An Algebraic Approach to Data Languages and Timed Languages », Information and Computation, vol. 182, no 2, , p. 137-162 (lire en ligne)
- Patricia Bouyer, Fabrice Chevalier et Nicolas Markey, « On the Expressiveness of TPTL and MTL », Information and Computation, vol. 208, no 2, , p. 97-116 (DOI 10.1016/j.ic.2009.10.004, lire en ligne)
- Patricia Bouyer, Uli Fahrenberg, Kim Guldstrand Larsen, Nicolas Markey, Joël Ouaknine et James Worrell, « Model Checking Real-Time Systems », dans E. Clarke, T. Henzinger, E. Veith, R. Bloem (éditeurs), Handbook of Model Checking, Springer, (ISBN 978-3-319-10575-8, DOI 10.1007/978-3-319-10575-8_29, lire en ligne), p. 1001-1046
- Patricia Bouyer, Uli Fahrenberg, Kim G. Larsen, Nicolas Markey et Jiří Srba, « Infinite Runs in Weighted Timed Automata with Energy Constraints », Lecture Notes in Computer Science, vol. 5215 « FORMATS 2008 », , p. 33–47 (ISSN 0302-9743, DOI 10.1007/978-3-540-85778-5_4, lire en ligne)
- Giovanni Bacci, Patricia Bouyer, Uli Fahrenberg, Kim Guldstrand Larsen, Nicolas Markey et Pierre-Alain Reynier, « Optimal and Robust Controller Synthesis », Lecture Notes in Computer Science, vol. 10951 « FM'18 », , p. 203–221 (ISSN 0302-9743, DOI 10.1007/978-3-319-95582-7_12, lire en ligne)
Liens externes
[modifier | modifier le code]
- Site officiel
- Ressources relatives à la recherche :
