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

program analysisKleene algebrasmodal operatorsprogram terminationidempotent semiringsNoetherityrewriting theorydivergence semiringsomega algebraswellfoundedness

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

(17)

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

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)