PROCESS ALGEBRA WITH LANGUAGE MATCHING

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.