03964.com

文档资料库 文档搜索专家

文档资料库 文档搜索专家

Petri Net Reachability Checking is Polynomial with Optimal Abstraction Hierarchies

Peep K¨ ngas u

Norwegian University of Science and Technology Department of Computer and Information Science peep@idi.ntnu.no

Abstract. The Petri net model is a powerful state transition oriented model to analyse, model and evaluate asynchronous and concurrent systems. However, like other state transition models, it encounters the state explosion problem. The size of the state space increases exponentially with the system complexity. This paper is concerned with a method of abstracting automatically Petri nets to simpler representations, which are ordered with respect to their size. Thus it becomes possible to check Petri net reachability incrementally. With incremental approach we can overcome the exponential nature of Petri net reachability checking. We show that by using the incremental approach, the upper computational complexity bound for Petri net reachability checking with optimal abstraction hierarchies is polynomial. The method we propose considers structural properties of a Petri net as well an initial and a ?nal marking. In addition to Petri net abstraction irrelevant transitions for a given reachability problem are determined. By removing these transitions from a net, impact of the state explosion problem is reduced even more.

1

Introduction

Petri nets and related graph models have been proposed for a wide variety of applications. These models are particularly suitable for representing concurrent hardware and software systems. A fundamental basis for studying the dynamic properties of systems described with Petri nets is the reachability property [11]. Unfortunately the complexity of Petri net reachability checking has been proven to be EXPSPACE-hard [10] in the general case. Although several less complex classes of nets have been determined [4], there still are problems, which can be presented only with “unconstrained” Petri nets. Therefore tools and algorithms for coping with that EXPSPACE-hard complexity are urgently needed. One possible way to reduce the state space is to apply net abstraction techniques in conjunction with Petri net reachability checking. Abstraction techniques have been used extensively in Arti?cial Intelligence (AI) planning [1, 3, 9] (especially in case-based and analogical reasoning), human problem solving and (automated) theorem proving [12]. Korf [8] has shown that while using abstraction it is possible to reduce the expected search space from O (n) to O (log n).

This improvement makes combinatorial problems tractable. For instance, if n is an exponential function of problem size, then log n is just linear (according to [8]). The essential reason why abstraction reduces complexity is that the total complexity is the sum of complexities of multiple searches, not their product. Thus with abstraction techniques we may cut solution search space from bd to kbd/k , where b is the branching factor and d is the depth of the search space while k is the ratio of abstraction space to base space. Although abstraction of Petri nets has been already explored for instance in [14, 13, 15], the proposed approaches are based on analysing merely structural properties of nets though in some cases also initial markings have been taken into account. The methodology we propose, on the contrary, considers structural properties as well the initial and the ?nal marking of a Petri net. While preparing the net for reachability checking we use the ?nal marking to determine transitions not relevant for the given reachability problem. Thereby it becomes possible to remove some transitions from a net, without changing the reachability result for the given ?nal marking. In that way more e?cient reachability checking could be implemented. The initial marking helps us to recognise the negative answer to a reachability problem. Thus, in some cases we can determine whether the ?nal marking is reachable from the initial one even before we start with reachability checking. Additionally we present a methodology for abstraction-based reachability checking and prove that if a Petri net has an optimal abstraction hierarchy, then the computational complexity of its reachability checking is polynomial. The remainder of the paper is as follows. In Section 2 we present the main de?nitions used in the rest of the paper. Section 3 introduces the abstraction algorithm and analyses its in?uence to Petri nets and their properties. In Section 4 reachability checking with abstraction is described. This methodology is evaluated in Section 5, where experimental results are presented and analysed. Section 6 gives an overview of related work and ?nally in Section 7 everything is summed up.

2

De?nitions

In this section we de?ne the Petri net concept and give the main notation and de?nitions to be used in the sequel. A (marked) Petri net is a 5-tuple N = (P, T, Pre, Post , M0 ), where P = {p1 , p2 , . . . , pn } is a ?nite set of places, T = {t1 , t2 , . . . , tm } is a ?nite set of transitions, Pre : P × T → N is the input incidence function, Post : T × P → N is the output incidence function and M0 : P → N is the initial marking. The number of places and transitions in a Petri net are represented with |P | and |T | respectively. The size S of a Petri net is the number of places it involves— S(N ) = |P |.

