Decisiveness and stochastic timed automata

Pierre Carlier
UMons
Friday, 26 February, 2016 - 11:45
NO Solvay (5th floor)

In 2007, Abdulla et al introduced the elegant concept of decisive Markov chain w.r.t. a given target set F. Intuitively, the concept of decisiveness allows to lift the good properties of finite Markov chains to infinite Markov chains. For instance, the approximate quantitative safety problem can be solved for decisive Markov chains (enjoying reasonable effectiveness assumptions) including PLCS and PVASS. In this paper, we extend the concept of decisiveness to more general stochastic processes. This extension is non trivial as we consider stochastic processes with a potentially continuous set of states and uncountable branching (common features of continuous-time stochastic process). This allow us to obtain decidability results for both qualitative and quantitative verification problems on continuous-time stochastic process, including GSMP and STA.

This is a joint work with Nathalie Bertrand, Patricia Bouyer and Thomas Brihaye.