Algorithmic Verification of Recursive Probabilistic State Machines
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 ω-regular specification. Namely, given an RMC A and a Büchi 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 ≥ 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.
KeywordsMarkov Chain Model Check Reachability Analysis Strongly Connect Component Model Check Problem
- [AEY01]Alur, R., Etessami, K., Yannakakis, M.: Analysis of recursive state machines. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol. 2102, pp. 304–313. Springer, Heidelberg (2001)Google Scholar
- [Can88]Canny, J.: Some algebraic and geometric computations in PSPACE. In: Prof. of 20th ACM STOC, pp. 460–467 (1988)Google Scholar
- [EE04]Esparza, J., Etessami, K.: Verifying probabilistic procedural programs. In: Lodaya, K., Mahajan, M. (eds.) FSTTCS 2004. LNCS, vol. 3328, pp. 16–31. Springer, Heidelberg (2004) (Invited survey paper)Google Scholar
- [EKM04]Esparza, J., Kučera, A., Mayr, R.: Model checking probabilistic pushdown automata. In: Proc. of 19th IEEE LICS (2004)Google Scholar
- [EY05]Etessami, K., Yannakakis, M.: Recursive markov chains, stochastic grammars, and monotone systems of non-linear equations. In: Diekert, V., Durand, B. (eds.) STACS 2005. LNCS, vol. 3404, pp. 340–352. Springer, Heidelberg (2005): (Tech. Report, U. Edinburgh) (June 2004) Google Scholar
- [GGJ76]Garey, M.R., Graham, R.L., Johnson, D.S.: Some NP-complete geometric problems. In: 8th ACM STOC, pp. 10–22 (1976)Google Scholar
- [Kwi03]Kwiatkowska, M.: Model checking for probability and time: from theory to practice. In: Proc. 18th IEEE LICS, pp. 351–360 (2003)Google Scholar
- [Ren92]Renegar, J.: On the computational complexity and geometry of the first-order theory of the reals. parts i,ii, iii. J. of Symbolic Computation, 255–352 (1992)Google Scholar
- [Tiw92]Tiwari, P.: A problem that is easier to solve on the unit-cost algebraic ram. Journal of Complexity, 393–397 (1992)Google Scholar
- [Var85]Vardi, M.: Automatic verification of probabilistic concurrent finite-state programs. In: Proc. of 26th IEEE FOCS, pp. 327–338 (1985)Google Scholar