Algorithmic Verification of Recursive Probabilistic State Machines

  • Kousha Etessami
  • Mihalis Yannakakis
Part of the Lecture Notes in Computer Science book series (LNCS, volume 3440)


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.


Markov Chain Model Check Reachability Analysis Strongly Connect Component Model Check Problem 
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.


  1. [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
  2. [BGR01]
    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)CrossRefGoogle Scholar
  3. [Bil95]
    Billingsley, P.: Probability and Measure, 3rd edn. J. Wiley and Sons, Chichester (1995)zbMATHGoogle Scholar
  4. [BKS05]
    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)CrossRefGoogle Scholar
  5. [BPR96]
    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)zbMATHCrossRefMathSciNetGoogle Scholar
  6. [BR00]
    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)CrossRefGoogle Scholar
  7. [Can88]
    Canny, J.: Some algebraic and geometric computations in PSPACE. In: Prof. of 20th ACM STOC, pp. 460–467 (1988)Google Scholar
  8. [CY95]
    Courcoubetis, C., Yannakakis, M.: The complexity of probabilistic verification. Journal of the ACM 42(4), 857–907 (1995)zbMATHCrossRefMathSciNetGoogle Scholar
  9. [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
  10. [EHRS00]
    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)CrossRefGoogle Scholar
  11. [EKM04]
    Esparza, J., Kučera, A., Mayr, R.: Model checking probabilistic pushdown automata. In: Proc. of 19th IEEE LICS (2004)Google Scholar
  12. [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
  13. [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
  14. [Har63]
    Harris, T.E.: The Theory of Branching Processes. Springer, Heidelberg (1963)zbMATHGoogle Scholar
  15. [Kwi03]
    Kwiatkowska, M.: Model checking for probability and time: from theory to practice. In: Proc. 18th IEEE LICS, pp. 351–360 (2003)Google Scholar
  16. [MS99]
    Manning, C., Schütze, H.: Foundations of Statistical Natural Language Processing. MIT Press, Cambridge (1999)zbMATHGoogle Scholar
  17. [PZ93]
    Pnueli, A., Zuck, L.D.: Probabilistic verification. Inf. and Comp. 103(1), 1–29 (1993)zbMATHCrossRefMathSciNetGoogle Scholar
  18. [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
  19. [Tiw92]
    Tiwari, P.: A problem that is easier to solve on the unit-cost algebraic ram. Journal of Complexity, 393–397 (1992)Google Scholar
  20. [Var85]
    Vardi, M.: Automatic verification of probabilistic concurrent finite-state programs. In: Proc. of 26th IEEE FOCS, pp. 327–338 (1985)Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2005

Authors and Affiliations

  • Kousha Etessami
    • 1
  • Mihalis Yannakakis
    • 2
  1. 1.School of InformaticsUniversity of Edinburgh 
  2. 2.Department of Computer ScienceColumbia University 

Personalised recommendations