Process Algebra with Iteration and Nesting

Abstract

We introduce iteration in process algebra by means of (the original, binary version of) Kleene's star operation: x^*y is the process that chooses between x and y, and upon termination of x has this choice again. We add this operation to a whole range of process algebra axiom systems, starting from BPA (Basic Process Algebra). In the case of the most complex system under consideration, ACP_τ, every regular process can be defined with handshaking (two-party communication) and auxiliary actions. Next we introduce nesting in process algebra: x^#y is defined by the equation x^#y = x(x^#y)x + y. We show that ^* and ^# are not interdefinable in most of the axiom systems we regard. The extension with ^#, and the extension with ^* and ^# of the systems considered also give a genuine hierarchy in expressivity. Finally, it is argued that each finitely branching, computable graph can be defined in ACP_τ extended with ^* and ^#, and using handshaking and auxiliary actions.

*

University of Amsterdam, Programming Research Group, Kruislaan 403, 1098 SJ Amsterdam, The Netherlands

§

Department of Philosophy, Heidelberglaan 8, 3584 CS Utrecht, The Netherlands

¶

CWI, Department of Software Technology, Kruislaan 413, 1098 SJ Amsterdam, The Netherlands

Author notes

1University of Amsterdam, Programming Research Group, Kruislaan 403, 1098 SJ Amsterdam, The Netherlands, 2Department of Philosophy, Heidelberglaan 8, 3584 CS Utrecht, The Netherlands, 3CWI, Department of Software Technology, Kruislaan 413, 1098 SJ Amsterdam, The Netherlands