Non-regular iterators in process algebra

We consider three forms of non-regular iteration in process algebra: the push-down operation $, defined by x$y=x((x$y)(x$y))+y, the nesting operation ♯, defined by x ♯ y=x((x ♯ y)x)+y, and the back and forth operation ⇆, defined by x ⇆ y=x((x ⇆ y)y)+y. In the process algebraic framework ACP with abstraction and one of $, ♯ or ⇆ we provide definitions of the following standard processes: stack, context-free process, bag, and queue. These definitions apply to all standard behavioural equivalences (we only use xτ=x, where τ is the silent step). Moreover, these results yield the expressive power to express computable processes modulo rooted branching bisimulation equivalence, and hence support the equational founding of process algebra: standard processes can be represented as terms.

Authors

• Jan A. Bergstra
• Alban Ponse

Keywords

• Concurrency
• Process algebra
• Iteration
• Kleene star
• Nesting operation
• Push-down operation
• Back and forth operation
• Expressiveness