University of Leicester

computerscience

Local Testing and Implementable Concurrent Processes,
Irek Ulidowski,
PhD Thesis, Department of Computing, Imperial College, University of London, 1994.

Abstract

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

  1. ISOS contexts capture only locally observable behaviour: ISOS trace precongruence refines copy+refusal preorder for sort-finite processes,
  2. ISOS contexts capture all locally observable behaviour: copy+refusal preorder refines ISOS trace precongruence for sort-finite processes.
As a result, ISOS contexts capture precisely the locally observable behaviour of processes.

The thesis can be obtained from the author.

| [University Home]|[Faculty of Science]|[MCS Home]|[CS Home]||[University Index A-Z]|[University Search]|[University Help]|

Author: Irek Ulidowski (I.Ulidowski@mcs.le.ac.uk).
University of Leicester. Last modified: 13th January 2004, 16:58:40
CS Web Maintainer.