- 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 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
- @InProceedings{EDI-INF-RR-0684,
- 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},
- }
|
