Termination in Modal Kleene Algebra
Jules Desharnais, Bernhard Möller, Georg Struth · Kluwer Academic Publishers eBooks · 2006
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.