Algebraic Notions of Termination

DOI10.2168/LMCS-7(1:1)2011zbMATH Open1214.68185arXiv1012.5803MaRDI QIDQ3003302FDOQ3003302

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)

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.

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

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

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)

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
• Title not available (Why is that?)
• 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
• Title not available (Why is that?)
• Left omega algebras and regular equations
• Taming Multirelations
• Title not available (Why is that?)
• Geographic wayfinders and space-time algebra

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)