Introduction:

What is CCS and CWB?

The Calculus of Communicating Systems (CCS) is an algebra for specifying and reasoning about concurrent systems. As an algebra, CCS provides a set of terms, operators and axioms that can be used to write and manipulate algebraic expressions. The expressions define the elements of a concurrent system and the manipulations of these expressions reveal how the system behaves.

The Concurrency WorkBench (CWB) is a public domain, interactive tool based on CCS. By using this tool, the specification or design of a concurrent system can be given and analyzed according to the theory of CCS. CWB is capable of displaying a simulation of a concurrent system described in CCS, searching for deadlock states, testing for equality between two agents, and determining if a system satisfies a given logical property (e.g., safety or liveness). In these notes, the notation of CWB will be used so that the reader may easily and immediately experiment with the presented examples using CWB. The reader is strongly encouraged to obtain CWB and use it learning about CCS.

Why Study CCS?

There are several reasons for studying the theoretical foundations of concurrency:

a well formulated theory of any aspect of computation helps to illuminate its fundamental elements. As the study of Turing machines helps to identify the essential notions of computation, so CCS and like theories help to identify the essential notions of concurrent computation.
CCS provides the foundation for answering very pragmatic questions. For example, the equality of two "agents" can be determined. If the two agents represent different implementations, then we can determine if one system is substitutable for the other. CCS also establishes the foundation for determining if an agent possesses certain "safety" or "liveness" properties, such as freedom from deadlock.
even very pragmatically-oriented professionals should occasionally study the theory relevant to their work, both because this is the hallmark of a professional and also because it helps to develop our patterns and habits of thinking.

What Aspects of Concurrent Computation does CCS Capture?

CCS

Agents with Sequential Behavior:

This section introduces two of the five CCS operators. The first operator, the action operator, allows the behavior of an agent to be defined by a sequence of events. The second operator, the relabelling operator, allows the actions of an agent to be changed, or relabelled.

The basic element in CCS is a uniquely named agent that exhibits a specified behavior. The behavior of an agent is defined by the set of events or actions that the agent is capable of performing. For example, a single element BUFFER agent may be defined to engage in the set of events (or actions) {in, out}. The sequence of events performed by a sequential agent is described by means of the "action" operator, denoted by a ".". For example, the BUFFER agent may be defined to perform the sequence of actions "in.out", intuitively to input a value and then output that same value.

In the CWB notation, the BUFFER agent is defined as:

            Command: bi  Buffer1  in.out.Buffer1

where "bi", short for "bind", is a command that takes the name of the agent (Buffer1 in this case) followed by the definition of the agents behavior. This definition means the the Buffer1 agent is repeatedly capable of performing the sequence "in" followed by "out". Note that this definition means the Buffer1 agent must first perform the "in" action followed by a single "out" action. No other behavior is possible. For example, Buffer1 can not perform an "out" action as its first action. It is also possible to define the same agent as follows:

            Command: bi  Buffer1  in.Buffer1'
            Command: bi  Buffer1' out.Buffer1

