{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,9,16]],"date-time":"2026-09-16T06:09:26Z","timestamp":1789538966311,"version":"build-2803163510"},"reference-count":43,"publisher":"Springer Science and Business Media LLC","issue":"2","license":[{"start":{"date-parts":[[2012,7,20]],"date-time":"2012-07-20T00:00:00Z","timestamp":1342742400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Form Methods Syst Des"],"published-print":{"date-parts":[[2013,10]]},"DOI":"10.1007\/s10703-012-0166-0","type":"journal-article","created":{"date-parts":[[2012,7,19]],"date-time":"2012-07-19T18:47:43Z","timestamp":1342723663000},"page":"124-163","source":"Crossref","is-referenced-by-count":36,"title":["Analyzing probabilistic pushdown automata"],"prefix":"10.1007","volume":"43","author":[{"given":"Tom\u00e1\u0161","family":"Br\u00e1zdil","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Javier","family":"Esparza","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Stefan","family":"Kiefer","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Anton\u00edn","family":"Ku\u010dera","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2012,7,20]]},"reference":[{"key":"166_CR1","doi-asserted-by":"crossref","first-page":"1987","DOI":"10.1137\/070697926","volume":"38","author":"E Allender","year":"2008","unstructured":"Allender E, B\u00fcrgisser P, Kjeldgaard-Pedersen J, Miltersen P (2008) On the complexity of numerical analysis. SIAM J Comput 38:1987\u20132006","journal-title":"SIAM J Comput"},{"key":"166_CR2","series-title":"Lecture notes in computer science","doi-asserted-by":"crossref","first-page":"61","DOI":"10.1007\/978-3-540-31980-1_5","volume-title":"Proceedings of TACAS 2005","author":"R Alur","year":"2005","unstructured":"Alur R, Chaudhuri S, Etessami K, Madhusudan P (2005) On-the-fly reachability and cycle detection for recursive state machines. In: Proceedings of TACAS 2005. Lecture notes in computer science, vol 3440. Springer, Berlin, pp 61\u201376"},{"key":"166_CR3","series-title":"Lecture notes in computer science","doi-asserted-by":"crossref","first-page":"207","DOI":"10.1007\/3-540-44585-4_18","volume-title":"Proceedings of CAV 2001","author":"R Alur","year":"2001","unstructured":"Alur R, Etessami K, Yannakakis M (2001) Analysis of recursive state machines. In: Proceedings of CAV 2001. Lecture notes in computer science, vol 2102. Springer, Berlin, pp 207\u2013220"},{"key":"166_CR4","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-642-65371-1","volume-title":"Branching processes","author":"K Athreya","year":"1972","unstructured":"Athreya K, Ney P (1972) Branching processes. Springer, Berlin"},{"key":"166_CR5","volume-title":"Principles of model checking","author":"C Baier","year":"2008","unstructured":"Baier C, Katoen JP (2008) Principles of model checking. MIT Press, Cambridge"},{"key":"166_CR6","series-title":"Lecture notes in computer science","doi-asserted-by":"crossref","first-page":"135","DOI":"10.1007\/3-540-63141-0_10","volume-title":"Proceedings of CONCUR\u201997","author":"A Bouajjani","year":"1997","unstructured":"Bouajjani A, Esparza J, Maler O (1997) Reachability analysis of pushdown automata: application to model checking. In: Proceedings of CONCUR\u201997. Lecture notes in computer science, vol 1243. Springer, Berlin, pp 135\u2013150"},{"key":"166_CR7","series-title":"Lecture notes in computer science","first-page":"65","volume-title":"Proceedings of VMCAI 2006","author":"L Bozzelli","year":"2006","unstructured":"Bozzelli L (2006) Complexity results on branching-time pushdown model checking. In: Proceedings of VMCAI 2006. Lecture notes in computer science, vol 3855. Springer, Berlin, pp 65\u201379"},{"key":"166_CR8","series-title":"Lecture notes in computer science","doi-asserted-by":"crossref","first-page":"230","DOI":"10.1007\/978-3-540-89439-1_17","volume-title":"Proceedings of LPAR 2008","author":"T Br\u00e1zdil","year":"2008","unstructured":"Br\u00e1zdil T, Bro\u017eek V, Hole\u010dek J, Ku\u010dera A (2008) Discounted properties of probabilistic pushdown automata. In: Proceedings of LPAR 2008. Lecture notes in computer science, vol 5330. Springer, Berlin, pp 230\u2013242"},{"key":"166_CR9","series-title":"Leibniz international proceedings in informatics","volume-title":"Proceedings of FST&TCS 2010","author":"T Br\u00e1zdil","year":"2010","unstructured":"Br\u00e1zdil T, Bro\u017eek V, Etessami K (2010) One-counter stochastic games. In: Proceedings of FST&TCS 2010. Leibniz international proceedings in informatics, vol\u00a08. Schloss Dagstuhl\u2013Leibniz-Zentrum f\u00fcr Informatik, pp 108\u2013119"},{"key":"166_CR10","series-title":"Lecture notes in computer science","doi-asserted-by":"crossref","first-page":"332","DOI":"10.1007\/978-3-642-22012-8_26","volume-title":"Proceedings of ICALP 2011, Part II","author":"T Br\u00e1zdil","year":"2011","unstructured":"Br\u00e1zdil T, Bro\u017eek V, Etessami K, Ku\u010dera A (2011) Approximating the termination value of one-counter MDPs and stochastic games. In: Proceedings of ICALP 2011, Part II. Lecture notes in computer science, vol 6756. Springer, Berlin, pp 332\u2013343"},{"key":"166_CR11","first-page":"863","volume-title":"Proceedings of SODA 2010","author":"T Br\u00e1zdil","year":"2010","unstructured":"Br\u00e1zdil T, Bro\u017eek V, Etessami K, Ku\u010dera A, Wojtczak D (2010) One-counter Markov decision processes. In: Proceedings of SODA 2010. SIAM, Philadelphia, pp 863\u2013874"},{"key":"166_CR12","doi-asserted-by":"crossref","first-page":"73","DOI":"10.1016\/j.entcs.2009.05.031","volume":"239","author":"T Br\u00e1zdil","year":"2009","unstructured":"Br\u00e1zdil T, Bro\u017eek V, Forejt V (2009) Branching-time model-checking of probabilistic pushdown automata. Electron Notes Theor Comput Sci 239:73\u201383","journal-title":"Electron Notes Theor Comput Sci"},{"issue":"5","key":"166_CR13","doi-asserted-by":"crossref","first-page":"520","DOI":"10.1016\/j.ic.2007.09.002","volume":"206","author":"T Br\u00e1zdil","year":"2008","unstructured":"Br\u00e1zdil T, Bro\u017eek V, Forejt V, Ku\u010dera A (2008) Reachability in recursive Markov decision processes. Inf Comput 206(5):520\u2013537","journal-title":"Inf Comput"},{"key":"166_CR14","first-page":"521","volume-title":"Proceedings of FOCS 2005","author":"T Br\u00e1zdil","year":"2005","unstructured":"Br\u00e1zdil T, Esparza J, Ku\u010dera A (2005) Analysis and prediction of the long-run behavior of probabilistic sequential programs with recursion. In: Proceedings of FOCS 2005. IEEE Computer Society, Los Alamitos, pp 521\u2013530"},{"key":"166_CR15","series-title":"Lecture notes in computer science","doi-asserted-by":"crossref","first-page":"208","DOI":"10.1007\/978-3-642-22110-1_18","volume-title":"Proceedings of CAV 2011","author":"T Br\u00e1zdil","year":"2011","unstructured":"Br\u00e1zdil T, Kiefer S, Ku\u010dera A (2011) Efficient analysis of probabilistic programs with an unbounded counter. In: Proceedings of CAV 2011. Lecture notes in computer science, vol 6806. Springer, Berlin, pp 208\u2013224"},{"key":"166_CR16","unstructured":"Br\u00e1zdil T, Kiefer S, Ku\u010dera A, Huta\u0159ov\u00e1 Va\u0159ekov\u00e1 I (2010) Runtime analysis of probabilistic programs with unbounded recursion. CoRR abs\/1007.1710"},{"key":"166_CR17","series-title":"Lecture notes in computer science","doi-asserted-by":"crossref","first-page":"319","DOI":"10.1007\/978-3-642-22012-8_25","volume-title":"Proceedings of ICALP 2011, Part II","author":"T Br\u00e1zdil","year":"2011","unstructured":"Br\u00e1zdil T, Kiefer S, Ku\u010dera A, Huta\u0159ov\u00e1 Va\u0159ekov\u00e1 I (2011) Runtime analysis of probabilistic programs with unbounded recursion. In: Proceedings of ICALP 2011, Part II. Lecture notes in computer science, vol 6756. Springer, Berlin, pp 319\u2013331"},{"key":"166_CR18","series-title":"Lecture notes in computer science","doi-asserted-by":"crossref","first-page":"193","DOI":"10.1007\/978-3-540-28644-8_13","volume-title":"Proceedings of CONCUR 2004","author":"T Br\u00e1zdil","year":"2004","unstructured":"Br\u00e1zdil T, Ku\u010dera A, Stra\u017eovsk\u00fd O (2004) Deciding probabilistic bisimilarity over infinite-state probabilistic systems. In: Proceedings of CONCUR 2004. Lecture notes in computer science, vol 3170. Springer, Berlin, pp 193\u2013208"},{"key":"166_CR19","series-title":"Lecture notes in computer science","doi-asserted-by":"crossref","first-page":"145","DOI":"10.1007\/978-3-540-31856-9_12","volume-title":"Proceedings of STACS 2005","author":"T Br\u00e1zdil","year":"2005","unstructured":"Br\u00e1zdil T, Ku\u010dera A, Stra\u017eovsk\u00fd O (2005) On the decidability of temporal properties of probabilistic pushdown automata. In: Proceedings of STACS 2005. Lecture notes in computer science, vol 3404. Springer, Berlin, pp 145\u2013157"},{"key":"166_CR20","first-page":"460","volume-title":"Proceedings of STOC\u201988","author":"J Canny","year":"1988","unstructured":"Canny J (1988) Some algebraic and geometric computations in PSPACE. In: Proceedings of STOC\u201988. ACM Press, New York, pp 460\u2013467"},{"key":"166_CR21","volume-title":"Markov chains with stationary transition probabilities","author":"K Chung","year":"1967","unstructured":"Chung K (1967) Markov chains with stationary transition probabilities. Springer, Berlin"},{"key":"166_CR22","first-page":"995","volume-title":"Handbook of theoretical computer science B","author":"E Emerson","year":"1991","unstructured":"Emerson E (1991) Temporal and modal logic. In: Handbook of theoretical computer science B, pp 995\u20131072"},{"key":"166_CR23","series-title":"Leibniz international proceedings in informatics","volume-title":"Proceedings of STACS 2010","author":"J Esparza","year":"2010","unstructured":"Esparza J, Gaiser A, Kiefer S (2010) Computing least fixed points of probabilistic systems of polynomials. In: Proceedings of STACS 2010. Leibniz international proceedings in informatics, vol 5. Schloss Dagstuhl\u2013Leibniz-Zentrum f\u00fcr Informatik, pp 359\u2013370"},{"key":"166_CR24","series-title":"Lecture notes in computer science","doi-asserted-by":"crossref","first-page":"232","DOI":"10.1007\/10722167_20","volume-title":"Proceedings of CAV 2000","author":"J Esparza","year":"2000","unstructured":"Esparza J, Hansel D, Rossmanith P, Schwoon S (2000) Efficient algorithms for model checking pushdown systems. In: Proceedings of CAV 2000. Lecture notes in computer science, vol 1855. Springer, Berlin, pp 232\u2013247"},{"key":"166_CR25","first-page":"12","volume-title":"Proceedings of LICS 2004","author":"J Esparza","year":"2004","unstructured":"Esparza J, Ku\u010dera A, Mayr R (2004) Model-checking probabilistic pushdown automata. In: Proceedings of LICS 2004. IEEE Computer Society, Los Alamitos, pp 12\u201321"},{"key":"166_CR26","first-page":"117","volume-title":"Proceedings of LICS 2005","author":"J Esparza","year":"2005","unstructured":"Esparza J, Ku\u010dera A, Mayr R (2005) Quantitative analysis of probabilistic pushdown automata: Expectations and variances. In: Proceedings of LICS 2005. IEEE Computer Society, Los Alamitos, pp 117\u2013126"},{"key":"166_CR27","first-page":"579","volume-title":"Proceedings of STOC 2012","author":"K Etessami","year":"2012","unstructured":"Etessami K, Stewart A, Yannakakis M (2012) Polynomial time algorithms for multi-type branching processes and stochastic context-free grammars. In: Proceedings of STOC 2012. ACM Press, New York, pp 579\u2013588"},{"key":"166_CR28","volume-title":"Proceedings of 5th Int. Conf. on Quantitative Evaluation of Systems (QEST\u201908)","author":"K Etessami","year":"2008","unstructured":"Etessami K, Wojtczak D, Yannakakis M (2008) 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\u201908). IEEE Computer Society, Los Alamitos"},{"key":"166_CR29","series-title":"Lecture notes in computer science","doi-asserted-by":"crossref","first-page":"253","DOI":"10.1007\/978-3-540-31980-1_17","volume-title":"Proceedings of TACAS 2005","author":"K Etessami","year":"2005","unstructured":"Etessami K, Yannakakis M (2005) Algorithmic verification of recursive probabilistic systems. In: Proceedings of TACAS 2005. Lecture notes in computer science, vol 3440. Springer, Berlin, pp 253\u2013270"},{"key":"166_CR30","first-page":"155","volume-title":"Proceedings of 2nd int conf on quantitative evaluation of systems (QEST\u201905)","author":"K Etessami","year":"2005","unstructured":"Etessami K, Yannakakis M (2005) Checking LTL properties of recursive Markov chains. In: Proceedings of 2nd int conf on quantitative evaluation of systems (QEST\u201905). IEEE Computer Society, Los Alamitos, pp 155\u2013165"},{"key":"166_CR31","series-title":"Lecture notes in computer science","doi-asserted-by":"crossref","first-page":"340","DOI":"10.1007\/978-3-540-31856-9_28","volume-title":"Proceedings of STACS 2005","author":"K Etessami","year":"2005","unstructured":"Etessami K, Yannakakis M (2005) Recursive Markov chains, stochastic grammars, and monotone systems of non-linear equations. In: Proceedings of STACS 2005. Lecture notes in computer science, vol 3404. Springer, Berlin, pp 340\u2013352"},{"key":"166_CR32","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1145\/1462153.1462154","volume":"56","author":"K Etessami","year":"2009","unstructured":"Etessami K, Yannakakis M (2009) Recursive Markov chains, stochastic grammars, and monotone systems of nonlinear equations. J Assoc Comput Mach 56:1\u201366","journal-title":"J Assoc Comput Mach"},{"issue":"1\u20132","key":"166_CR33","doi-asserted-by":"crossref","first-page":"65","DOI":"10.1016\/S0747-7171(88)80006-3","volume":"5","author":"D Grigoriev","year":"1988","unstructured":"Grigoriev D (1988) Complexity of deciding Tarski algebra. J Symb Comput 5(1\u20132):65\u2013108","journal-title":"J Symb Comput"},{"key":"166_CR34","doi-asserted-by":"crossref","first-page":"512","DOI":"10.1007\/BF01211866","volume":"6","author":"H Hansson","year":"1994","unstructured":"Hansson H, Jonsson B (1994) A logic for reasoning about time and reliability. Form Asp Comput 6:512\u2013535","journal-title":"Form Asp Comput"},{"key":"166_CR35","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-642-51866-9","volume-title":"The theory of branching processes","author":"T Harris","year":"1963","unstructured":"Harris T (1963) The theory of branching processes. Springer, Berlin"},{"key":"166_CR36","volume-title":"Introduction to automata theory, languages, and computation","author":"J Hopcroft","year":"1979","unstructured":"Hopcroft J, Ullman J (1979) Introduction to automata theory, languages, and computation. Addison-Wesley, Reading"},{"key":"166_CR37","first-page":"217","volume-title":"Proceedings of STOC 2007","author":"S Kiefer","year":"2007","unstructured":"Kiefer S, Luttenberger M, Esparza J (2007) On the convergence of Newton\u2019s method for monotone systems of polynomial equations. In: Proceedings of STOC 2007. ACM Press, New York, pp 217\u2013226"},{"key":"166_CR38","volume-title":"Electronic notes in theoretical computer science","author":"R Mayr","year":"1998","unstructured":"Mayr R (1998) Strict lower bounds for model checking BPA. In: Electronic notes in theoretical computer science, vol 18"},{"key":"166_CR39","doi-asserted-by":"crossref","DOI":"10.1142\/6300","volume-title":"A first look at rigorous probability theory","author":"J Rosenthal","year":"2006","unstructured":"Rosenthal J (2006) A first look at rigorous probability theory. World Scientific, Singapore"},{"key":"166_CR40","doi-asserted-by":"crossref","DOI":"10.1525\/9780520348097","volume-title":"A decision method for elementary algebra and geometry","author":"A Tarski","year":"1951","unstructured":"Tarski A (1951) A decision method for elementary algebra and geometry. Univ. of California Press, Berkeley"},{"issue":"2","key":"166_CR41","doi-asserted-by":"crossref","first-page":"285","DOI":"10.2140\/pjm.1955.5.285","volume":"5","author":"A Tarski","year":"1955","unstructured":"Tarski A (1955) A lattice-theoretical fixpoint theorem and its applications. Pac J Math 5(2):285\u2013309","journal-title":"Pac J Math"},{"key":"166_CR42","series-title":"Lecture notes in computer science","doi-asserted-by":"crossref","first-page":"127","DOI":"10.1007\/3-540-44450-5_10","volume-title":"Proceedings of FST&TCS\u20192000","author":"I Walukiewicz","year":"2000","unstructured":"Walukiewicz I (2000) Model checking CTL properties of pushdown systems. In: Proceedings of FST&TCS\u20192000. Lecture notes in computer science, vol 1974. Springer, Berlin, pp 127\u2013138"},{"key":"166_CR43","doi-asserted-by":"crossref","DOI":"10.1017\/CBO9780511813658","volume-title":"Probability with Martingales","author":"D Williams","year":"1991","unstructured":"Williams D (1991) Probability with Martingales. Cambridge University Press, Cambridge"}],"container-title":["Formal Methods in System Design"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-012-0166-0.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10703-012-0166-0\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-012-0166-0","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,1,22]],"date-time":"2022-01-22T07:42:00Z","timestamp":1642837320000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10703-012-0166-0"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012,7,20]]},"references-count":43,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2013,10]]}},"alternative-id":["166"],"URL":"https:\/\/doi.org\/10.1007\/s10703-012-0166-0","relation":{},"ISSN":["0925-9856","1572-8102"],"issn-type":[{"value":"0925-9856","type":"print"},{"value":"1572-8102","type":"electronic"}],"subject":[],"published":{"date-parts":[[2012,7,20]]}}}