Chapter 18

Comparing Basic LOTOS and Petri Nets

18.1 Growing Trees from Petri Nets

In Chapter 12 you learned how to grow trees from behaviour expressions. In this section we are about to grow trees from Petri nets and then relate these two types of trees.

Let LPN be a safe labeled Petri net (PN,Σ,lb) (see Section 17.2), and let M(LPN) be the set of all markings reachable from the initial marking M0 of LPN. With LPN we associate the labeled tree T(LPN) defined as follows.

(1) The nodes of the tree represent the set M(LPN)

(2) The root of the tree represents the initial marking M0

(3) There exists an arc from node n1 to node n2 labeled xεΣU{λ}, iff M1[t>M2, where Mi is the marking represented by ni and lb(t)=x.

18.2 Equivalences of Trees

The definitions 12.1 and 12.2 are evidently applicable to net trees, as defined above, provided a λ-label of the net tree is replaced by ‘i’. This approach also enables us to relate (safe, labeled) Petri nets to Basic LOTOS expressions.

To illustrate, let us grow trees on the net shown in Fig. 16.1 and the Blot expression X1.blot = a;c;$ ||b;c;$. Below is the relevant net tree.

M0 = {1,3}

a ↓ ↓b

{2,3} {1,4}

b ↓ ↓a

{2,4} {2,4}

c ↓ ↓c

{ } { }

We may get the corresponding blot-tree by replacing the above markings as shown below.

M0 → X1.blot

{2,3} → c;$||b;c;$

{1,4} → a;c;$||c;$

{2,4} → c;$

{ } → $

This shows that X1.blot and the net X1.net (Fig. 16.1) are strongly equivalent.

18.3 A Simple Net Algebra

In this section we introduce some algebraic operations on nets, modeled along the Basic LOTOS operators introduced in Chapter 3.

18.3.1The Prefix Operator

Let LPN=(PN,Σ,lb) be a safe labeled net, and let P(M0) be the set of places marked initially. Let x be a label not in Σ. Then we define the labeled net x;LPN as follows.

Let PN=(P,T,F,M). Assume p0 is a place not in P.

Then the set of places of x;LPN equals PU{p0}.

The set of transitions of x;LPN is TU{t0}, where t0 is a new transition not in T, labeled x.

Add an arc from p0 to t0. Add arcs from t0 to every place in P(M0).

Put a token in p0 and remove all tokens from the places in P(M0).

We shall refer to the place p0 as the initial place of x;LPN.

The above net operator evidently mirrors the prefix operator of Basic LOTOS. Namely, let Proc be a process strongly equivalent to the net LPN (with λ-labels replaced by ‘i’). Then x;Proc and x;LPN are obviously strongly equivalent.

The above net operator is illustrated in Fig. 18.1.

{insert Fig. 18.1}

Fig. 18.1 (a) net LPN1 (b) net x;LPN1

The above net LPN1 is clearly strongly equivalent to Proc1=a;$|||b;$. Namely, the tree specifying the behaviour of LPN1 is shown below (Fig. 18.2).

M0={p1,p2}

a ↓ ↓b

{p2} {p1}

b↓ ↓a

{ } { }

Fig. 18.2

The tree for Proc1 is obtained by the relabeling shown below.

M0 → Proc1

{p1} → a;$

{p2} → b;$

{ } → $

It follows that the trees for x;Proc1 and x;LPN1 are again isomorphic, and consequently, that x;Proc1 and x;LPN1 are strongly equivalent.

18.3.2The Choice Operator

The net choice operator is intended to mirror the choice operator of Basic LOTOS.

Thus, let x1;LPN1,…, x.k;LPNk be safe, labeled Petri nets, constructed as explained in the preceding subsection. We define their choice x1;LPN1 [ ] … [ ] xk;LPNk as the net obtained by merging all the initial places of the k nets into a single marked place p0.

One easily verifies that this construct indeed mirrors the choice operator of Basic LOTOS.

Exercise Ex18.1

Provide a detailed proof that the net choice operator indeed mirrors the Basic LOTOS operator.

18.3.3The Star Operator

Prior to defining the star operator for nets, we introduce the concept of Δ-net. Such a net is a safe labeled net with a unique start node (a node without incoming arcs), which is a marked place. All other places are not marked. Furthermore all terminal nodes (i.e., nodes without outgoing arcs) are transitions.

Given a Δ-net LPN1, its star closure *LPN1 is obtained by connecting each terminal transition to the start place of LPN1.

If *Proc1 is defined, and LPN1 and Proc1 are strongly equivalent, then so are *LPN1 and *Proc1. On the other hand, if Proc1* is defined, *LPN1 and Proc1* are not necessarily strongly equivalent, but they are at least obs. equivalent.

Exercise Ex18.2

Provide a detailed proof of the above statements related to the various star constructs.

18.4 Example

Let a;{} denote the marked net shown below.

{insert Fig.}

Let XOR.net = *(a;z;{} [ ] b;z;{}).

Similarly, let XOR.lot be defined by the Blot expression

XOR.lot=*(a;z;$ [ ] b;z;$)

In view of the preceding considerations (including the relevant exercises) we conclude that XOR.net and XOR.lot are strongly equivalent.

However, we may wish to prove directly that XOR.net and XOR.lot

are strongly equivalent, using Petrify and CADP.

To achieve this goal, we may proceed as follows.

(1) we convert the above specification of XOR.net into the Petrify-description listed below.

File xor.net

.model xor.net

.inputs a b

.outputs z

.graph

p0 a

a z

p0 b

b z/1

# so far we have specified the net (a;z;{} [ ] b;z;{})

# next we provide recursion

z p0

z/1 p0

.marking {p0}

.end

(2) next we convert xor.net into a state-graph xor.sg, by means of the command

write_sg xor.net -o xor.sg

The outcome is the following file xor.sg:

xor.sg

.model xor.sg

.inputs a b

.outputs z

.state graph

s0 a s1

s0 b s2

s1 z s0

s2 z s0

.marking {s0}

.end

(3) we now convert xor.lot into the corresponding lotos-program, as shown below.

File xor.lotos

specification xor[a,b,z]: noexit behaviour

xor[a,b,z]

where

process xor[a,b,z]:noexit:=

a;z;xor[a,b,z] [] b;z;xor[a,b,z]

endproc

endspec

(4) next we produce xor.aut by means of the command

caesar –aldebaran xor.lotos

the outcome is the following file xor.aut

File xor.aut

des (0,4,3)

(0,A,1)

(0,B,2)

(1,Z,0)

(2,Z,0)

Thus, xor.aut and xor.sg are isomorphic, and hence xor.lot and xor.net are strongly equivalent.

18.5 Net Specifications of Modules

Here are some further algebraic net specifications of modules (see Chapter 7), together with their Blot specifications.

C-Element

cel.lot = *[a;b;z;$ [ ] b;a;z;$]

cel.net = *(a;b;z;{} [ ] b;a;z;{})

TOGGLE

tog.lot = *[a;y;a;z]

tog.net = *(a;y;a;z)

18.6 Exercises

Exercise Ex18.3

Use CADP and Petrify to show that cel.lot and cel.net are indeed strongly equivalent.

Exercise Ex18.4

Same as before, with respect to TOGGLE.

{to be continued}

18.7 References

{to be completed}

18.8 Solutions

{to be completed}