$ACP_\tau$: a universal axiom system for process specification

Starting with Basic Process Algebra (BPA), an axiom system for alternative composition(+) and sequential composition(·) of processes, we give a presentation in several intermediate stages leading to $ACP_\tau$, Algebra of Communicating Processes with abstraction. At each successive stage an example is given showing that the specification power is increased. Also some graph models for the respective axiom systems are informally presented. We conclude with the Finite Specification Theorem for $ACP_\tau$ stating that each finitely branching, effectively presented process (as an element of the graph model) can be specified in $ACP_\tau$ by means of a finite system of guarded recursion equations.