In the graphical representation, circles denote places and vertical bars denote transitions, tokens are represented with dots inside places. The Pre incidence function describes the oriented arcs connecting places to transitions. It represents for each transition t the fragment of the state in which the system has to be before the state change corresponding to t occurs. Pre(p, t) is the weight of the arc (p, t), Pre(p, t) = 0 denotes that the place p is not connected to transition t. The Post incidence function describes arcs from transitions to places. Analogously to Pre, Post (t, p) is the weight of the arc (t, p). The vectors Pre(., t) and Post (t, .) denote respectively all input and output arcs of transition t with their weights. The Petri net dynamics is given by ?ring enabled transitions, whose occurrence corresponds to a state change of the system modeled by the net. A transition t is enabled for a marking M , if M ≥ Pre(., t). This enabling condition is equivalent to ?p ∈ P, M (p) ≥ Pre(p, t). Only enabled transitions can be ?red. If M is a marking of N enabling a transition t, and M ′ is the marking derived by the ?ring of a transition t from M , then M ′ = (M ? Pre(., t))+ Post (t, .). The t ?ring is denoted as M → M ′ . Firing of a sequence of transitions s = t1 . . . tn tn t2 t1 s is de?ned as M0 → Mn = M0 → M1 → . . . → Mn , where Mi , i = 0 . . . n ? 1 is a marking of N enabling a transition ti+1 and Mi+1 is a result of ?ring ti+1 from marking Mi . In a Petri net N it is said that a marking Mg is reachable from a marking s M i? there exists a sequence of transitions s such that M → Mg . We call the reachability problem for Petri nets the problem of ?nding a ?ring sequence s to reach a given marking Mg from the initial marking M0 . The coverability problem (sometimes also called the submarking reachability problem), given two markings M0 and Mg , is de?ned as the problem of ?nding a ?ring sequence s to reach a marking Ms from the initial marking M0 such that Mg ≤ Ms . To simplify representing a marking M , we use symbolic representation M(M ), de?ned in the following way: M(M ) = {pM(p) | p ∈ P, M (p) ≥ 1}. We shall write p instead of p1 . Abstraction hierarchy H for a Petri net N is a total order of abstractions such that ?Ai , Aj ∈ H, i = j, (S(Ai (N )) < S(Aj (N ))) ? Aj (N ) ? Ai (N ). Due to the way we construct abstraction levels, it is not possible that S(Ai (N )) ≡ S(Aj (N )), if i = j. If p is a Petri net place, then Level (p) is the highest abstraction level where p may appear. To explain this notion let us consider Figure 4. There Level (X) ≡ 2, meaning that place X occurs in all abstracted versions of a net starting from level 2. Similarily Level (F ) ≡ 1 and Level (M ) ≡ 0 on the same ?gure. The function E(M ) = {p | p ∈ P, M (p) > 0} returns a set consisting of nonempty places according to a marking M . A Petri net marking M at abstraction level i is denoted by Ai (M ), where Ai (M )(p) = M (p) if Level(p) ≥ i 0 otherwise

Abstracted Petri net N at abstraction level i is de?ned as

′ Ai (N ) = (P ′ , T ′ , Pre, Post , M0 ),

where: – P ′ = {p | p ∈ P, Level (p) ≥ i} – T ′ = {t | t ∈ T, E(Ai (Pre(., t))) ∪ E(Ai (Post (t, .))) = ?} ′ – M0 = Ai (M0 ) At abstraction level 0 an original Petri net is presented—A0 (N ) ≡ N . We write Ti and Pi to denote respectively a set of transitions and places of a Petri net Ai (N ). Abstracted sequence of Petri net transitions s = t1 , t2 , . . . , tn , tj ∈ T, j = 1 . . . n at abstraction level i is de?ned as Ai (s) = sj | 0 < j ≤ |s|, sj ∈ Ti . Basically it means that at abstraction level i in a sequence s only these transitions are allowed, which exist in the abstracted Petri net at abstraction level i. Other transitions are just discarded. Opposite operation to abstration of ?ring sequences is re?nement. Re?nement Rl , k > l of a ?ring sequence s = t1 , t2 , . . . , tn , tj ∈ T, j = 1 . . . n k from abstraction level k to abstraction level l is de?ned as a sequence Rl (s) = k α0 , t1 , α1 , . . . αn?1 , tn , αn , where αi , i = 0 . . . n is a sequence of transitions from

l

t∈

i=k?1

Ti . This means that during re?nement only transitions from lower ab-

straction levels may be inserted to ?ring sequences. We write Rj instead of Rj . j+1 We de?ne a nulltransition as a transition t such that E(P re(., t)) ≡ ? ∧ E(P ost(t, .)) ≡ ?. Source transition is a transition t such that E(P re(., t)) ≡ ?∧E(P ost(t, .)) ≡ ?. In the following we shall write level to denote an abstraction level and by net we mean a Petri net.

3

Automatic abstraction of Petri nets

In this section we describe how to construct abstraction hierarchies for Petri nets. These hierarchies are later used to gradually re?ne an abstract solution during reachability checking. The abstraction method, we propose here for Petri nets, has been inspired from an abstraction method [7] from the ?eld of AI planning. The signi?cant di?erence of our method from previous Petri net abstraction methods is that net fragments are not replaced with more abstract nets. Instead we simplify nets by removing places which are not so relevant at particular abstraction levels and nulltransitions, which were formed by removing speci?c places from a net representation. 3.1 The abstraction algorithm

Given a problem space, which consists of a Petri net and a reachability problem s (?nding a sequence s so that M0 → Mg ), our algorithm reformulates the original

