Jan A. Bergstra, Jan Willem Klop

*Theoretical Computer Science* 37, pages 77~~121~~

1985

<div>We present an axiom system ACP, for communicating processes with silent actions (‘τ-steps’). The system is an extension of ACP, Algebra of Communicating Processes, with Milner's τ-laws and an explicit abstraction operator. By means of a model of finite acyclic process graphs for ACP<sub>τ</sub>, syntactic properties such as consistency and conservativity over ACP are proved. Furthermore, the Expansion Theorem for ACP is shown to carry over to ACP<sub>τ</sub>. Finally, termination of rewriting terms according to the ACP<sub>τ</sub>, axioms is probed using the method of recursive path orderings.</div>