Decisive stochastic processes

In 2007, Abdulla et al. introduced the elegant concept of decisive Markov chain. Intuitively, decisiveness allows one to lift the good properties of finite Markov chains to infinite Markov chains. For instance, the approximate quantitative reachability problem can be solved for decisive Markov chains (enjoying reasonable effectiveness assumptions) including probabilistic lossy channel systems and probabilistic vector addition systems with states. 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 real-time stochastic processes). This allows us to obtain decidability results for both qualitative and quantitative verification problems on some classes of real-time stochastic processes, including generalized semi-Markov processes and stochastic timed automata. The results presented in this abstract are issued from a joint paper with Nathalie Bertrand, Patricia Bouyer and Pierre Carlier entitled Analysing decisive stochastic processes accepted to ICALP 2016.

Authors

• with Nathalie Bertrand
• Patricia Bouyer
• Pierre Carlier

Keywords

No keywords are indexed for this paper.