Modal design algebra

We give an algebraic model of (H3) designs based on a variant of modal semirings, hence generalising the original relational model. This makes the theory applicable to a wider class of settings, e.g., to algebras of sets of traces. Moreover, we set up the connection with the weakly and strongly demonic semantics of programs as discussed by a number of authors. This is done using commands (a, t) where a corresponds to the transition relation of a program and the condition t characterises the input states from which termination is guaranteed. The commands form not only a semiring but even a Kleene and omega algebra. This is used to calculate closed expressions for the least and greatest fixed point semantics of the demonic while loop.