Thesis topic

Compositional Model Checking of Stochastic Timed Automata

  • Type
    Doctorate Post-doctorate
  • Keywords
    Model 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).

About this topic

Related to
Effective Mathematics Unit
Thomas Brihaye

Contact us for more info