Local Testing and Implementable Concurrent Processes,
PhD Thesis, Department of Computing, Imperial College, University of London, 1994.
We develop a theory of implementable concurrent processes within the algebraic style introduced by Milner. The theory has the following components: the meaning of processes is based solely on their locally observable behaviour and process operators are defined by implementable transition rules. Throughout the thesis we consider processes which can perform both visible and silent actions and may possibly diverge.
Following earlier work on the testing of processes we agree that testing is a reasonable method to discover the behaviour of processes. We define locally observable behaviour as the behaviour which can be discovered by local testing as distinct from global testing in the sense of Abramsky which can determine the whole observable behaviour. We define a number of testing preorders, the finest of which is copy+refusal preorder. This preorder is generated by copy+refusal tests consisting of traces, refusals and copying. We show that copy+refusal preorder is the finest local preorder: adding any other local monotone tests to copy+refusal tests does not produce a finer preorder. Moreover, copy+refusal equivalence is the finest local equivalence, since adding any other finite and local (but not necessarily monotone) tests to copy+refusal tests does not generate a finer equivalence.
To support the claim that copy+refusal preorder is a natural and intuitive preorder we present a number of alternative characterisations of it. We define a simulation-like preorder, called refusal simulation, and show that it coincides with copy+refusal preorder for sort- and image-finite processes. Moreover, we propose a modal characterisation of copy+refusal preorder in terms of formulae of a subset of the Hennessy-Milner Logic.
A widely used method of defining the operational meaning of process operators is by structured transition rules. A transition rule for an operator tells us how the behaviour of a composite process, which is constructed from a number of subprocesses and the operator itself, depends on the behaviour of the subprocesses. We define a format of implementable and observation preserving transition rules called the Implementable Structured Operational Semantics (ISOS) format. The ISOS format is a subformat of the GSOS format. The ISOS rules are implementable because their form describes how the operators may be realistically implemented by certain process interfaces. The ISOS rules are observation preserving because the defined version of weak bisimulation is a precongruence for ISOS contexts. We show that refusal simulation is a precongruence for sort-finite processes and ISOS contexts.
As an example of an ISOS calculus, we present a language which is similar to the existing algebraic languages and in particular to CSP. It is worth noting that the CCS + operator is not implementable. We present a sound and complete axiom system with respect to copy+refusal equivalence for finite and divergence free processes in the language.
Our main results are
The thesis can be obtained from the author.