** **

** **

In this lecture you will learn how to go from
Blot descriptions to the corresponding LOTOS specifications, and how to apply
the toolbox CADP to convert such LOTOS specifications into corresponding LTSs.

**At this
stage it is important that you get access to CADP, so that you can actively
participate in the exercises we are about to discuss. Once you are enrolled in
this Course, you will have easy access to** **CADP****.**

Throughout this Course we will mainly be
concerned with Basic LOTOS, which deals with control aspects only, disregarding
any data-processing.

We now assume that
you have access to CADP and are thus in a position to actively follow
our instructions.

**3.1
****Getting Started with CADP**

** **

To get started with CADP, open a dedicated directory,
and into this directory copy the following LOTOS file exa3.1.lotos

__File exa3.1.lotos__

specification
exa[a,b]:exit behaviour

a;b;exit

endspec

If two processes are
strongly equivalent, we say that they have the same **behaviour.** A LOTOS program, such as the above,
specifies a behaviour by means of a representative process.

The above LOTOS-file specifies the behaviour of the
Blot process a;b;$ (see Fig. 2.1). The process is described in the second line
of the file, with ‘$’ replaced by ‘exit’. We name this process now ‘exa’; this
name appears in the heading, together with the (observable) actions involved.
The term ‘exit’ in the heading indicates that the process is terminating (no
recursion is involved).

Now issue the following
CADP command:

caesar -aldebaran exa3.1.lotos

The
outcome is a file exa3.1.aut, representing an extended version of the above LTS
2.1 , which is strongly equivalent to the process specified by exa3.1.lotos. File exa3.1.aut is shown
below.

__File exa3.1.aut__

des (0,3,4)

(0,A,1)

(1,B,2)

(2,exit,3)

This file differs from
the LTS 2.1 by the addition of a
heading, and a transition labeled ‘exit’. The heading ‘des (0,3,4)’ indicates
that the initial state is 0, the number of the following lines is 3, and the
number of states is 4. The transition labeled ‘exit’ connects the terminal
state of LTS 2.1 (state 2) to a new terminal state (state 3). This may be
viewed as an indication that state 2 is a proper terminal state of the basic
(non-augmented) LTS 2.1, and not a “deadlock” state. We will return to this
distinction later on.

**3.2
****Equivalences **

** **

You may use Aldebaran to check strong and observation
equivalences. To do so, issue the command ‘aldebaran’ followed by

-bequ to compare two LTSs with respect to strong equivalence

-oequ to compare two LTSs with respect to obs.
equivalence.

To illustrate, copy the following file into your
dedicated directory.

__File exa3.2.lotos__

specification exa[a,b]:exit behaviour

i;a;b;exit

endspec

Now use the command

caesar –aldebaran exa3.2.lotos

to obtain the file exa3.2.aut.

You may now verify that the processes specified in
files exa9.1.lotos and exa9.2.lotos are obs. equivalent by using the command

aldebaran –oequ exa3.1.aut
exa3.2.aut

You will get the outcome ‘TRUE’.

On the other hand, if you
replace in the above command
‘-oequ’ by
‘-bequ’, you will get an explanation, why the two processes are not strongly
equivalent.

You may also use Aldebaran to reduce a given LTS modulo
observation equivalence; i.e., to get a minimal LTS, obs. equivalent to the
original one. The relevant command is:

aldebaran –omin
file.aut

E.g., if you apply this command to exa3.2.aut you will get exa3.1.aut (with changed
state names).

**3.3
****Recursion **

** **

The following file pud.lotos illustrates how
recursion is dealt with in LOTOS.

__File pud.lotos__

specification pud[up,down]:noexit behaviour

P[up,down]

where

process P[up,down]:noexit:=

up;down;P[up,down]

endproc

endspec

Thus, when specifying the behaviour of pud[up,down],
the relevant recursive process (here denoted P[up,down]) has to be suitably
defined. If we use CADP, to convert pud[up,down] into an LTS , the outcome is
shown below.

__File pud.aut__

des(0,2,2)

(0,UP,1)

(1,DOWN,0)

We may also use mutual recursion, as illustrated in
Section 2.5.

Below is the corresponding LOTOS file pud1.lotos.

__File pud1.lotos__

specification pud1[up,down]:noexit behaviour

