Algebra of communicating processes with abstraction (Q1067408)

This paper presents an equational axiom system \(ACP_{\tau}\), for communicating processes with silent actions (\(\tau\)-steps). The system is an extension of ACP, Algebra of Communicating Processes [see the authors, Inf. Control 60, 109-137 (1984)] with Milner's \(\tau\)-laws [see \textit{R. Milner}, A calculus of communicating processes (Berlin 1980; Zbl 0452.68027)] and an explicit abstraction ('hiding') operator. By means of a model of finite acyclic process graphs syntactic properties such as consistency and conservativity over ACP are proved. Also, the Expansion Theorem (which breaks down a parallel composition of n processes) is proved. By means of a term rewriting analysis using Dershowitz's recursive path orderings, termination of rewriting terms according to the \(ACP_{\tau}\) axioms is proved.