Patricia Bouyer-Decitre
# Patricia Bouyer-Decitre

Patricia Bouyer-Decitre (* 18. Oktober 1976) ist eine französische Informatikerin. Für ihre Forschungsarbeit über zeitgesteuerte Automaten wurde sie 2011 mit dem Presburger Award ausgezeichnet.

## Leben

Patricia Bouyer hat an der École normale supérieure de Cachan (1996–1998) studiert und 1999 einen Abschluss in Mathematik (Agrégation) erhalten. Sie promovierte an der ENS Cachan unter der Leitung von Antoine Petit im Jahr 2002 mit einer Arbeit zum Thema "Modelle und Algorithmen für die Verifikation von zeitgesteuerten Systemen". Nach einem Postdoc an der Universität Aalborg wechselte sie zum CNRS, wo sie zunächst wissenschaftliche Mitarbeiterin und ab 2010 Forschungsdirektorin war. Im Rahmen eines Marie-Curie-Stipendiums verbrachte sie 2007 ein Sabbatjahr an der University of Oxford. Sie habilitierte 2009 an der Universität Paris VII für die Leitung von Forschungsarbeiten mit dem Thema "From Qualitative to Quantitative Analysis of Timed Systems".

Seit Januar 2021 ist sie Leiterin des Forschungslabors Laboratoire Méthodes Formelles. Davor war sie Leiterin des Forschungslabors für Informatik Laboratoire spécification et vérification an der ENS. Sie war Vorsitzende der Jury des Gilles-Kahn-Dissertationspreises der Société informatique de France (SIF) (2016–2018). Sie war Principal Investigator (PI) des Starting Grant-Projekts EQualIS (2013–2018) des Europäischen Forschungsrats.

Im Jahr 2007 wurde sie mit der Bronzemedaille des CNRS ausgezeichnet. Im Jahr 2011 wurde sie mit dem Presburger Award der European Association for Theoretical Computer Science (EATCS) ausgezeichnet.

## Arbeiten

Patricia Bouyer arbeitet in der theoretischen Informatik an Problemen, die sich aus der Programmverifikation und dem Model Checking ergeben, wobei sie Werkzeuge aus verschiedenen Bereichen verwendet: endliche Automaten, insbesondere zeitgesteuerte Automaten, verschiedene Logiken wie Modallogiken und insbesondere temporale Logiken, auf Graphenstrukturen; sie interessiert sich für Verifikationslogiken mit Strategien, in einer spieltheoretischen Formulierung, mit Ausarbeitung von Strategien im allgemeineren Rahmen der Multiagentensysteme. Der in diesem Zusammenhang eingeführte Begriff der Energie formalisiert eine Reihe von relevanten Eigenschaften.

Die frühen Forschungsarbeiten von Patricia Bouyer führten zu einer umfassenden Charakterisierung der Echtzeiteigenschaften, die durch die Analyse der Erreichbarkeit von Zeitautomaten im Rahmen von Testautomaten überprüft werden können.

Eines ihrer bekanntesten Ergebnisse betrifft die präzise Charakterisierung von Klassen zeitgesteuerter Automaten, für die das Vakuum-Problem entscheidbar ist. Es wurde 2004 in einer gemeinsamen Arbeit mit Catherine Dufourd, Emmanuel Fleury und Antoine Petit veröffentlicht.

Zusammen mit Antoine Petit und Denis Therien trug sie zur Verallgemeinerung der Grundlagen der Theorie der formalen Sprachen bei, um den Begriff der Zeit durch eine Erweiterung der klassischen Theoreme von Kleene und den Büchi-Automaten einzubeziehen.

Sie hat sich mit der Ausdruckskraft, Entscheidbarkeit und Komplexität von Eigenschaften verschiedener Fragmente und Erweiterungen der temporalen Logik mit Konstrukten für den Umgang mit zeitabhängigen Eigenschaften beschäftigt. Insbesondere löste sie ein lange offenes Problem bezüglich der vergleichenden Aussagekraft zweier solcher Standardlogiken, das gemeinsam mit Fabrice Chevalier und Nicolas Markey veröffentlicht wurde.

Ein Übersichtsartikel über die Modellprüfung von Echtzeitsystemen wurde 2018 veröffentlicht.

Energiegetaktete Automaten (energy timed automata) sind ein wichtiges Thema in der Forschung von Patricia Bouyer und ihren Mitautoren. Diese Automaten erweitern zeitgesteuerte Automaten um eine kontinuierliche Energievariable, die sich mit variabler Geschwindigkeit und diskreten Aktualisierungen während der Entwicklung des Modells entwickelt. Die kontinuierlichen und diskreten Veränderungen können positiv oder negativ sein und sogar mit einem gewissen Grad an Unsicherheit behaftet sein. Für die akkumulierte Energie kann es Ober- und Untergrenzen geben, die Kapazitätsbeschränkungen widerspiegeln. In diesem Zusammenhang ist das Problem der Existenz von unendlichen (Lauf-)Berechnungen entscheidbar.

