**Lecture 4**

**Basic LOTOS and CADP**

** **

In this lecture we provide an introduction to Basic LOTOS and the
associated toolbox CADP. We assume that you have access to CADP (see [CADP] and
[CADP_FAQ]) and will actively participate in the tutorial steps that follow.

**4.1
Labeled Transition Systems (LTSs) **

** **

In this section we introduce LTSs and show how they are related to
finite state machines as well as to processes.

A *Labeled Transition System*
(LTS)* *is a 4-tuple S= (Q,A,T,q0), where

Q is a finite, nonempty set of states

A is a finite, nonempty set of labels* *(denoting * *actions* *)

T, the transition relation*,* is a subset of QxAxQ

q0 is the initial* *state.

A finite, non-deterministic state machine is defined similarly, but
there A is the set of inputs and outputs. We now point out our way of
describing LTSs. In conformity with CADP (see Lecture 5) we let
Q={0,1,…,k} and q0=0.

We will specify an LTS by listing all elements of its transition
relation. Here are two examples of LTS specifications.

=====
=====

(0,a,1)
(0,a,1)

(1,b,2)
(0,a,2)

=====
(1,b,3)

** LTS 4.1** (2,c,3)

=====

**
LTS 4.2**

** **

The definitions of strong and obs. equivalence also apply to LTSs
in the evident sense, with ‘process’ replaced by ‘state’.

We may also relate LTSs to processes, using a further extension of the
above definition.

Thus, the above LTS 4.1 is strongly equivalent to the process a;b;$. The
states 0,1,2 of LTS 4.1 correspond to the processes a;b;$, b;$, and $,
respectively.

Similarly, the LTS 4.2 is strongly equivalent to the process
a;b;$[]a;c;$. Here, state 3 corresponds to $, state 1 to the process b;$ and
state 2 to the process c;$.

**4.2
**** About CADP (CAESAR/ALDEBARAN Development**

**
Package)**

In the next section you will
learn how to go from BLA descriptions to the corresponding LOTOS
specifications, and how to apply the toolbox CADP to convert such LOTOS
specifications into corresponding LTSs.

**4.3
Getting Started with CADP**

** **

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

__File exa4.1.lotos__

**specification exa4.1[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 process a;b;$. The process is described in the second line of
the file, with ‘$’ replaced by ‘exit’. We name this process now ‘exa4.1’; 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
exa4.1.lotos *

The outcome is a file exa4.1.aut, representing an extended version
of the above LTS 4.1 . File exa4.1.aut is shown below.

** **

__File exa4.1.aut__

**des (0,3,4)**

**(0,A,1)**

**(1,B,2)**

**(2,exit,3)**

This file differs from the LTS 4.1 by the addition of a heading,
and a the transition (2,exit,3). 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 additional transition connects the terminal state of LTS 4.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)
LTS4.1, and not a “deadlock” state.

**4.3
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 exa4.2.lotos__

**specification exa4.2[a,b]:exit
behaviour**

**
i;a;b;exit**

**endspec**

Now use the command

*
caesar –aldebaran exa4.2.lotos*

to obtain the file exa4.2.aut.

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

*
aldebaran –oequ exa4.1.aut exa4.2.aut*

You will get the outcome ‘TRUE’.

On the other hand, if you replace ‘-oequ’ in the
above command 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 exa4.2.aut you will get exa4.1.aut
(with changed state names).

**4.4
Recursion **

Consider the recursive behaviour
specification ** **

**PUD=*[up;down] **

The following file pud.lotos illustrates how such a 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.lotos 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 below.

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

**4.5
Choice **

** **

Below is a LOTOS-file specifying the behaviour of the process
i;a;$[]b;$.

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

**4.6
****Parallel Compositions**

There are some differences between the parallel operators of BLA and
those of Basic LOTOS. Let P and Q be processes where Act(P)=Act(Q). Then ‘||’
means the same in both approaches.

**Exa4.3**

To verify Exa3.1, consider the following two LOTOS-files.

__File exa4_3A.lotos__

specification exa4_3A [a,b]:exit behaviour

a;i;i;b;exit || i;a;i;b;exit

endspec

__File exa4_3B.lotos__

