| AND (2008) | |||||||||||||||||
Abstract | |||||||||||||||||
| Abstract. 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. | |||||||||||||||||
Details der Publikation | |||||||||||||||||
| |||||||||||||||||