Chapter 2

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!