{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,5]],"date-time":"2026-02-05T10:53:45Z","timestamp":1770288825789,"version":"3.49.0"},"reference-count":34,"publisher":"Centre pour la Communication Scientifique Directe (CCSD)","license":[{"start":{"date-parts":[[2011,2,11]],"date-time":"2011-02-11T00:00:00Z","timestamp":1297382400000},"content-version":"unspecified","delay-in-days":0,"URL":"https:\/\/arxiv.org\/licenses\/nonexclusive-distrib\/1.0"}],"funder":[{"DOI":"10.13039\/501100000038","name":"Natural Sciences and Engineering Research Council of Canada","doi-asserted-by":"crossref","id":[{"id":"10.13039\/501100000038","id-type":"DOI","asserted-by":"crossref"}]}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"abstract":"<jats:p>Five algebraic notions of termination are formalised, analysed and compared:\nwellfoundedness or Noetherity, L\\\"ob's formula, absence of infinite iteration,\nabsence of divergence and normalisation. The study is based on modal semirings,\nwhich are additively idempotent semirings with forward and backward modal\noperators. To model infinite behaviours, idempotent semirings are extended to\ndivergence semirings, divergence Kleene algebras and omega algebras. The\nresulting notions and techniques are used in calculational proofs of classical\ntheorems of rewriting theory. These applications show that modal semirings are\npowerful tools for reasoning algebraically about the finite and infinite\ndynamics of programs and transition systems.<\/jats:p>","DOI":"10.2168\/lmcs-7(1:1)2011","type":"journal-article","created":{"date-parts":[[2011,9,23]],"date-time":"2011-09-23T12:18:47Z","timestamp":1316780327000},"source":"Crossref","is-referenced-by-count":6,"title":["Algebraic Notions of Termination"],"prefix":"10.46298","volume":"Volume 7, Issue 1","author":[{"given":"Desharnais","family":"Jules","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Bernhard","family":"Moeller","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Struth","family":"Georg","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"25203","published-online":{"date-parts":[[2011,2,11]]},"reference":[{"key":"10.2168\/LMCS-7(1:1)2011_Abrial96","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511624162"},{"key":"10.2168\/LMCS-7(1:1)2011_BachmairDershowitz86","doi-asserted-by":"crossref","unstructured":"L. Bachmair and N. Dershowitz. Commutation, transformation, and termination. In J. H. Siekmann, editor,8th International Conference on Automated Deduction, volume 230 ofLecture Notes in Computer Science, pages 5-20. Springer, 1986.","DOI":"10.1007\/3-540-16780-3_76"},{"key":"10.2168\/LMCS-7(1:1)2011_Backhouse02","doi-asserted-by":"crossref","unstructured":"R. Backhouse. Galois connections and fixed point calculus. In R. Backhouse, R. Crole, and J. Gibbons, editors,Algebraic and Coalgebraic Methods in the Mathematics of Program Construction, volume 2297 ofLecture Notes in Computer Science, pages 89-148. Springer, 2002.","DOI":"10.1007\/3-540-47797-7_4"},{"key":"10.2168\/LMCS-7(1:1)2011_BackhouseEtAl94","first-page":"31","volume":"53","author":"R. Backhouse et al","year":"1995","journal-title":"Information Processing Letters"},{"key":"10.2168\/LMCS-7(1:1)2011_BlackburndeRijkeVenema01","doi-asserted-by":"crossref","unstructured":"P. Blackburn, M. de Rijke, and Y. Venema.Modal Logic. Cambridge University Press, 2001.","DOI":"10.1017\/CBO9781107050884"},{"key":"10.2168\/LMCS-7(1:1)2011_Chellas80","doi-asserted-by":"crossref","unstructured":"B. F. Chellas.Modal Logic: An Introduction. Cambridge University Press, 1980.","DOI":"10.1017\/CBO9780511621192"},{"key":"10.2168\/LMCS-7(1:1)2011_Cohen00","doi-asserted-by":"crossref","unstructured":"E. Cohen. Separation and reduction. In R. Backhouse and J. N. Oliveira, editors,5th International Conference on Mathematics of Program Construction, MPC 2000, volume 1837 ofLecture Notes in Computer Science, pages 45-59. Springer, 2000.","DOI":"10.1007\/10722010_4"},{"key":"10.2168\/LMCS-7(1:1)2011_DesharnaisMoellerStruth04c","first-page":"93","volume":"1","author":"J. Desharnais, B. M\u00f6ller, and G. Struth","year":"2004","journal-title":"Journal on Relational Methods in Computer Science 2004"},{"key":"10.2168\/LMCS-7(1:1)2011_DesharnaisMoellerStruth04","doi-asserted-by":"crossref","unstructured":"J. Desharnais, B. M\u00f6ller, and G. Struth. Termination in modal Kleene algebra. In J.-J. Levy, E. W. Mayr, and J. C. Mitchell, editors,3rd International Conference on Theoretical Computer Science, pages 647-660. Kluwer, 2004.","DOI":"10.1007\/1-4020-8141-3_49"},{"key":"10.2168\/LMCS-7(1:1)2011_DesharnaisMoellerStruth04d","doi-asserted-by":"crossref","first-page":"798","DOI":"10.1145\/1183278.1183285","volume":"7","author":"J. Desharnais, B. M\u00f6ller, and G. Struth","year":"2006","journal-title":"ACM Transactions on Computational Logic"},{"key":"10.2168\/LMCS-7(1:1)2011_Dijkstra76","unstructured":"E.W. Dijkstra.A Discipline of Programming. Prentice Hall, 1976."},{"key":"10.2168\/LMCS-7(1:1)2011_DoBaWo97","doi-asserted-by":"crossref","first-page":"103","DOI":"10.1016\/S0304-3975(96)00154-5","volume":"179","author":"H. Doornbos, R. C. Backhouse, and J. van","year":"1997","journal-title":"Theoretical Computer Science"},{"key":"10.2168\/LMCS-7(1:1)2011_EbertStruth05","doi-asserted-by":"crossref","unstructured":"M. Ebert and G. Struth. Diagram chase in relational system development. In M. Minas, editor,3rd IEEE workshop on Visual Languages and Formal Methods (VLFM'04 ), volume 127 ofElectronic Notes in Theoretical Computer Science, pages 87-105. Elsevier, 2005.","DOI":"10.1016\/j.entcs.2004.08.049"},{"issue":"4","key":"10.2168\/LMCS-7(1:1)2011_Goldblatt85","doi-asserted-by":"crossref","first-page":"422","DOI":"10.1007\/BF00370431","volume":"44","author":"R. Goldblatt","year":"1985","journal-title":"Studia Logica"},{"key":"10.2168\/LMCS-7(1:1)2011_HarelKozenTiuryn00","doi-asserted-by":"crossref","unstructured":"D. Harel, D. Kozen, and J. Tiuryn.Dynamic Logic. MIT Press, 2000.","DOI":"10.7551\/mitpress\/2516.001.0001"},{"key":"10.2168\/LMCS-7(1:1)2011_HoefnerStruth07","doi-asserted-by":"crossref","unstructured":"P. H\u00f6fner and G. Struth. Automated reasoning in Kleene algebra. In F. Pfenning, editor,CADE 2007, volume 4603 ofLecture Notes in Artificial Intelligence, pages 279-294. Springer, 2007.","DOI":"10.1007\/978-3-540-73595-3_19"},{"key":"10.2168\/LMCS-7(1:1)2011_AlloyBook","unstructured":"D. Jackson.Software Abstractions. The MIT Press, 2006."},{"issue":"2","key":"10.2168\/LMCS-7(1:1)2011_Kozen94","doi-asserted-by":"crossref","first-page":"366","DOI":"10.1006\/inco.1994.1037","volume":"110","author":"D. Kozen","year":"1994","journal-title":"Information and Computation"},{"issue":"3","key":"10.2168\/LMCS-7(1:1)2011_Kozen97","doi-asserted-by":"crossref","first-page":"427","DOI":"10.1145\/256167.256195","volume":"19","author":"D. Kozen","year":"1997","journal-title":"ACM Transactions on Programming Languages and Systems 19(3):427-443, 1997"},{"key":"10.2168\/LMCS-7(1:1)2011_MeltonEtAL86","doi-asserted-by":"crossref","unstructured":"A. Melton, D.A. Schmidt, and G.E. Strecker. Galois connections and computer science applications. In D. Pitt, S. Abramsky, A. Poign\u00e9, and D. Rydeheard, editors,Category Theory and Computer Programming, volume 240 ofLecture Notes in Computer Science, pages 299-312. Springer, 1986.","DOI":"10.1007\/3-540-17162-2_130"},{"key":"10.2168\/LMCS-7(1:1)2011_MolLazy04","doi-asserted-by":"crossref","unstructured":"B. M\u00f6ller. Lazy Kleene algebra. In D. Kozen, editor,Mathematics of Program Construction, volume 3125 ofLecture Notes in Computer Science, pages 252-273. Springer, 2004. Revised version: B. M\u00f6ller. Kleene getting lazy. Science of Computer Programming 65, 195-214 (2007).","DOI":"10.1016\/j.scico.2006.01.010"},{"key":"10.2168\/LMCS-7(1:1)2011_MoellerHoefnerStruth06","doi-asserted-by":"crossref","unstructured":"B. M\u00f6ller, P. H\u00f6fner, and G. Struth. Quantales and temporal logics. In M. Johnson and V. Vene, editors,Algebraic Methodology and Software Technology (AMAST 2006), volume 4019 ofLecture Notes in Computer Science, pages 263-277. Springer, 2006.","DOI":"10.1007\/11784180_21"},{"key":"10.2168\/LMCS-7(1:1)2011_MoellerStruth05a","doi-asserted-by":"crossref","first-page":"221","DOI":"10.1016\/j.tcs.2005.09.069","volume":"351","author":"B. M\u00f6ller and G. Struth","year":"2006","journal-title":"Theoretical Computer Science"},{"key":"10.2168\/LMCS-7(1:1)2011_MoellerStruth05","doi-asserted-by":"crossref","unstructured":"B. M\u00f6ller and G. Struth. \\sf wp is \\sf wlp. In W. MacCaull, M. Winter, and I. D\u00fcntsch, editors,Relational Methods in Computer Science, volume 3929 ofLecture Notes in Computer Science, pages 200-211. Springer, 2006.","DOI":"10.1007\/11734673_16"},{"key":"10.2168\/LMCS-7(1:1)2011_Nelson89","doi-asserted-by":"crossref","first-page":"517","DOI":"10.1145\/69558.69559","volume":"11","author":"G. Nelson","year":"1989","journal-title":"ACM Transactions on Programming Languages and Systems 11:517-561, 1989"},{"key":"10.2168\/LMCS-7(1:1)2011_SchmidtStroehlein93","unstructured":"G. Schmidt and T. Str\u00f6hlein.Relations and Graphs: Discrete Mathematics for Computer Scientists. EATCS Monographs on Theoretical Computer Science. Springer, 1993."},{"key":"10.2168\/LMCS-7(1:1)2011_Spivey92","unstructured":"M. Spivey.The Z notation: A reference manual. International Series in Computer Science. Prentice Hall, 1992. Available under http:\/\/spivey.oriel.ox.ac.uk\/ mike\/zrm\/."},{"key":"10.2168\/LMCS-7(1:1)2011_Struth96","unstructured":"G. Struth. Non-symmetric rewriting. Technical Report MPI-I-96-2-004, Max-Planck-Institut f\u00fcr Informatik, 1996."},{"key":"10.2168\/LMCS-7(1:1)2011_Struth98","unstructured":"G. Struth.Canonical Transformations in Algebra, Universal Algebra and Logic. PhD thesis, Institut f\u00fcr Informatik, Universit\u00e4t des Saarlandes, Germany, 1998."},{"key":"10.2168\/LMCS-7(1:1)2011_Struth02","doi-asserted-by":"crossref","unstructured":"G. Struth. Calculating Church-Rosser proofs in Kleene algebra. In \\mboxH.C.M. de Swart, editor,Relational Methods in Computer Science, 6th International Conference, volume 2561 ofLecture Notes in Computer Science, pages 276-290. Springer, 2002.","DOI":"10.1007\/3-540-36280-0_19"},{"issue":"2","key":"10.2168\/LMCS-7(1:1)2011_Struth05","doi-asserted-by":"crossref","first-page":"239","DOI":"10.1016\/j.jlap.2005.04.001","volume":"66","author":"G. Struth","year":"2006","journal-title":"Journal of Logic and Algebraic Programming 2006"},{"key":"10.2168\/LMCS-7(1:1)2011_Tarski55","doi-asserted-by":"crossref","first-page":"285","DOI":"10.2140\/pjm.1955.5.285","volume":"5","author":"A. Tarski","year":"1955","journal-title":"Pacific Journal of Mathematics"},{"key":"10.2168\/LMCS-7(1:1)2011_Terese03","unstructured":"Terese, editor.Term Rewriting Systems. Cambridge University Press, 2003."},{"key":"10.2168\/LMCS-7(1:1)2011_vWright02","doi-asserted-by":"crossref","unstructured":"J. von Wright. From Kleene algebra to refinement algebra. In B. M\u00f6ller and E. Boi\\-ten, editors,6th International Conference on Mathematics of Program Construction, MPC 2002, volume 2386 ofLecture Notes in Computer Science, pages 233-262. Springer, 2002.","DOI":"10.1007\/3-540-45442-X_14"}],"container-title":["Logical Methods in Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/lmcs.episciences.org\/777\/pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/lmcs.episciences.org\/777\/pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,4,11]],"date-time":"2023-04-11T19:55:45Z","timestamp":1681242945000},"score":1,"resource":{"primary":{"URL":"https:\/\/lmcs.episciences.org\/777"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2011,2,11]]},"references-count":34,"URL":"https:\/\/doi.org\/10.2168\/lmcs-7(1:1)2011","relation":{"is-same-as":[{"id-type":"arxiv","id":"1012.5803","asserted-by":"subject"},{"id-type":"doi","id":"10.48550\/arXiv.1012.5803","asserted-by":"subject"}]},"ISSN":["1860-5974"],"issn-type":[{"value":"1860-5974","type":"electronic"}],"subject":[],"published":{"date-parts":[[2011,2,11]]},"article-number":"777"}}