{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2023,1,6]],"date-time":"2023-01-06T03:19:21Z","timestamp":1672975161453},"reference-count":26,"publisher":"Association for Computing Machinery (ACM)","issue":"2","funder":[{"DOI":"10.13039\/100000143","name":"Division of Computing and Communication Foundations","doi-asserted-by":"publisher","award":["CCF-07-28736CCF-10-17955"]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Comput. Logic"],"published-print":{"date-parts":[[2012,4]]},"abstract":"\n Recursive Markov Chains (RMCs) are a natural abstract model of procedural probabilistic programs and related systems involving recursion and probability. They succinctly define a class of denumerable Markov chains that generalize several other stochastic models, and they are equivalent in a precise sense to probabilistic Pushdown Systems. In this article, we study the problem of model checking an RMC against an\n \u03c9<\/jats:italic>\n -regular specification, given in terms of a B\u00fcchi automaton or a Linear Temporal Logic (LTL) formula. Namely, given an RMC\n A<\/jats:italic>\n and a property, we wish to know the probability that an execution of\n A<\/jats:italic>\n satisfies the property. We establish a number of strong upper bounds, as well as lower bounds, both for\n qualitative<\/jats:italic>\n problems (is the probability =\u20091, or =\u20090?), and for\n quantitative<\/jats:italic>\n problems (is the probability \u2265\u2009\n p<\/jats:italic>\n ?, or, approximate the probability to within a desired precision). The complexity upper bounds we obtain for automata and LTL properties are similar, although the algorithms are different.\n <\/jats:p>\n \n We present algorithms for the qualitative model checking problem that run in polynomial space in the size |\n A<\/jats:italic>\n | of the RMC and exponential time in the size of the property (the automaton or the LTL formula). For several classes of RMCs, including single-exit RMCs (a class that encompasses some well-studied stochastic models, for instance, stochastic context-free grammars) the algorithm runs in polynomial time in |\n A<\/jats:italic>\n |. For the quantitative model checking problem, we present algorithms that run in polynomial space in the RMC and exponential space in the property. For the class of linearly recursive RMCs we can compute the exact probability in time polynomial in the RMC and exponential in the property. For deterministic automata specifications, all our complexities in the specification come down by one exponential.\n <\/jats:p>\n \n For lower bounds, we show that the qualitative model checking problem, even for a fixed RMC, is already EXPTIME-complete. On the other hand, even for simple reachability analysis, we know from our prior work that our PSPACE upper bounds in\n A<\/jats:italic>\n can not be improved substantially without a breakthrough on a well-known open problem in the complexity of numerical computation.\n <\/jats:p>","DOI":"10.1145\/2159531.2159534","type":"journal-article","created":{"date-parts":[[2012,4,24]],"date-time":"2012-04-24T18:41:10Z","timestamp":1335292870000},"page":"1-40","update-policy":"http:\/\/dx.doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":12,"title":["Model Checking of Recursive Probabilistic Systems"],"prefix":"10.1145","volume":"13","author":[{"given":"Kousha","family":"Etessami","sequence":"first","affiliation":[{"name":"University of Edinburgh"}]},{"given":"Mihalis","family":"Yannakakis","sequence":"additional","affiliation":[{"name":"Columbia University"}]}],"member":"320","published-online":{"date-parts":[[2012,4]]},"reference":[{"key":"e_1_2_2_1_1","doi-asserted-by":"publisher","DOI":"10.1137\/070697926"},{"key":"e_1_2_2_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/1075382.1075387"},{"key":"e_1_2_2_3_1","volume-title":"Probability and Measure","author":"Billingsley P.","unstructured":"Billingsley , P. 1995. Probability and Measure 3 rd Ed. J. Wiley and Sons . Billingsley, P. 1995. Probability and Measure 3rd Ed. J. Wiley and Sons.","edition":"3"},{"key":"e_1_2_2_4_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_2_5_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-31856-9_12"},{"key":"e_1_2_2_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/62212.62257"},{"key":"e_1_2_2_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/210332.210339"},{"key":"e_1_2_2_8_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 University Press. Durbin R. Eddy S. R. Krogh A. and Mitchison G. 1999. Biological Sequence Analysis: Probabilistic models of Proteins and Nucleic Acids . Cambridge University Press.","DOI":"10.1017\/CBO9780511790492"},{"key":"e_1_2_2_9_1","doi-asserted-by":"publisher","DOI":"10.5555\/1018438.1021838"},{"key":"e_1_2_2_10_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-31980-1_17"},{"key":"e_1_2_2_11_1","doi-asserted-by":"publisher","DOI":"10.1007\/11523468_72"},{"key":"e_1_2_2_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/1462153.1462154"},{"key":"e_1_2_2_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/335305.335362"},{"key":"e_1_2_2_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/800113.803626"},{"key":"e_1_2_2_15_1","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511629136"},{"key":"e_1_2_2_16_1","volume-title":"The Theory of Branching Processes","author":"Harris T. E.","unstructured":"Harris , T. E. 1963. The Theory of Branching Processes . Springer . Harris, T. E. 1963. The Theory of Branching Processes. Springer."},{"key":"e_1_2_2_17_1","doi-asserted-by":"crossref","unstructured":"Kimmel M. and Axelrod D. E. 2002. Branching Processes in Biology. Springer. Kimmel M. and Axelrod D. E. 2002. Branching Processes in Biology . Springer.","DOI":"10.1007\/b97371"},{"key":"e_1_2_2_18_1","doi-asserted-by":"publisher","DOI":"10.5555\/788023.789069"},{"key":"e_1_2_2_19_1","unstructured":"Manning C. and Sch\u00fctze H. 1999. Foundations of Statistical Natural Language Processing. MIT Press. Manning C. and Sch\u00fctze H. 1999. Foundations of Statistical Natural Language Processing . MIT Press."},{"key":"e_1_2_2_20_1","doi-asserted-by":"publisher","DOI":"10.1109\/SFCS.1977.32"},{"key":"e_1_2_2_21_1","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1993.1012"},{"key":"e_1_2_2_22_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0747-7171(10)80003-3"},{"key":"e_1_2_2_23_1","doi-asserted-by":"publisher","DOI":"10.1016\/0885-064X(92)90003-T"},{"key":"e_1_2_2_24_1","doi-asserted-by":"publisher","DOI":"10.1109\/SFCS.1985.12"},{"key":"e_1_2_2_25_1","volume-title":"Proceedings of the 1st Symposium on Logic in Comp. Sci. (LICS). 322--331","author":"Vardi M. Y.","unstructured":"Vardi , M. Y. and Wolper , P . 1986. An automata-theoretic approach to automatic program verification . In Proceedings of the 1st Symposium on Logic in Comp. Sci. (LICS). 322--331 . Vardi, M. Y. and Wolper, P. 1986. An automata-theoretic approach to automatic program verification. In Proceedings of the 1st Symposium on Logic in Comp. Sci. (LICS). 322--331."},{"key":"e_1_2_2_26_1","doi-asserted-by":"publisher","DOI":"10.1109\/QEST.2005.8"}],"container-title":["ACM Transactions on Computational Logic"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/2159531.2159534","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,12,29]],"date-time":"2022-12-29T19:01:08Z","timestamp":1672340468000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2159531.2159534"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012,4]]},"references-count":26,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2012,4]]}},"alternative-id":["10.1145\/2159531.2159534"],"URL":"http:\/\/dx.doi.org\/10.1145\/2159531.2159534","relation":{},"ISSN":["1529-3785","1557-945X"],"issn-type":[{"value":"1529-3785","type":"print"},{"value":"1557-945X","type":"electronic"}],"subject":["Computational Mathematics","Logic","General Computer Science","Theoretical Computer Science"],"published":{"date-parts":[[2012,4]]},"assertion":[{"value":"2008-07-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2010-11-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2012-04-01","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}