搜档网
当前位置:搜档网 › Modular Analysis of Petri Nets

Modular Analysis of Petri Nets

Modular Analysis of Petri Nets
Modular Analysis of Petri Nets

This paper shows how two of the most important analysis methods for Petri nets can be performed in a modular way.We illustrate our techniques by means of modular Place/Transitions nets(modular PT-nets)in which the individual modules interact via shared places and shared transitions.For place invariants we show that it is possible to construct invariants of the total modular PT-net from invariants of the individual modules.For state spaces,we show that it is possible to decide behavioural properties of the modular PT-net from state spaces of the individual modules plus a synchronization graph,without unfolding to the ordinary state space.The generalization of our techniques to high-level Petri nets is rather straightforward.

Received November6,1998;revised April13,2000

T HE C OMPUTER J OURNAL,V ol.43,No.3,2000

FIGURE1.Example of the resource allocation system. means that properties of a modular PT-net can be proved by means of formal analysis of the individual modules.

The resource allocation example has a set of processes which share a common pool of resources.There are two different kinds of processes,called p-processes and q-processes,and three different kinds of resources: r-resources,s-resources and t-resources.Each process is cyclic and during the individual parts of its cycle,the process needs to have exclusive access to a varying amount of the resources.The p-processes can be in four different states, while q-processes can be in?ve different states.In the initial state there are two p-processes and three q-processes plus one r-resource,three s-resources and two t-resources. The PT-net is presented in Figure1.It is so small that we would not decompose it in practice,but it can still be used to introduce the basic concepts of modular PT-nets.A?rst possibility to model this system in a modular way consists in modelling the p-processes and the q-processes separately. This leads to two modules,as shown in Figure2,each of them describing the interaction between processes of one kind and the resources.The modules are composed by fusion of the two shared resource places,i.e.the two places labelled with S are fused and likewise for the two places labelled with T.In Figure2the places to be fused together have the same name.The sets of places to be fused together are called place fusion sets.In a practical modelling tool we would need more elaborated techniques to identify members of a given fusion set,but this is not our purpose here.

You can view all places of a place fusion set as being representatives of the same underlying place.This means that they share the same marking:when a token is added to a place which belongs to a place fusion set,all places of the place fusion set will have the same token added.When a token is removed from a place which belongs to a place fusion set,all places of the place fusion set will have the same token removed.In addition,the fusion of the resource

FIGURE2.Modular PT-net with two modules and two place fusion sets with two members each.

places,of the same kind,ensures that the modular PT-net of Figure2has exactly the same behaviour as the PT-net of Figure1.All places in a place fusion set have identical initial markings.

Another way of modelling the resource allocation system is to separate the cycle of p-processes,that of q-processes and the use of resources,as shown in Figure3.The three modules share transitions,corresponding to synchronous actions.Transitions having the same names belong to the same fusion set.This means that we have nine transition fusion sets with two members each.Each transition of a transition fusion set describes a part of a more complex action and all parts must occur simultaneously,as one indivisible action.We say that a transition fusion set is enabled if all the transitions in the fusion set are enabled. The change produced by the occurrence of a transition fusion set is the sum of changes produced by all the transitions of the fusion set.

A transition can describe an action which is a basic part of a number of independent actions.This means that a transition can be a member of several transition fusion sets.Since the behaviour,in the resources module,of the three transitions T3p,T4p and T4q is identical,we could include only one of the three transitions and have it as a member of three transition fusion sets.If our main concern was guidelines for modelling we would have done this,but Figure3corresponds to a straightforward separation of the original PT-net.

The modular PT-net of Figure3has exactly the same behaviour as the PT-net in Figure 1.Each transition fusion set of the modular PT-net corresponds to exactly one transition of the PT-net.

We have presented two examples of modular PT-nets having the same behaviour.The?rst one was an example of modules related by place fusion while the second used

FIGURE3.Modular PT-net with three modules and nine transition fusion sets with two members each.

transition fusion.In general,both place fusion and transition fusion can coexist within a modular PT-net.In this paper we do not consider the problem of identifying place and transition fusions sets.We suppose that the model is already designed in a modular way.However,one should keep in mind that the choice of these sets has an in?uence on the performance of modular analysis.

In Section5we give formal de?nitions of a modular PT-net and of its equivalent PT-net.In the next section we present a modular approach of place invariants calculus.

3.PLACE INV ARIANTS OF MODULAR PT-NETS All analysis methods extract information about the prop-erties of a PT-net in a condensed way.Place invariants express invariant relations on the markings of places.A weight(positive or negative integer)is attached to the places. It speci?es the information we want to extract from the markings of a place.A weight function(vector of weights associated with places)determines a place invariant if the sum of the weighted markings of places is constant for all reachable markings.It is often the case that some place invariant ignores the marking of some places.This is done by assigning weight zero to the places which should be ignored.

3.1.Place invariants of the PT-net

For the example of Figure1we?nd several place invariants.One of the place invariants shows the cycle of the q-processes:the weight of places Aq,Bq,Cq,Dq, and Eq is one and the weight of all other places is zero. We can show that the sum of the weighted markings is constant for all reachable markings.This means that the set of q-processes does not change,only the location of the q-processes changes during their cycle.Instead of checking all reachable markings,we can also check that the weighted sum of tokens consumed by each transition is equal to the weighted sum of tokens produced.We say that a set of weights having this property de?nes a place?ow.It can be proved that the place?ow property is suf?cient to ensure that the weight function determines a place invariant.

In our notation of weight functions,places having a zero weight are simply left out and we use the names of the places to refer to their markings,e.g.we write Bp instead of M(Bp).For the example in Figure1we have?ve linearly independent place invariants:

W1:Bp+Cp+Dp+Ep=2,

W2:Aq+Bq+Cq+Dq+Eq=3,

W3:R+Bq+Cq=1,

W4:S+Bq

+2×(Cp+Dp+Ep+Cq+Dq+Eq)=3, W5:T+Dp+Eq+2×Ep=2.

All of the above place invariants can be interpreted in terms of the PT-net:W1shows that all the p-processes are in one of the states represented by Bp,Cp,Dp or Ep;and W3shows that the r-resources are either free,i.e.in state R,or occupied by a q-process in state Bq or Cq.We can construct other place invariants,but they can also be expressed as linear combinations of the?ve invariants W1to https://www.sodocs.net/doc/282130308.html,ing the ?ve place invariants above,it is straightforward to prove the deadlock-freeness and similar behavioural properties of the system.

3.2.Place invariants of the modular PT-net with place

sharing

In Figure2,we have two modules,one for the p-processes and one for the q-processes.The two modules are related through two place fusion sets,i.e.through the s-resources and t-resources.For the p-processes,we have three place invariants:

W p1:Bp+Cp+Dp+Ep=2,

W p2:S+2×(Cp+Dp+Ep)=3,

W p3:T+Dp+2×Ep=2.

For the q-processes,we have four place invariants:

W q1:Aq+Bq+Cq+Dq+Eq=3,

W q2:R+Bq+Cq=1,

W q3:S+Bq+2×(Cq+Dq+Eq)=3,

W q4:T+Eq=2.

We ask the question:is it possible to construct place invariants of the total system from the place invariants of the individual modules?

The place invariants W p1,W q1and W q2do not include any places which are shared,so W p1,W q1and W q2are place invariants of the total system,independent of the other modules in the modular PT-net.The rest of the place invariants have non-zero weights for some of the shared

places.In this situation we can only combine the place invariants if the weight functions assign the same weight to the shared places.This means that we can combine W p2and W q3,because they both have weight one for S and weight zero for T.Analogously,we can combine W p3and W q4 because they both have weight one for T and weight zero for S.From the place invariants of the individual modules we deduce the following place invariants of the modular PT-net:

W p1:Bp+Cp+Dp+Ep=2

W q1:Aq+Bq+Cq+Dq+Eq=3

W q2:R+Bq+Cq=1

W p2+W q3:2×(Cp+Dp+Ep+Cq+Dq+Eq)

+S+Bq=3

W p3+W q4:T+Dp+Eq+2×Ep=2.

These?ve place invariants correspond to linearly indepen-dent place invariants of the equivalent PT-net.

From the example above we see that a set of place invariants,one for each module,can be combined into a place invariant of the full system if they have the same weights for places which are shared.This is not true in the general case,but if we restrict ourselves to combining place ?ows it is a valid statement.This will be detailed in the formal de?nition of invariants,see Section6.If the sets of weights do not match,in the sense described above,we may sometimes obtain a matching by using a linear combination of the weights in the invariants.

3.3.Place invariants of the modular PT-net with

transition sharing

For the example shown in Figure3we have three modules, one for the p-processes,one for the q-processes and one for the resources.The three modules are related through transition fusion for each pair composed of a transition in the p-processes or q-processes and the corresponding transition in the resource module.If we view the modules independently of their context we can?nd a set of place invariants of the individual modules.For the p-processes, we have one place invariant:

W p:Bp+Cp+Dp+Ep=2,

for the q-processes,we have one place invariant:

W q:Aq+Bq+Cq+Dq+Eq=3,

