Modal Tools for Separation and Refinement

Kleene modules and modal Kleene algebras are applied to automatically verify refinement laws for infinite loops and separation of termination. The key concept in this analysis is divergence which, in some models, abstractly characterises that part of a state space from which infinite dynamics is possible. In other models it expresses infinite iteration. Equational axioms for divergence are introduced, and the concept is refined for different contexts. In particular it is related to Löb's formula, which describes termination in modal logics.