Pup[up,down[

where

process Pup[up,down]:noexit:=

up;Pdown[up,down]

endproc

process Pdown[up,down]:noexit:=

down;Pup[up,dow]

endproc

endspec

We can now prove that processes pud and pud1 have
equal behaviour. Namely, we convert pud1 into the corresponding LTS, which
turns out to be equal to pud.aut.

**3.4
****Choice **

** **

If P and Q are processes, then P[]Q denotes a process
that behaves either like P or like Q (see Section 2.6). To illustrate, consider
the following LOTOS-file choice.lotos.

__File choice.lotos__

specification choice[a,b]:exit behaviour

(i;a;exit) [] (b;exit)

endspec

Copy this file and generate the relevant choice.aut
file. You should get:

__File choice.aut__

des (0,4,4)

(0,i,1)

(1,A,2)

(0,B,2)

(2,exit,3)

The last line of this file again augments the basic
LTS, as explained in Section 3.1.

**3.5
****From LTS to LOTOS**

** **

It is rather easy to convert a given LTS into an
obs.equivalent process. To illustrate, consider the LTS shown in the file
lts.aut below.

__File lts.aut__

des (0,6,4)

(0,A,1)

(1,B,0)

(1,C,3)

(0,D,2)

(2,E,3)

(3,F,0)

To obtain an obs.equivalent process we associate a
process with each state, which has more than one incoming transition and/or
more than one outgoing transition. The corresponding lotos.file is shown below.

__File lts.lotos__

specification lts[a,b,c,d,e,f]:noexit behaviour

P0[a,b,c,d,e,f[

where

process P0[a,b,c,d,e,f]:noexit:=

a;P1[a,b,c,d,e,f] [] d;e;P3[a,b,c,d,e,f]

endproc

process
P1[a,b,c,d,e,f]:noexit:=

b;P0[a,b,c,d,e,f] [] c;P3[a,b,c,d,e,f[

endproc

process P3[a,b,c,d,e,f]:noexit:=

f;P0[a,b,c,d,e,f[

endproc

endspec

Here, process Pj represents state ‘j’ of the above
LTS.

**I suggest that you now verify that the
above process P0 and the LTS specified in lts.aut are strongly equivalent by
converting file lts.lotos into an aut-file. I assume that you can do this
without any problems.**

**3.6
****Parallel Operators**

** **

LOTOS provides a variety of facilities to represent
processes which operate concurrently.

** The
Interleaving Operator |||**

** **

If P and Q are processes, P|||Q represents their
parallel execution without any “synchronization”, i.e., each process proceeds
independently of the other. Using Blot, we have ,e.g.,

a;b;$
||| c;$ ≡ c;a;b;$ [] a;(c;b;$ [] b;c;$)

where ‘≡’ denotes strong equivalence.

** ****The Selective Composition Operator |[…]|**

** **

If A1,…,An are some observable actions common to
processes P and Q, then
P|[A1,…,An]|Q
represents the parallel execution of P and Q, provided they synchronize
on (perform simultaneously) the listed actions A1,…,An. Using Blot, we have,
e.g.,

a;b;c;$
|[b]| d;b;$ ≡ a;d;b;c;$ [] d;a;b;c;$

Formally, P|[L]|Q, where L is a set of observable
actions common to P and Q, may be
defined as follows.

(1) If P[a>P’ and ‘a’ is not in L then P|[L]|Q
[a>P’|[L]|Q

(2) If Q[b>Q’ and ‘b’ is not in L then P|[L]|Q [b> P|[L]|Q’

(3) If P[a>P’ , Q[a>Q’, and ‘a’ is in L then P|[L]|Q [a> P’|[L]|Q’

** ****The Full Synchronization Operator ||**

** **

Let P and Q be processes which have all their
observable actions in common. Let this common set of actions be L. Then

P||Q = P|[L]|Q .

The operator ‘||’ is referred to as the full synchronization operator. Thus, the composite process P||Q requires that
processes P and Q synchronize on all their observable actions, but not on ‘i’.
It might be possible that this cooperation of P and Q stops at some state,
before both processes have completed their tasks. Such a state is referred to
as deadlock*. *In Blot
we will use ‘stop’ to refer to such a deadlock state.

Let us now look at illustrating examples, formulated
in Blot.

__Example Syn1__ a;i;i;b;$ || i;a;i;b;$ == a;b;$

Here, ‘==’
denotes obs. equivalence. **Note that the two component**
**processes do not
synchronize on ‘i’.**

** **

__Example Syn2__ Let syn2 = a;b;$ || a;b;a;$ .

This process will encounter a deadlock state, after
performing the sequence a;b. Using Blot, we may state that the process
syn2 equals a;b;stop.

The corresponding aut-file is shown below.

__File syn2.aut__

des (0,2,3)

(0,A,1)

(1,B,2)

As compared with file exa3.1.aut (Section 3.1) no
transition labeled ‘exit’ appears. This is an indication that state 2 is now a
deadlock state. You may confirm this by issuing the command:

aldebaran –dead syn2.aut

The outcome is the statement:

“state 2 is a deadlock
state” .

**3.7
****Hiding**

** **

The hiding facility of LOTOS allows us to transform
some observable actions of a process into unobservable ones. This facility will
be illustrated in the next lecture.

**3.8
****Solved Exercises**

** **

** **[to be completed]

** **

**3.9
****Additional Exercises**

** **

** **[to be completed]

** **

**3.10
****References**

** **

[to be completed]