\omega -Algebra for pushdown actions? [loc-0018]

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 .

DefinitionMultiplication

We define a sequential composition operator for triples as follows: (w_1,s_1,s'_1)\ \mathit {seq}\ (w_2,s_2,s'_2) = \begin {cases} (w_1w_2, s_1, s'_2) & \text {if}\ s'_1 = s_2 \\ \text {undefined} & \text {otherwise} \end {cases} Note that for sequential composition to make sense, the initial stack of the second triple must match the final stack of the first triple. As the words w_1 and w_2 may be infinite, we define concatenation in the usual way, where w_1w_2 = w_1 when w_1 is infinite.

Then, the definition of multiplication in our algebra is the straightforward lifting to sets:

S_1 \cdot S_2 = \{ x\ \mathit {seq}\ y \mid x \in S_1, y \in S_2, x\ \mathit {seq}\ y\ \text {defined}\}

DefinitionThe Unit Element

The 1 element for multiplication here just consists of all triples with an empty word that leave the stack unchanged:

\mathbf {1} = \{ (\varepsilon , s, s) \mid s \in \Sigma ^\infty \}

DefinitionThe Kleene Star

Let S^n denote the n-times self-multiplication of S, where S^0 = \mathbf {1}. Then, the Kleene star for our algebra is:

S^\ast \triangleq \bigcup _{n \in \mathbb {N}}\ S^n

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.

DefinitionThe Omega Operator

We define the { }^\omega operator as follows: S^\omega \triangleq \{ (w, s_1, s_2) \mid \exists \text {an infinite run for}\ w\ \text {in}\ S\ \text {starting with stack}\ s_1\} The guard in the above set comprehension feels informal, so we will define momentarily a judgment or predicate S \vdash (w,s_1)\ \textbf {infinite} , which means the same thing:

S^\omega \triangleq \{ (w, s_1, s_2) \mid S \vdash (w,s_1)\ \textbf {infinite}\}

Note that this definition places no constraint on s_2, so any non-empty set S^\omega will include all possible final stacks.

It remains to formalise our predicate. Formally, it is the largest (i.e. coinductive) predicate satisfying the following rule:

\dfrac {w = xw' \quad (x,s_1,s_2) \in S \quad S \vdash (w',s_2)\ \textbf {infinite}}{S \vdash (w,s_1)\ \textbf {infinite}}

This means we can prove S \vdash (w,s_1)\ \textbf {infinite} if we can find an infinite chain of moves in S starting with stack s_1 that, when all combined, results in the word w.

Note that while the run is infinitely long, the word w need not be, due to the presence of \varepsilon -moves.

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!

References

    Reference. Verification of Pushdown Systems Using Omega Algebra with Domain [mathieu-desharnais-2005]

    Context

      Weeknotes 2025-W27 [2025-W27]

      Related

        Person. Jules Desharnais [jdesharnais]

        Person. Peter Höfner [hoefner]

        Person. Yi Yao [yiyao]