{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,23]],"date-time":"2026-07-23T22:31:54Z","timestamp":1784845914246,"version":"3.55.0"},"reference-count":44,"publisher":"Springer Science and Business Media LLC","issue":"3","license":[{"start":{"date-parts":[[2018,5,15]],"date-time":"2018-05-15T00:00:00Z","timestamp":1526342400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"funder":[{"name":"Excellence Initiative of the German federal and state governments"},{"name":"CDZ project CAP","award":["GZ 1023"],"award-info":[{"award-number":["GZ 1023"]}]},{"DOI":"10.13039\/501100001659","name":"Deutsche Forschungsgemeinschaft","doi-asserted-by":"publisher","award":["RTG 2236"],"award-info":[{"award-number":["RTG 2236"]}],"id":[{"id":"10.13039\/501100001659","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Acta Informatica"],"published-print":{"date-parts":[[2019,4]]},"DOI":"10.1007\/s00236-018-0321-1","type":"journal-article","created":{"date-parts":[[2018,5,15]],"date-time":"2018-05-15T06:51:55Z","timestamp":1526367115000},"page":"255-285","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":37,"title":["On the hardness of analyzing probabilistic programs"],"prefix":"10.1007","volume":"56","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-5185-2324","authenticated-orcid":false,"given":"Benjamin Lucien","family":"Kaminski","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"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-9151-0441","authenticated-orcid":false,"given":"Christoph","family":"Matheja","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2018,5,15]]},"reference":[{"key":"321_CR1","doi-asserted-by":"crossref","unstructured":"Arons, T., Pnueli, A., Zuck, L.D.: Parameterized Verification by Probabilistic Abstraction. In: FoSSaCS, LNCS, vol. 2620, pp. 87\u2013102. Springer (2003)","DOI":"10.1007\/3-540-36576-1_6"},{"key":"321_CR2","volume-title":"Probability and Measure Theory","author":"RB Ash","year":"2000","unstructured":"Ash, R.B., Doleans-Dade, C.: Probability and Measure Theory. Academic Press, Cambridge (2000)"},{"issue":"3","key":"321_CR3","doi-asserted-by":"publisher","first-page":"9","DOI":"10.1145\/2492061","volume":"35","author":"G Barthe","year":"2013","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 (2013)","journal-title":"ACM Trans. Program. Lang. Syst."},{"issue":"2","key":"321_CR4","doi-asserted-by":"publisher","first-page":"6:1","DOI":"10.1145\/2656210","volume":"7","author":"M Bl\u00e4ser","year":"2015","unstructured":"Bl\u00e4ser, M., Manthey, B.: Smoothed complexity theory. TOCT 7(2), 6:1\u20136:21 (2015)","journal-title":"TOCT"},{"key":"321_CR5","unstructured":"Bournez, O., Garnier, F.: Proving positive almost-sure termination. In: Proceedings of 16th International Conference on Term Rewriting and Applications, RTA 2005, Nara, Japan, April 19\u201321, 2005,LNCS, vol. 3467, pp. 323\u2013337. Springer (2005)"},{"key":"321_CR6","doi-asserted-by":"crossref","unstructured":"Bournez, O., Hoyrup, M.: Rewriting logic and probabilities. In: RTA, LNCS, vol. 2706, pp. 61\u201375. Springer (2003)","DOI":"10.1007\/3-540-44881-0_6"},{"key":"321_CR7","doi-asserted-by":"crossref","unstructured":"Chakarov, A., Sankaranarayanan, S.: Probabilistic program analysis with martingales. In: CAV, LNCS, vol. 8044, pp. 511\u2013526. Springer (2013)","DOI":"10.1007\/978-3-642-39799-8_34"},{"key":"321_CR8","doi-asserted-by":"crossref","unstructured":"Chatterjee, K., Fu, H., Goharshady, A.K.: Termination analysis of probabilistic programs through positivstellensatz\u2019s. In: CAV (1), LNCS, vol. 9779, pp. 3\u201322. Springer (2016)","DOI":"10.1007\/978-3-319-41528-4_1"},{"key":"321_CR9","doi-asserted-by":"crossref","unstructured":"Chatterjee, K., Fu, H., Novotn\u00fd, P., Hasheminezhad, R.: Algorithmic analysis of qualitative and quantitative termination problems for affine probabilistic programs. In: POPL, pp. 327\u2013342. ACM (2016)","DOI":"10.1145\/2914770.2837639"},{"key":"321_CR10","volume-title":"Computability and Unsolvability. McGraw-Hill Series in Information Processing and Computers","author":"MD Davis","year":"1958","unstructured":"Davis, M.D.: Computability and Unsolvability. McGraw-Hill Series in Information Processing and Computers. McGraw-Hill, New York (1958)"},{"key":"321_CR11","volume-title":"Computability, Complexity, and Languages: Fundamentals of Theoretical Computer Science","author":"MD Davis","year":"1994","unstructured":"Davis, M.D.: Computability, Complexity, and Languages: Fundamentals of Theoretical Computer Science. Academic Press, Cambridge (1994)"},{"key":"321_CR12","volume-title":"A Discipline of Programming","author":"EW Dijkstra","year":"1976","unstructured":"Dijkstra, E.W.: A Discipline of Programming. Prentice-Hall, Englewood Cliffs (1976)"},{"key":"321_CR13","doi-asserted-by":"crossref","unstructured":"Esparza, J., Gaiser, A., Kiefer, S.: Proving termination of probabilistic programs using patterns. In: CAV, LNCS, vol. 7358, pp. 123\u2013138. Springer (2012)","DOI":"10.1007\/978-3-642-31424-7_14"},{"key":"321_CR14","doi-asserted-by":"crossref","unstructured":"Fioriti, L.M.F., Hermanns, H.: Probabilistic termination: soundness, completeness, and compositionality. In: POPL 2015, pp. 489\u2013501. ACM (2015)","DOI":"10.1145\/2775051.2677001"},{"key":"321_CR15","doi-asserted-by":"crossref","unstructured":"Foster, N., Kozen, D., Mamouras, K., Reitblatt, M., Silva, A.: Probabilistic NetKAT. In: ESOP, LNCS, vol. 9632, pp. 282\u2013309. Springer (2016)","DOI":"10.1007\/978-3-662-49498-1_12"},{"issue":"4","key":"321_CR16","doi-asserted-by":"publisher","first-page":"675","DOI":"10.1137\/0206049","volume":"6","author":"J Gill","year":"1977","unstructured":"Gill, J.: Computational complexity of probabilistic turing machines. SIAM J. Comput. 6(4), 675\u2013695 (1977)","journal-title":"SIAM J. Comput."},{"key":"321_CR17","doi-asserted-by":"crossref","unstructured":"Gordon, A.D., Henzinger, T.A., Nori, A.V., Rajamani, S.K.: Probabilistic programming. In: Future of Software Engineering (FOSE), pp. 167\u2013181. ACM (2014)","DOI":"10.1145\/2593882.2593900"},{"key":"321_CR18","doi-asserted-by":"publisher","first-page":"110","DOI":"10.1016\/j.peva.2013.11.004","volume":"73","author":"F Gretz","year":"2014","unstructured":"Gretz, F., Katoen, J.P., McIver, A.: Operational versus Weakest pre-expectation semantics for the probabilistic guarded command language. Perform. Eval. 73, 110\u2013132 (2014)","journal-title":"Perform. Eval."},{"issue":"3","key":"321_CR19","doi-asserted-by":"publisher","first-page":"356","DOI":"10.1145\/2166.357214","volume":"5","author":"S Hart","year":"1983","unstructured":"Hart, S., Sharir, M., Pnueli, A.: Termination of probabilistic concurrent programs. TOPLAS 5(3), 356\u2013380 (1983)","journal-title":"TOPLAS"},{"key":"321_CR20","first-page":"199","volume":"319","author":"N Jansen","year":"2015","unstructured":"Jansen, N., Kaminski, B.L., Katoen, J.P., Olmedo, F., Gretz, F., McIver, A.: Conditioning in probabilistic programming. ENTCS 319, 199\u2013216 (2015)","journal-title":"ENTCS"},{"key":"321_CR21","doi-asserted-by":"crossref","unstructured":"Kaminski, B.L., Katoen, J.P.: On the hardness of almost\u2013sure termination. In: Proceedings of MFCS 2015, Part I, LNCS, vol. 9234, pp. 307\u2013318. Springer (2015)","DOI":"10.1007\/978-3-662-48057-1_24"},{"key":"321_CR22","doi-asserted-by":"crossref","unstructured":"Kaminski, B.L., Katoen, J.P., Matheja, C.: Inferring covariances for probabilistic programs. In: QEST 2016, pp. 191\u2013206 (2016)","DOI":"10.1007\/978-3-319-43425-4_14"},{"key":"321_CR23","unstructured":"Kaminski, B.L., Katoen, J.P., Matheja, C., Olmedo, F.: Weakest precondition reasoning for expected run-times of probabilistic programs. (2016). arXiv:1601.01001"},{"key":"321_CR24","doi-asserted-by":"crossref","unstructured":"Kaminski, B.L., Katoen, J.P., Matheja, C., Olmedo, F.: Weakest precondition reasoning for expected run-times of probabilistic programs. In: ESOP, LNCS, vol. 9632, pp. 364\u2013389. Springer (2016)","DOI":"10.1007\/978-3-662-49498-1_15"},{"key":"321_CR25","doi-asserted-by":"crossref","unstructured":"Katoen, J., McIver, A., Meinicke, L., Morgan, C.C.: Linear-invariant generation for probabilistic programs: automated support for proof-based methods. In: SAS, LNCS, vol. 6337, pp. 390\u2013406. Springer (2010)","DOI":"10.1007\/978-3-642-15769-1_24"},{"issue":"1","key":"321_CR26","doi-asserted-by":"publisher","first-page":"41","DOI":"10.1090\/S0002-9947-1943-0007371-8","volume":"53","author":"SC Kleene","year":"1943","unstructured":"Kleene, S.C.: Recursive predicates and quantifiers. Trans. AMS 53(1), 41\u201373 (1943)","journal-title":"Trans. AMS"},{"key":"321_CR27","volume-title":"Probability Theory: A Comprehensive Course","author":"A Klenke","year":"2013","unstructured":"Klenke, A.: Probability Theory: A Comprehensive Course. Springer, Berlin (2013)"},{"issue":"3","key":"321_CR28","doi-asserted-by":"publisher","first-page":"328","DOI":"10.1016\/0022-0000(81)90036-2","volume":"22","author":"D Kozen","year":"1981","unstructured":"Kozen, D.: Semantics of probabilistic programs. J. Comput. Syst. Sci. 22(3), 328\u2013350 (1981)","journal-title":"J. Comput. Syst. Sci."},{"issue":"2","key":"321_CR29","doi-asserted-by":"publisher","first-page":"162","DOI":"10.1016\/0022-0000(85)90012-1","volume":"30","author":"D Kozen","year":"1985","unstructured":"Kozen, D.: A probabilistic PDL. J. Comput. Syst. Sci. 30(2), 162\u2013178 (1985)","journal-title":"J. Comput. Syst. Sci."},{"key":"321_CR30","doi-asserted-by":"crossref","unstructured":"dal Lago, U., Grellois, C.: Probabilistic termination by monadic affine sized typing. In: ESOP, LNCS, vol. 10201, pp. 393\u2013419. Springer (2017)","DOI":"10.1007\/978-3-662-54434-1_15"},{"key":"321_CR31","volume-title":"Abstraction, Refinement and Proof for Probabilistic Systems","author":"A McIver","year":"2004","unstructured":"McIver, A., Morgan, C.: Abstraction, Refinement and Proof for Probabilistic Systems. Springer, Berlin (2004)"},{"key":"321_CR32","doi-asserted-by":"crossref","unstructured":"McIver, A., Morgan, C., Kaminski, B.L., Katoen, J.P.: A new proof rule for almost-sure termination. In: POPL [to appear] (2018)","DOI":"10.1145\/3158121"},{"key":"321_CR33","doi-asserted-by":"crossref","unstructured":"Morgan, C.: Proof rules for probabilistic loops. In: Proceedings of the BCS-FACS 7th Refinement Workshop, Workshops in Computing, p.\u00a07. Springer Verlag (1996)","DOI":"10.14236\/ewic\/RW1996.10"},{"key":"321_CR34","doi-asserted-by":"crossref","unstructured":"Murawski, A., Ouaknine, J.: On probabilistic program equivalence and refinement. In: CONCUR, LNCS, vol. 3653, pp. 156\u2013170. Springer (2005)","DOI":"10.1007\/11539452_15"},{"key":"321_CR35","volume-title":"Classical Recursion Theory: The Theory of Functions and Sets of Natural Numbers","author":"P Odifreddi","year":"1992","unstructured":"Odifreddi, P.: Classical Recursion Theory: The Theory of Functions and Sets of Natural Numbers. Elsevier, Amsterdam (1992)"},{"key":"321_CR36","volume-title":"Classical Recursion Theory","author":"P Odifreddi","year":"1999","unstructured":"Odifreddi, P.: Classical Recursion Theory, vol. II. Elsevier, Amsterdam (1999)"},{"key":"321_CR37","volume-title":"Computational Complexity","author":"CH Papadimitriou","year":"1994","unstructured":"Papadimitriou, C.H.: Computational Complexity. Addison-Wesley, Boston (1994)"},{"issue":"5","key":"321_CR38","doi-asserted-by":"publisher","first-page":"284","DOI":"10.1090\/S0002-9904-1944-08111-1","volume":"50","author":"EL Post","year":"1944","unstructured":"Post, E.L.: Recursively enumerable sets of positive integers and their decision problems. Bull. AMS 50(5), 284\u2013316 (1944)","journal-title":"Bull. AMS"},{"key":"321_CR39","volume-title":"Markov Decision Processes: Discrete Stochastic Dynamic Programming","author":"ML Puterman","year":"2005","unstructured":"Puterman, M.L.: Markov Decision Processes: Discrete Stochastic Dynamic Programming. Wiley, New York (2005)"},{"key":"321_CR40","volume-title":"Theory of Recursive Functions and Effective Computability","author":"H Rogers","year":"1967","unstructured":"Rogers, H.: Theory of Recursive Functions and Effective Computability, vol. 5. McGraw-Hill, New York (1967)"},{"issue":"2","key":"321_CR41","doi-asserted-by":"publisher","first-page":"292","DOI":"10.1137\/0213021","volume":"13","author":"M Sharir","year":"1984","unstructured":"Sharir, M., Pnueli, A., Hart, S.: Verification of probabilistic programs. SIAM J. Comput. 13(2), 292\u2013314 (1984). https:\/\/doi.org\/10.1137\/0213021","journal-title":"SIAM J. Comput."},{"key":"321_CR42","doi-asserted-by":"crossref","unstructured":"Sneyers, J., de Schreye, D.: Probabilistic termination of CHRiSM Programs. In: LOPSTR, LNCS, vol. 7225, pp. 221\u2013236. Springer (2011)","DOI":"10.1007\/978-3-642-32211-2_15"},{"issue":"3","key":"321_CR43","doi-asserted-by":"publisher","first-page":"333","DOI":"10.1016\/0304-3975(89)90158-8","volume":"66","author":"ML Tiomkin","year":"1989","unstructured":"Tiomkin, M.L.: Probabilistic termination versus fair termination. TCS 66(3), 333\u2013340 (1989)","journal-title":"TCS"},{"issue":"6","key":"321_CR44","doi-asserted-by":"publisher","first-page":"19","DOI":"10.1145\/2049706.2049708","volume":"33","author":"M Ying","year":"2011","unstructured":"Ying, M.: Floyd\u2013Hoare logic for quantum programs. ACM Trans. Program. Lang. Syst. 33(6), 19 (2011)","journal-title":"ACM Trans. Program. Lang. Syst."}],"container-title":["Acta Informatica"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00236-018-0321-1.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s00236-018-0321-1\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00236-018-0321-1.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,2]],"date-time":"2020-11-02T00:16:02Z","timestamp":1604276162000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s00236-018-0321-1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018,5,15]]},"references-count":44,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2019,4]]}},"alternative-id":["321"],"URL":"https:\/\/doi.org\/10.1007\/s00236-018-0321-1","relation":{},"ISSN":["0001-5903","1432-0525"],"issn-type":[{"value":"0001-5903","type":"print"},{"value":"1432-0525","type":"electronic"}],"subject":[],"published":{"date-parts":[[2018,5,15]]},"assertion":[{"value":"15 September 2016","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"20 April 2018","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"15 May 2018","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}