Algebraic notions of termination

  • Five algebraic notions of termination are formalised, analysed and compared: well-foundedness or Noetherity, Löb'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 reason about infinite behaviour, 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 behaviour of programs and state transition systems.

Download full text files

Export metadata

Statistics

Number of document requests

Additional Services

Share in Twitter Search Google Scholar
Metadaten
Author:Jules DesharnaisGND, Bernhard MöllerGND, Georg StruthGND
URN:urn:nbn:de:bvb:384-opus4-3511
Frontdoor URLhttps://opus.bibliothek.uni-augsburg.de/opus4/420
Series (Serial Number):Reports / Technische Berichte der Fakultät für Angewandte Informatik der Universität Augsburg (2006-23)
Publisher:Institut für Informatik, Universität Augsburg
Place of publication:Augsburg
Type:Report
Language:English
Year of first Publication:2006
Publishing Institution:Universität Augsburg
Release Date:2006/10/26
Tag:Idempotent semirings; Kleene algebras; omega-algebras; divergence semirings; modal operators
GND-Keyword:Kleene-Algebra
Institutes:Fakultät für Angewandte Informatik
Fakultät für Angewandte Informatik / Institut für Informatik
Fakultät für Angewandte Informatik / Institut für Informatik / Professur für Programmiermethodik und Multimediale Informationssysteme
Dewey Decimal Classification:0 Informatik, Informationswissenschaft, allgemeine Werke / 00 Informatik, Wissen, Systeme / 004 Datenverarbeitung; Informatik