Informatics Report Series



Related Pages

Report (by Number) Index
Report (by Date) Index
Author Index
Institute Index

Title:Algorithmic Verification of Recursive Probabilistic State Machines.
Authors: Kousha Etessami ; Mihalis Yannakakis
Date: 2005
Publication Title:Proceedings of 11th Int. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'05)
Publication Type:Conference Paper
Recursive Markov Chains (RMCs) ([EY05]) are a natural abstract model of procedural probabilistic programs and related systems involving recursion and probability. They succinctly define a class of denumerable Markov chains that generalize multi-type branching (stochastic) processes. In this paper, we study the problem of model checking an RMC against a given ohgr-regular specification. Namely, given an RMC A and a Bchi automaton B, we wish to know the probability that an execution of A is accepted by B. We establish a number of strong upper bounds, as well as lower bounds, both for qualitative problems (is the probability = 1, or = 0?), and for quantitative problems (is the probability ge p ?, or, approximate the probability to within a desired precision). Among these, we show that qualitative model checking for general RMCs can be decided in PSPACE in |A| and EXPTIME in |B|, and when A is either a single-exit RMC or when the total number of entries and exits in A is bounded, it can be decided in polynomial time in |A|. We then show that quantitative model checking can also be done in PSPACE in |A|, and in EXPSPACE in |B|. When B is deterministic, all our complexities in |B| come down by one exponential. For lower bounds, we show that the qualitative model checking problem, even for a fixed RMC, is EXPTIME-complete. On the other hand, even for reachability analysis, we showed in [EY05] that our PSPACE upper bounds in A can not be improved upon without a breakthrough on a well-known open problem in the complexity of numerical computation.
Links To Paper
1st Link
Bibtex format
author = { Kousha Etessami and Mihalis Yannakakis },
title = {Algorithmic Verification of Recursive Probabilistic State Machines.},
book title = {Proceedings of 11th Int. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'05)},
year = 2005,
url = {,17,42;journal,401,3275;linkingpublicationresults,1:105633,1},

Home : Publications : Report 

Please mail <> with any changes or corrections.
Unless explicitly stated otherwise, all material is copyright The University of Edinburgh