problem into more abstract ones. These more abstract ones are organised into an ordered hierarchy H with respect to their size. Thus the smallest representation is presented at the highest abstraction level and the largest respectively at the lowest (0) level. The original problem is mentioned in the further text also as the base problem, because all other representations are based on it. The ordered monotonicity property is used as the basis for generating abstraction hierarchies. This property captures the idea that if an abstract solution is re?ned, the structure of the abstract solution should be maintained. Hence elsi ements in a transition ?ring sequence si , such that Ai (M0 ) → Ai (Mg ), would not be reordered while extending this sequence at abstraction level i ? 1. The process of re?ning an abstract solution requires inserting additional transitions to achieve the tokens ignored at more abstract level. De?nition 1. Ordered monotonic re?nement R is a re?nement of an abstract solution s so that Ai (Rj (s)) = s, j ≤ i, where s is a sequence of transitions, i i denotes the abstraction level, where solution s was found and j is the target abstraction level. De?nition 2. Ordered monotonic hierarchy is an abstraction hierarchy with the property that for every solvable problem there exists an abstract solution that has a sequence of ordered monotonic re?nements into the base space. De?nition 3. Let A and B be arbitrary vertices in a directed graph. Then we say that they are strongly connected, if there exists a cycle with A as its initial and ?nal vertice such that this cycle includes vertice B. An ordered monotonic abstraction hierarchy is constructed by dividing places P in a Petri net N between abstraction levels such that the places at level i do not interact with any places at level i + 1. We say that places A and B do not interact with each other, if they are not strongly connected in the dependency graph of the particular Petri net. Our abstraction algorithm ?rst generates a graph representing dependencies (see Figure 1) between places in a Petri net, and then, using that graph, ?nally generates abstraction hierarchies (see Figure 2). The algorithm in Figure 1 considers every non-empty place, which has not yet been considered, from a given marking. Then all transitions, which increase the number of tokens in that place, are selected. Connections from the place under consideration to places a?ected by these transitions are created and search follows recursively, using Pre(., t ) as a new marking, until all reachable places have been processes. It has to be noted that although the algorithm starts from the goal marking Mg , weights of transition input arcs are considered when it proceeds recursively. After the dependency graph has been constructed, additional connections are created from places p ∈ E(Mg ) to places E(Pre(., t )) of transitions t, if E(Post (t , .)) ≡ ?. The latter is due to the fact that the dependency graph is extended by observing arcs (t , .) and, if E(Post (t , .)) ≡ ?, transition t is ignored. Anyway, these transitions may be needed during reachability checking.

Algorithm DetermineConstraints(graph, net, marking) inputs: a Petri net and a final marking output: constraints, which guarantee ordered monotonicity for a given marking begin for ?place ∈ E (marking)//a nonempty place is selected if not(ConstraintsDetermined (place, graph)) then ConstraintsDetermined (place, graph) ← true for ?t ∈ net.T //for all transitions if place ∈ E (net.Post(t, .)) then for ?p ∈ E (net.Post(t, .)) AddDirectedEdge(place, p, graph) end for for ?p ∈ E (net.Pre(., t)) AddDirectedEdge(place, p, graph) end for DetermineConstraints(graph, net, net.Pre(., t)) end if end for end if end for return graph end DetermineConstraints Fig. 1. Building a dependency graph.

Algorithm CreateHierarchy(net, marking) inputs: a Petri net and a final marking output: an ordered monotonic abstraction hierarchy begin graph ← DetermineConstraints({}, net, marking) components ← FindStronglyConnectedComponents(graph) partialOrder ← ConstructReducedGraph(graph, components) absHierarchy ← TopologicalSort(partialOrder ) return absHierarchy end CreateHierarchy Fig. 2. Creating an abstraction hierarchy.

To demonstrate the construction of abstraction hierarchies, let us consider the Petri net in Figure 4(a), where the reachability of marking Mg , M(Mg ) = {E, M, X 2 } is considered. The algorithm in Figure 1 starts with place E and sets it to be determined. The only transition having E in its outputs is H EIM . Thus edges E → I, E → M and E → H are constructed. Then the algorithm proceeds with new marking {H} at recursion level 2. H is set to be determined. The only transition having H in its output is EN H and thus edges H → E and H → N are constructed.

I

F

Y

E

M

N

X

H

IMNEH

F

XY

(a)

(b)

Fig. 3. A dependency graph (a) and strongly connected component groups (b) for a Petri net in Figure 4(a).

The algorithm proceeds at recursion level 3 with marking {E, N }. Since E was already set to be determined, it is not considered anymore. Thus N is selected. Transition M N has N in its outputs and thus edge N → M is constructed. The algorithm proceeds recursively at level 4 with {M } as its marking. M is set to be determined, transition H EIM is the only transition having M in its output and therefore edges M → I, M → E and M → H are constructed. The algorithm proceeds with marking {H} at recursion level 5. However, H has already been processed and is not considered anymore. Since there is nothing to do in previous recursion levels, the algorithm returns to level 1 and chooses X for its next target. X is set to be determined, transition X2Y2 X2 is chosen and edge X → Y is inserted. The algorithm proceeds at recursion level 2 with {X, Y } as an input marking. Y is chosen, transition FX Y2 is found and edges Y → F and Y → X are inserted. Then the algorithm proceeds at recursion level 3 witn {F, X} as its input marking. Since F is selected, transition I7 F is found and edge F → I is inserted. Now the algorithm proceeds with marking {I} at recursion level 4. Transition H EIM is selected and edges I → E, I → M plus I → H are generated. Finally the algorithm proceeds at recursion level 5 with {H} as its input marking. However, since there are no nondetermined places left, the algorithm returns to its initial recursion level and returns a graph containing all the edges pointed out so far. After applying the algorithm in Figure 1, ?rst a dependency graph in Figure 3(a) is generated. In that ?gure for the sake of simplicity we presented every

