Omega Algebra, Demonic Refinement Algebra and Commands
P. Höfner, B. Möller, K. Solin
2006-11
Technical Report, Institute of Computer Science, University of Augsburg, March 2006
Abstract:
Weak omega algebra and demonic refinement algebra
are two ways of describing systems with finite and infinite iteration.
We show that these independently introduced kinds of algebras can
actually be defined in terms of each other. By defining modal operators
on the underlying weak semiring, that result directly gives a demonic
refinement algebra of commands. This yields models in which
extensionality does not hold. Since in predicate-transformer
models extensionality always holds, this means that the axioms of
demonic refinement algebra do not characterise predicate-transformer
models uniquely. The omega and the demonic refinement algebra of commands
both utilise the convergence operator that is analogous to the halting
predicate of modal $\mu$-calculus. We show that the convergence operator
can be defined explicitly in terms of infinite iteration and domain if and
only if domain coinduction for infinite iteration holds.
Downloads: