Abstract representation theorems for demonic refinement algebras

AbstractThe main result of this article is that every demonic refinement algebra with enabledness and termination is isomorphic to an algebra of ordered pairs of elements of a Kleene algebra with domain and with a divergence operator satisfying a mild condition. Divergence is an operator producing a test interpreted as the set of states from which nontermination may occur. An example of a KAD where a divergence operator cannot be defined is given. In addition, it is shown that every demonic refinement algebra with enabledness is also a demonic refinement algebra with termination