two unidirectional edges in opposite directions between the same pair of elements as a bidirectional edge. A directed edge from node A to node B in the graph indicates that A cannot occur lower in the abstraction hierarchy than B. Hence a bidirectional edge between two nodes tells us that these nodes should appear at the same abstraction level.

X2Y2_X2 2 2 2

X

FX_Y2 2 I7_F 7

Y

F

X2Y2_X2 2 2 2

I M

H_EIM

X2Y2_X2 2 2 2

E

EN_H

M_N

X

FX_Y2 2 I7_F

H N

Y

X

FX_Y2 2

F

Y

(a) A0 (N ) ≡ N .

(b) A1 (N ).

(c) A2 (N ).

Fig. 4. Representation of the Petri net N at di?erent abstraction levels with M(Mg ) = {E, M, X 2 } and M(M0 ) = {E, M, X 3 }.

Given the algorithm in Figure 2 we ?nd as a second step strongly connected components. In that way we end up with 3 sets of strongly connected components—{I, M, N, E, H}, {F } and {X, Y }. By representing every group of strongly connected components as a separate node, we end up with a partial ordering in Figure 3(b). In the current example it is also a total order and would represent an achieved abstraction hierarchy. Otherwise we would have to apply topological sort to generate all possible total orderings and then select between those a suitable one. The abstraction hierarchy in Figure 3(b) determines that at the lowest abstraction level all places are presented, at the ?rst level all except I, M , N , E, H (thus F , X, Y ) are presented. And at the second abstraction level there are only X and Y . Given this abstraction hierarchy, two new Petri nets in Figure 4(b) and Figure 4(c) are constructed for abstraction levels 1 and 2, respectively. At abstraction level 0 the original Petri net is represented. Basically, the abstraction algorithm in Figure 2 divides Petri nets into subnets to ?t the general tree structure presented in Figure 5. Each subnet Ni there consists of new transitions at abstraction level i. Every leaf subnet of that tree involves at least one place p ∈ E(Mg ). There can be several transitions between di?erent subnets—every ti in Figure 5 represents a number (at least one) of transitions between two subnets. However, the direction of transitions in set ti

is the same—from lower level to higher level net. Transitions ti are abstracted to source transitions at level i, but at abstraction level i ? 1 they are not source transitions anymore.

t1

N0 N1

t2

N2

...

t3

N3

...

Fig. 5. The general structure of abstracted nets.

This structure is formed because all places p ∈ E(Post (t, .)) of a transition t are presented at the same abstraction level. Elements in E(Pre(., t)) belong to the same and/or to an lower abstraction level than elements in E(Post (t, .)). Ordered monotonic re?nement assures us that if a marking Ai (Mg ), i > 0 is not reachable at abstraction level i, Mg would not be reachable in the original Petri net N either. Therefore we do not need to explore the entire search space to get acknowledged about it. Every abstracted net at level i includes either at least one token from the initial marking (E(Ai (N )) ≡ ?) or at least one source transition. Every source transition represents a transition wherefrom tokens may enter the subnet. Therefore, if the marking Ai (Mg ) is not reachable under these relaxing conditions, the marking Ai (Mg ) would not be reachable without particular relaxing conditions either. 3.2 The role of the initial marking

While building a dependency graph for abstraction, dependencies between Petri net places are detected. If it should happen that at least one place p ∈ E(M0 ) is not included in the dependency graph and it does not occur in E(Mg ) either, s then there is no sequence of transitions s that M0 → Mg . This applies i? there are no sink transitions, which could consume tokens in p. Theorem 1. Given a Petri net N and a set of edges De of dependency graph D, which was constructed using N and Mg , then if it is satis?ed that ?p.(p ∈ E(M0 ) ∧ p ∈ E(Mg ) ∧ p ∈ De ∧ ??t.E(Post (t, .)) ≡ ?), then goal marking Mg is not reachable from marking M0 of Petri net N . Proof. While ?nding dependencies between Petri net places through dependency graph construction, roughly a way for token propagation is estimated for reaching the marking Mg and places on the way are inserted to the graph. Therefore, if

not all places p ∈ E(M0 ) are included in the dependency graph, then there is no way to reach from the marking M0 the marking Mg . Anyway, some tokens in the initial marking may be not ?red during reachability checking and thus they exist both in markings M0 and Mg . In that case the missing place from a dependency graph does not indicate that the marking Mg is not reachable. Similarily, sink transitions have to be considered, since they only consume tokens and therefore are rejected, when generating a dependency graph. This case is illustrated in Figure 6, where a dependency graph is generated for the marking M(Mg ) = {F }. As it can be seen in Figure 6(b) the Petri net place B, although having a token in the marking M0 , is not included in the dependency graph in Figure 6(b). The same applies for place A. Therefore the marking Mg is not reachable.

