Abstract
We study the runtime in probabilistic programs with unbounded recursion. As underlying formal model for such programs we use probabilistic pushdown automata (pPDA) which exactly correspond to recursive Markov chains. We show that every pPDA can be transformed into a stateless pPDA (called “pBPA”) whose runtime and further properties are closely related to those of the original pPDA. This result substantially simplifies the analysis of runtime and other pPDA properties. We prove that for every pPDA the probability of performing a long run decreases exponentially in the length of the run, if and only if the expected runtime in the pPDA is finite. If the expectation is infinite, then the probability decreases “polynomially”. We show that these bounds are asymptotically tight. Our tail bounds on the runtime are generic, i.e., applicable to any probabilistic program with unbounded recursion. An intuitive interpretation is that in pPDA the runtime is exponentially unlikely to deviate from its expected value.
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
Bini, D., Latouche, G., Meini, B.: Numerical methods for Structured Markov Chains. Oxford University Press, Oxford (2005)
Brázdil, T.: Verification of Probabilistic Recursive Sequential Programs. PhD thesis, Masaryk University, Faculty of Informatics (2007)
Brázdil, T., Brožek, V., Holeček, J., Kučera, A.: Discounted properties of probabilistic pushdown automata. In: Cervesato, I., Veith, H., Voronkov, A. (eds.) LPAR 2008. LNCS (LNAI), vol. 5330, pp. 230–242. Springer, Heidelberg (2008)
Brázdil, T., Brožek, V., Etessami, K.: One-counter stochastic games. In: Proceedings of ST&TCS 2010. Leibniz International Proceedings in Informatics, vol. 8, pp. 108–119. Schloss Dagstuhl–Leibniz-Zentrum für Informatik (2010)
Brázdil, T., Brožek, V., Etessami, K., Kučera, A., Wojtczak, D.: One-counter Markov decision processes. In: Proceedings of SODA 2010, pp. 863–874. SIAM, Philadelphia (2010)
Brázdil, T., Esparza, J., Kučera, A.: Analysis and prediction of the long-run behavior of probabilistic sequential programs with recursion. In: Proceedings of FOCS 2005, pp. 521–530. IEEE Computer Society Press, Los Alamitos (2005)
Brázdil, T., Kiefer, S., Kučera, A.: Efficient analysis of probabilistic programs with an unbounded counter. CoRR, abs/1102.2529 (2011)
Brázdil, T., Kiefer, S., Kučera, A., Hutařová Vařeková, I.: Runtime analysis of probabilistic programs with unbounded recursion. CoRR, abs/1007.1710 (2010)
Canny, J.: Some algebraic and geometric computations in PSPACE. In: Proceedings of STOC 1988, pp. 460–467. ACM Press, New York (1988)
Dubhashi, D.P., Panconesi, A.: Concentration of Measure for the Analysis of Randomized Algorithms. Cambridge University Press, Cambridge (2009)
Esparza, J., Kiefer, S., Luttenberger, M.: Convergence thresholds of Newton’s method for monotone polynomial equations. In: STACS 2008, pp. 289–300 (2008)
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: Proceedings of LICS 2004, pp. 12–21. IEEE Computer Society Press, Los Alamitos (2004)
Esparza, J., Kučera, A., Mayr, R.: Quantitative analysis of probabilistic pushdown automata: Expectations and variances. In: Proceedings of LICS 2005, pp. 117–126. IEEE Computer Society Press, Los Alamitos (2005)
Etessami, K., Wojtczak, D., Yannakakis, M.: Quasi-birth-death processes, tree-like QBDs, probabilistic 1-counter automata, and pushdown systems. In: Proceedings of 5th Int. Conf. on Quantitative Evaluation of Systems (QEST 2008). IEEE Computer Society Press, Los Alamitos (2008)
Etessami, K., Yannakakis, M.: Algorithmic verification of recursive probabilistic systems. In: Halbwachs, N., Zuck, L.D. (eds.) TACAS 2005. LNCS, vol. 3440, pp. 253–270. Springer, Heidelberg (2005)
Etessami, K., Yannakakis, M.: Checking LTL properties of recursive Markov chains. In: Proceedings of 2nd Int. Conf. on Quantitative Evaluation of Systems (QEST 2005), pp. 155–165. IEEE Computer Society Press, Los Alamitos (2005)
Etessami, K., Yannakakis, M.: Recursive Markov chains, stochastic grammars, and monotone systems of nonlinear equations. Journal of the Association for Computing Machinery 56 (2009)
Harris, T.E.: The Theory of Branching Processes. Springer, Heidelberg (1963)
Hopcroft, J.E., Ullman, J.D.: Introduction to Automata Theory, Languages, and Computation. Addison-Wesley, Reading (1979)
Kiefer, S., Luttenberger, M., Esparza, J.: On the convergence of Newton’s method for monotone systems of polynomial equations. In: STOC 2007, pp. 217–226 (2007)
Latouche, G., Ramaswami, V.: Introduction to Matrix Analytic Methods in Stochastic Modeling. ASA-SIAM series on statistics and applied probability (1999)
Manning, C., Schütze, H.: Foundations of Statistical Natural Language Processing. The MIT Press, Cambridge (1999)
Motwani, R., Raghavan, P.: Randomized Algorithms. Cambridge University Press, Cambridge (2006)
Pakes, A.G.: Some limit theorems for the total progeny of a branching process. Advances in Applied Probability 3(1), 176–192 (1971)
Quine, M.P., Szczotka, W.: Generalisations of the Bienayme-Galton-Watson branching process via its representation as an embedded random walk. The Annals of Applied Probability 4(4), 1206–1222 (1994)
Williams, D.: Probability with Martingales. Cambridge University Press, Cambridge (1991)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2011 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Brázdil, T., Kiefer, S., Kučera, A., Vařeková, I.H. (2011). Runtime Analysis of Probabilistic Programs with Unbounded Recursion. In: Aceto, L., Henzinger, M., Sgall, J. (eds) Automata, Languages and Programming. ICALP 2011. Lecture Notes in Computer Science, vol 6756. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-22012-8_25
Download citation
DOI: https://doi.org/10.1007/978-3-642-22012-8_25
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-22011-1
Online ISBN: 978-3-642-22012-8
eBook Packages: Computer ScienceComputer Science (R0)