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
specification exa[a,b]:exit behaviour
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.
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.
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.
specification exa[a,b]:exit behaviour
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).
The following file pud.lotos illustrates how recursion is dealt with in LOTOS.
specification pud[up,down]:noexit behaviour
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.
We may also use mutual recursion, as illustrated in Section 2.5.
Below is the corresponding LOTOS file pud1.lotos.
specification pud1[up,down]:noexit behaviour
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.
If P and Q are processes, then PQ denotes a process that behaves either like P or like Q (see Section 2.6). To illustrate, consider the following LOTOS-file choice.lotos.
specification choice[a,b]:exit behaviour
(i;a;exit)  (b;exit)
Copy this file and generate the relevant choice.aut file. You should get:
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.
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.
specification lts[a,b,c,d,e,f]:noexit behaviour
a;P1[a,b,c,d,e,f]  d;e;P3[a,b,c,d,e,f]
b;P0[a,b,c,d,e,f]  c;P3[a,b,c,d,e,f[
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.
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” .
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]
[to be completed]