A_E A BC_D B C_FE C F D E

F C

E

(a)

(b)

Fig. 6. A Petri net (a) with the initial marking M0 , M(M0 ) = {A, B, C} and the marking Mg , M(Mg ) = {F } plus the corresponding dependency graph (b).

3.3

Removing redundant transitions

After the places, where tokens are possibly propagated through, have been determined, we can throw away all transitions, which are connected at least to one place which is not included in the dependency graph. In that way the search space would be pruned and search made more e?cient. Reachability result would not be a?ected by removing these transitions. Theorem 2. Given a Petri net N and a set of edges De of dependency graph D, which was constructed using N and Mg , we can discard all transitions t ∈ T , which satisfy condition ?p.((p ∈ E(Pre(., t)) ∨ p ∈ E(Post (t, .))) ∧ p ∈ De ∧ s E(Post (t, .)) ≡ ?) without a?ecting reachability result for M0 → Mg . Proof. If there is a transition t ∈ T of a Petri net N such that ?p.((p ∈ E(Pre(., t)) ∨ p ∈ E(Post (t, .))) ∧ p ∈ De ), then it means that the transition t was not considered during construction of dependency graph D. Therefore

the transition is not considered relevant for achieving marking Mg and can be discarded. Transition reduction is illustrated in Figure 7, where a dependency graph is generated for the marking Mg , M(Mg ) = {F, E 2 }. Since B and D are not present in the dependency graph, they are considered irrelevant for the current reachability problem. Therefore all transitions t such that Pre(B, t) ∈ Pre or Pre(D, t) ∈ Pre or Post (t, B) ∈ Post or Post (t, D) ∈ Post can be removed without a?ecting the reachability result of the original problem. Hence the transition BC D can be removed.

A_E A BC_D B C_FE C F D E

F C

E

A

(a)

(b)

Fig. 7. A Petri net (a) including redundant transitions for Mg , M(Mg ) = {F, E 2 } plus the corresponding dependency graph (b).

3.4

The computational complexity of abstraction

According to [7] the complexity of building the dependency graph is O (n ? o ? l ), where n is the number of di?erent places in a Petri net, o is the maximum number of transitions t such that for any place p P re(p, t) > 0 or P ost(t, p) > 0, and l is the maximum number of di?erent places p such that P ost(t, p) > 0 with any transition t. The complexity of building an hierarchy is also O (n ? o ? l ), since the complexity of the graph algorithms is bounded by the number of edges, which is bounded in our case by n ? o ? l.

4

Reachability checking with abstraction

After an abstraction hierarchy has been generated, we start hierarchical reachability checking from the highest abstraction level by mapping the original Petri net N to Ah (N ), where h denotes the highest abstraction level. First we ?nd a sh sequence sh of transitions t ∈ Th so that Ah (M0 ) → Ah (Mg ). Then we gradually re?ne this sequence while moving lower in the abstraction hierarchy until we reach the lowest level of the abstraction hierarchy. If it should turn out that

from a certain abstraction level there is no re?nement to a lower abstraction level for a sequence, then the marking Mg is considered not reachable and search is halted. De?nition 4. New transitions t ∈ Tnew i at abstraction level i are de?ned as Tnew i = Ti \ (Ti ∩ Ti+1 ), i = 0 . . . n, with exception Tnew n = Tn , where n is the highest abstraction level, Ti is a set of transitions in a Petri net Ai (N ) and N is the original Petri net. It is crucial to note that at every abstraction level i only transitions t ∈ Tnew i may be used during re?nement. This is the basic search space reduction mechanism, supported by abstraction, which divides the initial search space into subspaces. A sequence of transitions, which shows the reachability of a marking Mg , found at an abstraction level higher than 0 may be viewed as a sequence including “gaps”, which have to be ?lled at a lower level of abstraction. It has to be emphasised that at one abstraction level several solutions may be found and not all of these, if any, lead to a solution at less abstract level. Thus several abstract solutions may have to be tried before a solution for less abstract problem is found. The ordered monotonicity determines that while extending a ?ring sequence s at a lower abstraction level with transitions, we can insert only new transitions, whereas the transitions which are already in s, after enriching their representation with places permitted at that abstraction level (if needed), possibly determine new submarking reachability problems we have to solve in order to solve the general reachability problem. Thus in that way we reduce one single reachability problem into several reachability problems and reduce distance between submarkings. By dividing transitions between di?erent abstraction levels the branching factor of search space is decreased. Following the former idea we de?ne the optimal abstraction hierarchy as an abstraction hierarchy, where at each level exactly one new transition is introduced and a Petri net at the highest abstraction level includes exactly one transition. De?nition 5. An optimal abstraction hierarchy Ho of a Petri net N is an abstraction hierarchy with n = |T | abstraction levels starting from level 0. Therefore, in Ho , |Ti \ (Ti ∩ Ti+1 )| = 1, i = 0 . . . n ? 2 and |Tn?1 | = 1. Theorem 3. Given that an optimal abstraction hierarchy Ho is used, computas tional complexity of solving a reachability problem M0 → Mg of a Petri net N with our algorithm is O(|T | ? |s|), where |T | is the number of transitions in a net and |s| is the expected length of the ?ring sequence s. Proof. We de?ne the exponential complexity of Petri net reachability checking l as lts , where lt is the number of transitions in a Petri net N and ls = |s| is the s length of a transition ?ring sequence s such that M0 → Mg . Since at the base abstraction level (level 0) of Ho we have ls transitions in the sequence s, there

