================================================================================ P9423 J.J. van Wamel "Process algebra with language matching" An axiom system "ACP-tau-LM" is presented as a variant of the process algebra ACP (Algebra of Communicating Processes). The acronym "ACP-tau-LM" stands for ACP with abstraction, extended with operators and axioms for language matching. Language matching is a technique based on trace information for labelling and cutting off process terms that do not match some given trace (or set of traces). It is shown that in combination with the axioms for action alphabets interesting results are derivable, the most important of which is the Redundancy Theorem, which roughly states that if no trace labels occur in the expression "encaps-H(p-l || q)", where "p-l" is a labelled version of some process "p", then it holds that "encaps-H(p-l || q) = encaps-H(p || q)". It is shown that under certain natural conditions a similar result holds when abstraction is applied to "p-l" and "p", respectively. As an example the Concurrent Alternating Bit Protocol (CABP) is verified. The CABP is a simple communication protocol, which can be recursively specified over the signature of "ACP-tau", and it can be regarded as a slightly more `sophisticated' variant of the well-known Alternating Bit Protocol. The verification is carried out using "ACP-tau" with language matching, extended with the abstraction rule "CFAR-b", and the conditional alphabet axioms. The verification is split in two parts so that it is `modular', and during the verification some basic knowledge about the expected behaviour of the system is used, in order to effectively apply language matching.