1.2 The CSP View of the World

CSP is a language where processes proceed from one state to another by engaging in (instantaneous) events. Processes may be composed by operators which require synchronisation on some events; each component must be willing to participate in a given event before the whole can make the transition. This, rather than assignments to shared state variables, is the fundamental means of interaction between agents.

The composition of processes is itself a process, allowing a hierarchical description of a system. The hiding operator makes a given set of events internal: invisible to, and beyond the control of, its environment; this provides an abstraction mechanism.

The theory of CSP has classically been based on mathematical models remote from the language itself. These models have been based on observable behaviours of processes such as traces, failures and divergences, rather than attempting to capture a full operational picture of how the process progresses.

On the other hand CSP can be given an operational semantics in terms of labelled transition systems. This operational semantics can be related to the mathematical models: that the standard semantics of CSP are congruent to a natural operational semantics is shown in, for example, [Roscoe88a] and [Scat98].

Given that each of our models represents a process by the set of its possible behaviours, it is natural to represent refinement as the reduction of these options: the reverse containment of the set of behaviours. If Q refines P we write PQsometimes subscripting to indicate which model the refinement it is respect to.

FDR directly supports a number of CSP models:

• The traces model: a process is represented by the set of finite sequences of communications it can perform. The set of P’s (finite) traces is given by traces(P).
• The stable failures model [JateMey]: a process is represented by its traces as above and also by its failures. A failure is a pair (s,X), where s is a finite trace of the process (i.e., in traces(P)) and X is a set of events it can refuse after s. This means (operationally) that after trace s, the process P has come into a state where it can do no internal action and no action from the set X. The set of P’s failures is given by failures(P).
• The failures/divergences model [BroRos85]: a process is represented by its failures as above, together with its divergences. A divergence is a finite trace during or after which the process can perform an infinite sequence of consecutive internal actions. The failures are extended so that we do not care how the process behaves after any divergence.
• The refusal testing model [Lowe08]: a process is represented by a sequence of alternating stable refusal sets and events, possibly terminating in deadlock. Unstable states, where the process does not have a well defined refusal set are represented by \bullet.
• The revivals model [ReeRosSin07,Roscoe09]: the concept of a failure is extended with an event a that the process might accept after completing the trace s: (s,X,a). This makes the revivals model more discriminating than the failures model.
• Lastly the tau priority model [LowOuk05] is a variant of the traces model where a set of events is defined as having less priority than \tau. As a result, the process can only offer an event from the defined set when it is in a stable state. One application of this is to model the passage of time with a tock event.

All of these models have the obvious congruence theorem with the standard operational semantics of CSP. In fact FDR works chiefly in the operational world: it computes how a process behaves by applying the rules of the operational semantics to expand it into a transition system. The congruence theorems are thus vital in supporting all its work: it can only claim to prove things about the abstractly-defined semantics of a process because we happen to know that this equals the set of behaviours of the operational process FDR works with.

The congruence theorems are also fundamental in supporting the hierarchical compressions described in Using Compressions. For we know that if C[.]is any CSP context then the value in one of our semantic models of C[P] depends only on the value (in the same model) of P, not on the precise way it is represented as a transition system. Therefore, it may greatly be to our advantage to find another representation of P with fewer states. If, for example, we are combining processes P and Q in parallel and each has 1000 states, but can be compressed to 100, the compressed composition can have no more than 10,000 states while the uncompressed one may have up to 1,000,000.

This document was generated by Phil Armstrong on May 17, 2012 using texi2html 1.82.