Abstract
Stochastic branching processes are a classical model for describing random trees, which have applications in numerous fields including biology, physics, and natural language processing. In particular, they have recently been proposed to describe parallel programs with stochastic process creation. In this paper, we consider the problem of model checking stochastic branching process. Given a branching process and a deterministic parity tree automaton, we are interested in computing the probability that the generated random tree is accepted by the automaton. We show that this probability can be compared with any rational number in PSPACE, and with 0 and 1 in polynomial time. In a second part, we suggest a tree extension of the logic PCTL, and develop a PSPACE algorithm for model checking a branching process against a formula of this logic. We also show that the qualitative fragment of this logic can be model checked in polynomial time.
This work was partially supported by the ERC Advanced Grant VERIWARE and EPSRC grant EP/F001096/1. Stefan Kiefer is supported by a DAAD postdoctoral fellowship.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Allender, E., Bürgisser, P., Kjeldgaard-Pedersen, J., Miltersen, P.B.: On the complexity of numerical analysis. In: IEEE Conference on Computational Complexity, pp. 331–339 (2006)
Athreya, K.B., Ney, P.E.: Branching Processes. Springer (1972)
Canny, J.: Some algebraic and geometric computations in PSPACE. In: STOC 1988, pp. 460–467 (1988)
Chen, T., Dräger, K., Kiefer, S.: Model checking stochastic branching processes. Technical report, arxiv.org (2012), http://arxiv.org/abs/1206.1317
Courcoubetis, C., Yannakakis, M.: The complexity of probabilistic verification. Journal of the ACM 42, 857–907 (1995)
Esparza, J., Gaiser, A., Kiefer, S.: Computing least fixed points of probabilistic systems of polynomials. In: Proceedings of STACS, pp. 359–370 (2010)
Esparza, J., Kiefer, S., Luttenberger, M.: Computing the least fixed point of positive polynomial systems. SIAM Journal on Computing 39(6), 2282–2335 (2010)
Esparza, J., Kučera, A., Mayr, R.: Model checking probabilistic pushdown automata. In: LICS 2004, pp. 12–21. IEEE (2004)
Etessami, K., Stewart, A., Yannakakis, M.: Polynomial-time algorithms for multi-type branching processes and stochastic context-free grammars. In: Proceedings of STOC, pp. 579–588 (2012)
Etessami, K., Yannakakis, M.: Recursive Markov chains, stochastic grammars, and monotone systems of nonlinear equations. Journal of the ACM 56(1), 1–66 (2009)
Etessami, K., Yannakakis, M.: Model checking of recursive probabilistic systems. ACM Transactions on Computational Logic 13(2) (to appear 2012)
Harris, T.E.: The Theory of Branching Processes. Springer (1963)
Kiefer, S., Wojtczak, D.: On Probabilistic Parallel Programs with Process Creation and Synchronisation. In: Abdulla, P.A., Leino, K.R.M. (eds.) TACAS 2011. LNCS, vol. 6605, pp. 296–310. Springer, Heidelberg (2011)
Renegar, J.: On the computational complexity and geometry of the first-order theory of the reals. Parts I–III. Journal of Symbolic Computation 13(3), 255–352 (1992)
Thomas, W.: Languages, automata, and logic. In: Rozenberg, G., Salomaa, A. (eds.) Handbook of Formal Languages. Beyond Words, vol. 3, pp. 389–455. Springer (1997)
Vardi, M.Y.: Probabilistic Linear-Time Model Checking: An Overview of the Automata-Theoretic Approach. In: Katoen, J.-P. (ed.) AMAST-ARTS 1999, ARTS 1999, and AMAST-WS 1999. LNCS, vol. 1601, pp. 265–276. Springer, Heidelberg (1999)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2012 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Chen, T., Dräger, K., Kiefer, S. (2012). Model Checking Stochastic Branching Processes. In: Rovan, B., Sassone, V., Widmayer, P. (eds) Mathematical Foundations of Computer Science 2012. MFCS 2012. Lecture Notes in Computer Science, vol 7464. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-32589-2_26
Download citation
DOI: https://doi.org/10.1007/978-3-642-32589-2_26
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-32588-5
Online ISBN: 978-3-642-32589-2
eBook Packages: Computer ScienceComputer Science (R0)