Termination in Modal Kleene Algebra

Abstract:
Modal Kleene algebras are Kleene algebras with forward and backward modal operators defined via domain and codomain operations. The paper investigates the algebraic structure of modal operators. It studies and compares different notions of termination in this class, including an algebraic correspondence proof of Löb's formula from modal logic. It gives calculational proofs of two fundamental statements from rewriting theory that involve termination: Bachmair's and Dershowitz's well-founded union theorem and Newman's lemma. These results are also of general interest for the termination analysis of programs and state transition systems.