{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,11]],"date-time":"2025-10-11T17:08:49Z","timestamp":1760202529972,"version":"3.41.2"},"reference-count":32,"publisher":"Centre pour la Communication Scientifique Directe (CCSD)","license":[{"start":{"date-parts":[[2006,3,7]],"date-time":"2006-03-07T00:00:00Z","timestamp":1141689600000},"content-version":"unspecified","delay-in-days":0,"URL":"https:\/\/arxiv.org\/licenses\/assumed-1991-2003"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"abstract":"<jats:p>We consider the model checking problem for probabilistic pushdown automata (pPDA) and properties expressible in various probabilistic logics. We start with properties that can be formulated as instances of a generalized random walk problem. We prove that both qualitative and quantitative model checking for this class of properties and pPDA is decidable. Then we show that model checking for the qualitative fragment of the logic PCTL and pPDA is also decidable. Moreover, we develop an error-tolerant model checking algorithm for PCTL and the subclass of stateless pPDA. Finally, we consider the class of omega-regular properties and show that both qualitative and quantitative model checking for pPDA is decidable.<\/jats:p>","DOI":"10.2168\/lmcs-2(1:2)2006","type":"journal-article","created":{"date-parts":[[2006,11,23]],"date-time":"2006-11-23T09:26:14Z","timestamp":1164273974000},"source":"Crossref","is-referenced-by-count":26,"title":["Model Checking Probabilistic Pushdown Automata"],"prefix":"10.46298","volume":"Volume 2, Issue 1","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-9862-4919","authenticated-orcid":false,"given":"Javier","family":"Esparza","sequence":"first","affiliation":[]},{"given":"Antonin","family":"Kucera","sequence":"additional","affiliation":[]},{"given":"Richard","family":"Mayr","sequence":"additional","affiliation":[]}],"member":"25203","published-online":{"date-parts":[[2006,3,7]]},"reference":[{"key":"10.2168\/LMCS-2(1:2)2006_ABIJ:CONCUR00-IC","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2004.12.001"},{"key":"10.2168\/LMCS-2(1:2)2006_AEY:recursive-state-machines","doi-asserted-by":"crossref","unstructured":"R. Alur, K. Etessami, and M. Yannakakis. Analysis of recursive state machines. InProceedings of CAV 2001, volume 2102 ofLecture Notes in Computer Science, pages 207-220. Springer, 2001.","DOI":"10.1007\/3-540-44585-4_18"},{"key":"10.2168\/LMCS-2(1:2)2006_AAP:prob-grammars-automata-ACL","doi-asserted-by":"crossref","unstructured":"A. Abney, D. McAllester, and F. Pereira. Relating probabilistic grammars and automata. InProceedings of ACP'99, pages 542-549, 1999.","DOI":"10.3115\/1034678.1034759"},{"key":"10.2168\/LMCS-2(1:2)2006_AR:prob-systems-faulty-FOSSACS","doi-asserted-by":"crossref","unstructured":"P.A. Abdulla and A. Rabinovich. Verification of probabilistic systems with faulty communication. InProceedings of FoSSaCS 2003, volume 2620 ofLecture Notes in Computer Science, pages 39-53. Springer, 2003.","DOI":"10.1007\/3-540-36576-1_3"},{"key":"10.2168\/LMCS-2(1:2)2006_ASBBV:logic-stochastic-CAV","doi-asserted-by":"crossref","unstructured":"A. Aziz, V. Singhal, F. Balarin, R. Brayton, and A. Sangiovanni-Vincentelli. It usually works: The temporal logic of stochastic systems. InProceedings of CAV'95, volume 939 ofLecture Notes in Computer Science, pages 155-165. Springer, 1995.","DOI":"10.1007\/3-540-60045-0_48"},{"key":"10.2168\/LMCS-2(1:2)2006_BE:probLCS-algorithms-ARTS","doi-asserted-by":"crossref","unstructured":"C. Baier and B. Engelen. Establishing qualitative properties for probabilistic lossy channel systems: an algorithmic approach. InProceedings of 5th International AMASTWorkshop on Real-Time and Probabilistic Systems {(ARTS'99)}, volume 1601 ofLecture Notes in Computer Science, pages 34-52. Springer, 1999.","DOI":"10.1007\/3-540-48778-6_3"},{"key":"10.2168\/LMCS-2(1:2)2006_BEM:PDA-reachability","doi-asserted-by":"crossref","unstructured":"A. Bouajjani, J. Esparza, and O. Maler. Reachability analysis of pushdown automata: application to model checking. InProceedings of CONCUR'97, volume 1243 ofLecture Notes in Computer Science, pages 135-150. Springer, 1997.","DOI":"10.1007\/3-540-63141-0_10"},{"key":"10.2168\/LMCS-2(1:2)2006_BKS:pPDA-temporal","doi-asserted-by":"crossref","unstructured":"T. Br\u00e1zdil, A. Ku\u010dera, and O. Stra\\v{z}ovsk\u00fd. On the decidability of temporal properties of probabilistic pushdown automata. InProceedings of STACS'2005, volume 3404 ofLecture Notes in Computer Science, pages 145-157. Springer, 2005.","DOI":"10.1007\/978-3-540-31856-9_12"},{"key":"10.2168\/LMCS-2(1:2)2006_BS:mu-calculus","doi-asserted-by":"crossref","unstructured":"O. Burkart and B. Steffen. Model checking the full modal mu-calculus for infinite sequential processes. InProceedings of ICALP'97, volume 1256 ofLecture Notes in Computer Science, pages 419-429. Springer, 1997.","DOI":"10.1007\/3-540-63165-8_198"},{"key":"10.2168\/LMCS-2(1:2)2006_BS:PLCS-prob-decidable","doi-asserted-by":"crossref","unstructured":"N. Bertrand and Ph. Schnoebelen. Model checking lossy channel systems is probably decidable. InProceedings of FoSSaCS 2003, volume 2620 ofLecture Notes in Computer Science, pages 120-135. Springer, 2003.","DOI":"10.1007\/3-540-36576-1_8"},{"key":"10.2168\/LMCS-2(1:2)2006_BW:book","doi-asserted-by":"crossref","unstructured":"J.C.M. Baeten and W.P. Weijland.Process Algebra. Number 18 in Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, 1990.","DOI":"10.1017\/CBO9780511624193"},{"key":"10.2168\/LMCS-2(1:2)2006_Canny:Tarski-exist-PSPACE","doi-asserted-by":"crossref","unstructured":"J. Canny. Some algebraic and geometric computations in PSPACE. InProceedings of STOC'88, pages 460-467. ACM Press, 1988.","DOI":"10.1145\/62212.62257"},{"key":"10.2168\/LMCS-2(1:2)2006_CSS:Prob-LTL-checking","doi-asserted-by":"crossref","unstructured":"J.M. Couvreur, N. Saheb, and G. Sutre. An optimal automata approach to LTL model checking of probabilistic systems. InProceedings of LPAR 2003, volume 2850 ofLecture Notes in Computer Science, pages 361-375. Springer, 2003.","DOI":"10.1007\/978-3-540-39813-4_26"},{"key":"10.2168\/LMCS-2(1:2)2006_CY:temporal-probabilistic-FOCS","doi-asserted-by":"crossref","unstructured":"C. Courcoubetis and M. Yannakakis. Verifying temporal properties of finite-state probabilistic programs. InProceedings of FOCS'88, pages 338-345. IEEE Computer Society Press, 1988.","DOI":"10.1109\/SFCS.1988.21950"},{"issue":"4","key":"10.2168\/LMCS-2(1:2)2006_CY:probab-verification-JACM","doi-asserted-by":"crossref","first-page":"857","DOI":"10.1145\/210332.210339","volume":"42","author":"C. Courcoubetis and M. Yannakakis","year":"1995","journal-title":"Journal of the Association for Computing Machinery 42(4):857-907, 1995"},{"key":"10.2168\/LMCS-2(1:2)2006_EHRS:MC-PDA","doi-asserted-by":"crossref","unstructured":"J. Esparza, D. Hansel, P. Rossmanith, and S. Schwoon. Efficient algorithms for model checking pushdown systems. InProceedings of CAV 2000, volume 1855 ofLecture Notes in Computer Science, pages 232-247. Springer, 2000.","DOI":"10.1007\/10722167_20"},{"key":"10.2168\/LMCS-2(1:2)2006_EKM:prob-PDA-PCTL","doi-asserted-by":"crossref","unstructured":"J. Esparza, A. Ku\u010dera, and R. Mayr. Model-checking probabilistic pushdown automata. InProceedings of LICS 2004, pages 12-21. IEEE Computer Society Press, 2004.","DOI":"10.1109\/LICS.2004.1319596"},{"key":"10.2168\/LMCS-2(1:2)2006_EKS:PDA-regular-valuations-IC","doi-asserted-by":"publisher","DOI":"10.1016\/S0890-5401(03)00139-1"},{"key":"10.2168\/LMCS-2(1:2)2006_EY:pPDA-LTL-complexity","doi-asserted-by":"crossref","unstructured":"K. Etessami and M. Yannakakis. Algorithmic verification of recursive probabilistic systems. Technical Report, School of Informatics, U. of Edinburgh, 2005.","DOI":"10.1007\/978-3-540-31980-1_17"},{"key":"10.2168\/LMCS-2(1:2)2006_EY:RMC-SG-equations","doi-asserted-by":"crossref","unstructured":"K. Etessami and M. Yannakakis. Recursive Markov chains, stochastic grammars, and monotone systems of non-linear equations. InProceedings of STACS'2005, volume 3404 ofLecture Notes in Computer Science, pages 340-352. Springer, 2005.","DOI":"10.1007\/978-3-540-31856-9_28"},{"key":"10.2168\/LMCS-2(1:2)2006_Feller:book","unstructured":"W. Feller.An Introduction to Probability Theory and Its Applications. Wiley & Sons, 1966."},{"key":"10.2168\/LMCS-2(1:2)2006_Grigoriev:Tarski-exponential-JSC","doi-asserted-by":"publisher","DOI":"10.1016\/S0747-7171(88)80006-3"},{"key":"10.2168\/LMCS-2(1:2)2006_HJ:logic-time-probability-FAC","doi-asserted-by":"publisher","DOI":"10.1007\/BF01211866"},{"key":"10.2168\/LMCS-2(1:2)2006_HK:quantitative-mu-calculus-LICS","doi-asserted-by":"crossref","unstructured":"M. Huth and M.Z. Kwiatkowska. Quantitative analysis and model checking. InProceedings of LICS'97, pages 111-122. IEEE Computer Society Press, 1997.","DOI":"10.1109\/LICS.1997.614940"},{"key":"10.2168\/LMCS-2(1:2)2006_HS:Prob-temp-logic","doi-asserted-by":"crossref","unstructured":"S. Hart and M. Sharir. Probabilistic temporal logic for finite and bounded models. InProceedings of POPL'84, pages 1-13. ACM Press, 1984.","DOI":"10.1145\/800057.808660"},{"key":"10.2168\/LMCS-2(1:2)2006_IN:probLCS-TACAS","doi-asserted-by":"crossref","unstructured":"S.P. Iyer and M. Narasimha. Probabilistic lossy channel systems. InProceedings of TAPSOFT'97, volume 1214 ofLecture Notes in Computer Science, pages 667-681. Springer, 1997.","DOI":"10.1007\/BFb0030633"},{"key":"10.2168\/LMCS-2(1:2)2006_LS:time-chance-IC","doi-asserted-by":"publisher","DOI":"10.1016\/S0019-9958(82)91022-1"},{"key":"10.2168\/LMCS-2(1:2)2006_MO:probPDA-properties-TCS","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(98)00059-0"},{"key":"10.2168\/LMCS-2(1:2)2006_Rabinovich:probLCS-LTL-ICALP","doi-asserted-by":"crossref","unstructured":"A. Rabinovich. Quantitative analysis of probabilistic lossy channel systems. InProceedings of ICALP 2003, volume 2719 ofLecture Notes in Computer Science, pages 1008-1021. Springer, 2003.","DOI":"10.1007\/3-540-45061-0_78"},{"key":"10.2168\/LMCS-2(1:2)2006_Tarski:reals-arithmetic","doi-asserted-by":"crossref","unstructured":"A. Tarski.A Decision Method for Elementary Algebra and Geometry. Univ. of California Press, Berkeley, 1951.","DOI":"10.1525\/9780520348097"},{"key":"10.2168\/LMCS-2(1:2)2006_Vardi:verif-prob-conc-syst","doi-asserted-by":"crossref","unstructured":"M. Vardi. Automatic verification of probabilistic concurrent finite-state programs. InProceedings of FOCS'85, pages 327-338. IEEE Computer Society Press, 1985.","DOI":"10.1109\/SFCS.1985.12"},{"key":"10.2168\/LMCS-2(1:2)2006_Walukiewicz:CAV96-IC","doi-asserted-by":"publisher","DOI":"10.1006\/inco.2000.2894"}],"container-title":["Logical Methods in Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/lmcs.episciences.org\/2256\/pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/lmcs.episciences.org\/2256\/pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,1,12]],"date-time":"2025-01-12T02:17:33Z","timestamp":1736648253000},"score":1,"resource":{"primary":{"URL":"https:\/\/lmcs.episciences.org\/2256"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2006,3,7]]},"references-count":32,"URL":"https:\/\/doi.org\/10.2168\/lmcs-2(1:2)2006","relation":{"is-same-as":[{"id-type":"arxiv","id":"cs\/0508003","asserted-by":"subject"},{"id-type":"doi","id":"10.48550\/arXiv.cs\/0508003","asserted-by":"subject"}],"is-referenced-by":[{"id-type":"doi","id":"10.2200\/s00430ed1v01y201206dtm027","asserted-by":"subject"}]},"ISSN":["1860-5974"],"issn-type":[{"type":"electronic","value":"1860-5974"}],"subject":[],"published":{"date-parts":[[2006,3,7]]},"article-number":"2256"}}