{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,27]],"date-time":"2026-06-27T00:46:37Z","timestamp":1782521197353,"version":"3.54.5"},"reference-count":64,"publisher":"Association for Computing Machinery (ACM)","issue":"1","license":[{"start":{"date-parts":[[2009,1,1]],"date-time":"2009-01-01T00:00:00Z","timestamp":1230768000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/100000143","name":"Division of Computing and Communication Foundations","doi-asserted-by":"publisher","award":["CCF-04-30946CCF-07-28736"],"award-info":[{"award-number":["CCF-04-30946CCF-07-28736"]}],"id":[{"id":"10.13039\/100000143","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["J. ACM"],"published-print":{"date-parts":[[2009,1]]},"abstract":"<jats:p>\n            We define\n            <jats:italic>Recursive Markov Chains<\/jats:italic>\n            (RMCs), a class of finitely presented denumerable Markov chains, and we study algorithms for their analysis. Informally, an RMC consists of a collection of finite-state Markov chains with the ability to invoke each other in a potentially recursive manner. RMCs offer a natural abstract model for probabilistic programs with procedures. They generalize, in a precise sense, a number of well-studied stochastic models, including Stochastic Context-Free Grammars (SCFG) and Multi-Type Branching Processes (MT-BP).\n          <\/jats:p>\n          <jats:p>\n            We focus on algorithms for\n            <jats:italic>reachability<\/jats:italic>\n            and\n            <jats:italic>termination<\/jats:italic>\n            analysis for RMCs: what is the probability that an RMC started from a given state reaches another target state, or that it terminates? These probabilities are in general irrational, and they arise as (least) fixed point solutions to certain (monotone) systems of nonlinear equations associated with RMCs. We address both the\n            <jats:italic>qualitative problem<\/jats:italic>\n            of determining whether the probabilities are 0, 1 or in-between, and the\n            <jats:italic>quantitative problems<\/jats:italic>\n            of comparing the probabilities with a given bound, or approximating them to desired precision.\n          <\/jats:p>\n          <jats:p>\n            We show that all these problems can be solved in PSPACE using a decision procedure for the Existential Theory of Reals. We provide a more practical algorithm, based on a decomposed version of multi-variate Newton's method, and prove that it always converges monotonically to the desired probabilities. We show this method applies more generally to any monotone polynomial system. We obtain polynomial-time algorithms for various special subclasses of RMCs. Among these: for SCFGs and MT-BPs (equivalently, for\n            <jats:italic>1-exit<\/jats:italic>\n            RMCs) the qualitative problem can be solved in P-time; for\n            <jats:italic>linearly recursive<\/jats:italic>\n            RMCs the probabilities are rational and can be computed exactly in P-time.\n          <\/jats:p>\n          <jats:p>\n            We show that our PSPACE upper bounds cannot be substantially improved without a breakthrough on long standing open problems: the\n            <jats:italic>square-root sum<\/jats:italic>\n            problem and an arithmetic circuit decision problem that captures P-time on the unit-cost rational arithmetic RAM model. We show that these problems reduce to the qualitative problem and to the approximation problem (to within any nontrivial error) for termination probabilities of general RMCs, and to the quantitative decision problem for termination (extinction) of SCFGs (MT-BPs).\n          <\/jats:p>","DOI":"10.1145\/1462153.1462154","type":"journal-article","created":{"date-parts":[[2009,2,4]],"date-time":"2009-02-04T13:01:58Z","timestamp":1233752518000},"page":"1-66","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":111,"title":["Recursive Markov chains, stochastic grammars, and monotone systems of nonlinear equations"],"prefix":"10.1145","volume":"56","author":[{"given":"Kousha","family":"Etessami","sequence":"first","affiliation":[{"name":"University of Edinburgh, Edinburgh, UK"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Mihalis","family":"Yannakakis","sequence":"additional","affiliation":[{"name":"Columbia University, New York, New York"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2009,2,3]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.3115\/1034678.1034759"},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1109\/CCC.2006.30"},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/1075382.1075387"},{"key":"e_1_2_1_4_1","volume-title":"Proceedings of the of 13th International Conference on Computer-Aided Verification. 304--313","author":"Alur R.","unstructured":"Alur , R. , Etessami , K. , and Yannakakis , M . 2001. Analysis of recursive state machines . In Proceedings of the of 13th International Conference on Computer-Aided Verification. 304--313 . Alur, R., Etessami, K., and Yannakakis, M. 2001. Analysis of recursive state machines. In Proceedings of the of 13th International Conference on Computer-Aided Verification. 304--313."},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/503502.503503"},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/103516.103517"},{"key":"e_1_2_1_7_1","doi-asserted-by":"crossref","unstructured":"Athreya K. B. and Ney P. E. 1972. Branching processes. Springer-Verlag Berlin Germany.  Athreya K. B. and Ney P. E. 1972. Branching processes. Springer-Verlag Berlin Germany.","DOI":"10.1007\/978-3-642-65371-1"},{"key":"e_1_2_1_8_1","volume-title":"Stochastic Processes: Theory and Methods. Handbook of Statist.","volume":"19","author":"Athreya K. B.","unstructured":"Athreya , K. B. , and Vidyashankar , A. N . 2001. Branching processes . In Stochastic Processes: Theory and Methods. Handbook of Statist. , vol. 19 . North-Holland, Amsterdam, the Netherlands, 35--53. Athreya, K. B., and Vidyashankar, A. N. 2001. Branching processes. In Stochastic Processes: Theory and Methods. Handbook of Statist., vol. 19. North-Holland, Amsterdam, the Netherlands, 35--53."},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1016\/0012-365X(73)90166-0"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/235809.235813"},{"key":"e_1_2_1_11_1","doi-asserted-by":"crossref","unstructured":"Basu S. Pollack F. and Roy M. F. 2003. Algorithms in Real Algebraic Geometry. Springer-Verlag Berlin Germany.   Basu S. Pollack F. and Roy M. F. 2003. Algorithms in Real Algebraic Geometry. Springer-Verlag Berlin Germany.","DOI":"10.1007\/978-3-662-05355-3"},{"key":"e_1_2_1_12_1","volume-title":"Proceedings of the 28th International Colloquium on Automata, Languages and Programming (ICALP). 652--666","author":"Benedikt M.","unstructured":"Benedikt , M. , Godefroid , P. , and Reps , T . 2001. Model checking of unrestricted hierarchical state machines . In Proceedings of the 28th International Colloquium on Automata, Languages and Programming (ICALP). 652--666 . Benedikt, M., Godefroid, P., and Reps, T. 2001. Model checking of unrestricted hierarchical state machines. In Proceedings of the 28th International Colloquium on Automata, Languages and Programming (ICALP). 652--666."},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/800076.802470"},{"key":"e_1_2_1_14_1","doi-asserted-by":"crossref","unstructured":"Blum L. Cucker F. Shub M. and Smale S. 1998. Complexity and Real Computation. Springer-Verlag Berlin Germany.   Blum L. Cucker F. Shub M. and Smale S. 1998. Complexity and Real Computation. Springer-Verlag Berlin Germany.","DOI":"10.1007\/978-1-4612-0701-6"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1109\/T-C.1973.223746"},{"key":"e_1_2_1_16_1","volume-title":"Proceedings of the 8th International Conference on Concurrency Theory (CONCUR). 135--150","author":"Bouajjani A.","unstructured":"Bouajjani , A. , Esparza , J. , and Maler , O . 1997. Reachability analysis of pushdown automata: Applications to model checking . In Proceedings of the 8th International Conference on Concurrency Theory (CONCUR). 135--150 . Bouajjani, A., Esparza, J., and Maler, O. 1997. Reachability analysis of pushdown automata: Applications to model checking. In Proceedings of the 8th International Conference on Concurrency Theory (CONCUR). 135--150."},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1109\/SFCS.2005.19"},{"key":"e_1_2_1_18_1","volume-title":"Proceedings of the 22nd Symposium on Theoretical Aspects of Computer Science (STACS).","author":"Br\u00e1zdil T.","unstructured":"Br\u00e1zdil , T. , Ku\u010dera , A. , and Stra\u017eovsk\u00fd , O . 2005b. Decidability of temporal properties of probabilistic pushdown automata . In Proceedings of the 22nd Symposium on Theoretical Aspects of Computer Science (STACS). Br\u00e1zdil, T., Ku\u010dera, A., and Stra\u017eovsk\u00fd, O. 2005b. Decidability of temporal properties of probabilistic pushdown automata. In Proceedings of the 22nd Symposium on Theoretical Aspects of Computer Science (STACS)."},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/62212.62257"},{"key":"e_1_2_1_20_1","first-page":"298","article-title":"Estimation of probabilistic context-free grammars","volume":"24","author":"Chi Z.","year":"1998","unstructured":"Chi , Z. , and Geman , S. 1998 . Estimation of probabilistic context-free grammars . Computat. Ling. 24 , 2, 298 -- 305 . Chi, Z., and Geman, S. 1998. Estimation of probabilistic context-free grammars. Computat. Ling. 24, 2, 298--305.","journal-title":"Computat. Ling."},{"key":"e_1_2_1_21_1","doi-asserted-by":"crossref","unstructured":"Durbin R. Eddy S. R. Krogh A. and Mitchison G. 1999. Biological Sequence Analysis: Probabilistic models of Proteins and Nucleic Acids. Cambridge Univ. Press Cambridge MA.  Durbin R. Eddy S. R. Krogh A. and Mitchison G. 1999. Biological Sequence Analysis: Probabilistic models of Proteins and Nucleic Acids. Cambridge Univ. Press Cambridge MA.","DOI":"10.1017\/CBO9780511790492"},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.5555\/647769.734087"},{"key":"e_1_2_1_23_1","volume-title":"Proceedings of the 25th International Symposium on Theoretical Aspects of Computer Science (STACS). 289--300","author":"Esparza J.","unstructured":"Esparza , J. , Kiefer , S. , and Luttenberger , M . 2008. Convergence thresholds of Newton's method for monotone polynomial equations . In Proceedings of the 25th International Symposium on Theoretical Aspects of Computer Science (STACS). 289--300 . Esparza, J., Kiefer, S., and Luttenberger, M. 2008. Convergence thresholds of Newton's method for monotone polynomial equations. In Proceedings of the 25th International Symposium on Theoretical Aspects of Computer Science (STACS). 289--300."},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.5555\/1018438.1021838"},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2005.39"},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1109\/QEST.2008.35"},{"key":"e_1_2_1_27_1","volume-title":"Proceedings of the 11th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS). 253--270","author":"Etessami K.","unstructured":"Etessami , K. , and Yannakakis , M . 2005a. Algorithmic verification of recursive probabilistic state machines . In Proceedings of the 11th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS). 253--270 . Etessami, K., and Yannakakis, M. 2005a. Algorithmic verification of recursive probabilistic state machines. In Proceedings of the 11th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS). 253--270."},{"key":"e_1_2_1_28_1","volume-title":"Proceedings of the 22nd Symposium on Theoretical Aspects of Computer Science (STACS). 340--352","author":"Etessami K.","unstructured":"Etessami , K. , and Yannakakis , M . 2005b. Recursive Markov chains, stochastic grammars, and monotone systems of nonlinear equations . In Proceedings of the 22nd Symposium on Theoretical Aspects of Computer Science (STACS). 340--352 . Etessami, K., and Yannakakis, M. 2005b. Recursive Markov chains, stochastic grammars, and monotone systems of nonlinear equations. In Proceedings of the 22nd Symposium on Theoretical Aspects of Computer Science (STACS). 340--352."},{"key":"e_1_2_1_29_1","volume-title":"Proceedings of the 32nd International Colloquium on Automata, Languages, and Programming (ICALP). 891--903","author":"Etessami K.","unstructured":"Etessami , K. , and Yannakakis , M . 2005c. Recursive Markov decision processes and recursive stochastic games . In Proceedings of the 32nd International Colloquium on Automata, Languages, and Programming (ICALP). 891--903 . Etessami, K., and Yannakakis, M. 2005c. Recursive Markov decision processes and recursive stochastic games. In Proceedings of the 32nd International Colloquium on Automata, Languages, and Programming (ICALP). 891--903."},{"key":"e_1_2_1_30_1","volume-title":"Proceedings of the 23rd Symposium on Theoretical Aspects of Computer Science (STACS). 634--645","author":"Etessami K.","unstructured":"Etessami , K. , and Yannakakis , M . 2006a. Efficient analysis of classes of recursive Markov decision processes and stochastic games . In Proceedings of the 23rd Symposium on Theoretical Aspects of Computer Science (STACS). 634--645 . Etessami, K., and Yannakakis, M. 2006a. Efficient analysis of classes of recursive Markov decision processes and stochastic games. In Proceedings of the 23rd Symposium on Theoretical Aspects of Computer Science (STACS). 634--645."},{"key":"e_1_2_1_31_1","volume-title":"Proceedings of the 33rd International Colloquium on Automata, Languages, and Programming (ICALP). 324--335","author":"Etessami K.","unstructured":"Etessami , K. , and Yannakakis , M . 2006b. Recursive concurrent stochastic games . In Proceedings of the 33rd International Colloquium on Automata, Languages, and Programming (ICALP). 324--335 . Etessami, K., and Yannakakis, M. 2006b. Recursive concurrent stochastic games. In Proceedings of the 33rd International Colloquium on Automata, Languages, and Programming (ICALP). 324--335."},{"key":"e_1_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1109\/FOCS.2007.48"},{"key":"e_1_2_1_33_1","unstructured":"Everett C. J. and Ulam S. 1948. Multiplicative systems Part I. II and III. Tech. Rep. 683 690 707 Los Alamos Scientific Laboratory.  Everett C. J. and Ulam S. 1948. Multiplicative systems Part I. II and III. Tech. Rep. 683 690 707 Los Alamos Scientific Laboratory."},{"key":"e_1_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/335305.335362"},{"key":"e_1_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/800113.803626"},{"key":"e_1_2_1_36_1","volume-title":"Lectures on Pattern Theory","author":"Grenander U.","unstructured":"Grenander , U. 1976. Lectures on Pattern Theory , Vol. 1 . Springer-Verlag . Grenander, U. 1976. Lectures on Pattern Theory, Vol. 1. Springer-Verlag."},{"key":"e_1_2_1_37_1","doi-asserted-by":"crossref","unstructured":"Gr\u00f6tschel M. Lov\u00e1sz L. and Schrijver A. 1993. Geometric Algorithms and Combinatorial Optimization 2nd ed. Springer-Verlag Berlin Germany.  Gr\u00f6tschel M. Lov\u00e1sz L. and Schrijver A. 1993. Geometric Algorithms and Combinatorial Optimization 2nd ed. Springer-Verlag Berlin Germany.","DOI":"10.1007\/978-3-642-78240-4"},{"key":"e_1_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511629136"},{"key":"e_1_2_1_39_1","volume-title":"The Theory of Branching Processes","author":"Harris T. E.","unstructured":"Harris , T. E. 1963. The Theory of Branching Processes . Springer-Verlag , Berlin, Germany . Harris, T. E. 1963. The Theory of Branching Processes. Springer-Verlag, Berlin, Germany."},{"key":"e_1_2_1_40_1","unstructured":"Hopcroft J. Motwani R. and Ullman J. D. 2000. Introduction to Automata Theory Languages and Computation. Addisson-Wesley Reading MA.   Hopcroft J. Motwani R. and Ullman J. D. 2000. Introduction to Automata Theory Languages and Computation. Addisson-Wesley Reading MA."},{"key":"e_1_2_1_41_1","doi-asserted-by":"crossref","unstructured":"Horn R. J. and Johnson C. R. 1985. Matrix Analysis. Cambridge Univ. Press Cambridge UK.   Horn R. J. and Johnson C. R. 1985. Matrix Analysis. Cambridge Univ. Press Cambridge UK.","DOI":"10.1017\/CBO9780511810817"},{"key":"e_1_2_1_42_1","volume-title":"Branching Processes with Biological Applications","author":"Jagers P.","unstructured":"Jagers , P. 1975. Branching Processes with Biological Applications . Wiley , New York . Jagers, P. 1975. Branching Processes with Biological Applications. Wiley, New York."},{"key":"e_1_2_1_43_1","doi-asserted-by":"publisher","DOI":"10.1145\/780542.780595"},{"key":"e_1_2_1_44_1","volume-title":"A First Course in Stochastic Processes","author":"Karlin S.","unstructured":"Karlin , S. 1966. A First Course in Stochastic Processes . Academic Press , Orlando, FL . Karlin, S. 1966. A First Course in Stochastic Processes. Academic Press, Orlando, FL."},{"key":"e_1_2_1_45_1","doi-asserted-by":"publisher","DOI":"10.1145\/1250790.1250822"},{"key":"e_1_2_1_46_1","doi-asserted-by":"crossref","unstructured":"Kimmel M. and Axelrod D. E. 2002. Branching processes in biology. Springer-Verlag Berlin Germany.  Kimmel M. and Axelrod D. E. 2002. Branching processes in biology. Springer-Verlag Berlin Germany.","DOI":"10.1007\/b97371"},{"key":"e_1_2_1_47_1","first-page":"783","article-title":"The calculation of final probabilities for branching random processes","volume":"56","author":"Kolmogorov A. N.","year":"1947","unstructured":"Kolmogorov , A. N. , and Sevastyanov , B. A. 1947 . The calculation of final probabilities for branching random processes . Dokaldy 56 , 783 -- 786 . (Russian). Kolmogorov, A. N., and Sevastyanov, B. A. 1947. The calculation of final probabilities for branching random processes. Dokaldy 56, 783--786. (Russian).","journal-title":"Dokaldy"},{"key":"e_1_2_1_48_1","unstructured":"Lancaster P. and Tismenetsky M. 1985. The Theory of Matrices 2nd ed. Academic Press Orlando FL.  Lancaster P. and Tismenetsky M. 1985. The Theory of Matrices 2nd ed. Academic Press Orlando FL."},{"key":"e_1_2_1_49_1","doi-asserted-by":"crossref","unstructured":"Latouche G. and Ramaswami V. 1999. Introduction to Matrix Analytic Methods in Stochastic Modeling. ASA-SIAM series on statistics and applied probability.  Latouche G. and Ramaswami V. 1999. Introduction to Matrix Analytic Methods in Stochastic Modeling. ASA-SIAM series on statistics and applied probability.","DOI":"10.1137\/1.9780898719734"},{"key":"e_1_2_1_50_1","unstructured":"Manning C. and Sch\u00fctze H. 1999. Foundations of Statistical Natural Language Processing. MIT Press Cambridge MA.   Manning C. and Sch\u00fctze H. 1999. Foundations of Statistical Natural Language Processing. MIT Press Cambridge MA."},{"key":"e_1_2_1_51_1","volume-title":"No. 34","author":"Mode C. J.","unstructured":"Mode , C. J. 1971. Multitype Branching Processes. Theory and Applications. Modern Analytic and Computational Methods in Science and Mathematics , No. 34 . American Elsevier . Mode, C. J. 1971. Multitype Branching Processes. Theory and Applications. Modern Analytic and Computational Methods in Science and Mathematics, No. 34. American Elsevier."},{"key":"e_1_2_1_52_1","doi-asserted-by":"publisher","DOI":"10.1007\/s11168-008-9052-8"},{"key":"e_1_2_1_53_1","volume-title":"Matrix-Geometric Solutions in Stochastic Models:an algorithmic approach","author":"Neuts M. F.","unstructured":"Neuts , M. F. 1981. Matrix-Geometric Solutions in Stochastic Models:an algorithmic approach . Johns Hopkins Univ. Press , Baltimore, MD . Neuts, M. F. 1981. Matrix-Geometric Solutions in Stochastic Models:an algorithmic approach. Johns Hopkins Univ. Press, Baltimore, MD."},{"key":"e_1_2_1_54_1","unstructured":"Ortega J. M. and Rheinbolt W. 1970. Iterative Solution of Nonlinear Equations in Several Variables. Academic Press Orlando FL.   Ortega J. M. and Rheinbolt W. 1970. Iterative Solution of Nonlinear Equations in Several Variables. Academic Press Orlando FL."},{"key":"e_1_2_1_55_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0747-7171(10)80005-7"},{"key":"e_1_2_1_56_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0950-5849(98)00093-7"},{"key":"e_1_2_1_57_1","doi-asserted-by":"publisher","DOI":"10.1093\/nar\/22.23.5112"},{"key":"e_1_2_1_58_1","doi-asserted-by":"publisher","DOI":"10.5555\/646233.682381"},{"key":"e_1_2_1_59_1","first-page":"47","article-title":"The theory of branching processes","volume":"6","author":"Sevastyanov B. A.","year":"1951","unstructured":"Sevastyanov , B. A. 1951 . The theory of branching processes . Uspehi Mathemat. Nauk 6 , 47 -- 99 . (Russian). Sevastyanov, B. A. 1951. The theory of branching processes. Uspehi Mathemat. Nauk 6, 47--99. (Russian).","journal-title":"Uspehi Mathemat. Nauk"},{"key":"e_1_2_1_60_1","volume-title":"Galois Theory","author":"Stewart I.","unstructured":"Stewart , I. 1989. Galois Theory , 2 nd ed. Chapman & Hall , London, UK . Stewart, I. 1989. Galois Theory, 2nd ed. Chapman & Hall, London, UK.","edition":"2"},{"key":"e_1_2_1_61_1","doi-asserted-by":"crossref","unstructured":"Stoer J. and Bulirsch R. 1993. Introduction to Numerical Analysis. Springer-Verlag Berlin Germany.  Stoer J. and Bulirsch R. 1993. Introduction to Numerical Analysis. Springer-Verlag Berlin Germany.","DOI":"10.1007\/978-1-4757-2272-7"},{"key":"e_1_2_1_62_1","doi-asserted-by":"publisher","DOI":"10.1016\/0885-064X(92)90003-T"},{"key":"e_1_2_1_63_1","volume-title":"Proceedings of the 13th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS). 66--71","author":"Wojtczak D.","unstructured":"Wojtczak , D. , and Etessami , K . 2007. Premo: An analyzer for probabilistic recursive models . In Proceedings of the 13th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS). 66--71 . Wojtczak, D., and Etessami, K. 2007. Premo: An analyzer for probabilistic recursive models. In Proceedings of the 13th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS). 66--71."},{"key":"e_1_2_1_64_1","doi-asserted-by":"publisher","DOI":"10.1109\/QEST.2005.8"}],"container-title":["Journal of the ACM"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1462153.1462154","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/1462153.1462154","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T13:30:14Z","timestamp":1750253414000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1462153.1462154"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2009,1]]},"references-count":64,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2009,1]]}},"alternative-id":["10.1145\/1462153.1462154"],"URL":"https:\/\/doi.org\/10.1145\/1462153.1462154","relation":{},"ISSN":["0004-5411","1557-735X"],"issn-type":[{"value":"0004-5411","type":"print"},{"value":"1557-735X","type":"electronic"}],"subject":[],"published":{"date-parts":[[2009,1]]},"assertion":[{"value":"2006-07-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2008-11-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2009-02-03","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}