Algebraic Notions of Termination

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

Georg Struth, Jules Desharnais, Bernhard Möller

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

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 (14)

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

Uses Software

• Z

Recommendations

• Title not available (Why is that?) 👍 👎
• Enabledness and termination in refinement algebra 👍 👎
• Verification, Model Checking, and Abstract Interpretation 👍 👎
• Refinement Algebra with Operators for Enabledness and Termination 👍 👎
• Termination Modulo Combinations of Equational Theories 👍 👎
• Term Rewriting and Applications 👍 👎
• Termination for a class of algorithms for constructing algebras given by generators and relations 👍 👎
• Terminal notions in set theory 👍 👎
• Termination of Semi-algebraic Loop Programs 👍 👎
• Equational Theories of Abnormal Termination Based on Kleene Algebra 👍 👎

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)