W determines a place invariant iff: - Finding Stubborn Sets of Coloured Petri Nets Without Unfo

Finding Stubborn Sets of Coloured Petri Nets Without Unfolding

2. W determines a place invariant iff:

The following theorem is central to place invariant analysis of CP-nets. It states that the static property of Def. 21 (1) is sufficient to guarantee the dynamic property of Def.

21 (2).

Theorem 2 ( [67], Theorem 4.7) W is a place flow^Ï W determines a place invariant.

11.2.2 Stubborn Sets

State space construction with stubborn sets follows the same procedure as the con-struction of the full state space of a Petri net, with one exception. When processing a marking, a set of transitions (or binding elements in the case of a CP-net), the so-called stubborn set, is constructed. Only the enabled transitions (binding elements) in it are used to construct new markings. This reduces the number of new markings, and may lead to significant reduction in the size of the state space. To get correct analysis results, stubborn sets should be chosen such that the state space obtained with them (from now on called SS state space) preserves certain properties of the full state space.

11.2. BACKGROUND 135 The choice of stubborn sets thus depends on the properties that are being analysed or verified of the system. This has led to the development of several versions of the stubborn set method. However, it is common to almost all of them that the following theorem should hold:

Theorem 3 Let ^µ be any marking of the net, ^ÐaÑÒ¡Ó a stubborn set in ^µ , ^?ÔÖÕ ,

s~x!ÐaÑÒ¡Ó , and^s ^jls ^j«««jls ^×^{x!ÐaÑÒ¡Ó} .

1. If^µ ^¸^s©.µ; ^¸^{s© «««} ^¸^s ^¡» ^t©µ ^<» ^¸^s ^©µ ^¸^s©µyT , then^µ ^¸^st©.

2. If ^µ ^¸^st©µ> ^¸^sl¹©««« ^¸^s ^<» ^©Xµ ^¡» ^¸^s ^©Xµ and^µ ^¸^s©¬µyT, then there are ^µyT ,

µ T

,^««« ,^µ ^T such that^µ ^T¬¸^s©.µ ^T ^¸^{s© «««} ^¸^s ^©.µ ^T , and^µ ^¸^s©.µ ^T . ^Î It is also required that if^µ ^¶ is not a dead marking (a marking without enabled transi-tions), then^ÐÑÒ<Ó contains at least one enabled transition (binding element).

From this theorem it is possible to prove that the SS state space contains all the dead markings of the full state space. Furthermore, if the full state space contains an infinite occurrence sequence, then so does the SS state space. By adding extra restrictions to the construction of stubborn sets, the stubborn set method can be made to preserve more properties, but that topic is beyond our present interest. With PT-nets, Theorem 3 holds if stubborn sets are defined as follows:

Definition 22 LetO=ejlk¯jmjÅjp:R be a PT-net. The set ÐÑÒ<Ó Ø;k is stubborn in mark-ing^µ , if the following hold for everys~x!ÐaÑÒ¡Ó :

1. If^s ^xkBaµ ^¸^s ^©, then^¹s x!ÐaÑÒ¡Ó ^µ ¸s © .

2. If^Ùµ ^¸^st©, then q²xÚs5^µBODqrR¿ÅODqvjlsRcÛÆÚqØBÐÑÒ<Ó .

3. If^µ ^¸^st© , thenO=ÚsR=Ú Ø1ÐaÑÒ¡Ó . ^Î

Because this definition analyses the dependencies between transitions at a rather coarse level, it is not an “optimal” definition in the sense of yielding smallest possible stub-born sets and smallest SS state spaces, but we will use it in the following because of its simplicity. Once the basic ideas of our new CP-net stubborn set construction method are understood, they can be applied to more detailed dependency analysis if required.

Definition 22 gives a condition with which one can check whether a given set of transitions is a stubborn set in a given marking. Part (1) says that unless the marking is a dead marking, the stubborn set should contain at least one enabled transition. Parts (2) and (3) can be thought of as rules that, given a transition^s that is intended to be in the stubborn set, produce a set of other transitions that must be included. In the case of (3), the set is justO=ÚstR=ÚËØAÐaÑÒ¡Ó . Part (2) requires the selection of some place

q¦x!Ús , such that^q contains fewer tokens than^s wants to consume, and then produces

the set^Úq . If there are several such places, most stubborn set algorithms just make an arbitrary choice between them. A somewhat expensive algorithm that investigates all choices for^q is explained in [121].