and the resource sharing module has only the trivial null place invariant.We ask:is it possible to construct place invariants of the total system from the place invariants of the modules?

In this case we have no shared places and this means that W p and W q are both invariants of the entire system. However,it should be obvious that we cannot construct all the place invariants from those of the individual modules. The problem is that we demand too much from the weight functions.We demand that each transition leaves the

FIGURE4.Two modules sharing a transition. invariant unchanged,while it would be suf?cient to require that each transition fusion set does this.In order to relax the conditions of the weight functions for the modules,we introduce the notion of?ow preservation.We say that a transition is?ow preserving if and only if it preserves the invariant.Then we are able to check that the non-fused transitions are?ow preserving for each module; and,also,that transition fusion sets are?ow preserving across modules,i.e.that the transitions together preserve the invariant.

The above examples allowed us to show the intuition behind modular PT-nets and their analysis by means of place invariants.In Section6we formalize the notion of place invariants and place?ows for modular PT-nets.

In the next section we present a modular approach to state spaces construction,which is the second main analysis method for PT-nets.

4.MODULAR STATE SPACES

In this section we introduce the basic ideas of modular state spaces.The main reason for working with modular state spaces is to alleviate the state space explosion problem.The idea is to generate a state space for each module and the information necessary to capture the interaction between modules,and in this way avoid the construction of the full state space.It is important that modular state spaces allow us to prove PT-net properties directly,i.e.without unfolding to the equivalent ordinary state space.Here,we will?rst consider modular PT-nets with fused transitions only.For that purpose we use another example which contains non-shared transitions,thus being more relevant.Then we will show how the problem can be solved for a modular PT-net with place fusion only.

4.1.Modular state spaces with transitions sharing

In this section,we concentrate on PT-nets composed by transition fusion only.As we will see later,it is theoretically easy to generate the state spaces of the individual modules and to compose these into the state space of the entire system.However,practical use is harder:a module can have an in?nite state space while the full state space is?nite,e.g. for the modules of Figure4composed by the fusion of the two grey transitions t.

To avoid handling in?nite state spaces,we would like to obtain an ef?cient construction of state spaces of modules,

FIGURE 5.An example of two communicating processes.

FIGURE 6.After the ?rst step of the modular state space

generation.

knowing that their behaviour is restricted by the behaviour of the other modules.Only the reachable parts of the state space should be constructed.Hence,our method is a balance between full reachability graph generation and on-the-?y veri?cation.

A modular state space is composed of one local state space per module and a synchronization graph which captures the communications.A local state space only contains local information,i.e.the sub-graphs representing all reachable markings obtained by occurrences of local transitions only.The markings are restricted to the places of the module.The synchronization graph provides information on the state space of the overall system and the occurrences of fused transitions.

The construction of a modular state space is similar to that of the

standard state space except that:?

the construction of local state spaces using

only transitions local to modules can be performed in parallel;

?

the construction of a modular state space requires one to keep track of the occurrence of shared transitions and to synchronize the modules using this information.

We use the example of Figure 5to introduce the algorithm for constructing modular state spaces.This is a toy example,but it models a behaviour which resembles that of a typical real system as concerns the ratio between local and shared

FIGURE 7.After the second step of the modular state space generation.

FIGURE 8.After the third step of the modular state space

generation.

actions.The system consists of two modules,called module A and module B,each having a behaviour consisting of a start-up phase,a main loop and a termination phase.The main loop can perform local actions and it can synchronize with the other module,the synchronization is achieved by a transition fusion set consisting of the two transitions labelled Sync .

In the rest of this section we construct the corresponding modular state space.In Figures 6–9,the sets of nodes in dashed boxes are strongly connected components (SCCs),e.g.in Figure 6,A2={a2,a3}.We conclude the example with a comparison to the ordinary state space.

In the ?rst step,we construct graphs containing all locally reachable states of each module.In the example the inscription a1speci?es that the place a1is marked by a token and all other places of module A are unmarked.We also construct the ?rst node of the synchronization graph,corresponding to the initial state.It is labelled by the set of SCCs of the modules to which the restriction of the initial state belongs;but it also represents the set of all reachable markings from the initial marking by occurrences of local transitions only.The result of this ?rst step is shown in Figure 6.

The result of the second step is presented in Figure 7.From the state spaces of the modules we ?nd reachable states which enable fused transitions.The combination of the states a2and b2enables the fused transition Sync leading to new states a4and b4.To the state space of module A we need to add a4,and all markings reachable from a4by occurrences of local transitions;and a similar construction

FIGURE 9.The ordinary state space.

is applied to module B and state b4.Note that the state spaces of the modules,obtained by this construction,are not necessarily connected graphs.Finally,we add the arc corresponding to Sync to the synchronization graph.The arc is labelled by the start marking,the occurring transition and the marking obtained.It connects two nodes which represent the SCCs of the two involved markings.

The third step (Figure 8)is similar to the second step.We inspect the state space of the local modules starting from A3and B3to ?nd reachable states which enable fused transitions,and since a2and b2are locally reachable from A3and B3,we have to add the arc corresponding to Sync .As no new nodes can be added to the local state spaces,we know that they are now complete.

If we compare the ordinary state space of the whole system,illustrated in Figure 9,with the modular state space,we observe that the modular state space is smaller than the ordinary one.The modular state space contains a total of 12nodes and 12

arcs,while the ordinary state space contains

21nodes and 37arcs.Hence,the memory necessary to store the state space is smaller.In Section 9.3,we discuss the size of the modular state space in general.

To construct a modular state space,it is necessary to calculate the SCCs.This is not the case when building an ordinary state space.However the SCCs are needed in order to

determine net properties,thus computing them on-the-?y when building the modular state space is not a waste of time.4.2.Modular state spaces—places sharing

The composition of state space graphs is more complex when sharing places rather than transitions.This can be seen in the example of Figure 10,where the grey place p2,initially empty,is the shared one.In this case,it is ensured

FIGURE 10.Two modules each with ?nite graphs,but a modular PT-net with in?nite graph.

FIGURE 11.A modular PT-net with transition fusion only.

that if at least one of the modules has an in?nite state space graph,the modular PT-net also has an in?nite state space graph.However,it is impossible to tell anything about the state space graph of the modular PT-net if those of the modules are ?nite.This is due to the fact that a module can provide enough tokens in a place fusion set to allow some transitions,in another module,to be enabled;and then this second module can provide some more tokens for the ?rst one and so on.

From a practical point of view it is important to be able to handle systems which use place fusion,since the kinds of Petri nets used in practical applications often rely on this.We de?ne a transformation from a modular PT-net using place fusion to a modular PT-net using only transition https://www.sodocs.net/doc/282130308.html,rmally this is done by collecting each place fusion set in a new module and then splitting the input and output transitions,in order to obtain a transition fusion set for each input and output transition of the place fusion set.Figure 11shows how the system of Figure 10can be translated into a behaviourally equivalent modular PT-net using transition fusion only.

The formal de?nition of the translation and the proof that the behaviour is preserved are not included in this paper.They contain a number of technical details which are of little importance here.

In this section we have presented a construction of modular state spaces.It is quite compact compared to the ordinary state space.It has independent parts which can be computed in parallel.In sections 7and 8we formalize the concepts presented here,and show the details of how to prove PT-net properties directly from the modular state space,i.e.without unfolding to the equivalent ordinary state space.

5.FORMAL DEFINITION OF MODULAR PT-NETS We will now give the de?nition of a modular PT-net.We start by giving the de?nition of PT-nets,and introducing the notations used in the rest of the paper.We use the following de?nition of PT-nets.

D EFINITION5.1.A PT-net is a tuple PN=(P,T, W,M0),satisfying:

(i)P is a?nite set of places;

(ii)T is a?nite set of transitions.The sets of net elements are disjoint:T∩P=?;

(iii)W is the arc weight function mapping from(P×T)∪(T×P)into N;

(iv)M0is the initial marking.M0is a function mapping from P into N.

Now,we de?ne markings and steps for PT-nets.

D EFINITION5.2.A marking is a function M mapping from P into N while a step is a non-empty and?nite multi-set over T.The sets of all markings and steps are denoted by M and Y,respectively.

We denote the set of multi-sets over a set A by A MS. The enabling and occurrence rules of a PT-net can now be de?ned.

