LAURENT.DOYEN [at] (Laurent Doyen)
STEFAN.GOELLER [at] (Stefan Göller)

Verification of stochastic timed automata

Pierre Carlier, LSV, ENS Paris-Saclay & Université de Mons, will give a lecture about "Verification of stochastic timed automata", November, Tuesday 14th.
Pavillon des Jardins, Conference room
Add to my Calendar11/14/2017 11:00am 11/14/2017 12:30pm Verification of stochastic timed automata Pavillon des Jardins, Conference room Europe/Paris public

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.