Important for the rest of this paper is that the rules can be thought of as spanning a dependency graph: the nodes of the graph are the transitions, and there is an edge from^sM to^s if and only if the above rules (with a fixed arbitrary choice of the^q in

(2)) demand that if^s is in the stubborn set, then also^s must be. A stubborn set then corresponds to a set of transitions that contains an enabled transition and that is closed under reachability in the dependency graph. Therefore, to construct a stubborn set, it suffices to know the dependency graph and the set of enabled transitions.

In this paper we will not actually give any concrete algorithm for finding stubborn sets of CP-nets. Instead, we describe a method for obtaining a “good” dependency graph, from which one can construct “good” stubborn sets with the old algorithms that rely on dependency graphs.

11.3 The Necessity of Unfolding

Because every CP-net can be unfolded to an equivalent PT-net, and because good dependency graphs for PT-nets are known, one can always construct a stubborn set of a CP-net by first unfolding it to a PT-net. Unfolding is, however, often expensive, so one wants to avoid it. We will demonstrate in this section that, unfortunately, there are situations where good stubborn sets cannot be constructed — not even named, as a matter of fact — without unfolding or doing something equally expensive. We will do that by analysing the behaviour of the CP-net in Fig. 11.1. The CP-net has 9 places, 8 transitions, and all but two of its places have colour set fÜ[Ý¹±¹jÞ¹j«««Sjl7 . The remaining places ^q:ß and^q8à have a colour set containing only one element (colour) denoted(). The variablex is of type ^f . In the initial marking place^qr contains the tokens with colour^±««« . The remaining places are initially empty.

Let^á be any subset ofN, and let^µâ be the marking whereµ1ODqrtR+[1µ1ODq:ßKR+[

µ1ODq à R([µBODq:ã¹R[?ä , ^µBODq R[?µ1ODq:åKR [á , µBODq8æKR [?µ1ODqrçtR([f?Zèá , and

µ1ODq:éKR~[Æf . This marking can be reached from the initial marking by letting^sM and

s occur with suitable bindings followed by the occurrence of^s ^ç . We will consider the stubborn sets in^µ·â obtained by unfolding the CP-net to a PT-net, and then using Def. 22.

In ^µ ^â , all binding elements of ^s ^ß are enabled, and they are the only enabled binding elements in^µ·â . Assume that a binding elementODsßKj:¨QG[ê©=R where^ê¦x>á is in a stubborn set^ÐaÑÒ¡Ó . Rule (3) of Def. 22 forces us to include the binding elements

ODséKj:¨Që[ê©=R and ^ODs ^å j:¨Qì[êv©=R into ^ÐÑÒ<Ó . The binding element ^ODs ^å j:¨Qì[ê©=R is disabled exactly because there is no token of colour ^ê in^q ^ç . So rule (2) forces the inclusion of ODslKj:¨Q1[êv©=R into the stubborn set. Rule (2) should then be applied to

only input place of^s has no input transitions.

The binding elementODsév¨Q[íêv©=R is disabled because there is no token on^q:à . Rule (2) of Def. 22 forces us to include the binding elements^ODs ^æ j:¨Q[î^©=R into^ÐaÑÒ¡Ó , where

contain tokens with the same colour. For those values of^î that are not in ^á , rule (2) takes the analysis through the token element^ODq ^{jî^R} to^s but not to anywhere else. But when the value of^î is in^á , the analysis proceeds through^ODq ^æ ^{jî^R} toODsßKj:¨Q[èî^©=R. So we see that ^ÐÑÒ<Ó must contain all the binding elementsODsßKj:¨Qz[î^©=R where^î,xíá . On the other hand, the set consisting of those binding elements together with certain disabled binding elements satisfies Def. 22, and is thus stubborn in^µâ .

11.3. THE NECESSITY OF UNFOLDING 137

Figure 11.1: CP-net demonstrating the necessity of unfolding.

Rule (3) leads to^ODs ^å j:¨Q,[êv©=R, from which rule (2) takes us through^ODq ^å ^jêvR and further through^q:ß toODsßKj:¨Q>[Æî^©=R for every^{î¦x f} . As a conclusion, ^ÐaÑÒ¡Ó must contain all enabled binding elements.

There are thus only two possibilities for the stubborn set in^µ·â : either the stub-born set consists of the binding elements ^ODs ^ß j:¨Q[ðî^©=R where ^î1xÝá plus some disabled binding elements, or the stubborn set contains all enabled binding elements.

The existence of the above CP-net implies the following lower bound result.

Theorem 4 The size of the equivalent PT-net PTN is a lower bound on the

In document View of State Space Methods for Coloured Petri Nets (Sider 148-151)