are at every abstraction level maximally ls gaps, which have to be ?lled. By assuming that there are lh abstraction levels in Ho , the resulting complexity is O(lh ? ls ? (lt /lh )ls ). Since we assumed usage of an optimal abstraction hierarchy (lt ≡ lh ), the exponential complexity of Petri net reachability checking is reduced to O(lh ? ls ? 1ls ) = O(lh ? ls ), which is polynomial.

5

Experimental results for abstraction-based reachability checking

All experiments were performed with the RAPS tool1 , where we applied basically on-the-?y depth-?rst search over a reachability graph. The maximum search depth was 30. The results are summarised in Table 1. Columns covered by labels “Collapsing” (state space collapsing with KarpMiller algorithm [6]) and “No collapsing” include numbers, which represent how many Petri net transitions were ?red before reachability was detected. “—” in ?elds of the table indicates that reachability was not detected. This illustrates that, if we apply Karp-Miller algorithm together with abstraction, we may not discover that a marking is reachable. Columns “Problem”, “Sol length” and “Abs levels” represent information respectively about net descriptions, ?ring sequence lengths and the number of abstraction levels per problem, if abstraction was used. “Abs” and “No abs” distinguish whether abstraction was used or not. “Collapsing” and “No collapsing” in turn determine whether state space collapsing [6] was applied or not. |T | and |P |, as de?ned in Section 2, in column headers denote to the numbers of transitions and places in a sample net.

Table 1. Reachability checking with and without abstraction. Collapsing Abs No abs 8 179 — 181 4 17 6 8 2 5 — 22 No collapsing Abs No abs Sol length Abs levels 26 81 24 3 28 69 26 6 10 99 10 2 6 8 6 3 2 5 2 4 9 22 9 3

Problem Figure 4(a) Figure 8(a) Figure 8(b) Figure 8(c) Figure 8(d) Figure 8(e)

|T | 6 8 4 4 5 8

|P | 8 11 6 6 8 11

M(Mg ) {E, M, X 2 } {E, M, X 2 } {E, M, F } {F, M } {F } {E, I 2 }

Dashed lines in ?gures of Figure 8 separate di?erent abstraction levels. Thus it is easy to follow how abstraction levels were formed for di?erent nets and reachability problems. If a fragment of a net is not encircled with a dashed line, then this part is discarded as irrelevant for a given reachability problem. The

1

Downloadable from http://www.idi.ntnu.no/~peep/RAPS.

letter L followed by a number indicates there the abstraction level of a particular subnet.

L5

2

X2Y2_X2 2 2

I2_F 2

G

L2 F

H

E_GH

GH_E

X

I7_F 7

L1 I J

C_IJK

L4 F

W_M

FX_Y2 2

JK_I

Y

I

I3_F 3

E

M L1

D_E

G

H

EF_GH

F

L1

BN_IM

I M

H_EIM

I

W L2

H_EIM

D

M_N

F

C_F

L3

L2

M L0

E

C_EF

F

K

C_D

L2 C

C_D

E

EN_H

M_N

UV_W

E

EN_H

M_N

C

AB_C

AB_C

D

D_AB

B

NU_B

N

H U L3 N L1 V L0

H

A B L0

L0 A B

N

U L0

L1

(a) 1.

(b) 2.

(c) 3.

(d) 4.

(e) 5.

Fig. 8. Sample nets used in experiments.

Although one may argue that only toy examples were considered while perfoming experiments, these examples still illustrate advantages of abstractionbased reachability checking over ordinary reachability checking. One can see that the di?erence between “ordinary” and abstraction-based reachability checking may be up to 22 times in the current case. These experimental results encourage us to apply abstraction-based reachability checking for larger problems. While experimenting with abstraction and Petri nets we experienced cases, where with abstraction, although more Petri net transitions were ?red, less overall time was spent on it than with ordinary reachability checking. This “anomaly” arises from the way we probe whether a transition is enabled or not. In the case of ordinary reachability analysis one vector is subtracted from another and then it is checked whether the result is not negative. Anyway, if we use abstraction, then transitions indicate to a speci?c abstraction level where they may be applied only. In that case a lot of transitions are disquali?ed just by comparing the integer indicating the abstraction level where the transition may be ?red. And comparing two integers is computationally cheaper than comparing two state vectors. Therefore, by using abstraction, we do not search blindly anymore, but use instead abstraction as search heuristics.

6

Related work

Abstraction of Petri nets has been explored previously by several researchers [14, 13, 15]. These approaches are based on analysing structural properties of a net. Abstraction is performed by substituting subnets with single transitions or places. Berthelot [2] considers Petri net reduction by applying a set of transformation rules. Although this work does not consider abstraction itself, some of the transformation rules may be viewed as abstraction operators.

