The LSV seminar takes place on Tuesday at 11:00 AM. The usual location is the conference room at Pavillon des Jardins (venue). If you wish to be informed by e-mail about upcoming seminars, please contact Stéphane Le Roux and Matthias Fuegger.
The seminar is open to public and does not require any form of registration.
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.