In our weekly meeting, Yi Yao, Peter Höfner and I were examining a paper by Vincent Mathieu and Jules Desharnais about verification of pushdown systems using \omega -algebras with domain. One thing that we got hung up on was that the underlying algebra seems to insist that the underlying set be of mixed type, where control actions (i.e. the labels on transitions, or expected inputs to the automaton) are interleaved with stack actions (either pushing or popping symbols from the stack). The result is that a bunch of axioms must be added to deal with cancelling pushes and pops, and reordering actions to enable such cancellations.
Following a proposal from Peter Höfner, I formalised the following alternative algebra, which should work just as well as the algebra in the paper but avoids this extra complexity. Instead of having strings of mixed types of actions, we instead have our algebra consist of sets of triples, which includes a (possibly infinite) string of control actions, a (possibly infinite) initial stack, and a (possibly infinite) final stack. S \triangleq \mathcal {P}(A^\infty \times \Sigma ^\infty \times \Sigma ^\infty )
In our notation, A is the set of control actions, \Sigma is the set of stack symbols, and the {}^\infty superscript denotes both finite and infinite strings of elements, i.e. X^\infty = X^\ast \cup X^\omega .
These definitions are sufficient to show that (S, \cup ,\cdot , \emptyset , \mathbf {1}, {}^\ast ) is a Kleene algebra. Then, to extend this to an \omega -algebra, one needs only the {}^\omega operator.
One thing we noticed here is that it doesn't matter to the operators what the type of the stack is. Indeed, replace stacks with tapes and you'd get something describing actions on a turing machine. This gives us compelling directions to take this!