The paradigm of computer science is nowadays shifting from computation to
communication. In this paper we aim to give an impression of the algebra of
actions and communications as it has been developed during the past quarter
of a century.
We present specifically the system ACP, Algebra of Communicating
Processes. Here $a, b, c, \ldots$ denote atomic events (or actions,
or steps). For example, $a{\cdot}a{\cdot}(b + c)$ is the process able to perform two
$a$-steps followed by a $b$-step or a $c$-step. This differs from the process
$a{\cdot}a{\cdot}b + a{\cdot}a{\cdot}c$, due to the different timing of the choice
between a $b$- and a $c$-step. Process $x$ can operate in parallel with process $y$,
notation $x \| y$, where some actions in $x$ may happen simultaneously with some actions
in $y$; the resulting actions are called communication actions. Such actions
are `half actions', needing their counterpart for the execution as a full action.
In daily life a handshake is an example of a pair of half actions. We even have
ternary communication actions on the keyboard of a PC: control-alt-delete.
In music we find also quaternary actions, etc. The results of such internal
communications we want to abstract away. This is formalised with the invisible
action $\tau$ (`silent move'), facilitating the composition of modular hierarchies
of process systems. The classical triple specification-implementation-verification
then takes a straightforward form. The specification of the desired external behaviour is
a simple process SPEC. The implementation is a complicated process IMP. The
verification that the implementation is indeed correct, can be a purely algebraic,
equational computation that a suitable abstraction of IMP yields SPEC:
ABS(IMP) = SPEC.
Next to an overview of the process algebraic framework, we present a soundness
and completeness proof for the axiom system underlying this framework, with respect
to a fundamental semantics called rooted branching bisimulation. Thus
a derivation of ABS(IMP) = SPEC implies that the implementation and its
specification satisfy the same behavioural properties (soundness), while on
the other hand the absence of such a derivation implies that the implementation and its
specification are not rooted branching bisimulation equivalent (completeness).
Computing with actions and communications, process algebra, is logically and
mathematically interesting. On top of that, process algebra contributes to
security and comfort: current process algebra tools are used to prove correctness
of railway emplacements, helicopter software, and communication protocols in the
remote control of a television set.
This paper has grown out of an invited lecture of the second author
at the Joint Mathematical BeNeLuxFra Conference in Ghent, May 2005.
Slides of that lecture can be found at www.cs.vu.nl/~jwk.