« Patricia Bouyer-Decitre » : différence entre les versions
→Lien externes : mieux |
+ Travaux |
||
| Ligne 11 : | Ligne 11 : | ||
== Travaux == |
== Travaux == |
||
Bouyer-Decitre travaille notamment sur les [[Problème d'accessibilité|problèmes d'accessibilité]] des [[automate temporisé|automates temporisés]] et les [[logique temporelle|logiques temporelles]]<ref name=presburger/>. |
Bouyer-Decitre travaille notamment sur les [[Problème d'accessibilité|problèmes d'accessibilité]] des [[automate temporisé|automates temporisés]] et les [[logique temporelle|logiques temporelles]]<ref name=presburger/>. == Travaux == |
||
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 [[Automate fini|automates finis]], en particuliers les [[Automate temporisé|automates temporises]], diverses logiques comme la [[logique modale]], sur des structures de [[Graphe (mathématiques discrètes)|graphes]] ; elle s'intéresse aux logiques de vérification avec stratégies, dans une formulation en [[Théorie des jeux|théorie de jeux]], avec élaboration de stratégies dans le cadre plus général d'[[Système multi-agents|évolutions multi-agents]]. Le concept d'énergie introduit dans ce contexte formalise un certain nombre de propriétés relevantes. |
|||
| ⚫ | |||
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<ref name="AcetoBouyer2003">{{cite journal|last1=Aceto|first1=Luca|last2=Bouyer|first2=Patricia|last3=Burgueño|first3=Augusto|last4=Larsen|first4=Kim G|title=The power of reachability testing for timed automata|journal=Theoretical Computer Science|volume=300|issue=1-3|year=2003|pages=411–475|issn=0304-3975|doi=10.1016/S0304-3975(02)00334-1}}.</ref>. |
|||
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écidabilité|décidable]], publie en 2004 dans un article conjoint avec Catherine Dufourd, Emmanuel Fleury et Antoine Petit<ref name="BouyerDufourd2004">{{cite journal|last1=Bouyer|first1=Patricia|last2=Dufourd|first2=Catherine|last3=Fleury|first3=Emmanuel|last4=Petit|first4=Antoine|title=Updatable timed automata|journal=Theoretical Computer Science|volume=321|issue=2-3|year=2004|pages=291–345|issn=0304-3975|doi=10.1016/j.tcs.2004.04.003}}.</ref>. |
|||
Elle a contribué, avec Antoine Petit et Denis Therien<ref>{{article |
|||
| auteur1= Patricia Bouyer |
|||
| auteur2= Antoine Petit |
|||
| auteur3= Denis Thérien |
|||
| titre = An Algebraic Approach to Data Languages and Timed Languages |
|||
| journal = Information and Computation |
|||
| volume = 182 |
|||
| numéro = 2 |
|||
| page = 137-162 |
|||
| année = 2003 |
|||
| url = https://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BPT-IetC.pdf}}</ref>, à la généralisation des fondamentaux de la [[Langage formel|théorie des langages formels]] pour inclure la notion du temps, par une extension des [[Théorème de Kleene|théorèmes classiques de Kleene]] et [[Automate de Büchi|Buchi]]. |
|||
Elle a travaillé sur l'expressivité, la [[décidabilité]] et la [[Complexite algorithmique|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<ref>{{article |
|||
| auteur1= Patricia Bouyer |
|||
| auteur2= Fabrice Chevalier |
|||
| auteur3= Nicolas Markey |
|||
| titre = On the Expressiveness of TPTL and MTL |
|||
| journal = Information and Computation |
|||
| volume = 208 |
|||
| numéro = 2 |
|||
| page = 97-116 |
|||
| année = 2010 |
|||
| url = http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BCM-icomp09.pdf |
|||
| doi = 10.1016/j.ic.2009.10.004}} |
|||
</ref>. |
|||
Un article de synthèse sur le model checking de systèmes temps réel est paru en 2018<ref>{{chapitre |
|||
|auteur1 = Patricia Bouyer|auteur2 = Uli Fahrenberg|auteur3 = Kim Guldstrand Larsen|auteur4 = Nicolas Markey|auteur5 = Joël Ouaknine|auteur6 = James Worrell |
|||
|titre = Model Checking Real-Time Systems |
|||
|titre ouvrage = Handbook of Model Checking |
|||
|année = 2018 |
|||
|passage = 1001-1046 |
|||
|auteurs ouvrage = E. Clarke, T. Henzinger, E. Veith, R. Bloem (éditeurs) |
|||
|éditeur = Springer |
|||
|isbn = 978-3-319-10575-8 |
|||
|doi = 10.1007/978-3-319-10575-8_29 |
|||
|url=https://www.lsv.fr/Publis/PAPERS/PDF/BFLMOW-hmc17.pdf |
|||
}}</ref> |
|||
Les automates temporisés à énergie (''energy timed automata'') sont un des thèmes importants des recherches de Bouyer et ses coauteurs<ref name="BouyerFahrenberg2008">{{cite journal |
|||
|last1=Bouyer|first1=Patricia|last2=Fahrenberg|first2=Uli|last3=Larsen|first3=Kim G.|last4=Markey|first4=Nicolas|last5=Srba|first5=Jiří |
|||
|title=Infinite Runs in Weighted Timed Automata with Energy Constraints |
|||
|périodique= Lecture Notes in Computer Science |
|||
|volume=5215|year=2008|pages=33–47|issn=0302-9743|doi=10.1007/978-3-540-85778-5_4 |
|||
|titre volume = FORMATS 2008 |
|||
|url=https://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BFLMS-formats08.pdf |
|||
}}</ref>. 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<ref name="BacciBouyer2018">{{cite journal |
|||
|last1=Bacci|first1=Giovanni |
|||
|last2=Bouyer|first2=Patricia |
|||
|last3=Fahrenberg|first3=Uli |
|||
|last4=Larsen|first4=Kim Guldstrand |
|||
|last5=Markey|first5=Nicolas |
|||
|last6=Reynier|first6=Pierre-Alain |
|||
|title=Optimal and Robust Controller Synthesis |
|||
|périodique= Lecture Notes in Computer Science |
|||
|volume=10951 |
|||
|titre volume = FM'18 |
|||
|year=2018 |
|||
|pages=203–221 |
|||
|issn=0302-9743 |
|||
|doi=10.1007/978-3-319-95582-7_12 |
|||
|url=https://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BBFLMR-fm18.pdf |
|||
}}</ref>. |
|||
| ⚫ | |||
{{Références}} |
{{Références}} |
||
== Lien externes == |
== Lien externes == |
||
* {{lien web|titre=Page web de Patricia Bouyer-Decitre|url=http://www.lsv.fr/~bouyer/}} |
* {{lien web|titre=Page web de Patricia Bouyer-Decitre|url=http://www.lsv.fr/~bouyer/}} |
||
* [https://dblp.uni-trier.de/pers/hd/b/Bouyer:Patricia Publications de Patricia Bouyer] sur [[DBLP]] |
|||
* {{Autorité}} |
|||
* {{Bases recherche}} |
|||
{{Palette Lauréats du prix Presburger}} |
{{Palette Lauréats du prix Presburger}} |
||
{{Portail|informatique théorique}} |
{{Portail|informatique théorique}} |
||
Version du 14 septembre 2018 à 06:31
Patricia Bouyer-Decitre est une chercheuse en informatique. Elle a obtenu le prix Presburger en 2011, pour ses travaux sur les automates temporisés.
Biographie
Patricia Bouyer est née le 18 octobre 1976[1],[2]. Elle étudie à l'ENS Cachan (1996-1998) et passe l'agrégation de mathématiques en 1999. Elle obtient son doctorat, toujours à l'ENS Cachan, sous la direction d'Antoine Petit en 2002[3] avec 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 fellowship . 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 adjointe du Laboratoire spécification et vérification. Elle est présidente du 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).
En 2007 elle obtient la médaille de bronze du CNRS[4]. Le prix Presburger de l'EATCS lui est attribué en 2011[2].
Travaux
Bouyer-Decitre travaille notamment sur les problèmes d'accessibilité des automates temporisés et les logiques temporelles[2]. == Travaux ==
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 particuliers les automates temporises, diverses logiques comme la logique modale, 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 relevantes.
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[5].
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, publie en 2004 dans un article conjoint avec Catherine Dufourd, Emmanuel Fleury et Antoine Petit[6].
Elle a contribué, avec Antoine Petit et Denis Therien[7], à 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[8].
Un article de synthèse sur le model checking de systèmes temps réel est paru en 2018[9]
Les automates temporisés à énergie (energy timed automata) sont un des thèmes importants des recherches de Bouyer et ses coauteurs[10]. 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[11].
Notes et références
- Patricia Bouyer, « Curriculum vitæ »
- « Presburger Award 2011 », sur EATCS
- (en) « Patricia Bouyer », sur le site du Mathematics Genealogy Project.
- « « 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)
Lien externes
- « Page web de Patricia Bouyer-Decitre »
- Publications de Patricia Bouyer sur DBLP
- Ressources relatives à la recherche :
