Lecture 2

Processes and Trees

In Lecture 1 we introduced processes in a rather informal way. Now we wish to discuss processes again, in a more formal way. We start with the following definition.

2.1  Definition of Process

A process P consists of the following.

(1) A finite or countable set Des(P)  of P-descendants containing P as  element;

(2) A finite set Act(P) of actions or events, not containing the special event ‘i’;

Note. Following LOTOS we use ‘i’ to denote the “non-observable” (internal, hidden) event. It roughly corresponds to ε in automata theory and τ (tau) in CCS. Consequently, Act(P) is also referred to as set of observable actions.

(3) A transition relation Tr(P) , namely a subset of

Des(P) x Act(P)U{i} x Des(P)

Elements of Tr (P) are transitions (of P).

If <Q,y,Q> is a transition , we also write Q[y>Q’. Q’ is a son of Q, and Q is a parent of Q’. The transitive closure of a (binary) relation R is R+.

If Des(P) contains an element without sons, this element is

denoted either \$ or stop.

Note. Informally, \$ indicates a “successful” termination, whereas ‘stop’ indicates “deadlock”. These concepts will be formalized in the sequel.

Furthermore, the process P satisfies the following requirement:

P( parent+)Q  iff Q is an element of Des(P), i.e., is a P-descendant.

If Q is a P-descendant, we may view Q as a process, where the Q-descendants are defined by {Q’| Q(parent+)Q’} and Tr(Q) is the corresponding restriction of Tr(P).

If Q[y>Q’, we say that y is applicable to Q. If <Q,y,Q> is the only transition outgoing from Q,  we set Q=y;Q’ .  Here ‘;’ is referred to as prefix operator .

In Lecture 1 we introduced the concept of process graph. Such a graph represents a process, as defined above, in the evident way: namely, Des(P) is represented by the set of node labels, and Tr(P) by the labelled arcs of the process graph.

2.2          Process Trees

In Lecture 1 we introduced various process operators, explaining their meaning in an  informal way. We now wish to formally define such process operators, by means of labelled trees. This approach is based on [BB87]. The corresponding algebra of processes will be denoted BLA (Basic-LOTOS oriented Algebra).

Consider a process P as defined above. In what follows it will be convenient to “represent” P by means of a labelled tree specified as follows.

Definition 2.2

Let P be a process  (Definition 2.1) and T a tree with node set V(T), the arcs of which are labelled by elements of Act(T)U{i}, where Act(T)=Act(P).  Let r(T) denote the root of T. If v is a node of T, we denote by T(v) the subtree of T which has v as its root. If <v,y,v> is an arc of T, we also write T(v)[y>T(v’).  The set of arcs of T is denoted Arc(T).

T represents  P iff there exists a function f from V(T) onto Des(P) such that:

(1)      f(r(T))= P;

(2)      T contains a labelled arc <v,y,v> iff < f(v),y,f(v’)> is a transition of P.

(3)      Let f(v)=Q. There exists a 1-1 mapping between the sons of v in T, and the transitions outgoing from Q. Leaves of T are either denoted X and Xi (i>0), or STOP and STOPi.

Note. Leaves denoted X and Xi correspond to \$  and STOP(i) to stop (Definition 2.1).

One easily verifies that the above tree T is uniquely detemined by P (up to a renaming of its nodes). We set T=T(P), and refer to T as process tree representing P.

Example Exa2.1

Consider the process P3 represented by the process graph of Figure 1.3.  The corresponding tree T(P3) is shown below.

b     a     c

X1 ← v ← r → X2

Here f(X1)=f(X2)=\$, f(r)= P3,  f(v)=b;\$ .

2.3          Tree Equivalences

Definition 2.3

Let T1 and T2 be process trees with roots r1 and r2, respectively. The two trees are strongly equivalent iff there exists a relation R between their node sets satisfying the following conditions:

(i)             whenever v1Rv2 and v1[x>v’1 in T1, then there exists a

node v’2 in T2 such that v2[x>v’2 in T2 and v’1Rv’2.

(ii)            whenever v1Rv2 and v2[x>v’2 in T2, then there exists a

node v’1 in T1 such that v1[x>v’1 in T1 and v’1Rv’2.

(iii)          r1Rr2

If this is indeed the case we also say that P1 and P2 are strongly equivalent, where Pi (i=1,2) is a process represented by Ti.

Exa2.2

The two trees shown below are strongly equivalent. The corresponding relation R is easily established.

r                             r

a / \ a                      a |

v1   v2                        v

b|   | b                   b /   \ b

X1  X2                   X3   X4

It follows that a;b;\$ [ ] a;b;\$ = a;(b;\$ [ ] b;\$), where ‘=’ denotes strong equivalence.

Definition 2.4

Let a be some label. An extension of a is any sequence in i*ai*, where i* denotes a finite, possibly empty, sequence of i’s.

Definition 2.5

Let T1 and T2 be process trees and let a be an observable action of one of the processes represented by Ti (i=1,2). Let v[a>> v’ indicate that node v’ is reachable from node v by an extension of a. Then T1 and T2 are observation-equivalent, iff the conditions (i), (ii), and (iii) of Definition 2.3  are satisfied, with [x> everywhere replaced by [a>>.

Furthermore, we require:

(iv)          if <r1,i,v1> is an arc of T1, where r1 is its root, then T1 may be replaced by T(v1), without affecting the conditions (i)-(iv).  Similarly, with respect to T2.

We use ‘==’ to denote observation equivalence of trees as well as processes. We set P==Q iff T(P)==T(Q).

Exa2.3

Consider the following two trees.

T1                         T2

r                            r

a / \ b                     i /  \ b

X1  X2                   v    X3

a |

X4

The above trees are not obs.equivalent  since T1 and T(v) in T2 are not obs. equivalent.

Exa2.4

On the other hand the following two trees are obs.equivalent.

T1                     T2

r1                       r2

a |                       a |

v1                       u1

b |                        i |

X1                       u2

b |

X2

Exa2.5

The following example, made “famous” by R. Milner ([Mil80], [Mil89]), distinguishes between process algebras and the algebra of regular expressions (recall Exercise Ex1.3 !).

r                               r

| a                        a /  \ a

v                          v’1  v’2

b /  \ c                     b |     | c

X1   X2                    X3   X4

The above two trees are not obs. equivalent, since a suitable relation R can not be established. On the other hand, regular expression algebra admits the distributive law

a.(b+c) = a.b + a.c

2.4          Operations on Process Trees

We now define operations on labelled trees. It is easily seen that such operations on process trees again produce process trees. Thus, the following tree operations also define process operations with respect to the processes represented by the process trees involved.

2.4.1      Prefix

Let T be a labelled tree, and y a label not necessarily a label of T. We define the labelled tree y:T as follows:

(1)  Let w be a node not in V(T).

(2)  Add to Arc(T) a new arc <w,y,r>, where r is the root of T.

In the new tree T’=y;T generated we evidently have r(T’) =w.

T’

------

w

|y

Clearly, P=y;Q (see Lecture 1)  iff  T(P)=y;T(Q).

The tree with <r,y,X> as its only arc, is denoted y;X; it represents the process y;\$.

2.4.2   Choice

Consider two trees T1 and T2. The tree T1[ ]T2 is obtained from T1 and T2 by merging their roots into a single root.

Now let T1=T(P1) and T2=T(P2).  Then we set  P=P1 [ ] P2 iff

T(P)=T(P1) [ ] T(P2) .

Assume now that the processes P1 and P2 are given by their process graphs G(P1) and G(P2). We wish to construct a process graph G representing P1[ ]P2, i.e., G=G(P1[ ] P2).

If the start nodes of G(P1) and G(P2) have no incoming arcs, G is obtained by merging the two start nodes into a single start node labelled P.  Otherwise, we apply the following transformation to the graph (graphs) in question.

2.4.3   A  Process Graph Transformation

Consider now a process graph G(P) the start node of which (labelled P) has incoming arcs. This graph may be transformed into a process graph G’(P) without incoming arcs to its start node. The process represented by G’(P) is strongly equivalent to P. The graph G’(P) is constructed as follows.

(1)  split the start node of G(P) into two, labelled by P’ and P”.

(2)  connect all arcs incoming to P in G(P) to P” in G’(P).

(3)  connect all arcs outgoing from P in G(P) to P’ in G’(P) as well as to P” in G’(P).

(4)  consider the node labelled P’ in G’(P) as start node of a    process graph G(P’) .

It is easily verified that the processes P and P’ are strongly equivalent.

Exa2.6

Consider the process PBL represented by the process graph of Figure 1.2. The above construction will produce a process PBL’ which can be specified as follows.

PBL’ = push;on;push;off; PBL

Exa2.7

This example shows that the replacement of ‘a’ by ‘i;a does not necessarily preserve obs. equivalence.

Let P1:=i;a;\$ [ ] b;\$

P2:=a;\$ [ ] b;\$

In view of Exa2.3, P1 and P2 are not obs.equivalent!

Exa2.8

Let P1:= i;a;\$

P2:= a;\$ [ ] i;a;\$

Then P1==P2.

Proof.

The required relation R is easily established.

Exa2.9

Let P1:= a;(b;\$ [ ] i;c;\$)

P2:= a;(b;\$ [ ] i;c;\$) [ ] a;c;\$

Then P1==P2.

Proof.

We leave it to you to establish the required relation R (cf. [Mil89]).

2.4.4    Sequential  Composition

Let T1 be a finite labelled tree (without STOP leaves), and T2 some other tree. The sequential composition T1>>T2 is the tree obtained from T1 by replacing all its terminal nodes (leaves) by T2 (and renaming nodes as required).

2.4.5     Recursion

Let T be a  finite, non-trivial labelled tree, properly terminating (no STOP leaves) .  It can be proven that the following equation

Y=T>>Y

has a unique solution for Y, denoted *T. We also set  *P=Q iff *T(P)=T(Q).

We omit here the details of the proof involved (cf. [Hoare85]/Section 2.8.3).

Note. When specifying *P we usually omit ‘\$’ within the description of P. Also, we write ,e.g., *[a;b] instead of *(a;b;\$). If viewed as tree, *[a;b] stands for *(a;b;X).

Exa2.10

Prove formally the Law 1.1:

[a;b] = a;*[b;a]

Proof.

The corresponding trees are evidently strongly equivalent.

2.5   Laws

Most of the following laws follow easily from the above definitions. We use ‘=’ to denote strong equivalence and ‘==’ for obs. equivalence.

The trivial tree coinciding with its root is denoted \$.

Laws on [ ]

Law 2.1:   T1[ ]T2 = T2 [ ] T1

Law 2.2:   (T1[ ]T2)[ ]T3 = T1[ ](T2[ ]T3)

Law 2.3:   T[ ]T = T

Law 2.4:   T[ ]\$ = T

Law 2.5    T1 = T’1 /\  T2 = T’2 => T1[ ]T2 = T’1 [ ] T’2

Laws on >>

Let T1 and T2 be finite, deadlock-free labelled trees.

Law 2.6: (T1>>T2)>>T3 = T1>>(T2>>T3)

Law 2.7: (T1[ ]T2)>>T3 = (T1>>T3) [ ] (T2>>T3)

i-Laws

Law 2.8: a;i;T == a;T

Law 2.9: T [ ] i;T == i;T

Evidently, all the above laws also apply to processes, with T replaced by P, and Ti by Pi.

There is some similarity between our process algebra BLA (oriented toward Basic LOTOS: see Lecture 4) and the process algebra CCS [Mil89]. In particular, you may learn more about i-laws (corresponding to τ-laws in [Mil89]) by studying [Mil89]/p.62-63.

For a somewhat different approach to a tree algebra based on LOTOS, see [BB87].  However, the main purpose of [BB87] is an introduction to LOTOS.

2.6          References

[BB87]    B.Bolognesi and E.Brinksma, Introduction to the ISO

Specification Language LOTOS, Computer Networks

and ISDN Systems 14 (1987) pp.25-59.

[Mil89]      R.Milner, Communication and Concurrency, Prentice-

Hall, 1989.