Several abstraction techniques have been proposed in AI planning and theorem proving disciplines. The ?rst explicit use of abstraction in automated deduction was in the planning version of GPS [12]. Other approaches to automatic generation of abstraction spaces in the AI planning ?eld include [1, 3, 9]. In [5] another abstraction technique, STAR, for AI planning is proposed. Unfortunately it abstracts the generated state space and not the initial problem representation. The main idea there is to collapse a state and its adjacent states into a single one thereby reducing the state space. Although this methodolody may turn out to be useful for applications, where a Petri net state space is ?rst generated and then analysed, we are interested in on-the-?y reachability checking.

7

Conclusions

In this paper we presented an algorithm for automatically abstracting Petri nets. While other approaches of abstracting Petri nets are based merely on the structural properties of nets, we considered also the initial and the ?nal marking, whose reachability has to be checked. Our algorithm ?rst generates an abstraction hierarchy, which divides an original Petri net into several abstracted representations. These abstracted nets are ordered into an abstraction hierarchy by their size. Abstraction hierarchies are generated by observing connections between transitions and places of nets. Given a net and the ?nal marking, ?rst a dependency graph is generated, which determines transitions, possibly to be ?red in order to reach the ?nal marking. Then this graph is transformed into abstraction hierarchies. The greatest bene?ts of our abstraction and reachability checking algorithms are achieved on tree-like Petri net structures like the one depictured in Figure 5. If a whole Petri net represents a tree, optimal abstraction hierarchies are constructed. By using optimal abstraction hierarchies the computational complexity of reachability checking is reduced to polynomial. It turns out that the dependency graph, which is a byproduct of the abstraction algorithm, can be used also to determine these transitions in a net, which are not relevant for solving a given reachability problem. In some cases the dependency graph also helps to determine the lack of a solution even before starting with reachability checking. Additionally we sketched an algorithm for using generated abstraction hierarchies for reachability checking. Reachability checking starts from the highest abstraction level. Then a ?ring sequence of transitions reaching a particular marking is gradually extended until the lowest abstraction level is reached. Finally experimental results were presented, which show that while using our abstraction methodology roughly up to 20 times less Petri net transitions are ?red during reachability checking. These results motivate us to proceed with research on abstraction-based reachability checking.

Acknowledgements

This work was partially supported by the Norwegian Research Foundation in the framework of Information and Communication Technology (IKT-2010) program— the ADIS project. The author would like to thank the anonymous referees for their comments.

References

1. J. S. Anderson and A. M. Farley. Plan abstraction based on operator generalization. In Proceedings of the Seventh National Conference on Arti?cial Intelligence, Saint Paul, MN, 1988, pages 100–104, 1988. 2. G. Berthelot. Transformations and decompositions of nets. In Petri Nets: Central Models and Their Properties, Advances in Petri Nets ’86, West Germany, Bad Honnef, September 1986, volume 254 of Lecture Notes in Computer Science, pages 359–376. Springer-Verlag, 1987. 3. J. Christensen. Automatic Abstraction in Planning. PhD thesis, Department of Computer Science, Stanford University, 1991. 4. J. Esparza and M. Nielsen. Decidability issues for Petri nets—a survey. Journal of Information Processing and Cybernetics, 30:143–160, 1995. 5. R. C. Holte, T. Mkadmi, R. M. Zimmer, and A. J. MacDonald. Speeding up problem solving by abstraction: A graph oriented approach. Arti?cial Intelligence, 85:321–361, 1996. 6. R. M. Karp and R. E. Miller. Parallel program schemata. Journal of Computer and Systems Sciences, 3(2):147–195, 1969. 7. C. A. Knoblock. Automatically generating abstractions for planning. Arti?cial Intelligence, 68:243–302, 1994. 8. R. E. Korf. Planning as search: A quantitative approach. Arti?cial Intelligence, 33:65–88, 1987. 9. A. Y. Levy. Creating abstractions using relevance reasoning. In Proceedings of the Twelfth National Conference on Arti?cial Intelligence (AAAI’94), pages 588–594, 1994. 10. R. J. Lipton. The reachability problem requires exponential space. Research Report 62, Department of Computer Science, Yale University, 1976. 11. T. Murata. Petri nets: Properties, analysis and applications. Proceedings of IEEE, 77(4):541–580, 1989. 12. A. Newell and H. A. Simon. Human Problem Solving. Prentice-Hall, 1972. 13. J.-S. Song, S. Satoh, and C. V. Ramamoorthy. The abstraction of petri net. In Proceedings of TENCON’87, Seoul, Korea, August 25–28, 1987, pages 467–471. IEEE Press, 1987. 14. I. Suzuki and T. Murata. A method for stepwise re?nement and abstraction of petri nets. Journal of Computer and System Sciences, 27:51–76, 1983. 15. R. Vallette. Analysis of petri nets by stepwise re?nement. Journal of Computer and System Sciences, 18(1):35–46, 1979.

相关文章:

- The use of Petri nets to analyze coherent fault trees_图文_....pdf
- The fault tree
*is*represented by a*Petri**net*, and using*reachability*... the modeling capability of the system at various levels of*abstraction*. ...

