{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,11]],"date-time":"2025-10-11T08:24:37Z","timestamp":1760171077307},"publisher-location":"Cham","reference-count":28,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319906850"},{"type":"electronic","value":"9783319906867"}],"license":[{"start":{"date-parts":[[2018,1,1]],"date-time":"2018-01-01T00:00:00Z","timestamp":1514764800000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2018]]},"DOI":"10.1007\/978-3-319-90686-7_9","type":"book-chapter","created":{"date-parts":[[2018,4,23]],"date-time":"2018-04-23T17:49:55Z","timestamp":1524505795000},"page":"132-148","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":6,"title":["On Probabilistic Term Rewriting"],"prefix":"10.1007","author":[{"given":"Martin","family":"Avanzini","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Ugo","family":"Dal Lago","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Akihisa","family":"Yamada","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2018,4,24]]},"reference":[{"issue":"2","key":"9_CR1","doi-asserted-by":"publisher","first-page":"213","DOI":"10.1016\/j.entcs.2005.10.040","volume":"153","author":"G Agha","year":"2006","unstructured":"Agha, G., Meseguer, J., Sen, K.: PMaude: rewrite-based specification language for probabilistic object systems. Electr. Notes Theor. Comput. Sci. 153(2), 213\u2013239 (2006)","journal-title":"Electr. Notes Theor. Comput. Sci."},{"key":"9_CR2","unstructured":"Avanzini, M.: Verifying polytime computability automatically. Ph.D. thesis, University of Innsbruck (2013)"},{"key":"9_CR3","unstructured":"Avanzini, M., Dal Lago, U., Yamada, A.: On probabilistic term rewriting (Technical report). CoRR cs\/CC\/1802.09774 (2018). \nhttp:\/\/www.arxiv.org\/abs\/1802.09774"},{"key":"9_CR4","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9781139172752","volume-title":"Term Rewriting and All That","author":"F Baader","year":"1998","unstructured":"Baader, F., Nipkow, T.: Term Rewriting and All That. Cambridge University Press, Cambridge (1998)"},{"key":"9_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"323","DOI":"10.1007\/978-3-540-32033-3_24","volume-title":"Term Rewriting and Applications","author":"O Bournez","year":"2005","unstructured":"Bournez, O., Garnier, F.: Proving positive almost-sure termination. In: Giesl, J. (ed.) RTA 2005. LNCS, vol. 3467, pp. 323\u2013337. Springer, Heidelberg (2005). \nhttps:\/\/doi.org\/10.1007\/978-3-540-32033-3_24"},{"key":"9_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"357","DOI":"10.1007\/11805618_27","volume-title":"Term Rewriting and Applications","author":"O Bournez","year":"2006","unstructured":"Bournez, O., Garnier, F.: Proving positive almost sure termination under strategies. In: Pfenning, F. (ed.) RTA 2006. LNCS, vol. 4098, pp. 357\u2013371. Springer, Heidelberg (2006). \nhttps:\/\/doi.org\/10.1007\/11805618_27"},{"key":"9_CR7","doi-asserted-by":"publisher","first-page":"252","DOI":"10.1007\/3-540-45610-4_18","volume-title":"Rewriting Techniques and Applications","author":"Olivier Bournez","year":"2002","unstructured":"Bournez, O., Kirchner, C.: Probabilistic rewrite strategies. Applications to ELAN. In: Proceedings of 13th RTA, pp. 252\u2013266 (2002)"},{"key":"9_CR8","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4757-3124-8","volume-title":"Marcov Chains","author":"P Br\u00e9maud","year":"1999","unstructured":"Br\u00e9maud, P.: Marcov Chains. Springer, New York (1999). \nhttps:\/\/doi.org\/10.1007\/978-1-4757-3124-8"},{"key":"9_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1007\/978-3-319-41528-4_1","volume-title":"Computer Aided Verification","author":"K Chatterjee","year":"2016","unstructured":"Chatterjee, K., Fu, H., Goharshady, A.K.: Termination analysis of probabilistic programs through Positivstellensatz\u2019s. In: Chaudhuri, S., Farzan, A. (eds.) CAV 2016. LNCS, vol. 9779, pp. 3\u201322. Springer, Cham (2016). \nhttps:\/\/doi.org\/10.1007\/978-3-319-41528-4_1"},{"issue":"3","key":"9_CR10","first-page":"413","volume":"46","author":"U Lago Dal","year":"2012","unstructured":"Dal Lago, U., Zorzi, M.: Probabilistic operational semantics for the lambda calculus. RAIRO - TIA 46(3), 413\u2013450 (2012)","journal-title":"RAIRO - TIA"},{"key":"9_CR11","doi-asserted-by":"publisher","first-page":"393","DOI":"10.1007\/978-3-662-54434-1_15","volume-title":"Programming Languages and Systems","author":"Ugo Dal Lago","year":"2017","unstructured":"Dal Lago, U., Grellois, C.: Probabilistic termination by monadic affine sized typing. In: Proceedings of 26th ESOP, pp. 393\u2013419 (2017)"},{"issue":"3","key":"9_CR12","first-page":"1","volume":"8","author":"U Lago Dal","year":"2012","unstructured":"Dal Lago, U., Martini, S.: On constructor rewrite systems and the lambda calculus. LMCS 8(3), 1\u201327 (2012)","journal-title":"LMCS"},{"issue":"3","key":"9_CR13","doi-asserted-by":"publisher","first-page":"195","DOI":"10.1007\/s10817-007-9087-9","volume":"40","author":"J Endrullis","year":"2008","unstructured":"Endrullis, J., Waldmann, J., Zantema, H.: Matrix interpretations for proving termination of term rewriting. JAR 40(3), 195\u2013220 (2008)","journal-title":"JAR"},{"key":"9_CR14","doi-asserted-by":"crossref","unstructured":"Ferrer Fioriti, L.M., Hermanns, H.: Probabilistic termination: soundness, completeness, and compositionality. In: Proceedings of 42nd POPL, pp. 489\u2013501. ACM (2015)","DOI":"10.1145\/2676726.2677001"},{"key":"9_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"340","DOI":"10.1007\/978-3-540-72788-0_33","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2007","author":"C Fuhs","year":"2007","unstructured":"Fuhs, C., Giesl, J., Middeldorp, A., Schneider-Kamp, P., Thiemann, R., Zankl, H.: SAT solving for termination analysis with polynomial interpretations. In: Marques-Silva, J., Sakallah, K.A. (eds.) SAT 2007. LNCS, vol. 4501, pp. 340\u2013354. Springer, Heidelberg (2007). \nhttps:\/\/doi.org\/10.1007\/978-3-540-72788-0_33"},{"key":"9_CR16","doi-asserted-by":"crossref","unstructured":"Gnaedig, I.: Induction for positive almost sure termination. In: PPDP 2017, pp. 167\u2013178. ACM (2007)","DOI":"10.1145\/1273920.1273943"},{"issue":"2","key":"9_CR17","first-page":"270","volume":"28","author":"S Goldwasser","year":"1984","unstructured":"Goldwasser, S., Micali, S.: Probabilistic encryption. JCSS 28(2), 270\u2013299 (1984)","journal-title":"JCSS"},{"key":"9_CR18","unstructured":"Goodman, N.D., Mansinghka, V.K., Roy, D.M., Bonawitz, K., Tenenbaum, J.B.: Church: a language for generative models. In: Proceedings of 24th UAI, pp. 220\u2013229. AUAI Press (2008)"},{"key":"9_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"257","DOI":"10.1007\/978-3-319-08918-8_18","volume-title":"Rewriting and Typed Lambda Calculi","author":"N Hirokawa","year":"2014","unstructured":"Hirokawa, N., Moser, G.: Automated complexity analysis based on context-sensitive rewriting. In: Dowek, G. (ed.) RTA 2014. LNCS, vol. 8560, pp. 257\u2013271. Springer, Cham (2014). \nhttps:\/\/doi.org\/10.1007\/978-3-319-08918-8_18"},{"key":"9_CR20","doi-asserted-by":"publisher","first-page":"307","DOI":"10.1007\/978-3-662-48057-1_24","volume-title":"Mathematical Foundations of Computer Science 2015","author":"Benjamin Lucien Kaminski","year":"2015","unstructured":"Kaminski, B.L., Katoen, J.: On the hardness of almost-sure termination. In: MFCS 2015, Proceedings, Part I, Milan, Italy, 24\u201328 August 2015, pp. 307\u2013318 (2015)"},{"key":"9_CR21","unstructured":"Lankford, D.: Canonical algebraic simplification in computational logic. Technical report ATP-25, University of Texas (1975)"},{"issue":"3","key":"9_CR22","first-page":"547","volume":"39","author":"S Lucas","year":"2005","unstructured":"Lucas, S.: Polynomials over the reals in proofs of termination: from theory to practice. ITA 39(3), 547\u2013586 (2005)","journal-title":"ITA"},{"key":"9_CR23","doi-asserted-by":"publisher","DOI":"10.1002\/9780470316887","volume-title":"Markov Decision Processes: Discrete Stochastic Dynamic Programming","author":"ML Puterman","year":"1994","unstructured":"Puterman, M.L.: Markov Decision Processes: Discrete Stochastic Dynamic Programming, 1st edn. Wiley, New York (1994)","edition":"1"},{"issue":"3","key":"9_CR24","doi-asserted-by":"publisher","first-page":"230","DOI":"10.1016\/S0019-9958(63)90290-0","volume":"6","author":"MO Rabin","year":"1963","unstructured":"Rabin, M.O.: Probabilistic automata. Inf. Control 6(3), 230\u2013245 (1963)","journal-title":"Inf. Control"},{"key":"9_CR25","doi-asserted-by":"publisher","first-page":"442","DOI":"10.1007\/3-540-08921-7_92","volume-title":"Mathematical Foundations of Computer Science 1978","author":"N. Saheb-Djahromi","year":"1978","unstructured":"Saheb-Djahromi, N.: Probabilistic LCF. In: MFCS, pp. 442\u2013451 (1978)"},{"issue":"3","key":"9_CR26","doi-asserted-by":"publisher","first-page":"704","DOI":"10.1090\/S0002-9939-1969-0249221-4","volume":"22","author":"ES Santos","year":"1969","unstructured":"Santos, E.S.: Probabilistic turing machines and computability. Proc. Am. Math. Soc. 22(3), 704\u2013710 (1969)","journal-title":"Proc. Am. Math. Soc."},{"key":"9_CR27","unstructured":"Terese (ed.): Term Rewriting Systems. Cambridge Tracts in Theoretical Computer Science, vol. 55. Cambridge University Press, Cambridge (2003)"},{"key":"9_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"466","DOI":"10.1007\/978-3-319-08918-8_32","volume-title":"Rewriting and Typed Lambda Calculi","author":"A Yamada","year":"2014","unstructured":"Yamada, A., Kusakari, K., Sakabe, T.: Nagoya termination tool. In: Dowek, G. (ed.) RTA 2014. LNCS, vol. 8560, pp. 466\u2013475. Springer, Cham (2014). \nhttps:\/\/doi.org\/10.1007\/978-3-319-08918-8_32"}],"container-title":["Lecture Notes in Computer Science","Functional and Logic Programming"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-90686-7_9","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2018,4,23]],"date-time":"2018-04-23T17:52:31Z","timestamp":1524505951000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-90686-7_9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018]]},"ISBN":["9783319906850","9783319906867"],"references-count":28,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-90686-7_9","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2018]]}}}