Where academic tradition
meets the exciting future

You are here: TUCS > PUBLICATIONS > Publication Search > Omega Algebra, Demonic Refinem...

Omega Algebra, Demonic Refinement Algebra and Commands

Peter Höfner, Bernhard Möller, Kim Solin, Omega Algebra, Demonic Refinement Algebra and Commands. In: Relations and Kleene Algebra in Computer Science, Lecture Notes in Computer Science 4136, 222–234, Springer, 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.

BibTeX entry:

@INPROCEEDINGS{inpHoMoSo06a,
  title = {Omega Algebra, Demonic Refinement Algebra and Commands},
  booktitle = {Relations and Kleene Algebra in Computer Science},
  author = {Höfner, Peter and Möller, Bernhard and Solin, Kim},
  volume = {4136},
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  pages = {222–234},
  year = {2006},
  keywords = {Omega algebra, demonic refinement algebra , commands},
}

Belongs to TUCS Research Unit(s): FUNDIM, Fundamentals of Computing and Discrete Mathematics

Publication Forum rating of this publication: level 1

Edit publication