 Abstract:

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 multitype branching (stochastic) processes. In this paper, we study the problem of model checking an RMC against a given ohgrregular 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 singleexit 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 EXPTIMEcomplete. 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 wellknown open problem in the complexity of numerical computation.
 Links To Paper
 1st Link
 Bibtex format
 @InProceedings{EDIINFRR0684,
 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 = {http://springerlink.metapress.com/(jrr2kxqn3p4yhh45sgumtjvd)/app/home/contribution.asp?referrer=parent&backto=issue,17,42;journal,401,3275;linkingpublicationresults,1:105633,1},
 }
