**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

TΔ

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.

**2.5
****Additional ****Reading**

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.*