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 ω-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.
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
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)
Benedikt, M., Godefroid, P., Reps, T.: Model checking of unrestricted hierarchical state machines. In: Orejas, F., Spirakis, P.G., van Leeuwen, J. (eds.) ICALP 2001. LNCS, vol. 2076, pp. 652–666. Springer, Heidelberg (2001)
Billingsley, P.: Probability and Measure, 3rd edn. J. Wiley and Sons, Chichester (1995)
Brázdil, T., Kučera, A., Stražovský, O.: Decidability of temporal properties of probabilistic pushdown automata. In: Diekert, V., Durand, B. (eds.) STACS 2005. LNCS, vol. 3404, Springer, Heidelberg (2005)
Basu, S., Pollack, R., Roy, M.F.: On the combinatorial and algebraic complexity of quantifier elimination. J. of the ACM 43(6), 1002–1045 (1996)
Ball, T., Rajamani, S.: Bebop: A symbolic model checker for boolean programs. In: Havelund, K., Penix, J., Visser, W. (eds.) SPIN 2000. LNCS, vol. 1885, pp. 113–130. Springer, Heidelberg (2000)
Canny, J.: Some algebraic and geometric computations in PSPACE. In: Prof. of 20th ACM STOC, pp. 460–467 (1988)
Courcoubetis, C., Yannakakis, M.: The complexity of probabilistic verification. Journal of the ACM 42(4), 857–907 (1995)
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)
Esparza, J., Hansel, D., Rossmanith, P., Schwoon, S.: Efficient algorithms for model checking pushdown systems. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol. 1855, pp. 232–247. Springer, Heidelberg (2000)
Esparza, J., Kučera, A., Mayr, R.: Model checking probabilistic pushdown automata. In: Proc. of 19th IEEE LICS (2004)
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)
Garey, M.R., Graham, R.L., Johnson, D.S.: Some NP-complete geometric problems. In: 8th ACM STOC, pp. 10–22 (1976)
Harris, T.E.: The Theory of Branching Processes. Springer, Heidelberg (1963)
Kwiatkowska, M.: Model checking for probability and time: from theory to practice. In: Proc. 18th IEEE LICS, pp. 351–360 (2003)
Manning, C., Schütze, H.: Foundations of Statistical Natural Language Processing. MIT Press, Cambridge (1999)
Pnueli, A., Zuck, L.D.: Probabilistic verification. Inf. and Comp. 103(1), 1–29 (1993)
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)
Tiwari, P.: A problem that is easier to solve on the unit-cost algebraic ram. Journal of Complexity, 393–397 (1992)
Vardi, M.: Automatic verification of probabilistic concurrent finite-state programs. In: Proc. of 26th IEEE FOCS, pp. 327–338 (1985)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2005 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Etessami, K., Yannakakis, M. (2005). Algorithmic Verification of Recursive Probabilistic State Machines. In: Halbwachs, N., Zuck, L.D. (eds) Tools and Algorithms for the Construction and Analysis of Systems. TACAS 2005. Lecture Notes in Computer Science, vol 3440. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-31980-1_17
Download citation
DOI: https://doi.org/10.1007/978-3-540-31980-1_17
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-25333-4
Online ISBN: 978-3-540-31980-1
eBook Packages: Computer ScienceComputer Science (R0)