- Reachability is decidable for ground AC rewrite systems.pdf
- 0 by applying to the following
*abstraction*rules as j Abstract 1: a !...The relation R1 corresponds to*Petri**net**reachability*, which*is*decidable 3...

- The sat problem of mu-calculus over Petri Nets.pdf
- cation : given a system or its
*abstraction*and ...The model*checking*problem for*Petri**nets**is*...The mu-calculus sentence provides*reachability*, ...

- ...and Infinite Model Checking of Dual Transition Petri Net ....pdf
- An approach aimed to reduce the complexity of
*reachability*trees in*Petri*...*Abstraction**is*a key issue in in?nite model*checking*. When reasoning about...

- Meta-Modelling, Graph Transformation and Model Checking for ....pdf
- and multiple levels of
*abstraction*for the modelling, analysis and ...3. The*Reachability*Graph for the*Petri**Net**with*Priorities. 3 Related ...

- Hierarchical Object-Oriented Petri Net Modeling Method based ....pdf
*Petri**nets*for structural analysis and incremental*reachability*analysis for ...The abstract place shows different behaviors depending on that the*abstraction*...

- Roméo A Tool for Analyzing time Petri nets.pdf
- Roméo A Tool for Analyzing time
*Petri**nets*_专业...y model-*checking*of*reachability*properties. It ...*abstraction*Oris DBM SCGc Timed analysis RTTL...

- 17. Petri Net Analysis (PNA).pdf
- 17.
*Petri**Net*Analysis (PNA)_能源/化工_工程...*Reachability*graphs show all of the possible ...*abstraction*, its mathematical representation can ...

- Optimization in Graph Transformation Systems Using Petri Net ....pdf
- A
*Petri**net**abstraction*of GTS. These cuts*are*...Varr?. Joint optimization and*reachability*analysis...*Optimal*scheduling using branch and bound*with*...

- D. A Petri Net Based Methodology to Integrate Qualitative and....pdf
- The results gained depend on the
*abstraction*level of the underlying*net*.... In model*checking*, the*reachability*graph of a*Petri**net**is*interpreted...

- CTL model checking for time Petri nets.pdf
- CTL model
*checking*for time*Petri**nets*_专业资料...erent kinds of properties (*reachability*, LTL, ...3. TPN STATE SPACE*ABSTRACTIONS**Abstraction*...

- Reachability and Timing Analysis in Data Flow Networks A Case....pdf
*abstraction*where the designer does not want to deal*with*the exact ...The equivalent*Petri**net*preserves the timing and*reachability*properties of ...

- Groebner Basis Procedures for Testing Petri Nets.pdf
- The
*reachability*problem for a*Petri**net*N*with*...De?nition 3.6 (*Polynomial*Associated*with*a ...[6] A.Chandler : “Optimum and Safe Design of...

- Fleischhack Model Checking of Time Petri Nets Based on ....pdf
- Fleischhack Model
*Checking*of Time*Petri**Nets*...(an*abstraction*of) the McMillan unfolding of ...The*reachability**checking*algorithm*is*based on a...

- High level petri nets analysis with Helena.pdf
- presents the high level
*Petri**nets*analyzer Helena...*abstraction*(or slicing) of a program and to ... Quasar does not perform*reachability*analysis but...

- Monotonic extensions of petri nets Forward and backward ....pdf
- considering the counting
*abstraction*, the model of (in?nite)*Petri**Nets*...of the previous algorithm when we want to answer*reachability*of an upward...

- Monotonic extensions of petri nets Forward and backward ....pdf
- counting
*abstraction*, the model of (in?nite)*Petri**Nets*and its ?...But note that, for those cases, we only*need*the*reachability*relation ...

- underlying a stochastic Petri net.pdf
- underlying a stochastic
*Petri**net*_专业资料。A ...The*polynomial*and exponential abled in the ...4. The*reachability*graph for the model. sure ...

- A Petri net-based approach for computer-aided implementation ....pdf
- A
*Petri**net*-based approach for computer-aided implementation in FPGA of ...*optimal*path in an extended version of the*reachability*graph of the TPN....

- Control and Error Recovery of Petri Net Models with Event ....pdf
- construction of the
*reachability*graph of a*Petri**net*controlled in a ...We observe that: The closed loop behavior*with*observer*is*not*optimal*. ...

更多相关标签:

- Andor hierarchies and round abstraction
- Abstract—The software Petri Net Toolbox, dealing with Petri
- a Petri net based expert system with memory
- Liveness and finiteness of Large Systems with S_Petri Net
- Stotts - Petri-Net-Based Hypertext Document Structure with Browsing Semantics - 1989
- Planning with Abstraction Hierarchies can be Exponentially Less Efficient
- Paper III Planning with Abstraction Hierarchies can be Exponentially Less Efficient
- Online Partial Evaluation,Infinite Model Checking,and Petri net algorithms
- Bounded Model Checking for Reachability Testing in Time Petri Nets
- Data Encapsulation and Data Abstraction with Petri Nets -- a graphical Visualization of Mod