{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,1,12]],"date-time":"2025-01-12T05:08:54Z","timestamp":1736658534730,"version":"3.32.0"},"publisher-location":"Berlin, Heidelberg","reference-count":44,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540472377"},{"type":"electronic","value":"9783540472384"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2006]]},"DOI":"10.1007\/11901914_1","type":"book-chapter","created":{"date-parts":[[2006,10,10]],"date-time":"2006-10-10T05:21:43Z","timestamp":1160457703000},"page":"1-5","source":"Crossref","is-referenced-by-count":0,"title":["Analysis of Recursive Probabilistic Models"],"prefix":"10.1007","author":[{"given":"Mihalis","family":"Yannakakis","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"issue":"3","key":"1_CR1","doi-asserted-by":"publisher","first-page":"273","DOI":"10.1145\/503502.503503","volume":"23","author":"R. Alur","year":"2001","unstructured":"Alur, R., Yannakakis, M.: Model checking of hierarchical state machines. ACM Trans. Prog. Lang. Sys.\u00a023(3), 273\u2013303 (2001)","journal-title":"ACM Trans. Prog. Lang. Sys."},{"key":"1_CR2","doi-asserted-by":"publisher","first-page":"786","DOI":"10.1145\/1075382.1075387","volume":"27","author":"R. Alur","year":"2005","unstructured":"Alur, R., Benedikt, M., Etessami, K., Godefroid, P., Reps, T.W., Yannakakis, M.: Analysis of recursive state machines. ACM Trans. Progr. Lang. Sys.\u00a027, 786\u2013818 (2005)","journal-title":"ACM Trans. Progr. Lang. Sys."},{"key":"1_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"135","DOI":"10.1007\/3-540-63141-0_10","volume-title":"CONCUR\u201997: Concurrency Theory","author":"A. Bouajjani","year":"1997","unstructured":"Bouajjani, A., Esparza, J., Maler, O.: Reachability analysis of pushdown automata: Applications to model checking. In: Mazurkiewicz, A., Winkowski, J. (eds.) CONCUR 1997. LNCS, vol.\u00a01243, pp. 135\u2013150. Springer, Heidelberg (1997)"},{"key":"1_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/11817949_24","volume-title":"CONCUR 2006 \u2013 Concurrency Theory","author":"T. Br\u00e1zdil","year":"2006","unstructured":"Br\u00e1zdil, T., Brozek, V., Forejt, V., Ku\u010dera, A.: Reachability in recursive Markov decision processes. In: Baier, C., Hermanns, H. (eds.) CONCUR 2006. LNCS, vol.\u00a04137, Springer, Heidelberg (2006)"},{"key":"1_CR5","doi-asserted-by":"crossref","unstructured":"Br\u00e1zdil, T., Ku\u010dera, A., Esparza, J.: Analysis and prediction of the long-run behavior of probabilistic sequential programs with recursion. In: Proc. of FOCS 2005, pp. 521\u2013530 (2005)","DOI":"10.1109\/SFCS.2005.19"},{"key":"1_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-31856-9_12","volume-title":"STACS 2005","author":"T. Br\u00e1zdil","year":"2005","unstructured":"Br\u00e1zdil, T., Ku\u010dera, A., Stra\u017eovsk\u00fd, O.: Decidability of temporal properties of probabilistic pushdown automata. In: Diekert, V., Durand, B. (eds.) STACS 2005. LNCS, vol.\u00a03404, Springer, Heidelberg (2005)"},{"issue":"6","key":"1_CR7","doi-asserted-by":"publisher","first-page":"1002","DOI":"10.1145\/235809.235813","volume":"43","author":"S. Basu","year":"1996","unstructured":"Basu, S., Pollack, R., Roy, M.F.: On the combinatorial and algebraic complexity of quantifier elimination. J. ACM\u00a043(6), 1002\u20131045 (1996)","journal-title":"J. ACM"},{"key":"1_CR8","doi-asserted-by":"crossref","unstructured":"Canny, J.: Some algebraic and geometric computations in PSPACE. In: Prof. of 20th ACM STOC, pp. 460\u2013467 (1988)","DOI":"10.1145\/62212.62257"},{"issue":"2","key":"1_CR9","doi-asserted-by":"publisher","first-page":"203","DOI":"10.1016\/0890-5401(92)90048-K","volume":"96","author":"A. Condon","year":"1992","unstructured":"Condon, A.: The complexity of stochastic games. Inf. & Comp.\u00a096(2), 203\u2013224 (1992)","journal-title":"Inf. & Comp."},{"issue":"4","key":"1_CR10","doi-asserted-by":"publisher","first-page":"857","DOI":"10.1145\/210332.210339","volume":"42","author":"C. Courcoubetis","year":"1995","unstructured":"Courcoubetis, C., Yannakakis, M.: The complexity of probabilistic verification. Journal of the ACM\u00a042(4), 857\u2013907 (1995)","journal-title":"Journal of the ACM"},{"issue":"10","key":"1_CR11","doi-asserted-by":"publisher","first-page":"1399","DOI":"10.1109\/9.720497","volume":"43","author":"C. Courcoubetis","year":"1998","unstructured":"Courcoubetis, C., Yannakakis, M.: Markov decision processes and regular events. IEEE Trans. on Automatic Control\u00a043(10), 1399\u20131418 (1998)","journal-title":"IEEE Trans. on Automatic Control"},{"key":"1_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"395","DOI":"10.1007\/3-540-46419-0_27","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"L. Alfaro de","year":"2000","unstructured":"de Alfaro, L., Kwiatkowska, M., Norman, G., Parker, D., Segala, R.: Symbolic model checking of probabilistic processes using MTBDDs and the kronecker representation. In: Schwartzbach, M.I., Graf, S. (eds.) ETAPS 2000 and TACAS 2000. LNCS, vol.\u00a01785, pp. 395\u2013410. Springer, Heidelberg (2000)"},{"issue":"2","key":"1_CR13","doi-asserted-by":"publisher","first-page":"374","DOI":"10.1016\/j.jcss.2003.07.009","volume":"68","author":"L. Alfaro de","year":"2004","unstructured":"de Alfaro, L., Majumdar, R.: Quantitative solution of omega-regular games. J. Comp. Sys. Sc.\u00a068(2), 374\u2013397 (2004)","journal-title":"J. Comp. Sys. Sc."},{"key":"1_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"232","DOI":"10.1007\/10722167_20","volume-title":"Computer Aided Verification","author":"J. Esparza","year":"2000","unstructured":"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.\u00a01855, pp. 232\u2013247. Springer, Heidelberg (2000)"},{"key":"#cr-split#-1_CR15.1","doi-asserted-by":"crossref","unstructured":"Esparza, J., Ku??era, A., Mayr, R.: Model checking probabilistic pushdown automata. In: Proc. of 19th IEEE LICS 2004 (2004);","DOI":"10.1109\/LICS.2004.1319596"},{"key":"#cr-split#-1_CR15.2","unstructured":"Full version in Logical Methods in Computer Science, vol.??2(1) (2006)"},{"key":"1_CR16","doi-asserted-by":"crossref","unstructured":"Esparza, J., Ku\u010dera, A., Mayr, R.: Quantitative analysis of probabilistic pushdown automata: expectations and variances. In: Proc. of 20th IEEE LICS (2005)","DOI":"10.1109\/LICS.2004.1319596"},{"key":"1_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-31856-9_28","volume-title":"STACS 2005","author":"K. Etessami","year":"2005","unstructured":"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.\u00a03404. Springer, Heidelberg (2005); Full expanded version available from: http:\/\/homepages.inf.ed.ac.uk\/kousha\/bib_index.html"},{"key":"1_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"253","DOI":"10.1007\/978-3-540-31980-1_17","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"K. Etessami","year":"2005","unstructured":"Etessami, K., Yannakakis, M.: Algorithmic verification of recursive probabilistic state machines. In: Halbwachs, N., Zuck, L.D. (eds.) TACAS 2005. LNCS, vol.\u00a03440, pp. 253\u2013270. Springer, Heidelberg (2005)"},{"key":"1_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"891","DOI":"10.1007\/11523468_72","volume-title":"Automata, Languages and Programming","author":"K. Etessami","year":"2005","unstructured":"Etessami, K., Yannakakis, M.: Recursive Markov Decision Processes and Recursive Stochastic Games. In: Caires, L., Italiano, G.F., Monteiro, L., Palamidessi, C., Yung, M. (eds.) ICALP 2005. LNCS, vol.\u00a03580, pp. 891\u2013903. Springer, Heidelberg (2005)"},{"key":"1_CR20","volume-title":"Proc. 2nd Intl. Conf. on Quantitative Evaluation of Systems","author":"K. Etessami","year":"2005","unstructured":"Etessami, K., Yannakakis, M.: Checking LTL Properties of Recursive Markov Chains. In: Proc. 2nd Intl. Conf. on Quantitative Evaluation of Systems. IEEE, Los Alamitos (2005)"},{"key":"1_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"634","DOI":"10.1007\/11672142_52","volume-title":"STACS 2006","author":"K. Etessami","year":"2006","unstructured":"Etessami, K., Yannakakis, M.: Efficient Analysis of Classes of Recursive Markov Decision Processes and Stochastic Games. In: Durand, B., Thomas, W. (eds.) STACS 2006. LNCS, vol.\u00a03884, pp. 634\u2013645. Springer, Heidelberg (2006)"},{"key":"1_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"324","DOI":"10.1007\/11787006_28","volume-title":"Automata, Languages and Programming","author":"K. Etessami","year":"2006","unstructured":"Etessami, K., Yannakakis, M.: Recursive concurrent stochastic games. In: Bugliesi, M., Preneel, B., Sassone, V., Wegener, I. (eds.) ICALP 2006. LNCS, vol.\u00a04052, pp. 324\u2013335. Springer, Heidelberg (2006)"},{"key":"1_CR23","unstructured":"Everett, C.J., Ulam, S.: Multiplicative systems, part i., ii, and iii. Technical Report 683, 690, 707, Los Alamos Scientific Laboratory (1948)"},{"key":"1_CR24","doi-asserted-by":"crossref","unstructured":"Fagin, R., Karlin, A., Kleinberg, J., Raghavan, P., Rajagopalan, S., Rubinfeld, R., Sudan, M., Tomkins, A.: Random walks with \u201cback buttons\u201d (extended abstract). In: ACM Symp. on Theory of Computing, pp. 484\u2013493 (2000)","DOI":"10.1145\/335305.335362"},{"volume-title":"Handbook of Markov Decision Processes","year":"2002","key":"1_CR25","unstructured":"Feinberg, E., Shwartz, A. (eds.): Handbook of Markov Decision Processes. Kluwer, Dordrecht (2002)"},{"key":"1_CR26","volume-title":"Competitive Markov Decision Processes","author":"J. Filar","year":"1997","unstructured":"Filar, J., Vrieze, K.: Competitive Markov Decision Processes. Springer, Heidelberg (1997)"},{"key":"1_CR27","doi-asserted-by":"crossref","unstructured":"Garey, M.R., Graham, R.L., Johnson, D.S.: Some NP-complete geometric problems. In: 8th ACM Symp. on Theory of Computing, pp. 10\u201322 (1976)","DOI":"10.1145\/800113.803626"},{"key":"1_CR28","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511629136","volume-title":"Branching Processes: Variation, Growth, and Extinction of Populations","author":"P. Haccou","year":"2005","unstructured":"Haccou, P., Jagers, P., Vatutin, V.A.: Branching Processes: Variation, Growth, and Extinction of Populations. Cambridge University Press, Cambridge (2005)"},{"key":"1_CR29","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-642-51866-9","volume-title":"The Theory of Branching Processes","author":"T.E. Harris","year":"1963","unstructured":"Harris, T.E.: The Theory of Branching Processes. Springer, Heidelberg (1963)"},{"key":"1_CR30","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"441","DOI":"10.1007\/11691372_29","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"A. Hinton","year":"2006","unstructured":"Hinton, A., Kwiatkowska, M.Z., Norman, G., Parker, D.: PRISM: A tool for automatic verification of probabilistic systems. In: Hermanns, H., Palsberg, J. (eds.) TACAS 2006 and ETAPS 2006. LNCS, vol.\u00a03920, pp. 441\u2013444. Springer, Heidelberg (2006)"},{"key":"1_CR31","volume-title":"Branching Processes with Biological Applications","author":"P. Jagers","year":"1975","unstructured":"Jagers, P.: Branching Processes with Biological Applications. Wiley, Chichester (1975)"},{"key":"1_CR32","first-page":"783","volume":"56","author":"A.N. Kolmogorov","year":"1947","unstructured":"Kolmogorov, A.N., Sevastyanov, B.A.: The calculation of final probabilities for branching random processes. Dokl. Akad. Nauk SSSR\u00a056, 783\u2013786 (1947) (Russian)","journal-title":"Dokl. Akad. Nauk SSSR"},{"key":"1_CR33","doi-asserted-by":"crossref","unstructured":"Kwiatkowska, M.: Model checking for probability and time: from theory to practice. In: 18th IEEE LICS, pp. 351\u2013360 (2003)","DOI":"10.1109\/LICS.2003.1210075"},{"key":"1_CR34","volume-title":"Foundations of Statistical Natural Language Processing","author":"C. Manning","year":"1999","unstructured":"Manning, C., Sch\u00fctze, H.: Foundations of Statistical Natural Language Processing. MIT Press, Cambridge (1999)"},{"key":"1_CR35","volume-title":"Introduction to Probabilistic Automata","author":"A. Paz","year":"1971","unstructured":"Paz, A.: Introduction to Probabilistic Automata. Academic Press, London (1971)"},{"issue":"1","key":"1_CR36","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1006\/inco.1993.1012","volume":"103","author":"A. Pnueli","year":"1993","unstructured":"Pnueli, A., Zuck, L.D.: Probabilistic verification. Inf. and Comp.\u00a0103(1), 1\u201329 (1993)","journal-title":"Inf. and Comp."},{"key":"1_CR37","doi-asserted-by":"publisher","DOI":"10.1002\/9780470316887","volume-title":"Markov Decision Processes","author":"M.L. Puterman","year":"1994","unstructured":"Puterman, M.L.: Markov Decision Processes. Wiley, Chichester (1994)"},{"issue":"3","key":"1_CR38","doi-asserted-by":"publisher","first-page":"255","DOI":"10.1016\/S0747-7171(10)80003-3","volume":"13","author":"J. Renegar","year":"1992","unstructured":"Renegar, J.: On the computational complexity and geometry of the first-order theory of the reals, parts I-III. J. Symb. Comp.\u00a013(3), 255\u2013352 (1992)","journal-title":"J. Symb. Comp."},{"issue":"23","key":"1_CR39","doi-asserted-by":"publisher","first-page":"5112","DOI":"10.1093\/nar\/22.23.5112","volume":"22","author":"Y. Sakakibara","year":"1994","unstructured":"Sakakibara, Y., Brown, M., Hughey, R., Mian, I.S., Sjolander, K., Underwood, R., Haussler, D.: Stochastic context-free grammars for tRNA modeling. Nucleic Acids Research\u00a022(23), 5112\u20135120 (1994)","journal-title":"Nucleic Acids Research"},{"key":"1_CR40","first-page":"47","volume":"6","author":"B.A. Sevastyanov","year":"1951","unstructured":"Sevastyanov, B.A.: The theory of branching processes. Uspehi Mathemat. Nauk\u00a06, 47\u201399 (1951) (Russian)","journal-title":"Uspehi Mathemat. Nauk"},{"key":"1_CR41","doi-asserted-by":"publisher","first-page":"1095","DOI":"10.1073\/pnas.39.10.1095","volume":"39","author":"L.S. Shapley","year":"1953","unstructured":"Shapley, L.S.: Stochastic games. Proc. Nat. Acad. Sci.\u00a039, 1095\u20131100 (1953)","journal-title":"Proc. Nat. Acad. Sci."},{"key":"1_CR42","doi-asserted-by":"crossref","unstructured":"Tiwari, P.: A problem that is easier to solve on the unit-cost algebraic ram. Journal of Complexity, 393\u2013397 (1992)","DOI":"10.1016\/0885-064X(92)90003-T"},{"key":"1_CR43","doi-asserted-by":"crossref","unstructured":"Vardi, M.: Automatic verification of probabilistic concurrent finite-state programs. In: Proc. of 26th IEEE FOCS, pp. 327\u2013338 (1985)","DOI":"10.1109\/SFCS.1985.12"}],"container-title":["Lecture Notes in Computer Science","Automated Technology for Verification and Analysis"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/11901914_1.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,1,11]],"date-time":"2025-01-11T09:47:55Z","timestamp":1736588875000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/11901914_1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2006]]},"ISBN":["9783540472377","9783540472384"],"references-count":44,"URL":"https:\/\/doi.org\/10.1007\/11901914_1","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2006]]}}}