Lecture 1


                   An Informal Introduction to Processes


In this tutorial we are concerned with discrete systems and digital circuits. Examples of such systems are counters and communication protocols and vending machines. Digital circuits are either combinational or sequential (i.e., have memory).

Discrete systems and digital circuits may be viewed as a single process, or alternatively as being composed of subsystems (processes) which suitably cooperate or communicate.

The characteristic feature of a (non-trivial) process is its capability to perform some action. Usually, by performing an action the given process evolves into some other process.  The actions of a process, which is modeling some system, are either inputs to the system or outputs generated by the system. We assume that all process actions are instantaneous, i.e., their duration in time is negligible. With a given system, to be modeled by a process, we associate a restricted set of actions, we are interested in, disregarding other actions we are not concerned with in our analysis.


1.1          An Example of a  Process


Consider a light which is controlled (switched on and off) by means of a push button. Let push denote the activation of the push button, let on denote the changing of the light to ‘on’ and off its changing to ‘off’.  If we assume that this button-light system never fails, and that it starts with the light being off, its behavior may be described by the following process PBL:

                 PBL = push;on;push;off;push;on;push;off; …

Here the behavior of PBL is specified by an infinite repetitive sequence of actions. The three dots ... indicate “repeat forever”.

To avoid this three-dot convention, we introduce the following notation:

                 PBL =  *[push;on;push;off]

Thus the star * denotes here “repeat forever”.

We shall refer to the right-hand side of the above equation as the behaviour expression of PBL.

Alternatively, this process may be defined recursively as follows:

                  PBL = push;on;push;off;PBL

This notation is based on the fact that after the first occurrence of the sequence push;on;push;off; the system returns to its beginning state.

Note that the set {push, on,off} is referred to as the set of events or actions of the process PBL, denoted Act(PBL).

Similarly, an (old-fashioned) clock which ticks forever (and this is all we are concerned with) may be represented by the process clock, where

                        clock = *[tick]     {behaviour expression}

or                     clock = tick;clock      {recursive equation}


A Simple Law


Informally,  *[a;b] = a;b;a;b;a;b;…

Hence, the following law is rather evident.


Law 1.1    [a;b] = a;*[b;a]

This law also holds if a and b are replaced by finite sequences of actions.


1.2          A Very Simple Protocol


We now look at a very simple protocol. It relates to a point-to-point data transmission channel, sending messages from the Sender station to the Receiver station over a reliable data channel. The Receiver station acknowledges the receipt of any message by sending back an ACK signal over a reliable ACK channel.

To be more precise, the Sender station performs the activity represented  by the following process:

                    PSEND = *[PUT;msg;ack]

Here, ‘PUT’ refers to getting the next message ready to be sent. ‘msg’ refers to the action of sending this message, and ‘ack’ indicates the event of receiving an ACK signal.

The corresponding activity of the Receiver station is represented by the following process

                     PREC = *[msg;GET;ack]

‘GET’ refers to getting and suitably handling the received message. Here, ‘msg’ is the event of receiving the message sent, and ‘ack’ refers to the action of sending an ACK signal. In the “parallel composition” of the two processes it is assumed that equally named actions/events occur simultaneously. Thus the parallel composition , denoted by ‘||’ becomes:

   SPROT =  PSEND || PREC  = *[PUT;msg;GET;ack]

If in SPROT all actions except ‘PUT’ and ‘GET’ are “hidden”, the outcome is evidently:


All the above concepts will be properly formalized in subsequent lectures.


1.3          Terminating Processes


The processes we have considered so far are never-ending. Of course, we are also interested in processes which terminate at some point. Presently, we will only be concerned with processes which terminate “successfully”, i.e., after performing their intended task. Later on we also discuss processes which do not terminate properly, i.e., they get “stuck” , for some reason, typically due to an non-intended deadlock.

We will use $ to denote the trivial process unable to perform any action. Thus the process P1 = a;$ will perform action a and then consider its task completed. The symbol ‘;’, which we have already used in the previous sections,  is called the prefix operator. In general, if P is any process, then a;P is the process capable of performing only action a, and after doing so, will change into process P. Let now P2 = a;(b;P). This may be written as P2=a;b;P.


1.4          Process Graphs


Processes may also be represented by so-called “process-graphs”.                          

For example, the process a;b;c;$ is represented by the graph of Figure 1.1.

                                   a               b          c

                      a;b;c;$    b;c;$    c;$    $


                                        Figure 1.1


In such a graph the nodes represent processes and the labelled arrows represent transitions which are immediately executable.

The process graph representing the process PBL of Section 1.1 is shown next (Fig. 1.2).



                              PBL    Q

                          off            on

                                S        R



                                Figure 1.2


Here PBL=push;Q ,  Q=on;R ,  R=push;S  and S=off;PBL .


Process graphs are evidently closely related to state graphs representing FSMs (Finite State Machines). For example, the state

graph below represents the same behaviour as the process graph of Fig. 1.1, in the evident way.




1.5          The Choice Operator


Consider now process P3 represented by the process graph of Figure 1.3.



                                b         a       c

                           $ ← b;$ P3 →  $


                                   Figure 1.3


Process P3 may be specified by the behaviour expression

                               P3= a;b;$ [ ] c;$

where ‘[ ]’ is the choice operator.  

Generally, P[ ] Q denotes the process which behaves either the same way as P or alternatively as Q.


1.6          Exercises


Exercise  Ex1.1


Let PX1.1 = *[a;b] [ ] *[c;d].

Construct the relevant process graph.

Hint: (1) In a process-graph a label may appear more than once.

         (2) Use Law 1.1.


Exercise  Ex1.2


Let PX1.2 = (a;*[b;c]) [ ] *[c;d].

Design the corresponding process-graph .


1.7          Additional  Reading


If you wish to read an alternative introduction to processes, formulated in a very friendly, popular style,  I recommend that you look at pages 23-31 of [Hoare85]. This text is the standard  introduction  to a CSP (Communicating Sequential Processes) based analysis of systems. However, there are differences between Hoare’s CSP-based notation and ours, which is LOTOS oriented (see Lecture 4).


Exercise Ex1.3


Consider a vending machine VMCT (see [Hoare85]/p.30) which serves either a chocolate or a toffee on each insertion of a coin. Let Act(VMCT) = {coin,choc,toffee}.

Specify this machine by a suitable behaviour expression:

(a)   assume the customer has the choice between choc and toffee (machine VMCTa).

(b)   the customer has no choice; the choice is up to the machine (machine VMCTb).


1.8          References


[Hoare85]   C.A.R. Hoare, Communicating Sequential Processes, Prentice-Hall, 1985.


1.9          Solutions of Exercises


1.9.1   Exercise Ex1.1



                    a      c            

                   *[b;a]    *[d;c]


The construction of the subgraph for *[b;a] is straightforward:



                                 b ↑a



The subgraph for *[d;c] is constructed similarly.


1.9.2   Exercise Ex1.2



                        a      c

                        *[b;c]   *[d;c]


Now continue as indicated above.


1.9.3   Exercise Ex1.3


VMCTa = *[coin;(choco [ ] toffee)]

VMCTb = *[coin;choco [ ] coin;toffee]