Register-machine based processes
Jan Aldert Bergstra, Alban Ponse · Journal of the ACM · 2001
We study extensions of the process algebra axiom system ACP with two recursive operations: the binary Kleene star * , which is defined by x * y = x ( x * y + y , and the push-down operation $ , defined by x $ y = x (( x $ y )( x $ y )) + y . In this setting it is easy to represent register machine computation, and an equational theory results that is not decidable. In order to increase the expressive power, abstraction is then added: with rooted branching bisimulation equivalence each computable process can be expressed, and with rooted ô-bisimilarity each semi-computable process that initially is finitely branching can be expressed. Moreover, with abstraction and a finite number of auxiliary actions these results can be obtained without binary Kleene star. Finally, we consider two alternatives for the push-down operation. Each of these gives rise to similar results.