A theory of testing for ACP

This paper introduces a process algebra which incorporates the auxiliary operators of ACP, [BK85], and is tailored towards algebraic verifications in the theory of testing equivalence. The process algebra we consider is essentially a version of ACP with the empty process in which the nondeterministic choice operators familiar from TCSP, [BHR84], and TCCS, [DH87], are used in lieu of the internal action τ and the single choice operator favoured by CCS, [Mil89], and ACP. We present a behavioural semantics for the language based upon a natural notion of testing equivalence, [DH84], and show that, contrary to what happens in a setting with the internal action τ, the left-merge operator is compatible with it. A complete equational characterization of the behavioural semantics is given for finite processes, thus providing an algebraic theory supporting the use of the auxiliary operators of ACP in algebraic verifications for testing equivalence. Finally we give a fully-abstract denotational model for finite processes with respect to the testing preorder based on a variation on Hennessy's Acceptance Trees suitable for our language.