Algebraic Notions of Termination

DOI10.2168/LMCS-7(1:1)2011MaRDI QIDQ3003302zbMATH OpenFDO

Authors Jules Desharnais, Bernhard Möller, Georg Struth

Publication date 26 May 2011

Published in Logical Methods in Computer Science (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1012.5803

zbMATH Keywords

divergence semiringsidempotent semiringsKleene algebrasmodal operatorsNoetherityomega algebrasprogram analysisprogram terminationrewriting theorywellfoundedness

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Grammars and rewriting systems (68Q42)

Abstract: Five algebraic notions of termination are formalised, analysed and compared: wellfoundedness or Noetherity, L"ob's formula, absence of infinite iteration, absence of divergence and normalisation. The study is based on modal semirings, which are additively idempotent semirings with forward and backward modal operators. To model infinite behaviours, idempotent semirings are extended to divergence semirings, divergence Kleene algebras and omega algebras. The resulting notions and techniques are used in calculational proofs of classical theorems of rewriting theory. These applications show that modal semirings are powerful tools for reasoning algebraically about the finite and infinite dynamics of programs and transition systems.

Recommendations

• scientific article; zbMATH DE number 2163052
• Termination for a class of algorithms for constructing algebras given by generators and relations
• Termination of semi-algebraic loop programs
• Enabledness and termination in refinement algebra
• Terminal notions in set theory
• Termination Modulo Combinations of Equational Theories
• Refinement Algebra with Operators for Enabledness and Termination
• Verification, Model Checking, and Abstract Interpretation
• Term Rewriting and Applications
• Equational theories of abnormal termination based on Kleene algebra

Cited in

(18)

• Left omega algebras and regular equations
• Relational characterisations of paths
• Geographic wayfinders and space-time algebra
• scientific article; zbMATH DE number 4016171 (Why is no real title available?)
• On the Structure of Demonic Refinement Algebras with Enabledness and Termination
• Non-termination in Idempotent Semirings
• Reactive Probabilistic Programs and Refinement Algebra
• Hopscotch -- reaching the target hop by hop
• scientific article; zbMATH DE number 2163052 (Why is no real title available?)
• scientific article; zbMATH DE number 2087344 (Why is no real title available?)
• Algebraic coherent confluence and higher globular Kleene algebras
• Taming multirelations
• Abstract representation theorems for demonic refinement algebras
• Algebraic notions of nontermination: Omega and divergence in idempotent semirings
• Higher catoids, higher quantales and their correspondences
• Algebras for iteration and infinite computations
• Normal design algebra
• Enabledness and termination in refinement algebra

Describes a project that uses

Uses Software

• Z

This page was built for publication: Algebraic Notions of Termination

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3003302)