When are stochastic transition systems tameable?

1^st May 2018, 16:00 ELEC-202
Prof. Thomas Brihaye
Department of Mathematics
Université de Mons

Abstract

A decade ago, Abdulla et al introduced the elegant concept of decisiveness for denumerable Markov chains. Roughly decisiveness allows one to lift most good properties from finite Markov chains to denumerable ones, and therefore to adapt existing verification algorithms to infinite-state models. Denumerable Markov chains however do not encompass stochastic real-time systems, and general stochastic transition systems (STSs) are needed. In this talk, we discuss a framework to perform both the qualitative and the quantitative analysis of STSs. In order to do so, we first need to adapt the concept of decisiveness for general STSs. Then we define a notion of abstraction and provide some transfer properties. Then we focus on both qualitative and quantitative analysis. Beyond (repeated) reachability properties for which our technics are strongly inspired by the work on denumerable Markov chains, we use abstractions to design algorithms for the model-checking of arbitrary omega-regular properties, for subclasses of STS. Last we instantiate our framework with stochastic timed automata Some of these results were known from the literature, but our generic approach permits to view them in a unified framework. We also derive interesting new approximability results.

This talk is based on joint work with Nathalie Bertrand, Patricia Bouyer, and Pierre Carlier