{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,27]],"date-time":"2026-06-27T00:46:31Z","timestamp":1782521191556,"version":"3.54.5"},"publisher-location":"Cham","reference-count":30,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783030992521","type":"print"},{"value":"9783030992538","type":"electronic"}],"license":[{"start":{"date-parts":[[2022,1,1]],"date-time":"2022-01-01T00:00:00Z","timestamp":1640995200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2022,3,29]],"date-time":"2022-03-29T00:00:00Z","timestamp":1648512000000},"content-version":"vor","delay-in-days":87,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2022]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>Probabilistic pushdown automata (pPDA) are a standard operational model for programming languages involving discrete random choices, procedures, and returns. Temporal properties are useful for gaining insight into the chronological order of events during program execution. Existing approaches in the literature have focused mostly on <jats:inline-formula><jats:alternatives><jats:tex-math>$$\\omega $$<\/jats:tex-math><mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\">\n                <mml:mi>\u03c9<\/mml:mi>\n              <\/mml:math><\/jats:alternatives><\/jats:inline-formula>-regular and LTL properties. In this paper, we study the model checking problem of pPDA against <jats:inline-formula><jats:alternatives><jats:tex-math>$$\\omega $$<\/jats:tex-math><mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\">\n                <mml:mi>\u03c9<\/mml:mi>\n              <\/mml:math><\/jats:alternatives><\/jats:inline-formula>-visibly pushdown languages that can be described by specification logics such as CaRet and are strictly more expressive than <jats:inline-formula><jats:alternatives><jats:tex-math>$$\\omega $$<\/jats:tex-math><mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\">\n                <mml:mi>\u03c9<\/mml:mi>\n              <\/mml:math><\/jats:alternatives><\/jats:inline-formula>-regular properties. With these logical formulae, it is possible to specify properties that explicitly take the structured computations arising from procedural programs into account. For example, CaRet is able to match procedure calls with their corresponding future returns, and thus allows to express fundamental program properties like total and partial correctness.<\/jats:p>","DOI":"10.1007\/978-3-030-99253-8_23","type":"book-chapter","created":{"date-parts":[[2022,3,28]],"date-time":"2022-03-28T20:02:48Z","timestamp":1648497768000},"page":"449-469","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":8,"title":["Model Checking Temporal Properties of Recursive Probabilistic Programs"],"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-6548-3432","authenticated-orcid":false,"given":"Christina","family":"Gehnen","sequence":"additional","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":[[2022,3,29]]},"reference":[{"key":"23_CR1","doi-asserted-by":"publisher","unstructured":"Alur, R., Arenas, M., Barcel\u00f3, P., Etessami, K., Immerman, N., Libkin, L.: First-Order and Temporal Logics for Nested Words. In: 22nd IEEE Symposium on Logic in Computer Science (LICS 2007), 10-12 July 2007, Wroclaw, Poland, Proceedings. pp. 151\u2013160. IEEE Computer Society (2007). https:\/\/doi.org\/10.1109\/LICS.2007.19","DOI":"10.1109\/LICS.2007.19"},{"key":"23_CR2","doi-asserted-by":"publisher","unstructured":"Alur, R., Bouajjani, A., Esparza, J.: Model Checking Procedural Programs. In: Clarke, E.M., Henzinger, T.A., Veith, H., Bloem, R. (eds.) Handbook of Model Checking, pp. 541\u2013572. Springer (2018). https:\/\/doi.org\/10.1007\/978-3-319-10575-8_17","DOI":"10.1007\/978-3-319-10575-8_17"},{"key":"23_CR3","doi-asserted-by":"publisher","unstructured":"Alur, R., Etessami, K., Madhusudan, P.: A Temporal Logic of Nested Calls and Returns. In: Tools and Algorithms for the Construction and Analysis of Systems, 10th International Conference, TACAS 2004, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2004, Barcelona, Spain, March 29 - April 2, 2004, Proceedings. Lecture Notes in Computer Science, vol.\u00a02988, pp. 467\u2013481. Springer (2004). https:\/\/doi.org\/10.1007\/978-3-540-24730-2_35","DOI":"10.1007\/978-3-540-24730-2_35"},{"key":"23_CR4","doi-asserted-by":"publisher","unstructured":"Alur, R., Madhusudan, P.: Visibly Pushdown Languages. In: Proceedings of the 36th Annual ACM Symposium on Theory of Computing, Chicago, IL, USA, June 13-16, 2004. pp. 202\u2013211. ACM (2004). https:\/\/doi.org\/10.1145\/1007352.1007390","DOI":"10.1145\/1007352.1007390"},{"key":"23_CR5","doi-asserted-by":"publisher","unstructured":"Audebaud, P., Paulin-Mohring, C.: Proofs of randomized algorithms in Coq. Sci. Comput. Program. 74(8), 568\u2013589 (2009). https:\/\/doi.org\/10.1016\/j.scico.2007.09.002","DOI":"10.1016\/j.scico.2007.09.002"},{"key":"23_CR6","unstructured":"Baier, C., Katoen, J.P.: Principles of Model Checking. MIT Press (2008)"},{"key":"23_CR7","doi-asserted-by":"publisher","unstructured":"Barthe, G., K\u00f6pf, B., Olmedo, F., B\u00e9guelin, S.Z.: Probabilistic Relational Reasoning for Differential Privacy. ACM Trans. Program. Lang. Syst. 35(3), 9:1\u20139:49 (2013). https:\/\/doi.org\/10.1145\/2492061","DOI":"10.1145\/2492061"},{"key":"23_CR8","doi-asserted-by":"publisher","unstructured":"Bozzelli, L., S\u00e1nchez, C.: Visibly Linear Temporal Logic. J. Autom. Reason. 60(2), 177\u2013220 (2018). https:\/\/doi.org\/10.1007\/s10817-017-9410-z","DOI":"10.1007\/s10817-017-9410-z"},{"key":"23_CR9","doi-asserted-by":"publisher","unstructured":"Br\u00e1zdil, T., Esparza, J., Kiefer, S., Kucera, A.: Analyzing probabilistic pushdown automata. Formal Methods Syst. Des. 43(2), 124\u2013163 (2013). https:\/\/doi.org\/10.1007\/s10703-012-0166-0","DOI":"10.1007\/s10703-012-0166-0"},{"key":"23_CR10","doi-asserted-by":"publisher","unstructured":"Br\u00e1zdil, T., Kucera, A., Strazovsk\u00fd, O.: On the Decidability of Temporal Properties of Probabilistic Pushdown Automata. In: STACS 2005, 22nd Annual Symposium on Theoretical Aspects of Computer Science, Stuttgart, Germany, February 24-26, 2005, Proceedings. Lecture Notes in Computer Science, vol.\u00a03404, pp. 145\u2013157. Springer (2005). https:\/\/doi.org\/10.1007\/978-3-540-31856-9_12","DOI":"10.1007\/978-3-540-31856-9_12"},{"key":"23_CR11","unstructured":"Casini, L., Illari, P.M., Russo, F., Williamson, J.: Recursive Bayesian Networks. Theoria. Revista de Teoria, Historia y Fundamentos de la Ciencia 26(1), 5\u201333 (2008)"},{"key":"23_CR12","doi-asserted-by":"publisher","unstructured":"Chiari, M., Mandrioli, D., Pradella, M.: Operator precedence temporal logic and model checking. Theor. Comput. Sci. 848, 47\u201381 (2020). https:\/\/doi.org\/10.1016\/j.tcs.2020.08.034","DOI":"10.1016\/j.tcs.2020.08.034"},{"key":"23_CR13","doi-asserted-by":"publisher","unstructured":"Dubslaff, C., Baier, C., Berg, M.: Model checking probabilistic systems against pushdown specifications. Inf. Process. Lett. 112(8-9), 320\u2013328 (2012). https:\/\/doi.org\/10.1016\/j.ipl.2012.01.006","DOI":"10.1016\/j.ipl.2012.01.006"},{"key":"23_CR14","doi-asserted-by":"publisher","unstructured":"Esparza, J., Kucera, A., Mayr, R.: Model Checking Probabilistic Pushdown Automata. In: 19th IEEE Symposium on Logic in Computer Science (LICS 2004), 14-17 July 2004, Turku, Finland, Proceedings. pp. 12\u201321. IEEE Computer Society (2004). https:\/\/doi.org\/10.1109\/LICS.2004.1319596","DOI":"10.1109\/LICS.2004.1319596"},{"key":"23_CR15","doi-asserted-by":"publisher","unstructured":"Etessami, K., Yannakakis, M.: Algorithmic Verification of Recursive Probabilistic State Machines. In: Tools and Algorithms for the Construction and Analysis of Systems, 11th International Conference, TACAS 2005, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2005, Edinburgh, UK, April 4-8, 2005, Proceedings. Lecture Notes in Computer Science, vol.\u00a03440, pp. 253\u2013270. Springer (2005). https:\/\/doi.org\/10.1007\/978-3-540-31980-1_17","DOI":"10.1007\/978-3-540-31980-1_17"},{"key":"23_CR16","doi-asserted-by":"publisher","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). https:\/\/doi.org\/10.1145\/1462153.1462154","DOI":"10.1145\/1462153.1462154"},{"key":"23_CR17","doi-asserted-by":"publisher","unstructured":"Gordon, A.D., Henzinger, T.A., Nori, A.V., Rajamani, S.K.: Probabilistic programming. In: Proceedings of the on Future of Software Engineering, FOSE 2014, Hyderabad, India, May 31 - June 7, 2014. pp. 167\u2013181. ACM (2014). https:\/\/doi.org\/10.1145\/2593882.2593900","DOI":"10.1145\/2593882.2593900"},{"key":"23_CR18","doi-asserted-by":"publisher","unstructured":"Gutsfeld, J.O., M\u00fcller-Olm, M., Nordhoff, B.: A Branching Time Variant of CaRet. In: Model Checking Software - 25th International Symposium, SPIN 2018, Malaga, Spain, June 20-22, 2018, Proceedings. Lecture Notes in Computer Science, vol. 10869, pp. 153\u2013170. Springer (2018). https:\/\/doi.org\/10.1007\/978-3-319-94111-0_9","DOI":"10.1007\/978-3-319-94111-0_9"},{"key":"23_CR19","doi-asserted-by":"publisher","unstructured":"Jaeger, M.: Complex Probabilistic Modeling with Recursive Relational Bayesian Networks. Ann. Math. Artif. Intell. 32(1-4), 179\u2013220 (2001). https:\/\/doi.org\/10.1023\/A:1016713501153","DOI":"10.1023\/A:1016713501153"},{"key":"23_CR20","unstructured":"Jones, C.: Probabilistic non-determinism. Ph.D. thesis, University of Edinburgh, UK (1990), http:\/\/hdl.handle.net\/1842\/413"},{"key":"23_CR21","doi-asserted-by":"publisher","unstructured":"Kucera, A., Esparza, J., Mayr, R.: Model Checking Probabilistic Pushdown Automata. Log. Methods Comput. Sci. 2(1) (2006). https:\/\/doi.org\/10.2168\/LMCS-2(1:2)2006","DOI":"10.2168\/LMCS-2(1:2)2006"},{"key":"23_CR22","doi-asserted-by":"publisher","unstructured":"L\u00f6ding, C., Madhusudan, P., Serre, O.: Visibly Pushdown Games. In: FSTTCS 2004: Foundations of Software Technology and Theoretical Computer Science, 24th International Conference, Chennai, India, December 16-18, 2004, Proceedings. Lecture Notes in Computer Science, vol.\u00a03328, pp. 408\u2013420. Springer (2004). https:\/\/doi.org\/10.1007\/978-3-540-30538-5_34","DOI":"10.1007\/978-3-540-30538-5_34"},{"key":"23_CR23","doi-asserted-by":"publisher","unstructured":"McIver, A., Morgan, C.: Partial correctness for probabilistic demonic programs. Theor. Comput. Sci. 266(1-2), 513\u2013541 (2001). https:\/\/doi.org\/10.1016\/S0304-3975(00)00208-5","DOI":"10.1016\/S0304-3975(00)00208-5"},{"key":"23_CR24","unstructured":"van\u00a0de Meent, J., Paige, B., Yang, H., Wood, F.: An Introduction to Probabilistic Programming. CoRR abs\/1809.10756 (2018), http:\/\/arxiv.org\/abs\/1809.10756"},{"key":"23_CR25","doi-asserted-by":"publisher","unstructured":"Olmedo, F., Kaminski, B.L., Katoen, J., Matheja, C.: Reasoning about Recursive Probabilistic Programs. In: Proceedings of the 31st Annual ACM\/IEEE Symposium on Logic in Computer Science, LICS \u201916, New York, NY, USA, July 5-8, 2016. pp. 672\u2013681. ACM (2016). https:\/\/doi.org\/10.1145\/2933575.2935317","DOI":"10.1145\/2933575.2935317"},{"key":"23_CR26","unstructured":"Pfeffer, A., Koller, D.: Semantics and Inference for Recursive Probability Models. In: Proceedings of the Seventeenth National Conference on Artificial Intelligence and Twelfth Conference on on Innovative Applications of Artificial Intelligence, July 30 - August 3, 2000, Austin, Texas, USA. pp. 538\u2013544. AAAI Press \/ The MIT Press (2000), http:\/\/www.aaai.org\/Library\/AAAI\/2000\/aaai00-082.php"},{"key":"23_CR27","unstructured":"Stuhlm\u00fcller, A., Goodman, N.D.: A Dynamic Programming Algorithm for Inference in Recursive Probabilistic Programs. CoRR abs\/1206.3555 (2012), http:\/\/arxiv.org\/abs\/1206.3555"},{"key":"23_CR28","unstructured":"Winkler, T., Gehnen, C., Katoen, J.: Model Checking Temporal Properties of Recursive Probabilistic Programs. CoRR abs\/2111.03501 (2021), https:\/\/arxiv.org\/abs\/2111.03501"},{"key":"23_CR29","doi-asserted-by":"publisher","unstructured":"Wojtczak, D., Etessami, K.: PReMo : An Analyzer for Probabilistic Recursive Models. In: Tools and Algorithms for the Construction and Analysis of Systems, 13th International Conference, TACAS 2007, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2007 Braga, Portugal, March 24 - April 1, 2007, Proceedings. Lecture Notes in Computer Science, vol.\u00a04424, pp. 66\u201371. Springer (2007). https:\/\/doi.org\/10.1007\/978-3-540-71209-1_7","DOI":"10.1007\/978-3-540-71209-1_7"},{"key":"23_CR30","doi-asserted-by":"publisher","unstructured":"Yannakakis, M., Etessami, K.: Checking LTL Properties of Recursive Markov Chains. In: Second International Conference on the Quantitative Evaluaiton of Systems (QEST 2005), 19-22 September 2005, Torino, Italy. pp. 155\u2013165. IEEE Computer Society (2005). https:\/\/doi.org\/10.1109\/QEST.2005.8","DOI":"10.1109\/QEST.2005.8"}],"container-title":["Lecture Notes in Computer Science","Foundations of Software Science and Computation Structures"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-99253-8_23","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,3,28]],"date-time":"2022-03-28T20:09:52Z","timestamp":1648498192000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-030-99253-8_23"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022]]},"ISBN":["9783030992521","9783030992538"],"references-count":30,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-99253-8_23","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2022]]},"assertion":[{"value":"29 March 2022","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"FoSSaCS","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Foundations of Software Science and Computation Structures","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Munich","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Germany","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2022","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"4 April 2022","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"6 April 2022","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"25","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"fossacs2022","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/etaps.org\/2022\/fossacs","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Single-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":"77","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":"23","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":"0","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":"30% - 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":"9","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)"}}]}}