{"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":1782521197345,"version":"3.54.5"},"publisher-location":"Cham","reference-count":47,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783031308192","type":"print"},{"value":"9783031308208","type":"electronic"}],"license":[{"start":{"date-parts":[[2023,1,1]],"date-time":"2023-01-01T00:00:00Z","timestamp":1672531200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2023,4,20]],"date-time":"2023-04-20T00:00:00Z","timestamp":1681948800000},"content-version":"vor","delay-in-days":109,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2023]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>Probabilistic pushdown automata (pPDA) are a standard model for discrete probabilistic programs with procedures and recursion. In pPDA, many quantitative properties are characterized as least fixpoints of polynomial equation systems. In this paper, we study the problem of<jats:italic>certifying<\/jats:italic>that these quantities lie within certain bounds. To this end, we first characterize the polynomial systems that admit easy-to-check certificates for validating bounds on their least fixpoint. Second, we present a sound and complete Optimistic Value Iteration algorithm for computing such certificates. Third, we show how certificates for polynomial systems can be transferred to certificates for various quantitative pPDA properties. Experiments demonstrate that our algorithm computes succinct certificates for several intricate example programs as well as stochastic context-free grammars with<jats:inline-formula><jats:tex-math>$$&gt; 10^4$$<\/jats:tex-math><\/jats:inline-formula>production rules.<\/jats:p>","DOI":"10.1007\/978-3-031-30820-8_24","type":"book-chapter","created":{"date-parts":[[2023,4,19]],"date-time":"2023-04-19T19:02:36Z","timestamp":1681930956000},"page":"391-409","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":5,"title":["Certificates for Probabilistic Pushdown Automata via Optimistic Value Iteration"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-1084-6408","authenticated-orcid":false,"given":"Tobias","family":"Winkler","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-6143-1926","authenticated-orcid":false,"given":"Joost-Pieter","family":"Katoen","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2023,4,20]]},"reference":[{"key":"24_CR1","doi-asserted-by":"crossref","unstructured":"Azeem, M., Evangelidis, A., Kret\u00ednsk\u00fd, J., Slivinskiy, A., Weininger, M.: Optimistic and topological value iteration for simple stochastic games. In: ATVA. Lecture Notes in Computer Science, vol. 13505, pp. 285\u2013302. Springer (2022)","DOI":"10.1007\/978-3-031-19992-9_18"},{"key":"24_CR2","unstructured":"Baier, C., Katoen, J.: Principles of model checking. MIT Press (2008)"},{"key":"24_CR3","doi-asserted-by":"crossref","unstructured":"Baier, C., Klein, J., Leuschner, L., Parker, D., Wunderlich, S.: Ensuring the Reliability of Your Model Checker: Interval Iteration for Markov Decision Processes. In: CAV (1). Lecture Notes in Computer Science, vol. 10426, pp. 160\u2013180. Springer (2017)","DOI":"10.1007\/978-3-319-63387-9_8"},{"key":"24_CR4","doi-asserted-by":"crossref","unstructured":"Barbosa, H., Barrett, C.W., Brain, M., Kremer, G., Lachnitt, H., Mann, M., Mohamed, A., Mohamed, M., Niemetz, A., N\u00f6tzli, A., Ozdemir, A., Preiner, M., Reynolds, A., Sheng, Y., Tinelli, C., Zohar, Y.: cvc5: A versatile and industrial-strength SMT solver. In: TACAS (1). Lecture Notes in Computer Science, vol. 13243, pp. 415\u2013442. Springer (2022)","DOI":"10.1007\/978-3-030-99524-9_24"},{"key":"24_CR5","doi-asserted-by":"crossref","unstructured":"Batz, K., Chen, M., Kaminski, B.L., Katoen, J., Matheja, C., Schr\u00f6er, P.: Latticed k-induction with an application to probabilistic programs. In: CAV (2). Lecture Notes in Computer Science, vol. 12760, pp. 524\u2013549. Springer (2021)","DOI":"10.1007\/978-3-030-81688-9_25"},{"key":"24_CR6","doi-asserted-by":"crossref","unstructured":"Bishop, C.M.: Model-based machine learning. Philosophical Transactions of the Royal Society A: Mathematical, Physical and Engineering Sciences 371(1984), 20120222 (2013)","DOI":"10.1098\/rsta.2012.0222"},{"key":"24_CR7","doi-asserted-by":"crossref","unstructured":"Br\u00e1zdil, T., Esparza, J., Kiefer, S., Kucera, A.: Analyzing probabilistic pushdown automata. Formal Methods Syst. Des. 43(2), 124\u2013163 (2013)","DOI":"10.1007\/s10703-012-0166-0"},{"key":"24_CR8","doi-asserted-by":"crossref","unstructured":"Br\u00e1zdil, T., Kiefer, S., Kucera, A., Varekov\u00e1, I.H.: Runtime analysis of probabilistic programs with unbounded recursion. J. Comput. Syst. Sci. 81(1), 288\u2013310 (2015)","DOI":"10.1016\/j.jcss.2014.06.005"},{"key":"24_CR9","unstructured":"Chiang, D., Riley, D.: Factor Graph Grammars. In: NeurIPS (2020)"},{"key":"24_CR10","unstructured":"Esparza, J., Gaiser, A., Kiefer, S.: Computing Least Fixed Points of Probabilistic Systems of Polynomials. In: STACS. LIPIcs, vol.\u00a05, pp. 359\u2013370. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik (2010)"},{"key":"24_CR11","doi-asserted-by":"crossref","unstructured":"Esparza, J., Kiefer, S., Luttenberger, M.: Convergence Thresholds of Newton\u2019s Method for Monotone Polynomial Equations. In: STACS. LIPIcs, vol.\u00a01, pp. 289\u2013300. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik, Germany (2008)","DOI":"10.1145\/1250790.1250822"},{"key":"24_CR12","doi-asserted-by":"crossref","unstructured":"Esparza, J., Kiefer, S., Luttenberger, M.: Computing the Least Fixed Point of Positive Polynomial Systems. SIAM J. Comput. 39(6), 2282\u20132335 (2010)","DOI":"10.1137\/090749591"},{"key":"24_CR13","doi-asserted-by":"crossref","unstructured":"Esparza, J., Kucera, A., Mayr, R.: Model Checking Probabilistic Pushdown Automata. In: LICS. pp. 12\u201321. IEEE Computer Society (2004)","DOI":"10.1109\/LICS.2004.1319596"},{"key":"24_CR14","doi-asserted-by":"crossref","unstructured":"Esparza, J., Kucera, A., Mayr, R.: Quantitative Analysis of Probabilistic Pushdown Automata: Expectations and Variances. In: LICS. pp. 117\u2013126. IEEE Computer Society (2005)","DOI":"10.1109\/LICS.2005.39"},{"key":"24_CR15","doi-asserted-by":"crossref","unstructured":"Esparza, J., Lammich, P., Neumann, R., Nipkow, T., Schimpf, A., Smaus, J.: A fully verified executable LTL model checker. In: CAV. Lecture Notes in Computer Science, vol.\u00a08044, pp. 463\u2013478. Springer (2013)","DOI":"10.1007\/978-3-642-39799-8_31"},{"key":"24_CR16","doi-asserted-by":"crossref","unstructured":"Etessami, K., Yannakakis, M.: Recursive Markov Chains, Stochastic Grammars, and Monotone Systems of Nonlinear Equations. In: STACS. Lecture Notes in Computer Science, vol.\u00a03404, pp. 340\u2013352. Springer (2005)","DOI":"10.1007\/978-3-540-31856-9_28"},{"key":"24_CR17","doi-asserted-by":"crossref","unstructured":"Etessami, K., Yannakakis, M.: Recursive Markov chains, stochastic grammars, and monotone systems of nonlinear equations. J. ACM 56(1), 1:1\u20131:66 (2009)","DOI":"10.1145\/1462153.1462154"},{"key":"24_CR18","doi-asserted-by":"crossref","unstructured":"Flajolet, P., Sedgewick, R.: Analytic Combinatorics. Cambridge University Press (2009)","DOI":"10.1017\/CBO9780511801655"},{"key":"24_CR19","doi-asserted-by":"crossref","unstructured":"Funke, F., Jantsch, S., Baier, C.: Farkas Certificates and Minimal Witnesses for Probabilistic Reachability Constraints. In: TACAS (1). Lecture Notes in Computer Science, vol. 12078, pp. 324\u2013345. Springer (2020)","DOI":"10.1007\/978-3-030-45190-5_18"},{"key":"24_CR20","doi-asserted-by":"crossref","unstructured":"Haddad, S., Monmege, B.: Reachability in mdps: Refining convergence of value iteration. In: RP. Lecture Notes in Computer Science, vol.\u00a08762, pp. 125\u2013137. Springer (2014)","DOI":"10.1007\/978-3-319-11439-2_10"},{"key":"24_CR21","doi-asserted-by":"crossref","unstructured":"Hartmanns, A.: Correct Probabilistic Model Checking with Floating-Point Arithmetic. In: TACAS (2). Lecture Notes in Computer Science, vol. 13244, pp. 41\u201359. Springer (2022)","DOI":"10.1007\/978-3-030-99527-0_3"},{"key":"24_CR22","doi-asserted-by":"crossref","unstructured":"Hartmanns, A., Kaminski, B.L.: Optimistic value iteration. In: CAV (2). Lecture Notes in Computer Science, vol. 12225, pp. 488\u2013511. Springer (2020)","DOI":"10.1007\/978-3-030-53291-8_26"},{"key":"24_CR23","unstructured":"Jantsch, S.: Certificates and Witnesses for Probabilistic Model Checking. Ph.D. thesis, Dresden University of Technology, Germany (2022)"},{"key":"24_CR24","doi-asserted-by":"crossref","unstructured":"Jantsch, S., Funke, F., Baier, C.: Minimal Witnesses for Probabilistic Timed Automata. In: ATVA. Lecture Notes in Computer Science, vol. 12302, pp. 501\u2013517. Springer (2020)","DOI":"10.1007\/978-3-030-59152-6_28"},{"key":"24_CR25","doi-asserted-by":"crossref","unstructured":"Jurafsky, D., Wooters, C., Segal, J., Stolcke, A., Fosler, E., Tajchman, G.N., Morgan, N.: Using a stochastic context-free grammar as a language model for speech recognition. In: ICASSP. pp. 189\u2013192. IEEE Computer Society (1995)","DOI":"10.1109\/ICASSP.1995.479396"},{"key":"24_CR26","doi-asserted-by":"crossref","unstructured":"Karp, R.M.: An introduction to randomized algorithms. Discret. Appl. Math. 34(1-3), 165\u2013201 (1991)","DOI":"10.1016\/0166-218X(91)90086-C"},{"key":"24_CR27","doi-asserted-by":"crossref","unstructured":"Kiefer, S., Luttenberger, M., Esparza, J.: On the convergence of newton\u2019s method for monotone systems of polynomial equations. In: STOC. pp. 217\u2013226. ACM (2007)","DOI":"10.1145\/1250790.1250822"},{"key":"24_CR28","doi-asserted-by":"crossref","unstructured":"Knudsen, B., Hein, J.: Pfold: RNA secondary structure prediction using stochastic context-free grammars. Nucleic Acids Res. 31(13), 3423\u20133428 (2003)","DOI":"10.1093\/nar\/gkg614"},{"key":"24_CR29","doi-asserted-by":"crossref","unstructured":"Kobayashi, N., Dal Lago, U., Grellois, C.: On the Termination Problem for Probabilistic Higher-Order Recursive Programs. Log. Methods Comput. Sci. 16(4) (2020)","DOI":"10.1109\/LICS.2019.8785679"},{"key":"24_CR30","doi-asserted-by":"crossref","unstructured":"Kucera, A., Esparza, J., Mayr, R.: Model checking probabilistic pushdown automata. Log. Methods Comput. Sci. 2(1) (2006)","DOI":"10.2168\/LMCS-2(1:2)2006"},{"key":"24_CR31","doi-asserted-by":"crossref","unstructured":"McConnell, R.M., Mehlhorn, K., N\u00e4her, S., Schweitzer, P.: Certifying algorithms. Comput. Sci. Rev. 5(2), 119\u2013161 (2011)","DOI":"10.1016\/j.cosrev.2010.09.009"},{"key":"24_CR32","unstructured":"van\u00a0de Meent, J., Paige, B., Yang, H., Wood, F.: An Introduction to Probabilistic Programming. CoRR abs\/1809.10756 (2018)"},{"key":"24_CR33","doi-asserted-by":"crossref","unstructured":"Michail, D., Kinable, J., Naveh, B., Sichi, J.V.: Jgrapht - A java library for graph data structures and algorithms. ACM Trans. Math. Softw. 46(2), 16:1\u201316:29 (2020)","DOI":"10.1145\/3381449"},{"key":"24_CR34","doi-asserted-by":"crossref","unstructured":"de\u00a0Moura, L.M., Bj\u00f8rner, N.S.: Z3: an efficient SMT solver. In: TACAS. Lecture Notes in Computer Science, vol.\u00a04963, pp. 337\u2013340. Springer (2008)","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"24_CR35","doi-asserted-by":"crossref","unstructured":"Olmedo, F., Kaminski, B.L., Katoen, J., Matheja, C.: Reasoning about Recursive Probabilistic Programs. In: LICS. pp. 672\u2013681. ACM (2016)","DOI":"10.1145\/2933575.2935317"},{"key":"24_CR36","doi-asserted-by":"crossref","unstructured":"Quatmann, T., Katoen, J.: Sound Value Iteration. In: CAV (1). Lecture Notes in Computer Science, vol. 10981, pp. 643\u2013661. Springer (2018)","DOI":"10.1007\/978-3-319-96145-3_37"},{"key":"24_CR37","doi-asserted-by":"crossref","unstructured":"Rothblum, U.G.: Nonnegative matrices and stochastic matrices. In: Hogben, L. (ed.) Handbook of Linear Algebra. CRC press (2006)","DOI":"10.1201\/9781420010572-9"},{"key":"24_CR38","doi-asserted-by":"crossref","unstructured":"Saad, Y.: Numerical methods for large eigenvalue problems: revised edition. SIAM (2011)","DOI":"10.1137\/1.9781611970739"},{"key":"24_CR39","doi-asserted-by":"crossref","unstructured":"Simistira, F., Katsouros, V., Carayannis, G.: Recognition of online handwritten mathematical formulas using probabilistic SVMs and stochastic context free grammars. Pattern Recognit. Lett. 53, 85\u201392 (2015)","DOI":"10.1016\/j.patrec.2014.11.015"},{"key":"24_CR40","doi-asserted-by":"crossref","unstructured":"Stewart, A., Etessami, K., Yannakakis, M.: Upper Bounds for Newton\u2019s Method on Monotone Polynomial Systems, and P-Time Model Checking of Probabilistic One-Counter Automata. J. ACM 62(4), 30:1\u201330:33 (2015)","DOI":"10.1145\/2789208"},{"key":"24_CR41","doi-asserted-by":"crossref","unstructured":"Wimmer, S., von Mutius, J.: Verified Certification of Reachability Checking for Timed Automata. In: TACAS (1). Lecture Notes in Computer Science, vol. 12078, pp. 425\u2013443. Springer (2020)","DOI":"10.1007\/978-3-030-45190-5_24"},{"key":"24_CR42","doi-asserted-by":"crossref","unstructured":"Winkler, T., Gehnen, C., Katoen, J.: Model Checking Temporal Properties of Recursive Probabilistic Programs. In: FoSSaCS. Lecture Notes in Computer Science, vol. 13242, pp. 449\u2013469. Springer (2022)","DOI":"10.1007\/978-3-030-99253-8_23"},{"key":"24_CR43","doi-asserted-by":"publisher","unstructured":"Winkler, T., Katoen, J.: Artifcat Evaluation for TACAS \u201923 Paper: \u201cCertificates for Probabilistic Pushdown Automata via Optimistic Value Iteration\u201d (2023). https:\/\/doi.org\/10.5281\/zenodo.7506305","DOI":"10.5281\/zenodo.7506305"},{"key":"24_CR44","doi-asserted-by":"publisher","unstructured":"Winkler, T., Katoen, J.P.: Certificates for Probabilistic Pushdown Automata via Optimistic Value Iteration (2023). https:\/\/doi.org\/10.48550\/ARXIV.2301.08657","DOI":"10.48550\/ARXIV.2301.08657"},{"key":"24_CR45","unstructured":"Wojtczak, D.: Recursive probabilistic models : efficient analysis and implementation. Ph.D. thesis, University of Edinburgh, UK (2009)"},{"key":"24_CR46","doi-asserted-by":"crossref","unstructured":"Wojtczak, D., Etessami, K.: PReMo : An Analyzer for Probabilistic Recursive Models. In: TACAS. Lecture Notes in Computer Science, vol.\u00a04424, pp. 66\u201371. Springer (2007)","DOI":"10.1007\/978-3-540-71209-1_7"},{"key":"24_CR47","doi-asserted-by":"crossref","unstructured":"Yannakakis, M., Etessami, K.: Checking LTL properties of recursive markov chains. In: QEST. pp. 155\u2013165. IEEE Computer Society (2005)","DOI":"10.1109\/QEST.2005.8"}],"container-title":["Lecture Notes in Computer Science","Tools and Algorithms for the Construction and Analysis of Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-30820-8_24","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,10,18]],"date-time":"2024-10-18T20:03:51Z","timestamp":1729281831000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-30820-8_24"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023]]},"ISBN":["9783031308192","9783031308208"],"references-count":47,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-30820-8_24","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2023]]},"assertion":[{"value":"20 April 2023","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"TACAS","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Tools and Algorithms for the Construction and Analysis of Systems","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Paris","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"France","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2023","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"22 April 2023","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"27 April 2023","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"29","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"tacas2023","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/etaps.org\/2023\/tacas","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Double-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"EasyChair","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"169","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"56","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"6","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"33% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"11","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Yes","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}