Patricia Bouyer-Decitre

Patricia Bouyer-Decitre (published as Patricia Bouyer, born 1976) is a French theoretical computer scientist known for her research on timed automata, model checking, and temporal logic. She is a senior researcher for the French National Centre for Scientific Research (CNRS), and director of the Laboratoire Méthodes Formelles (Formal Methods Lab) of CNRS and the École normale supérieure Paris-Saclay.

Education and career Patricia Bouyer was born in 1976. She became a student at ENS Paris-Saclay (known at that time as ENS Cachan) in 1996, earning a maîtrise (master's degree) in mathematics in 1997, a second maîtrise and diplôme d'études approfondies in computer science in 1998, and passing the agrégation in mathematics in 1999.

She completed her Ph.D. in 2002 at the Laboratoire Spécification et Vérification of CNRS and ENS Cachan; her dissertation, Modèles et Algorithmes pour la Vérification des Systèmes Temporisés (Models and Algorithms for the Verification of Timed Systems), was supervised by . She completed a habilitation at Paris Diderot University in 2009, with the habilitation thesis From Qualitative to Quantitative Analysis of Timed Systems.

She was a postdoctoral researcher at Aalborg University in 2002, and also in 2002 became a junior researcher for CNRS. She was promoted to senior researcher in 2010.

Contributions Bouyer is known for several significant results on timed automata. In work beginning in 1997, and culminating in a 2003 publication with Luca Aceto, Augusto Burgueno and Kim Larsen, Bouyer characterized the properties that can be described in terms of reachability in timed automata. With Petit and Denis Thérien, she found analogues of Kleene's theorem for timed automata, showing their equivalence with certain classes of formal languages. With Catherine Dufourd, Emmanuel Fleury and Antoine Petit, she introduced updatable timed automata, extensions of timed automata with operations that update the timing variables rather than merely resetting them to zero, and found several important subclasses of these automata for which the emptiness problem is decidable.

In temporal logic, Bouyer worked with Fabrice Chevalier and Nicolas Markey to prove the greater expressiveness of one form of temporal logic, timed propositional temporal logic, over another, metric temporal logic. Other topics in her research include the application of timed automata to fault detection, the addition of costs and energy constraints to timed automata, and the existence of Nash equilibria in timed versions of game theory.

Recognition Bouyer-Decitre won the CNRS Bronze Medal in 2007 and the CNRS Silver Medal in 2026. She was the 2011 winner of the Presburger Award of the European Association for Theoretical Computer Science.

Selected publications