KeywordsModel Checking, Stochastic Timed Automata, Composition, Bisimulation
Stochastic timed automata (STA), as defined by Baier et al in 2007, enrich the well know model of Timed Automata (TA) with probability distributions on both delays and discrete transitions. Large subclasses of STA enjoys nice properties, for instance, the almost-sure LTL model-checking of reactive STA has been proved decidable (Bouyer et al, 2012). More recently, adequate composition operators have been defined for STA (Bouyer et al, 2016) together with an adequate notion of bisimulation. The goal of the research would be to study further compositional aspects of STA, this could include a logical characterization of the bisimulation, the development of compositional verification (or approximation) methods, as it is done for instance for interactive Markov chains. This could also lead to the study of control/game problems on STA.
These research could be co-advised by Patricia Bouyer (CNRS-Université Paris-Saclay).