Termination in Modal Kleene algebra

Abstract

Modal Kleene algebras (MKAs) are Kleene algebras with forward and backward modal operators defined via domain and codomain operations. The paper formalizes and compares different notions of termination, including Löb's formula, in MKA. It studies exhaustive iteration and gives calculational proofs of two fundamental termination-dependent statements from rewriting theory: the well-founded union theorem by Bachmair and Dershowitz and Newman's lemma. These results are also of general interest for the termination analysis of programs and state transition systems. © 2004 Springer Science + Business Media, Inc.