{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,18]],"date-time":"2026-04-18T23:02:48Z","timestamp":1776553368028,"version":"3.51.2"},"publisher-location":"Cham","reference-count":19,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783032041661","type":"print"},{"value":"9783032041678","type":"electronic"}],"license":[{"start":{"date-parts":[[2025,9,15]],"date-time":"2025-09-15T00:00:00Z","timestamp":1757894400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2025,9,15]],"date-time":"2025-09-15T00:00:00Z","timestamp":1757894400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2026]]},"abstract":"<jats:title>Abstract<\/jats:title>\n          <jats:p>We introduce the notion of weighted abstract reduction systems (weighted ARSs), generalising standard and relative ARSs by allowing non-uniform weights on transition steps. Weighted ARSs give rise to a theory of rewriting where quantitative properties\u2014noteworthy complexity related properties\u2014can be more directly studied. Unlike these standard notions, weighted ARSs permit the study of quantitative properties of reduction systems of non-uniform weight, such as the analysis of expectation-based properties of probabilistic systems. We establish ranking functions as a means to analyse (strong) boundedness of weighted ARSs, i.e., the property that weights of reductions are bounded from above. We showcase their applicability by instantiating them to weighted term rewrite systems and probabilistic reduction systems, the latter generalising Lyapunov ranking functions to reason about expected derivation heights.<\/jats:p>","DOI":"10.1007\/978-3-032-04167-8_11","type":"book-chapter","created":{"date-parts":[[2025,9,14]],"date-time":"2025-09-14T22:03:30Z","timestamp":1757887410000},"page":"191-208","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["Weighted Rewriting"],"prefix":"10.1007","author":[{"given":"Martin","family":"Avanzini","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Akihisa","family":"Yamada","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2025,9,15]]},"reference":[{"key":"11_CR1","doi-asserted-by":"publisher","unstructured":"Avanzini, M., Barthe, G., Dal\u00a0Lago, U.: On continuation-passing transformations and expected cost analysis. Proc. ACM Program. Lang. 5(ICFP), 1\u201330 (2021). https:\/\/doi.org\/10.1145\/3473592","DOI":"10.1145\/3473592"},{"key":"11_CR2","doi-asserted-by":"publisher","unstructured":"Avanzini, M., Dal\u00a0Lago, U.: Automating sized-type inference for complexity analysis. Proc. ACM Program. Lang. 1(ICFP), 43:1\u201343:29 (2017). https:\/\/doi.org\/10.1145\/3110287","DOI":"10.1145\/3110287"},{"key":"11_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"132","DOI":"10.1007\/978-3-319-90686-7_9","volume-title":"Functional and Logic Programming","author":"M Avanzini","year":"2018","unstructured":"Avanzini, M., Dal Lago, U., Yamada, A.: On probabilistic term rewriting. In: Gallagher, J.P., Sulzmann, M. (eds.) FLOPS 2018. LNCS, vol. 10818, pp. 132\u2013148. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-90686-7_9"},{"key":"11_CR4","doi-asserted-by":"publisher","unstructured":"Avanzini, M., Dal\u00a0Lago, U., Yamada, A.: On probabilistic term rewriting. Sci. Comput. Program. 185 (2020). https:\/\/doi.org\/10.1016\/J.SCICO.2019.102338","DOI":"10.1016\/J.SCICO.2019.102338"},{"key":"11_CR5","doi-asserted-by":"publisher","unstructured":"Avanzini, M., Moser, G., P\u00e9choux, R., Perdrix, S., Zamdzhiev, V.: Quantum expectation transformers for cost analysis. In: Baier, C., Fisman, D. (eds.) LICS 2022: 37th Annual ACM\/IEEE Symposium on Logic in Computer Science, Haifa, Israel, 2\u20135 August 2022, pp. 10:1\u201310:13. ACM (2022). https:\/\/doi.org\/10.1145\/3531130.3533332","DOI":"10.1145\/3531130.3533332"},{"key":"11_CR6","doi-asserted-by":"publisher","unstructured":"Avanzini, M., Moser, G., Schaper, M.: A modular cost analysis for probabilistic programs. Proc. ACM Program. Lang. 4(OOPSLA), 172:1\u2013172:30 (2020). https:\/\/doi.org\/10.1145\/3428240","DOI":"10.1145\/3428240"},{"key":"11_CR7","doi-asserted-by":"crossref","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":"11_CR8","doi-asserted-by":"publisher","unstructured":"Baillot, P., Ghyselen, A., Kobayashi, N.: Sized types with usages for parallel complexity of pi-calculus processes. In: Haddad, S., Varacca, D. (eds.) 32nd International Conference on Concurrency Theory, CONCUR 2021, 24\u201327 August 2021, Virtual Conference. LIPIcs, vol.\u00a0203, pp. 34:1\u201334:22. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik (2021). https:\/\/doi.org\/10.4230\/LIPICS.CONCUR.2021.34","DOI":"10.4230\/LIPICS.CONCUR.2021.34"},{"key":"11_CR9","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). https:\/\/doi.org\/10.1007\/978-3-540-32033-3_24"},{"key":"11_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"105","DOI":"10.1007\/11780342_11","volume-title":"Logical Approaches to Computational Barriers","author":"U Dal Lago","year":"2006","unstructured":"Dal Lago, U., Martini, S.: An invariant cost model for the lambda calculus. In: Beckmann, A., Berger, U., L\u00f6we, B., Tucker, J.V. (eds.) CiE 2006. LNCS, vol. 3988, pp. 105\u2013114. Springer, Heidelberg (2006). https:\/\/doi.org\/10.1007\/11780342_11"},{"key":"11_CR11","doi-asserted-by":"publisher","unstructured":"Danielsson, N.A.: Lightweight semiformal time complexity analysis for purely functional data structures. In: Necula, G.C., Wadler, P. (eds.) Proceedings of the 35th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2008, San Francisco, California, USA, 7\u201312 January 2008, pp. 133\u2013144. ACM (2008). https:\/\/doi.org\/10.1145\/1328438.1328457","DOI":"10.1145\/1328438.1328457"},{"key":"11_CR12","doi-asserted-by":"publisher","unstructured":"Droste, M., Kuske, D.: Weighted automata. In: Pin, J. (ed.) Handbook of Automata Theory, pp. 113\u2013150. European Mathematical Society Publishing House, Z\u00fcrich, Switzerland (2021). https:\/\/doi.org\/10.4171\/AUTOMATA-1\/4","DOI":"10.4171\/AUTOMATA-1\/4"},{"key":"11_CR13","doi-asserted-by":"publisher","unstructured":"Faggian, C.: Probabilistic rewriting and asymptotic behaviour: on termination and unique normal forms. Log. Methods Comput. Sci. 18(2) (2022). https:\/\/doi.org\/10.46298\/LMCS-18(2:5)2022","DOI":"10.46298\/LMCS-18(2:5)2022"},{"key":"11_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"468","DOI":"10.1007\/978-3-030-11245-5_22","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"H Fu","year":"2019","unstructured":"Fu, H., Chatterjee, K.: Termination of nondeterministic probabilistic programs. In: Enea, C., Piskac, R. (eds.) VMCAI 2019. LNCS, vol. 11388, pp. 468\u2013490. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-11245-5_22"},{"key":"11_CR15","doi-asserted-by":"publisher","unstructured":"Gavazzo, F., Florio, C.D.: Elements of quantitative rewriting. Proc. ACM Program. Lang. 7(POPL), 1832\u20131863 (2023). https:\/\/doi.org\/10.1145\/3571256","DOI":"10.1145\/3571256"},{"key":"11_CR16","doi-asserted-by":"publisher","unstructured":"Laird, J., Manzonetto, G., McCusker, G., Pagani, M.: Weighted relational models of typed lambda-calculi. In: 28th Annual ACM\/IEEE Symposium on Logic in Computer Science, LICS 2013, New Orleans, LA, USA, 25\u201328 June 2013, pp. 301\u2013310. IEEE Computer Society (2013). https:\/\/doi.org\/10.1109\/LICS.2013.36","DOI":"10.1109\/LICS.2013.36"},{"key":"11_CR17","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"132","DOI":"10.1007\/978-3-319-66167-4_8","volume-title":"Frontiers of Combining Systems","author":"M Naaf","year":"2017","unstructured":"Naaf, M., Frohn, F., Brockschmidt, M., Fuhs, C., Giesl, J.: Complexity analysis for term rewriting by integer transition systems. In: Dixon, C., Finger, M. (eds.) FroCoS 2017. LNCS (LNAI), vol. 10483, pp. 132\u2013150. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-66167-4_8"},{"key":"11_CR18","doi-asserted-by":"publisher","unstructured":"van Oostrom, V., Toyama, Y.: Normalisation by random descent. In: Kesner, D., Pientka, B. (eds.) 1st International Conference on Formal Structures for Computation and Deduction, FSCD 2016, June 22-26, 2016, Porto, Portugal. LIPIcs, vol.\u00a052, pp. 32:1\u201332:18. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik (2016). https:\/\/doi.org\/10.4230\/LIPICS.FSCD.2016.32","DOI":"10.4230\/LIPICS.FSCD.2016.32"},{"issue":"7","key":"11_CR19","doi-asserted-by":"publisher","first-page":"689","DOI":"10.1016\/j.jlap.2010.07.010","volume":"79","author":"C Thrane","year":"2010","unstructured":"Thrane, C., Fahrenberg, U., Larsen, K.G.: Quantitative analysis of weighted transition systems. J. Logic Algebraic Program. 79(7), 689\u2013703 (2010). https:\/\/doi.org\/10.1016\/j.jlap.2010.07.010","journal-title":"J. Logic Algebraic Program."}],"container-title":["Lecture Notes in Computer Science","Frontiers of Combining Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-032-04167-8_11","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,9,14]],"date-time":"2025-09-14T22:03:31Z","timestamp":1757887411000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-032-04167-8_11"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,9,15]]},"ISBN":["9783032041661","9783032041678"],"references-count":19,"URL":"https:\/\/doi.org\/10.1007\/978-3-032-04167-8_11","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025,9,15]]},"assertion":[{"value":"15 September 2025","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"FroCoS","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Symposium on Frontiers of Combining Systems","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Reykjavik","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Iceland","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2025","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"27 September 2025","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"3 October 2025","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"15","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"frocos2025","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/icetcs.github.io\/frocos-itp-tableaux25\/frocos\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}