Keynote Speaker: Patricia Bouyer-Decitre

LMF (Laboratoire Méthodes Formelles), Gif-sur-Yvette, France
Title: On the (Approximate) Analysis of Stochastic Real-Time Systems
Abstract

Analyzing stochastic systems with real-time features is notably difficult, and often calls for approximation technics. In this talk I will present a crucial property of stochastic systems, which allows for provably sound approximated model-checking technics. This property, called decisiveness, was first proposed by Abdulla et al in 2007 for infinite-state discrete Markov chains. This was later extended to general stochastic transition systems, and general approximation schemes were proven correct for large classes of properties. Finally it turns out that several classes of real-time stochastic systems that have been considered in the literature do actually satisfy the property, which implies that they can safely be analysed. Finally, I plan to discuss ongoing work on statistical simulation. This talk is based on joint works with Nathalie Bertrand, Thomas Brihaye, Pierre Carlier, Mickael Randour, Cedric Riviere and Pierre Vandenhove.



Bio

Patricia Bouyer-Decitre holds a PhD in Computer Science from ENS Cachan (2002). She has been a CNRS researcher from 2002 to 2020 at "Laboratoire Spécification et Vérification" (LSV, CNRS & ENS Cachan, France). She is now the head of the newly created "Laboratoire Méthodes Formelles" (LMF, Université Paris-Saclay, CNRS, ENS Paris-Saclay, France). She has held visiting positions at Aalborg University (Denmark) in 2002 and Oxford University (UK) in 2007. Patricia Bouyer-Decitre's main research topics are model checking, game theory, and quantitative aspects of verification. She has been the principal investigator of ERC Starting Grant project EQualIS (2013-2019). She was the recipient of a Marie Curie fellowship in 2006, of the Bronze medal of CNRS in 2007 and of the Presburger Award given by the EATCS in 2011.