LSV Seminar

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.

Past Seminars

Verification of stochastic timed automata

Tuesday, November 14 2017 at 11:00AM
Salle de Conférence (Pavillon des Jardins)
Pierre Carlier (LSV, ENS Cachan & Université de Mons)

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.

About LSV