D EFINITION5.3.A step Y is enabled in a marking M, denoted by M[Y ,iff the following property is satis?ed:

?p∈P: t∈Y W(p,t)≤M(p).

When a step Y is enabled in a marking M1it may occur, changing the marking M1to another marking M2,de?ned by

?p∈P:M2(p)= M1(p)? t∈Y W(p,t) + t∈Y W(t,p).

Note the summations above are over a multi-set Y.This means that W(p,t)and W(t,p)appear as many times as t appears in Y.

We say that M2is directly reachable from M1by the occurrence of step Y,which is denoted by:M1[Y M2.[M denotes the set of markings reachable from M.

Now we are ready to de?ne modular nets.Some motivation and explanation of the individual parts of the de?nition are given immediately below it,and it is recommended to read both in parallel.

D EFINITION5.4.A modular PT-net is a triple MN= (S,PF,TF),satisfying the following requirements:

(i)S is a?nite set of modules such that:

(a)each module,s∈S,is a PT-net:

s=(P s,T s,W s,M0

s );

(b)the sets of nodes corresponding to different

modules are pair-wise disjoint1:?s1,s2∈S:

[s1=s2?(P s

1∪T s

1

)∩(P s

2

∪T s

2

)=?].

T HE C OMPUTER J OURNAL,V ol.43,No.3,2000

Next,we extend the arc weight function W to place groups and transition groups:

?(g1,g2)∈(PG×TG)∪(TG×PG):

W(g1,g2)= x∈g1,y∈g2W(x,y).

Now,we extend the de?nitions of markings and steps to modular PT-nets.

D EFINITION5.6.A marking is a function M:PG→N while a step is a non-empty and?nite multi-set over TG. The sets of all markings and steps are denoted by M and Y, respectively.

The restriction of a marking M to a module s is denoted by M s.The enabling and occurrence rules of a modular PT-net can now be expressed.

D EFINITION5.7.A step Y is enabled in a marking M, denoted by M[Y ,iff the following property is satis?ed:?pg∈PG: tg∈Y W(pg,tg)≤M(pg).

When a step Y is enabled in a marking M1it may occur, changing the marking M1to another marking M2,de?ned by:

?pg∈PG:

M2(pg)=(M1(pg)? tg∈Y W(pg,tg))+ tg∈Y W(tg,pg).

We say that M2is directly reachable from M1by the occurrence of step Y,which we also denote by:M1[Y M2. [M denotes the set of markings reachable from M,and we generalize this notation to cover the following cases which are all useful in relation to modular PT-nets.

(i)M2is reachable from M1by the occurrence of an

internal transition t:M1[[t M2,and[[M denotes the set of all markings reachable from M by internal transitions only or no transition(i.e.M∈[[M ). (ii)M2is reachable from M1by the occurrence of a fused transition tf:M1[tf M2,and[M denotes the set of all markings reachable from M by the occurrence of

a fused transition.This implies that in general M∈

[M .

(iii)M2is reachable from M1by a sequence of internal transitions followed by a fused transitionσ= t1...t n tf:M1[[σ M2,and[[M denotes the set of all markings reachable by a sequence of internal transitions(or none)followed by a fused transition,

i.e.the closure of M[[ .As case n=0is allowed,

[M ?[[M .

For a local marking M s in a module s,[M s s denotes the set of markings reachable from M s by occurrences of local transitions of module s only.

Next,we show that each modular PT-net has a behavioural equivalent PT-net.Some motivation and explanation of individual parts of the de?nition of the equivalent PT-net is given immediately below it,and it is recommended to read

both in parallel.All names that refer to the equivalent PT-net are marked by an asterisk,e.g.M0refers to the initial marking of the modular PT-net and M?

to the initial marking of its equivalent PT-net.

D EFINITION5.8.Let a modular PT-net MN=(S, PF,TF)be given.Then we de?ne the equivalent PT-net to

be PN?=(P?,T?,W?,M?

)where:

(i)P?=PG.

(ii)T?=TG.

(iii)?(x?,y?)∈(P?×T?)∪(T?×P?):

W?(x?,y?)=W(x?,y?).

(iv)?p?∈P?:M?

(p?)=M0(p?).

E XPLANATION.(i)The equivalent PT-net has one place for each place group.

(ii)The equivalent PT-net has one transition for each transition group.

(iii)The weight associated with a pair(place group, transition group)is unchanged.

(iv)From De?nitions5.4(ii)and5.5,we know that all places of a place group have the same initial marking and we know that all place groups have at least one member.The initial marking of a place group is determined by one of the members of the place group.

The following theorem shows that a modular PT-net and its equivalent PT-net have the same behaviour.

P ROPOSITION5.1.Let MN be a modular PT-net and let PN?be the equivalent PT-net.Then we have the following properties:

1.M=M?∧M0=M?0.

2.Y=Y?.

3.?M1,M2∈M,?Y∈Y:

M1[Y MN M2?M1[Y PN?M2.

Proof.(i)M=M?,follows from De?nitions5.2, 5.6 and5.8(i).From De?nition5.8(iv),the two initial markings

are identical.Thus,M0=M?

.

(ii)From De?nition5.2,Y?consists of all non-empty and

?nite multi-sets in T?

MS

.From De?nition5.6,Y consists of all non-empty and?nite multi-sets in TG MS.From De?nition5.8(ii),T?=TG.Thus Y=Y?.

(iii)First,we prove that the enabling rules coincide,i.e.

M1[Y MN?M1[Y PN?.

From De?nition5.3it follows that M1[Y PN?iff:

?p?∈P?: t?∈Y W?(p?,t?)≤M1(p?),

which by De?nition5.8(i)and(ii)is equivalent to:

?pg∈PG: tg∈Y W?(pg,tg)≤M1(pg).

which by De?nition5.8(iii)is equivalent to:

?pg∈PG: tg∈Y W(pg,tg)≤M1(pg).

From De?nition5.7,it follows that this is exactly the enabling condition for M1[Y MN.

Next we must prove that the occurrence rules coincide,i.e.

M1[Y MN M2?M1[Y PN?M2.

This part of the proof can be structured like the part regarding enabling rules and we will not include it.

In Section2,we claimed that the presented modular PT-nets and the PT-net,given as examples,were equivalent according to the behaviour.This can be checked using De?nition5.8and Proposition5.1.

6.PLACE INV ARIANT ANALYSIS

In this section we show how the concepts of place invariants and place?ows can be extended to modular PT-nets.Place invariants can be used in the proofs of properties of a PT-net, e.g.to show that there is no dead marking.In this paper we focus on the concepts of place invariants and place?ows, more than on the use of invariants in the proof of properties of PT-nets.

6.1.Place?ows and invariants of PT-nets

In this subsection we recall the concepts of place?ow and place invariant.

D EFINITION6.1.For a PT-net PN=(P,T,W,M0),a weight function is a function F mapping from P into Z: (i)F is a place?ow iff:

?t∈T: p∈P F(p)?W(p,t)= p∈P F(p)?W(t,p); (ii)F determines a place invariant iff:

?M∈[M0 : p∈P F(p)?M(p)= p∈P F(p)?M0(p).

A weight function F maps each place p to an integer F(p).

(i)We say that a transition t is?ow preserving with respect

to a weight function F iff t possesses the property described in(i).For a subset of transitions T′′?T, we say that F is T′′-?ow preserving iff all t∈T′′are ?ow preserving,with respect to F.

(ii)The intuition of a transition t being?ow preserving is that t removes—when the weights of F are taken into account—the same number of tokens as it adds.

For a given marking M,we calculate the weighted sum as the sum of the weights multiplied by the marking of the individual places.The weight function F determines an invariant iff all reachable markings have the same weighted sum.

Note that any linear combination of two place?ows is a place?ow,i.e.if F1and F2are place?ows,and z1,z2∈Z then z1?F1+z2?F2is a place?ow.The weight function which assigns zero weights to all places is always a place ?ow.We say that a place p is included in F if F(p)=0. The main reason for introducing place?ows is the dif?culty checking place invariants on the total set of reachable states. Place?ows can be checked on the structure of the PT-net. In practice we do not need to sum through all the places, it is suf?cient to sum through the input places of t for the ?rst sum,and through the output places of t for the second sum.

The following theorem describes the relationship between place invariants and place?ows.

T HEOREM6.1.Let a PT-net with no dead transition be given and let F be a weight function.

F is a place?ow?F determines a place invariant. Proof.The theorem is part of the classical theory for invariant analysis(see e.g.[9]).

?is satis?ed for all PT-nets with no dead transition.

?is satis?ed for all PT-nets.

6.2.Place invariants of modular PT-nets

In this section we show how the formal de?nitions of place invariants and place?ows can be given for modular PT-nets. This subsection is structured like the previous one and it should be easy to compare the de?nitions given for PT-nets and modular PT-nets.

D EFINITION6.2.For a modular PT-net MN=(S, PF,TF),a weight function is a function F mapping from PG into Z.

(i)F is a place?ow iff:

?tg∈TG:

pg∈PG F(pg)?W(pg,tg)

= pg∈PG F(pg)?W(tg,pg).

(ii)F determines a place invariant iff:

?M∈[M0 :

pg∈PG F(pg)?M(pg)= pg∈PG F(pg)?M0(pg).

A weight function F of a modular PT-net maps each place group pg into an integer F(pg).

(i)We say that a transition group tg is?ow preserving with respect to a weight function F iff tg possesses the property described in De?nition6.2(i).For a subset of transitions groups TG′′?TG,we say that F is TG′′-?ow preserving iff all tg∈TG′′are?ow preserving,with respect to F.

The intuition of a transition group tg being?ow preserving is that tg removes—when the weights of F are taken into account—the same number of tokens as it adds. (ii)For a given marking M we calculate the weighted sum as the sum of the weights multiplied by the marking of the individual place groups.The weight function F determines an invariant iff all reachable markings have the same weighted sum.

T HEOREM6.2.Let a modular PT-net with no dead transition be given and let F be a weight function.

F is a place?ow?F determines a place invariant.

Proof.The theorem can be proved similarly to Theorem6.1, we just need to consider place groups and transition groups instead of places and transitions.

?is satis?ed for all modular PT-nets.

?is satis?ed for all modular PT-nets with no dead transition.

6.3.How to?nd place invariants of modular PT-nets In the examples presented in sections2and3,we have shown some compositions of place invariants and place ?ows,using either place fusion only or transition fusion only.

We use the term global weight function for a weight function of the entire modular PT-net,while we use the term local weight function for a weight function of a single module.In the present section,we state and prove a number of theorems specifying how local place?ows and local place invariants are related to global place?ows and global place invariants.

D EFINITION6.3.Let MN=(S,PF,TF)be a modular PT-net.

(i)A set of local weight functions{F s}s∈S of the modules

is consistent iff they assign the same weight to all members of each place group:

?pg∈PG:?p1,p2∈pg:F S(p

1)(p1)=F S(p

2)

(p2).

(ii)A global weight function F of MN determines a consistent set of local weight functions{F s}s∈S of the modules:

?p∈P:F S(p)(p)=F([p]).

(iii)A consistent set of local weight functions{F s}s∈S of the modules of MN determines a global weight function F:?pg∈PG,?p∈P:pg=[p]?F(pg)=F S(p)(p).

Note that the construction ful?ls:if F1determines{F s}s∈S and{F s}s∈S determines F2then F1=F2.

T HEOREM6.3.Let MN=(S,PF,TF)be a modular PT-net and let{F s}s∈S be a consistent set of local weight functions of the modules which determine the global weight function F.Then we have

[?s∈S:F s is a place?ow of T s]

?F is a place?ow of MN.

Proof.The theorem follows directly from the observation that all transitions of the individual modules are?ow preserving,i.e.we know that each member of a transition group is?ow preserving.This is a much stronger demand than the transition group being?ow preserving as a group.

In the next theorem we show how Theorem6.3can be extended to place invariants if we consider modular PT-nets without place fusion.

T HEOREM6.4.Let MN=(S,?,TF)be a modular PT-net without place fusion,and let{F s}s∈S be a consistent set of local weight functions of the modules which determine the global weight function F.Then we have

[?s∈S:F s determines a place invariant of module s]?F determines a place invariant of MN. Proof.From the de?nition of enabling for modular PT-nets, we know that a transition group will only be enabled if all transitions of the group are enabled.This means that the set of reachable states for the modular PT-net is covered by the set of reachable states of the local modules.

Note that we can?nd place invariants of the total system which cannot be expressed as place invariants of the individual modules.

T HEOREM6.5.Let MN=(S,PF,?)be a modular PT-net without transition fusion,and let F be a global weight function of MN which determines a set of local weight functions{F s}s∈S.Then we have

F is a place?ow of MN

?[?s∈S:F s is a place?ow of T s].

Proof.Since transition fusion is not used,we know that each transition group consists of exactly one member.Thus each individual transition is?ow preserving.

From De?nition6.3and Theorem6.5we know that we can?nd all place?ows of the total system from the place ?ows of the individual modules.

T HEOREM6.6.Let MN=(S,PF,TF)be a modular PT-net and let F be a global weight function of MN which determines a set of local weight functions{F s}s∈S.Then we have

F is a place?ow of the modular PT-net

?[?s∈S:F s is a place?ow of IT s]

∧[TF is?ow preserving for F].

Proof.In this proof,it is suf?cient to establish a correspondence between the transition groups and the union of the set of internal transitions and the set of fusion sets.If a transition group contains exactly one transition it corresponds to an internal transition and otherwise it corresponds to a transition fusion set.

Theorem6.6is a key result.All place?ows of a modular PT-net can be determined from consistent sets of weight functions which are place?ows for the internal transitions IT and are?ow preserved by all transition fusion sets.A corresponding theorem for coloured Petri nets(CP-nets)has been shown for place fusion only in[10].

To illustrate how we envision the use of the results from this section,we describe how a place?ow could be found for a modular PT-net.We will assume that a modular PT-net has mainly internal,i.e.non-fused,nodes,and the main work is to check that the internal transitions are?ow preserving.When performing place invariant analysis one can be interested either in all possible?ows of the system or in a few,but descriptive,place?ows.Theorem6.6allows one to calculate all possible place?ows in a modular way: calculate all?ows for the internal transitions and combine those which are consistent and,?nally,check the transition fusion sets.

The result of this theorem is also attractive when using an interactive process where the weights of places are gradually added.It consists in starting with a single module and specifying weights that are?ow preserved by all internal transitions.After this,the rest of the weight functions can be restricted,using the weights of the module.Both place fusion sets and transition fusion sets can be used.We know that the weight functions must be consistent and this means that all places of a place fusion set must have the same weight.We also know that the transition fusion sets must be?ow preserving and if only one of the surrounding places needs a weight,it can be calculated directly from the known weights.After these restrictions have been applied,the internal transitions of the next module can be checked.In the end it is necessary to check that all transition fusion sets are?ow preserving.

In the next section,we present another main analysis method,i.e.modular state spaces.

7.STATE SPACES

In the following,we formally de?ne modular state spaces; but?rst we introduce some notations and recall the de?nition of state spaces of PT-nets.

7.1.State spaces of PT-nets

We want to represent state spaces as directed graphs.Since we want to be able to have multiple arcs between pairs of nodes we use the following de?nition from[9].

D EFINITION7.1.A directed graph is a tuple DG= (V,A,N)such that:

(i)V is a set of nodes(or vertices);(ii)A is a set of arcs(or edges)such that

V∩A=?;

(iii)N is a node function.It is de?ned from A into V×V. The node function N maps an arc a into a pair of nodes (x1,x2),where x1is the source and x2the destination of arc a.

D EFINITION7.2.Let PN=(P,T,W,M0),be a PT-net. The state space of PN is the directed graph SS=(V,A,N), where:

(i)V=[M0 ;

(ii)A={(M1,t,M2)∈V×T×V|M1[t M2};

(iii)?a=(M1,t,M2)∈A:N(a)=(M1,M2).

The state space contains a node for each reachable marking and an arc for each possible transition occurrence. For two nodes v s and v e we use DP F(v s,v e)to denote the set of all directed?nite paths connecting v s to v e,i.e. all?nite sequences of nodes and arcs v1,a1,v2,a2,...,v n where v1=v s,v n=v e,and for all i in1,...n,N(a i)= (v i,v i+1).

Next we consider SCCs.Two nodes v1,v2∈V are strongly connected iff there exists a?nite directed path which starts in v1and ends in v2and a?nite directed path which starts in v2and ends in v1.It is easy to see that strong-connectedness is an equivalence relation and hence determines a set of disjoint equivalence classes.An SCC is a directed graph DG′=(V′,A′,N′),where V′?V is an equivalence class of strongly connected nodes,A′?A are all those arcs where both the source and destination belong to V′,and N′is the restriction of N to A′.

The set of all SCCs is denoted by SCC.For a node v∈V and a component c∈SCC we use the notation v∈c to denote that v is one of the nodes in c.A similar notation is used for arcs.We use v c to denote the component to which v∈V belongs.We also denote the source(respectively destination)of an arc a by srce(a)(respectively dest(a)).

D EFINITION7.3.The directed graph SS?=(V?, A?,N?)is the SCC-graph of state space SS iff the following properties are satis?ed:

1.V?=SCC;

2.A?={a∈A|srce(a)c=dest(a)c};

3.?a∈A?:N?(a)=(srce(a)c,dest(a)c).

De?nition7.3allows us to talk about the SCC graph of a state space and this will turn out to be a very useful tool when we have to specify ef?cient proof rules for deciding properties of systems.This will be discussed in Section8.

7.2.Modular state spaces

In this section we consider modular PT-nets with transition fusion only,i.e.no place fusion.To conclude that this is not a severe restriction please recall the arguments of Section4. In the de?nition of modular state spaces we need a compact notation to capture the states reachable from M in

all the individual modules,i.e.[[M .It turns out that we can use a product of SCCs of the individual modules to express this representative node:for any reachable marking M,we use M c to denote the product of SCCs M c s of the individual modules:

?M∈[M0 :M c= s∈S M c s.

This notation is also extended to a set X of markings:

X c= M∈X{M c}.

In the de?nition of a modular state space,we have two parts:the synchronization graph and the state spaces of the individual modules.The de?nition is followed by an explanation and both should be read in parallel.

D EFINITION7.4.Let MN=(S,?,TF)be a modular PT-net without place fusion and with the initial marking M0.The modular state space of MN is a pair MSS= ((SS s)s∈S,SG),where:

(i)SS s=(V s,A s,N s)is the local state space of module s:

(a)V s= v∈(V SG)s[v s,

(b)A s={(M1,t,M2)∈V s×IT s×V s|M1[t M2},

(c)?a=(v1,t,v2)∈A s:N s(a)=(v1,v2);

(ii)SG=(V SG,A SG,N SG)is the synchronization graph of MN:

(a)V SG=[[M0 c∪{M c0},

(b)A SG={(M c

1,(M′

1

,tf,M2),M c

2

)∈

V SG×([M0 ×TF×[M0 )×V SG|

M′

1∈[[M1 ∧M′

1

[tf M2},

(c)?a=(v1,X,v2)∈A SG:N SG(a)=(v1,v2).

E XPLANATION.(i)The de?nition of the state space graphs of the modules is a generalization of the usual de?nition of state spaces:

(a)the set of nodes of the state space graph of a module

contains all states locally reachable from any node of the synchronization graph;

(b)likewise the arcs of the state space graph of a module

correspond to all enabled internal transitions of the module;

(c)an arc(v1,t,v2)starts from node v1and ends in node

v2.

(ii)Each node of the synchronization graph is labelled by an M c and represents all the nodes reachable from M by occurrences of local transitions only,i.e.[[M .The de?nition of M c ensures that any marking having the same set of markings reachable by internal transitions will be represented by the same node in V SG.The synchronization graph contains the information on the nodes reachable by occurrences of fused transitions:

(a)the nodes of the synchronization graph represent

all markings reachable from another marking by a sequence of internal transitions followed by a fused transition.The initial node is also represented;(b)the arcs of the synchronization graph represent all

occurrences of fused transitions;

(c)an arc(v1,X,v2)starts from node v1and ends in node

v2.

The state space graphs of the modules only contain local information,i.e.the markings of the module and the arcs corresponding to local transitions,but not the arcs corresponding to fused transitions.All the information concerning the occurrences of fused transitions is stored in the synchronization graph.This structure is designed in order to ef?ciently check properties directly in modular state spaces,as will be shown in Section8.

The modular state space can be unfolded into an ordinary state space.Let M denote the set of markings of the full system and M s the set of markings of module s.The explanation is given just below the de?nition and both should be read in parallel.

For a marking m s of module s,we use m?s to denote the marking of the full system where all places of all other modules are empty.

D EFINITION7.5.Let MN=(S,PF,TF)be a modular PT-net and MSS=((SS s)s∈S,SG)its modular state space. The unfolded state space of MSS is SS=(V,A,N),where: (i)V= v∈V SG[[v ;

(ii)A= (v,(m,[t],m′),v′)∈A SG{(m,[t],m′)}

∪ m∈V,s∈S,(m s,t,m′s)∈A s{(m,t,(m+m′s?)?m?s)}; (iii)?a=(v1,X,v2)∈A:N(a)=(v1,v2).

E XPLANATION.(i)The set of nodes of the equivalent state space is the set of markings represented by nodes in V SG,i.e.the set of markings reachable by internal transitions from any of the nodes of V SG.

(ii)An arc label of the synchronization graph is an arc of the equivalent state space.For each marking m,if a local transition is enabled,there is a corresponding arc in the equivalent state space.The marking obtained is changed for the module concerned as speci?ed in its state space graph. (iii)An arc(v1,X,v2)starts from node v1and ends in node v2.

The following theorem states that the equivalent ordinary state space of a MSS and the state space of the equivalent PT-net of MN are the same.

T HEOREM7.1.Let MN be a modular PT-net,MSS its modular state space and PN its equivalent PT-net.Let SS MSS be the unfolded state space of MSS and SS PN the state space of PN:

SS MSS is isomorphic to SS PN.

Proof.The main idea of the proof is to follow the constructive de?nitions given in De?nitions5.8,7.2,7.4, and7.5.De?nition5.8shows how we can construct an equivalent PT-net PN from a modular PT-net MN;note that we have a transition in PN for each transition group in MN. Using De?nition7.2,we can then construct the state space SS PN corresponding to https://www.sodocs.net/doc/282130308.html,ing De?nition7.4,we can construct the modular state space MSS from MN and?nally

we must show that De?nition7.5maps MSS to an unfolded state space SS MSS which by construction is isomorphic to SS PN.

We now de?ne an abstract algorithm to construct modular state spaces.We use primitive functions similar to those of[9](Proposition1.4).Waiting SG is a set of nodes of the synchronization graph.Node SG(v)is a procedure which creates a new node v in the synchronization graph and adds v to Waiting SG.If v is already a node,Node SG(v)has no effect. Analogously,Arc SG(v1,(M1,t,M2),v2)creates an arc with source v1,destination v2,and inscription(M1,t,M2)in the synchronization graph,if it does not exist yet.Next SG(v) is used to denote the set of possible next moves using fused transitions.These moves can be performed from any marking in[[v ,i.e.reachable from v by occurrences of local transitions only.In addition to this,we use the function AddInternalSuccessors(M)which takes a marking and develops the corresponding state space of each module, i.e.all local markings reachable from M s using transitions from IT s only.This procedure is similar to the state spaces construction algorithm for all modules,with initial marking M s.AddInternalSuccessors(M)is able to determine the SCCs of M s for each of the local state spaces and from these construct M c as the returned value.

P ROPOSITION7.1.The following algorithm constructs the modular state space:

Waiting SG:=?

v0:=AddInternalSuccessors(M0)

Node SG(v0)

repeat

select a node v1∈Waiting SG

for all(M1,t,M2)∈Next SG(v1)do

begin

v2:=AddInternalSuccessors(M2)

Node SG(v2)

Arc SG(v1,(M1,t,M2),v2)

end

Waiting SG:=Waiting SG\{v1}

until Waiting SG=?

This algorithm is a generalization of the one for constructing state spaces.The generalizations follow directly from De?nition7.4.

In the next section,we will show how to prove properties directly on the modular state space,i.e.without unfolding to the ordinary state space.

8.PROVING PROPERTIES

Here,we will prove properties for modular PT-nets.It has been our main concern to ensure that all properties are de?ned in such a way that they are consistent with the de?nitions known for PT-nets.For each of the PT-net properties we present proof rules which take advantage of the characteristics of modular state spaces.We also sketch algorithms showing how these proof rules can be

FIGURE12.Modular PT-net with modules A and B.

FIGURE13.The full state space of the system. implemented in order to obtain ef?cient analysis of modular PT-nets and avoid unfolding to ordinary state spaces.

We?rst introduce the example that will be used throughout this section.In Figure12we present a modular PT-net consisting of two modules A and B which share four common transitions TF1,TF2,TF3,and TF4.Module A is presented on the left-hand side while module B is on the right-hand side.This system will be used to illustrate the properties in the following subsections.

The modular PT-net is equivalent to a PT-net where the transitions shared by both modules are fused,i.e.TF1of module A is fused with TF1of module B,TF2of module A is fused with TF2of module B,and so on.The occurrence graph of this PT-net is presented in Figure13.The modular state space of the system is presented in Figure14.Note that we do not distinguish between nodes and SCCs,since they all contain exactly one node.

8.1.Reachability

Here,our purpose is to?nd whether a given marking M is reachable or not.The set of ancestors of a local marking M s in the state space graph of module s is the set of SCCs from which M s can be reached,i.e.for all s in S and for all local

B3

B2

B1Module A A1A5

A2A3

A4Module B t4t1t2t3FIGURE 14.The modular state space.

markings M s in V s ,we de?ne:

anc s (M s )={M c i |M i ∈V s ∧M s ∈[M i s }.We now express the reachability properties.P ROPOSITION 8.1.

(i)M ∈[M 0 ??v ∈V SG :M ∈[[v .(ii)M ∈[M 0 ?[(?s ∈S :M s ∈V s )∧((

s ∈S anc s (M s )∩V SG )=?)].

E XPLANATION .(i)A global marking is reachable iff it is internally reachable from one of the nodes in V SG .

(ii)The ?rst part of the conjunction ensures that all local markings are reachable.This is a necessary but not suf?cient condition,and the second part of the conjunction ensures that there exists a node in V SG from where the required combination of local states is reachable.

Proof.(i)Follows directly from De?nition 7.4.

(ii)The ?rst part of the conjunction ensures that the ancestors of all M s are well de?ned.Reachability then follows from De?nition 7.4and the de?nition of function anc s .

S KETCH OF ALGORITHM .The process to check that a marking M is reachable can easily be implemented by ?rst looking at the restrictions of M to the modules.If for one module s ,M s is not in SS s ,then M is not reachable.Otherwise,we check if there exists a node v in the synchronization graph from which M is locally reachable.This can be done ef?ciently,using the information of the SCCs of the modules.

E XAMPLE .Let us apply Proposition 8.1(ii)to the example presented in Figures 12–14,to check whether A4B2is reachable or not.Node A4is in SS A .Node B2is in SS B .Node A4B2is locally reachable from node A1B1:the ancestors of A4in SS A are A4,A2and A1,and the ancestors of B2in SS B are B2,B1.Thus all the conditions are satis?ed and A4B2is reachable.We also check if A5B2is reachable.Node A5is in SS A .Node B2is in SS B .The only ancestor of A5in SS A is itself,the ancestors of B2in SS B are B2,B1.Thus the cross-products of ancestors are {A5B2,A5B1}which are not in SG .Hence,the last condition of the proposition is not satis?ed and A5B2is not reachable.

8.2.Dead markings

We will now give properties to ?nd dead markings.

P ROPOSITION 8.2.

(i)M ∈[M 0 is dead ?

[(?s ∈S :?(m 1,t,m 2)∈A s :m 1=M s )

∧(?(v 1,(M 1,tf,M 2),v 2)∈A SG :M 1=M)].(ii)M ∈[M 0 is dead ?

[(?s ∈S :(M s )c ∈Term (SCC s )∩Trivial (SCC s ))∧(?(v 1,(M 1,tf,M 2),v 2)∈A SG :M 1=M)].(iii)M ∈[M 0 is not dead ?

?s ∈S :?m ∈V s :?(m,t,m ′)∈A s .(iv)M ∈[M 0 is not dead ?

?s ∈S :Term (SCC s )∩Trivial (SCC s )=?.E XPLANATION .(i)A marking is dead iff there is no enabled transition,neither local nor fused.

(ii)A marking is dead iff it belongs to terminal and trivial components of all local state spaces and does not enable any fused transitions.We use function Term which returns the set of terminal SCCs and function Trivial which returns the set of trivial SCCs.An SCC is terminal if it has no outgoing arcs,and it is trivial if it has exactly one node and no arc.(iii)We know that there is no reachable dead marking if there exists a local module which for any marking has an enabled transition.

(iv)We know that there is no reachable dead marking if there exists a local module without strongly connected components being both terminal and trivial.

Proof.(i)?Let M be a reachable dead marking.No local transition is enabled.Thus,for all s in S ,M s cannot be the source of an arc.No fused transition is enabled.Hence there is no arc labelled by M in SG .

?The proof is similar to that of ?.

(ii)The right-hand sides of (i)and (ii)are equivalent.(iii)Let us suppose that there exists a module s in S such that all nodes have at least one outgoing arc.Then from each reachable marking a local transition of s is enabled.Thus M is not dead.

(iv)The right-hand sides of (iii)and (iv)are equivalent.S KETCH OF ALGORITHM .Here we want to ?nd all reach-able dead markings of the system using Proposition 8.2(ii).We will consider all the nodes of SG .For each node m ,we will only consider for all m s the leaves of [m s s ,in the state space graph of module s .These are the terminal and trivial M s .We construct the sets of s ∈S M c s

for all the SG nodes.We remove from this set all the markings labelling SG arcs.Thus the remaining markings satisfy the conditions of the proposition above and form the set of all reachable dead markings.

E XAMPLE .We apply this algorithm to the example presented in Figures 12–14,to ?nd all reachable dead markings.

There are two nodes in SG labelled by the SCCs’cross-products A1B1and A5B3.The set of trivial leaves of [A1 A is {A3,A4},the one of [B1 B is {B2}.The set of trivial leaves of [A5 A is {A5},the one of [B3 B is {B3}.Thus

the set of cross-products to check is{A3B2,A4B2,A5B3}. The set of arc labels in SG is{A3B1,A4B1,A2B2,A5B3}. Hence,the set of reachable dead markings is{A3B2,A4B2}.

8.3.Liveness

We now want to determine whether a given set of transitions is live or not.We?rst express the liveness properties for a fused transition,then for a local one and?nally for a set of transitions in general.

P ROPOSITION8.3.

(i)tf∈TF is live?

[?scc∈Term(SCC SG):tf∈Trans(scc)]

∧[?v∈V SG:?M∈[[v :

(?s∈S:M c s∈Term(SCC s))?

?(v,(M1,tf′,M2),v2)∈A SG:M1∈[[M ]. (ii)t∈IT s is live?

[?scc∈Term(SCC SG):

?v∈scc:t∈Trans([v s s)]

∧[?v∈V SG:?M∈[[v :

(M c s∈Term(SCC s))?

(t∈Trans(M c s)

∨?(v,(M1,tf,M2),v2)∈A SG:M1∈[[M )]. (iii)X?T is live?

[?scc∈Term(SCC SG):

(X∩Trans(scc)=?

∨?v∈scc:X∩Trans([[v )=?]

∧[?v∈V SG:?M∈[[v :

(?s∈S:M c s∈Term(SCC s))?

(?s∈S:X∩Trans(M c s)=?)

∨(?(v,(M1,tf,M2),v2)∈A SG:M1∈[[M )].

E XPLANATION.We use SCC SG to denote the set of SCCs of the synchronization graph.Trans maps an SCC into the set of transitions which occur in the labels of the arcs in the component.Similarly,we use Trans to map a set of reachable markings to the set of transitions which occur in the labels of the arcs between two nodes of the set.

(i)A fused transition tf is live iff it occurs in all terminal strongly connected components of the synchronization graph,and furthermore it is always possible to get to a combination of local states which enables a fused transition. (ii)A transition local to module s is live iff,for all terminal SCCs of the synchronization graph,there exists a node which enables t,and furthermore it is always possible to get to a combination of local states which enables a fused transition,or to a state enabling t.

(iii)A set of transitions X is live iff for each terminal SCC of the synchronization graph there is an occurrence of some element of X,or some node enabling an internal transition in X.Furthermore it is always possible to get to a combination of local states which enables a fused transition,or to a state enabling an element in X.

Proof.(i)and(ii)are particular cases of(iii).Thus,we will only prove(iii).

?Let X be a live set of transitions.This means that it is possible from any reachable marking to reach another marking in which one of the transitions of X is enabled.For each terminal SCC of the synchronization graph either there exists a fused transition in X belonging to the component(X∩Trans(scc)=?)or there exists a node v in scc for which a local transition of X is enabled (?v∈scc:X∩Trans([[v )=?).Moreover,from each node in the synchronization graph it is possible to reach a set of terminal SCCs either containing a local transition of X(X∩Trans(M c s)=?)or enabling a fused transition (?(v,(M1,t,M2),v2)∈A SG:M1∈[[M ).This ensures that it is possible from each node of the synchronization graph either to locally reach a marking enabling a transition of X or to attain another node in the synchronization graph. If we apply this last case several times,we will reach a node in a terminal SCC of the synchronization graph.From the ?rst condition,one of its successors enables a transition of X.

?The proof is similar to that of?.

S KETCH OF ALGORITHM.Here,we want to check the liveness of a given set X of transitions.We mark the nodes that satisfy the?rst part of the condition on the right-hand side of(iii).To do that we mark the nodes in the SCC graphs of modules which enable or contain a local transition of X, as well as their ancestors.Then we mark the nodes in the terminal SCCs of the synchronization graph that are built from at least one marked SCC.We also mark the nodes of the terminal SCCs of the synchronization graph which enable a fused transition of X.Then,if there exists a terminal SCC of the synchronization graph without any marked node, the?rst part of the condition is not satis?ed,thus X is not live.Otherwise,we have to check the second part of the condition.For each node in the synchronization graph we take the local successors which are built from terminal SCCs only.For each of these we check that it either contains a local transition of X or labels an arc of the synchronization graph. If one node does not satisfy this requirement X is not live, otherwise it is.

E XAMPLE.We apply this algorithm to the example presented in Figures12–14,to check that X=T is not live.We could of course deduce this property from the fact that the system has dead markings,but this is just an illustration of the algorithm to check liveness.In the SS s of modules A and B we mark nodes A1,A2and B1.The synchronization graph contains only one SCC.Node A1B1 is built from a marked local node(e.g.A1),so we mark it. Hence,the terminal SCC has a marked node,and the?rst part of the condition is satis?ed.The terminal nodes we have to check now are A3B2,A4B2and A5B3.Node A3B2 does not contain a transition of X nor labels an arc of the synchronization graph.Thus X is not live.Note that the same problem arises with A4B2,and that A5B3satis?es the condition.

8.4.Home properties

Here,we want to check whether a given set of reachable markings is a home space or not.We?rst express the home

properties for a marking and then for a set of markings.

P ROPOSITION8.4.

(i)M H∈[M0 is a home marking?

[?scc∈Term(SCC SG):?v∈scc:M H∈[[v ]

∧[?v∈V SG:?M∈[[v :

(?s∈S:M c s∈Term(SCC s))?

(M H∈[[M

∨?(v,(M1,tf,M2),v2)∈A SG:M1∈[[M )]. (ii)X?[M0 is a home space?

[?scc∈Term(SCC SG):?v∈scc:X∩[[v =?]

∧[?v∈V SG:?M∈[[v :

(?s∈S:M c s∈Term(SCC s))?

(X∩[[M =?

∨?(v,(M1,tf,M2),v2)∈A SG:M1∈[[M )].

E XPLANATION.(i)A marking M H is a home marking if it is always possible to reach this marking.To prove this we must show that all terminal SCCs of the synchronization graph have a node which contains M H in its local successors;and we must show that if we cannot enable any transition fusion we must be able to reach M H using internal transitions only.

(ii)Checking a home space is similar to(i),we just check for a non-empty intersection instead of membership. Proof.The proof is similar to the proof of liveness.(i)is a particular case of(ii)where X contains only one marking. Thus,we will only prove(ii).

?Let X be a home space.This means that it is possible, from any reachable marking,to reach a marking of X.Let scc be a terminal SCC of the synchronization graph.From a node v of scc,it is possible to reach any node in[[v .Then, from the hypothesis,X∩[[v =?.Now,let v be a node of the synchronization graph,M be a marking in[[v which is in a terminal SCC of all modules,then either[[M contains a node of X or it is possible to leave v in order to reach another node in the synchronization graph.

?The proof is similar to that of?.

S KETCH OF ALGORITHM.Here we want to check whether a given set X of markings is a home space or not. We mark the nodes that satisfy the?rst part of the condition. To do that we mark the nodes of X in the SCC graphs of the modules as well as their ancestors.Then we look at the nodes in the terminal SCCs of the synchronization graph which are built only from marked SCCs.We mark those which contain at least one marking of X in their local successors.We have to do that because it might be the case that the component in one module is marked due to the restriction of a marking M1in X and the component in another module is marked due to the restriction of another marking M2in X.Then,if there exists a terminal SCC of the synchronization graph without any marked node,the?rst part of the condition is not satis?ed,thus X is not a home space.Otherwise,we have to check the second part of the condition.For each node in the synchronization graph we take the local successors which are built from terminal SCCs only.For each of these,we check that it either contains a marking of X or labels an arc of the synchronization graph. If one node does not satisfy this requirement,X is not a home space,otherwise it is.

E XAMPLE.We apply this algorithm to the example presented in Figures12–14,to check that X1={A2B2} is not a home space and that X2={A3B2,A4B2}is.Let us start with X1.In the SS s of modules A and B we mark nodes A1,A2and B1,B2.The synchronization graph contains only one SCC.Node A1B1is built from only marked local nodes and has A2B2as a local successor,so we mark it. Hence,the terminal SCC has a marked node and the?rst part of the condition is satis?ed.The terminal nodes we have to check now are A3B2,A4B2and A5B3.Node A3B2has no outgoing arc.Thus X1is not a home space.Note that the same problem arises with A4B2and that A5B3satis?es the condition.

Now let us check that X2is a home space.In the state space graphs of modules A and B we mark nodes A1,A2, A3,A4and B1,B2.The synchronization graph contains only one SCC.Node A1B1is built only from marked local nodes,and has A3B2as a local successor,so we mark it. Hence,the terminal SCC has a marked node and the?rst part of the condition is satis?ed.The terminal nodes we have to check now are A3B2,A4B2and A5B3.Both A3B2,A4B2 are in X2.Node A5B3labels an arc of the synchronization graph.Thus X2is a home space.

8.5.Boundedness

We explain how boundedness properties can be checked. Here we use the fact that we have no place fusion,i.e.that all places are members of one local module.

P ROPOSITION8.5.For the boundedness properties,we have the following proof rules,valid for all s∈S,and all p∈P s:

(i)BestUpperBound(p)=max M

s∈V s

M s(p);

(ii)BestLowerBound(p)=min M

s∈V s

M s(p).

E XPLANATION.(i)The best upper bound for a place p in P s can be found directly in the local state space of module s. (ii)States the same result for lower bounds.

Proof.(i)The BestUpperBound for a given place is local to the module s of this place.As the state space graph of module s contains exactly the reachable markings of this module,we just have to?nd the BestUpperBound in SS s. (ii)The arguments in the proof of(i)also apply to(ii).

R EMARKS.Bounds of places can be generalized in several ways.Bounds can be de?ned for a set of places instead of a single place and even a general function can be applied to the reachable markings.Similar generalizations could be speci?ed for modular state spaces.One important observation is that these general bounds can be checked very ef?ciently if they only depend on a single module,or if they can be expressed as a positive linear combination of bounds of the modules.

S KETCH OF ALGORITHM.The bounds of a single place are local properties.Thus they are very easy to check on the state space of the module containing place p.This allows us to investigate the state space graph of one module instead of the state space of the entire system.

E XAMPLE.We apply this to the example presented in Figures12–14.

If we want to check that A1is bounded by one,we traverse the nodes of module A,this means that it is necessary to check?ve nodes.Similarly,it is necessary to traverse three nodes to check the bound of a place of module B.In the ordinary state space it is always necessary to traverse the nine nodes.

To illustrate the remark on the extension to general bounds above,we want to check the mutual exclusion between A5 and B2.For that purpose,we use a function F so that F(M)=M(A5)+M(B2).The projections of this function on both modules are F A and F B such that:F A(M A)= M A(A5)and F B(M B)=M B(B2).

Now we compute the maxima of these functions for each node in SG.There are only two nodes A1B1and A5B3.For the?rst node we get max(F A)=0and max(F B)=1,thus max(F)=1for this node.For the second node,we obtain max(F A)=1and max(F B)=0,thus max(F)=1for this node.Thus the maximum for function F in SG is one and the mutual exclusion between places A5and B2is proved. If we investigate the complexity of the algorithms required in order to decide the properties described in this section we ?nd that all of them are linear in the size of the modular state space.In particular,it should be noted that a number of properties of local modules can be checked more ef?ciently when using the modular state spaces than the ordinary state spaces.

In the next section we apply the results presented up to now to larger models.

https://www.sodocs.net/doc/282130308.html,RGER EXAMPLES

There exists a large number of industrial applications of Petri nets,in particular for high-level Petri nets such as CP-nets.This is the reason why parts of this section discuss models which are not PT-nets.As explained in the introduction,the results shown in the previous sections can also be generalized to CP-nets.

9.1.An example of a modular approach to place

invariants

We have tried to use the results from Section6.3to?nd place?ows of the hierarchical CP-net described in[11]. This is a model describing a detailed design of the network management system of the RcPAX X.25wide area network. It consists of30modules(pages),many of these having up to seven instances due to the reuse of pages.The modular approach made it easy to?nd the place invariants needed in the proof of properties which were local to a few pages.The modular approach also made it possible to compose place?ows of the individual page instances into place?ows of the total system.An example of a property which could be proved directly by means of a place invariant and which involved many pages was the preservation of packets in the system.The handling of packages was relatively complex and involved grouping packages into larger logical units.By adding extra places which would keep a log of the information passed on the network,it was possible to investigate how messages could be lost and check that the information which was re-established either matched the original message,or the originating sender would be noti?ed.The work on modular place invariants was performed after the design of the model was completed, and not as an integrated part of the modelling process.It should also be noted that the work on the examples was performed by hand.Tool support will be necessary if place invariants should be used as part of the development of large descriptions.A similar approach could easily be applied to other hierarchical CP-net models,e.g.the ISDN Basic Rate Interface described in[12].

We have not investigated how a modular approach can be used for large systems related by means of transition fusion, since we have no models of this nature at our disposal. From our own experiments with small systems it seems to be possible to use a modular approach for larger ones too.

9.2.An example of a modular approach to occurrence

graph analysis

To test the ideas of modular state spaces before doing an actual implementation we have investigated a larger example using an existing tool,Design/CPN[13].

Design/CPN supports analysis of CP-nets by means of state spaces.The facilities of Design/CPN allowed us to emulate the algorithm described in Proposition7.1by manually calling appropriate routines.The lack of full tool support is the reason for choosing an example which is still of a moderate size.

The aim of this testing is twofold:?rst of all we want to show how modular state spaces work for concrete examples, second we want to illustrate that the basic functionalities of the Design/CPN tool can be used as a basis for an implementation of a tool supporting analysis by means of modular state spaces.

The example we have chosen is constructed to re?ect some of the important properties that we expect to?nd in industrial applications:the system consists of three modules, each of them has an initialization phase,a cyclic main phase and a termination phase.The modules communicate pairwise,and the communications lead to new behaviour of the modules.Thus this example has a structure similar to that of Figure5,but using more modules.

The ordinary state space has1728nodes and7368arcs. The system has a single non-trivial SCC,which implies that the system has no dead markings and every reachable state is a home state.

The modular state space has four nodes and54arcs in the synchronization graph,and three modules with altogether 18nodes and18arcs.The generation was performed using

the facilities proposed in Design/CPN to specify breakpoints in the construction.Thus it was possible not to?re fused transitions or transitions of another module,but only build local parts of the graph.Moreover,the generation could be continued after determining the nodes obtained by?ring a shared transition.If we inspect the SCC graphs of the modules we?nd that none of them has a trivial terminal component.According to Proposition8.2(iv)this implies that the system has no dead state.To show that every reachable state is a home state,we use Proposition8.4(i) and prove that the initial marking is a home state.First we observe that all combinations of local terminal components enable at least one fused transition,i.e.we cannot be trapped in the combination of local components.We conclude by checking that the initial marking is included in the nodes locally reachable in the terminal SCC of the synchronization graph.

In the example we have a system where communication does not involve all modules.This means the number of arcs in the synchronization graph grows with the number of states of the modules which do not take part in the communication.If we handle this case by introducing a special symbol denoting that a module does not participate in the communication the number of arcs of the synchronization graph will decrease from54to10.

9.3.Practical use of modular analysis

The modular method to obtain place invariants is rather satisfactory since it works both for place fusion and transition fusion.Thus a superset of the actual?ows that will be relevant for the entire system can be calculated locally to each module.Then their combination can be performed, leading to?ows of the entire system.We have to note that from the experience of our groups a modularly designed net consists of different modules with often several instances of the same module.In that case the calculus of the?ow would be the same for all instances and obtaining it for a single instance is suf?cient.Moreover,modules do not participate in all?ows,and that can be seen very easily when performing the combinations.This is an advantage compared to the non-modular calculus,where all the places would be examined.Our method could be seen as a module-guided heuristic for invariants calculus.

As concerns the modular occurrence graphs,the practical use of the method is not as obvious,but we are convinced of its relevance in practical cases.

In the worst case,where all the transitions of the modules are shared,the synchronization graph will be isomorphic to the ordinary occurrence graph,i.e.have the same number of nodes and arcs,while the state spaces of the modules will have no arcs and as many disconnected nodes as the restriction of the occurrence graph nodes to the corresponding module.Thus,in the worst case there will be more nodes and as many arcs.

In the best case,where there is no synchronization at all, the synchronization graph will contain exactly one node(the initial one)and no arc.The individual state spaces of the modules will be the restriction of the usual occurrence graph to each module.They are also the normal occurrence graph obtained for the module.Thus the synchronous product of the graphs will be avoided.

In a real application there would often be a few transitions to be fused,and thus we can expect to be not very far from the best case.

Another parameter to consider that affects the size of the synchronization graph,and thereby of the modular state space,is the number of modules.In the large example of Section9.2,there were three modules and for each communication one of the modules did not participate.This implies that the local behaviour of this module appears in the initial markings of arcs in the synchronization graph, although it is useless.As suggested for the example,such a situation can be handled in practice by,for example,adding a?ag.Hence even if there is a large number of modules, their local behaviour would not be duplicated.

10.CONCLUSION

In this paper,we have presented a framework for modular analysis of PT-nets.We have considered sets of individual PT-nets related by transition fusion and by place fusion. Transition fusion can be used to model synchronous actions, while place fusion can be used to model shared data. Modular PT-nets form a simple,but yet very general, framework to discuss analysis of structured net models. We also introduced analysis of modular PT-nets by means of place?ows.It allows us to determine place?ows of the modular PT-net from the individual modules,only transition fusion needs to be checked globally.This means that it is not necessary to recompute all place?ows when a single module is modi?ed.Previous works(e.g.[10])have focused on modules communicating via places only.

Finally,we have presented a way of generating state spaces of systems exploiting their modular structure.We have shown how to construct this for systems without place fusion,and we have shown a translation from a modular PT-net with place fusion into a modular PT-net using transition fusion only.

If the results of De?nition7.5and Theorem7.1are used to construct the ordinary state space,then the modular state space method is only a faster way of generating the ordinary state space.Except for degenerated cases it is faster since the local behaviour is only developed once,not for each global state allowing this particular behaviour.

Moreover,it is possible to check properties using the modular state space directly,i.e.without unfolding to the ordinary state space.When designing algorithms there is often a trade-off between time and space complexity.For state space analysis it is attractive to have a rather fast way to decide properties,but the state space explosion problem makes it absolutely necessary to minimize memory usage.

A similar approach was presented in[14],but it starts by constructing the full state space of the modules,i.e.states that may not be reachable in the full system,as we point out in Section4.Several reduction methods have been proposed

to avoid the state space explosion problem,but they have drawbacks:they do not allow one to check all properties of the system or lead to a construction of the full ordinary state space(e.g.[15,16,9,17,18,19]).

One of the next steps in the development of the modular state space approach is to implement a?rst version of a tool supporting it.In Section7,we showed an abstract algorithm for the construction of modular state spaces, and in Section9,we argued that the capabilities of an existing tool could be used to emulate this algorithm. In Section8,the discussion of each property included an abstract algorithm which can be used directly in the implementation of a tool.

Having access to tool support will allow us to test the ideas for industrial size models.As described in Section9,many industrial models seem to have a structure which makes them suited for this kind of analysis,i.e.they consist of relatively independent parts.

REFERENCES

[1]Battiston,E.,De Cindio,F.and Mauri,G.(1991)OBJSA nets

systems:a class of high-level nets having objects as domains.

In G.Rozenberg(ed.),Advances in Petri Nets1988(Lect.

Notes Comput.Sci.,vol.340),pp.20–43.Springer,New York.

Also in Jensen,K.and Rozenberg,G.(eds)(1991)High-level Petri Nets:Theory and Application,pp.189–212.Springer.

[2]Christensen,S.and Damgaard Hansen,N.(1994)Coloured

Petri nets extended with channels for synchronous commu-nication.In R.Valette(ed.),Application and Theory of Petri Nets1994(Lect.Notes Comput.Sci.,vol.815),pp.159–178.

Springer,New York.Also available as:Daimi PB-390,ISSN 0105-8517.

[3]Huber,P.,Jensen,K.and Shapiro,R.M.(1990)Hierarchies in

coloured Petri nets.In G.Rozenberg(ed.),Advances in Petri Nets1990(Lect.Notes Comput.Sci.,vol.383),pp.342–416.

Springer,New York.Also in Jensen,K.and Rozenberg,G.

(eds)(1991)High-level Petri Nets:Theory and Application, pp.215–243.Springer.

[4]Jensen,K.(1992)Coloured Petri Nets.Basic Concepts,

Analysis Methods and Practical Use.Volume1,Basic Concepts.Monographs in Theoretical Computer Science.

Springer.

[5]Jensen,K.(1986)Coloured Petri nets.In G.Rozenberg(ed.),

Advances in Petri Nets1986,Part I(Lect.Notes Comput.Sci., vol.254),pp.248–299.Springer,New York.

[6]Reisig,W.(1991)Petri nets and algebraic speci?cations.

https://www.sodocs.net/doc/282130308.html,put.Sci.,80,1–34.Also in Jensen,K.and Rozenberg,G.(eds)(1991)High-level Petri Nets:Theory and Application,pp.137–170.Springer.

[7]Christensen,S.and Petrucci,L.(1992)Towards a modular

analysis of coloured Petri nets.In K.Jensen(ed.),Application and Theory of Petri Nets1992(Lect.Notes Comput.Sci., 616),pp.113–133.Springer,New York.Also available as: Daimi PB-391,ISSN0105-8517.

[8]Christensen,S.and Petrucci,L.(1995)Modular state space

analysis of coloured Petri nets.In G.de Michelis and M.Diaz (eds),Application and Theory of Petri Nets1995(Lect.Notes Comput.Sci.,vol.935),pp.201–217.Springer,New York. [9]Jensen,K.(1994)Coloured Petri Nets.Basic Concepts,

Analysis Methods and Practical Use.Volume2,Analysis Methods.Monographs in Theoretical Computer Science.

Springer.

[10]Narahari,Y.and Viswanadham,N.(1985)On the invariants

of coloured Petri nets.In G.Goos and J.Hartmanis(eds), Advances in Petri Nets1985(Lect.Notes Comput.Sci., vol.222),pp.330–341.Springer,New York.

[11]Christensen,S.and Jepsen,L.O.(1991)Modelling

and simulation of a network management system using hierarchical coloured Petri nets.In Erik Mosekilde(ed.), Proc.1991European Simulation Multiconference,ISBN0-911801-92-8,pp.47–52.An extended version available as: Daimi PB-349,ISSN0105-8517.

[12]Huber,P.and Pinci,V.O.(1991)A formal,executable

speci?cation of the ISDN basic rate interface.Proc12th Int.

Conf.on Application and Theory of Petri Nets,pp.1–21. [13]Design/CPN3.0.META Software and Aarhus University,

(1996)Also available as:

http://www.daimi.au.dk/designCPN.

[14]Notomi,M.and Murata,T.(1994)Hierarchical reachability

graph of bounded Petri nets for concurrent software analysis.

IEEE Trans.Software Eng.,20,325–336.

[15]Dimitrovici, C.,Hummert,U.and Petrucci,L.(1991)

Semantics,composition and net properties of algebraic high-level nets.In G.Rozenberg(ed.),Advances in Petri Nets1991 (Lect.Notes Comput.Sci.,vol.524),pp.93–117.Springer, New York.

[16]Finkel,A.and Petrucci,L.(1991)Avoiding state explosion

by composition of minimal covering graphs.Proc.3rd Computer-Aided Veri?cation Workshop(Lect.Notes Comput.

Sci.,vol.575),pp.169–180.Springer,New York.

[17]Valmari, A.(1990)Compositional state space generation.

Proc.11th Int.Conf.on Application and Theory of Petri Nets, pp.43–62.

[18]Valmari,A.(1990)Stubborn sets for reduced state space

generation.In Rozenberg,G.(ed.),Advances in Petri Nets 1990(Lect.Notes Comput.Sci.,vol.483),pp.491–515.

Springer,New York.

[19]Vernadat, F.and Michel F.(1997)Covering step graph

preserving failure semantics.In P.Az′e ma and G.Balbo (eds),Application and Theory of Petri Nets1997(Lect.Notes Comput.Sci.,vol.1248),pp.253–270.Springer,New York.

相关主题