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.

Let ℚ₀ denote the rational numbers expanded to a ‘meadow’, that is, after taking its zero-totalized form (0⁻¹=0) as the preferred interpretation. In this paper, we consider ‘cancellation meadows’, i.e. meadows without proper zero divisors, such as ℚ₀ and prove a generic completeness result. We apply this result to cancellation meadows expanded with differentiation operators, the sign function, and with floor, ceiling and a signed variant of the square root, respectively. We give an equational axiomatization of these operators and thus obtain a finite basis for various expanded cancellation meadows.

We extend process algebra with guards, comparable to the guards in guarded commands or conditions in common programming constructs such as ‘if — then — else — fi’ and ‘while — do — od’. The extended language is provided with an operational semantics based on transitions between pairs of a process and a (data-)state. The data-states are given by a data environment that also defines in which data-states guards hold and how atomic actions (non-deterministically) transform these states. The operational semantics is studied modulo strong bisimulation equivalence. For basic process algebra (without operators for parallelism) we present a small axiom system that is complete with respect to a general class of data environments. Given a particular data environmentL we add three axioms to this system, which is then again complete, provided weakest preconditions are expressible andL is sufficiently deterministic. Then we study process algebra with parallelism and guards. A two phase-calculus is provided that makes it possible to prove identities between parallel processes. Also this calculus is complete. In the last section we show that partial correctness formulas can easily be expressed in this setting. We use process algebra with guards to prove the soundness of a Hoare logic for linear processes by translating proofs in Hoare logic into proofs in process algebra.