specification exa4_3B[a,b]:exit behaviour

a;b;exit

endspec

Now convert both files into the corresponding aut-files and check for
obs. equivalence.

Similarly, the notation |[L]| has the same meaning in the two
approaches.

**Exa4.4**

Consider the following two LOTOS-files.

__File exa4_4A.lotos__

specification exa4_4A[a,b,c]:exit behaviour

a;c;exit |[c]| b;c;exit

endspec

__File exa4_4B.lotos__

specification exa4_4B[a,b,c]:exit behaviour

a;b;c;exit [ ]
b;a;c;exit

endspec

Proceed similarly to Exa4.3 to prove that

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

where ‘=’ denotes strong equivalence.

However, if P and Q are processes and L is the intersection of Act(P)
and Act(Q), we may write P||Q instead of P|[L]|Q in BLA, but **not** in
LOTOS!

Furthermore, if L=Ф (the empty set) we write P|||Q instead of
P|[L]|Q in both BLA and LOTOS.

**Exa4.5**

Here we wish to use CADP to verify Exa3.4.

First, we formulate the following LOTOS-file.

__File exa4_5.lotos__

specification exa4_5[a,b,c,d]:exit behaviour

a;(b;d;exit [ ] c;exit) ||
a;(b;c;exit [ ] d;exit)

endspec

Next, we convert the above file into its aut-file and get:

__File exa4_5.aut__

des(0,2,3)

(0,A,1)

(1,B,2)

To make sure that state 2 is indeed a deadlock state, we issue the
command:

* aldebaran
–dead exa4_5.aut*

The outcome is:

*2 is a
deadlock state*

* *

**4.7 Exercises**

**Exercise Ex4.1**

Let **PX4a =
*[a;b] [ ] *[c]**

** PX4b = *[a;i;b] [ ] *[c]**

(1) Apply the
relevant definition to show that the two processes are obs. equivalent.

(2) Use CADP to
confirm the preceding statement.

**Exercise Ex4.2**

Let **P==P’ **and
**Q==Q’**, where ‘==’ denotes obs. equivalence. Does it follow that **P[ ]
Q == P’[ ]Q’ **? Prove or show a counter-example.

**Exercise Ex4.3**

Use CADP to
verify:

a;i;b;$
|| a;i;b;$ = a;i;i;b;$

**Exercise
Ex4.4**

Use CADP to
verify Prop. 3.1

**4.8
**** Further ****Reading**

For a further inside into Basic LOTOS, I presently recommend the
relevant part of the excellent tutorial [LFH92]. You will find further
references to various aspects of LOTOS in the following lectures.

**4.9
****References**

[LFH92] L.Logrippo, M.Faci,
M.Haj-Hussein, An Introduction to

LOTOS: Learning by
Examples,

*Computer
Networks and ISDN Systems 23*, 1992,

pp. 325-342.

**4.10
****Solutions of Exercises**

**4.10.1
****Exercise Ex4.1**

(1) Both processes have the same set of
(immediately) applicable

** **actions, namely {a,c}. If **c **is applied to each
process, we get

the same outcome *[c]. If **a **is
applied, we get *[b;a] from the

first process, and *[i;b;a] from the
second process. Those two

sub-processes are obs. equivalent, in
view of the relevant

definition. Hence the two processes in
question are indeed

obs. equivalent

(2) Here is the file PX4b.lotos:

specification PX4b[a,b,c]:noexit behaviour

PX4b[a,b,c]

where

process PX4b[a,b,c]:noexit:=

cy3[a,i,b] [] cy1[c]

endproc

process
cy3[a,b,c]:noexit:=

a;b;c;cy3[a,b,c]

endproc

process
cy1[a]:noexit:=

a;cy1[a]

endproc

endspec

Now proceed as follows.

(i)
prepare a file PX2a.lotos, similarly to the above.

(ii)
convert both lotos-files into the corresponding aut-

files.

(iii) show that the two aut-files are obs.
equivalent.

**Exercise Ex4.2**

Let **PX2c =
i;*[a;b] [ ] *[c]**

Here we have **i;*[a;b]
== *[a;b] **, but

**PX2c ==
PX2a **does
not hold!