An axiom system ACP(LM)(tau), is presented as a variant of the process
algebra ACP. The acronym ACP(LM)(tau) stands for ACP with abstraction
, extended with operators and axioms for langunge matching. Language m
atching is a technique based on trace information for labelling and cu
tting off process terms that do not match some given language, or set
of traces. It is shown that in combination with the axioms for action
alphabets interesting results are derivable, the most important of whi
ch is the Redundancy Theorem 3.3.6, which roughly states that if no tr
ace labels occur in the expression delta(H)(p(l) \\ q), where p(l) is
a labelled version of some process p, then it holds that delta(H)(p(l)
\\ q) = delta(H)(p \\ q). It is shown that under certain natural cond
itions a similar result holds when abstraction is applied to p(l) and
p. In order to illustrate the use of language matching the Concurrent
Alternating Bit Protocol (CABP) is verified. The CABP is a simple comm
unication protocol, which can be recursively specified over the signat
ure of ACP(tau), and it may be regarded as a slightly more 'sophistica
ted' variant of the well-known Alternating Bit Protocol. Earlier studi
es of this protocol have already demonstrated that 'redundancies in a
context' make this protocol hard to verify. Our verification is carrie
d out by means of ACP(tau) with language matching, extended with the a
bstraction rule CFAR(b), and the conditional alphabet axioms. The veri
fication is split into two parts so that it is 'modular', and in the v
erification some basic knowledge about the expected behaviour of the s
ystem is used, in order to allow the effective application of language
matching.