Verification of stochastic timed automata
In this talk, I will present the contributions of my thesis. We are interested in the stochastic timed automaton model (STA), which is a probabilistic extension of the timed automaton model. The contributions of this thesis are twofold.
I will mainly focus on the first one: the qualitative and quantitative model-checking problems. STA are, in particular, general probabilistic systems and with such model, one is thus interested in questions like « Is a property satisfied, within a given model, with probability 1 ? » (qualitative) or « Can we compute an approximation of the probability that the model satisfies a given property ? » (quantitative).
We first study those questions for general stochastic systems.
The notion of decisiveness, that was already studied in denumerable Markov chains by Abdulla et al., plays a key role in order to get results. I will present some of our results, some being extensions of previous work on Markov chains, other being new. I will then briefly explain how we could apply those results to subclasses of STA. Finally, I will have a brief word on our second contribution, which is the definition of an operator of composition for STA.