Beschreibung:
<jats:p>
We study extensions of the process algebra axiom system
<jats:bold>ACP</jats:bold>
with two recursive operations: the
<jats:italic>binary Kleene star</jats:italic>
<jats:sup>*</jats:sup>
, which is defined by
<jats:italic>x</jats:italic>
<jats:sup>*</jats:sup>
<jats:italic>y</jats:italic>
=
<jats:italic>x</jats:italic>
(
<jats:italic>x</jats:italic>
<jats:sup>*</jats:sup>
<jats:italic>y</jats:italic>
+
<jats:italic>y</jats:italic>
, and the
<jats:italic>push-down</jats:italic>
operation
<jats:sup>$</jats:sup>
, defined by
<jats:italic>x</jats:italic>
<jats:sup>$</jats:sup>
<jats:italic>y</jats:italic>
=
<jats:italic>x</jats:italic>
((
<jats:italic>x</jats:italic>
<jats:sup>$</jats:sup>
<jats:italic>y</jats:italic>
)(
<jats:italic>x</jats:italic>
<jats:sup>$</jats:sup>
<jats:italic>y</jats:italic>
)) +
<jats:italic>y</jats:italic>
. 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
<jats:italic>rooted branching bisimulation equivalence</jats:italic>
each computable process can be expressed, and with
<jats:italic>rooted ô-bisimilarity</jats:italic>
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.
</jats:p>