This definition uses two agents (Buffer1 and Buffer1'). Informally we can think of these as representing different "states" of the same single agent: Buffer1 is the empty state, in which only an "in" action is possible; Buffer1' is the full state, in which only an "out" action is possible.

The structure of an agen (the relationship among its "states") is important in CCS; the names of the actions are not significant. The names of actions are chosen to suggest the corresponding activity in the "real world" that the action is meant to represent. The "relabelling" operator in CCS allows the name of one or more actions to be changed. For example:

	 Command: bi MsgBuffer  Buffer1[receive/in, send/out]

defines an agent that is structurally identical to Buffer1, but uses the name "receive" ("send") wherever Buffer1 uses the name "in" ("out"). Relabelling is very useful when several replicates of an agent are used in defining a complex behavior as it is often necessary to change the name of the actions to achieve the desired interaction among the replicates.

Agents with Alternative Behavior:

In this section the CCS selection operator is defined. Using this operator an agent may be defined so as to engage in one of several alternative actions. This operator allows agents to model such structures as the select construct in Ada and the alternative guarded command construct in CSP.

Consider a two element buffer agent. When this buffer contains one element, either of two actions is possible: an "in" action accepting another element or and "out" action to dispense its stored element. The behavior of a two element buffer can be defined in CCS as follows:

Command: bi Buffer2 in.Buffer2' Command: bi Buffer2' in.Buffer2'' + out.Buffer Command: bi Buffer2'' out.Buffer2'

Notice that each equation defines a "state" of the agent. In the Buffer2' state either the "in" or the "out" action is possible. In the Buffer2'' state, the buffer is full and only an "out" action is possible

Viewing the Behavior of an Agent:

In addition to the algrebraic representation of an agent, the behavior of an agent may also be represented in a graphical form and may be randomly simulated by CWB.

The graphical representation of an agent's behavior is in terms of a labelled transition system. In a labelled transition system, the vertices in a directed graph represent CCS expressions (or agent states) and each arc is labelled by the event/action that causes the expression (state) from which the arc emmanates to become the expression (state) to which the arc is directed. The behavior of the Buffer2 agent can be depicted by the following graph:


         +--------------+
         |              |
         |   Buffer2    |
         |              |
         +--------------+
             |     ^
             |     |
         in  |     | out
             |     |
             V     |
         +--------------+
         |              |
         |   Buffer2'   |
         |              |
         +--------------+
             |     ^
             |     |
         in  |     | out
             |     |
             V     |
         +--------------+
         |              |
         |   Buffer2''  |
         |              |
         +--------------+

The graphical form is a useful, visual technique for understanding the behavior of simple agents. For complex systems, the graph becomes as large as the state space of the agent.

The behavior of an agent can also be explored by using the CWB "random" command. This command makes a random choice when evaluating an expression with a selection. As an example, consider the following CWB command and it associated output:

        Command: random  20 Buffer


        in,in,out,out,in,in,out,out,in,out,
        in,in,out,in,out,out,in,in,out,in

The output from the command represents a randomly generated behavior of 20 actions of the Buffer2 agent. This is, of course, only one of the many initial behaviors for this agent.

Interacting Agents :

Realistic, interesting concurrent systems consist of two or more interacting agents. The agents are concurrent in the sense that they may take some action independently of each other. The agents are interacting in the sense that some action require the collaborative participation of two or more agents. In CCS, the interaction occurs between exactly two agents.

The CCS composition operator, denoted by "|", is used to define an agents whose behavior is determined by composing two (or more) existing agents. Such composed agents, may interact. The interaction in CCS synchronous, both agents must be willing at the same time to interact. This is similar to the way process interactions are defined in languages like Ada and CSP.

Agents indicate their desire to participate in an interaction with another agent by means of a convention on the names of their actions. This convention is illustrated by the following example which uses the composition operator:

	 Command: bi F   a.x.F 
	 Command: bi G  'x.b.G
	 Command: bi H  ( F | G )

In this example, agent H is defined as the composition of agents F and G. Notice that agent F has the action "x" as one of its events and that the agent G has the action "'x" as one of its events. Two events with the same base name (in this case, "x") where the name occurs in one of the agents with a preceeding "'" (tick) mark indicates that the two agents may interact through the action. It does not matter which of the two agents uses the tick mark.

Because interaction is synchronous, the only possible first action in the system H above is the "a" action in agent F. At this point, agent F is willing to perform an "x" action while agent G is willing to perform an "'x" action. The interaction occurs, allowing F to return to its original state and allowing G to subsequently perform its "b" action.

We might (incorrectly) expect that the behavior of agent H could be written as:

Command: bi HSpec a.t.b.HSpec

However, if we use CWB we might see the following behavior of agent H being revealed:

Command: random 20 H a,a,b,b,a,b,a,b,'x,b,a,a,b,b,'x,b,a,a,x,a

Notice that the actions x and 'x are present in this visible behavior. This occurs because we have not indicated that x and 'x should have a scope any different than that of the actions a or b. That is, the system H allows outside agents to interact with it at any of its ports a,b,x or 'x.

It is often the case that the interaction between two agents is intended to be limited in scope, insuring that no external agent can participate in, or observe the occurrence of, the interaction between the two agents.

The restriction operator in CCS, denoted by "\{}, is used to limit the visibility of its port names. This operator is used as shown in the following redefinition of the agent H (renamed here H' to avoid any confusion):

	 Command: bi F   a.x.F 
	 Command: bi G  'x.b.G
	 Command: bi H'  ( F | G )\{x}

If we now use CWB to observe the behavior of H, we would obtain:

Command: random 20 H' a,b,a,a,b,b,a,a,b,b,a,a,b,a,b,b,a,b,a,a

This behavior has no occurrences of the actions x or 'x.

Equality of Agents:

Coming Soon!!!

Go Back to the Operating Systems page.

Last updated: 22 Feb 1995 / cs5204@ie.cs.vt.edu