Exploitation of the structure of a Petri net is widely believed to be an inecient approach to solving the reachability problem. We show that structure analysis can be combined with integer programming and partial order reduction to obtain a fast reachability solver.
The reachability problem for Petri nets, i.e. if a nal marking can be reached in a given net from the initial marking, is known to be decidable [May84,Kos82,Lam92] but EXPSPACE-hard [Lip76]. Ecient tools exist, but they cannot solve all instances of the problem (at least not in a lifetime). Model checkers, symbolic [CMS06] or with partial order reduction [Wol10], have been used successfully to solve quite large reachability problems.
Here we present an approach that is a mixture of several methods, the main ones being integer programming and structure analysis. The marking equation, a linear system of integer equations, is known to be a necessary condition for reachability. When a solution of the marking equation is found, it may represent the parikh vector of a ring sequence solving the reachability problem or not. If it does, the ring sequence needs to be found, otherwise the marking equation can be constrained to discriminate the found solution. The needed constraints are found by analysing the net structure. Consider the example net in Fig. 1. s b1 a1 c1 y1 x1 z b2 c2 y2 b3 a2 x2 The marking equation m0 + Cx = mf (where m0 = 1s, mf = 1s + 3f are initial and nal marking and C is the incidence matrix of the net N ) can be solved by any integer programming tool. The smallest solution is 3 a1 + 3a2 + 3‘, i.e. each of the three transitions should re three times (in some unknown order). If we notice that a token is needed on y2 to re a2, but none of the three transitions produces such a token, we might add a constraint \a token should be produced on y2" to our marking equation to discriminate our rst solution. A still viable solution is now 2a1 + 2a2 + b1 + b2 + b3 + 3‘, as b2 can produce that token. But now a token on z is missing. If required by a similar constraint, we come to 2a1 + 2a2 + b1 + c1 + b2 + c2 + b3 + 3‘ but the token on y2 is still not there when needed for a2. Requiring a higher token production on y2 will nally lead to the solution 3b1 + c1 + 3b2 + c2 + 3b3 + 3‘ and now we \only" have to nd a correct ring sequence, e.g. b1c1b2b3‘b1b2b3‘b1b2c2b3‘. 2
We expect the reader to be familiar with the basic Petri net terminology and some knowledge in linear algebra. All Petri nets here are general ones, i.e. they may have arbitrary multi-arcs including loops. Vectors are sometimes written as nite sums (multisets) over the vector’s domain.
Denition 1 (Reachability problem). A reachability problem is the question, when given a tuple (N; m; m0) of a Petri net N = (S; T; F ) and two markings m; m0 2 NS , whether m0 can be reached from m, i.e. if 2 T with m[ im0 exists. The reachability problem then is the set RP = f(N; m; m0) j N = (S; T , F ) is a Petri net, m; m0 2 NS , 9 2 T : m[ im0g. A reachability problem (N; m; m0) is also called an instance of RP, to which the answer is \yes" if (N; m; m0) 2 RP and \no" otherwise.
The reachability problem is decidable [May84] and making it solvable for as many instances as possible is our goal. It is well-known that a necessary condition for a positive answer to a reachability problem is the feasibility of the marking equation.
Denition 2 (Marking equation). For a Petri net N = (S; T; F ) let C 2 NS T , dened by Cs;t = F (t; s) F (s; t), be the incidence matrix of N . For two markings m and m0 the system of linear equations m + Cx = m0 is the marking equation of N for m and m0. A vector x 2 NT fullling the equation is called a solution.
For a ring sequence the Parikh vector }( ): T ! N is dened by }( )(t) = #t( ), where #t( ) is the number of occurrences of t in . If x is a solution of the marking equation m + Cx = m0, any ring sequence with }( ) = x and m[ i positively solves the instance ( N; m; m0) of the reachability problem. From linear algebra the following is known: Theorem 1 (Solution space). For any marking equation m + Cx = m0 over a net N = (S; T; F ) there are nite sets of base vectors B NT and pePriod vectors P NT such that all and only the solutions can be expressed as b + i nipi with b 2 B, pi 2 P , and ni 2 N.
In other words, the solution space is a semilinear set over nonnegative integer vectors. Period vectors are nonnegative T -invariants where for a ring sequence with }( ) to be a T -invariant, m[ im must hold for all markings m enabling . Adding a T -invariant to a solution of the marking equation will produce another solution. Apart from multiples, our example net from Fig. 1 contains only one nonnegative T -invariant: c1 + c2. The base vectors take the form i(a1 + a2) + (3 i)(b1 + b2 + b3) + 3‘ with 0 i 3. 3
Integer Programming (IP) solvers come in two avors. Some can compute the whole solution space at once, but are too slow for practical purposes, others can only compute one solution. The latter, like lp solve [BEN10], can be directed to compute a minimal solution (with respect to the sum over all values, leading to shortest ring sequences). Constraints can be used to discriminate a solution and force the IP solver to produce another (greater) one until no more solutions exist.
Denition 3 (Constraints). We dene two forms of constraints, both being linear inequations over transitions: { a jump constraint takes the form t < n wPitkh n 2 N for a transition t. { an increment constraint takes the form i=1 niti n with ni 2 N, n 2 N, and transitions ti.
Assume a linear system with a minimal solution b with b(t) = n, then an additional jump constraint t < n discriminates b and leads to an incomparable solution. An increment constraint on the other hand may enforce a greater solution, adding some T -invariant to b. This idea is depicted in Fig. 2 where dashed arrows represent jumps and normal arrows the adding of T -invariants.
Since the solution space is semilinear we need jumps to get to other solution cones and increment constraints to go upwards in a cone. Jump and increment constraints can contradict each other, but it is possible to remove a jump constraint. Assume we have a solution a before and a solution b after adding a jump constraint. We construct one increment constraint per transition t with t b(t). This enforces at least the solution b. Removing the jump constraint now will not lead to an old (smaller) solution, especially not to a. 4
Let us rst argue that for a marking equation, any of the minimal solution vectors in B can be obtained by using jump constraints. For two solutions b and b0 let b b0 if we can change the solution our IP solver produces from b to b0 by adding new constraints to a system consisting of the marking equation plus some (old) constraints.
Lemma 1 (Jumps to minimal solutions). Let b; b0 2 B (b 6= b0) be base vectors of the solution space of the marking equation m + Cx = m0 plus some set of constraints C. Assume b to be the minimal solution of the system. Then, we can obtain b0 as output of our IP solver by consecutively adding jump constraints of the form ti < ni with ni 2 N to C.
Proof. b b0 and since b0 is a minimal solution, b 6 b0. Thus, 9t 2 T : b0(t) < b(t). Add the constraint t < b(t) to C, then b is not a solution anymore. Assume b00 to be our IP solver’s new solution. As b0 fullls t < b(t) it is still a solution, so from b0 6= b00 we conclude b00 b0, and the same argument as above holds. Termination is guaranteed since there are only nitely many solutions b00 b0.
Non-minimal solutions may not be reachable this way, since the argument \b0(t) < b(t) for some t" does not necessarily hold. To determine those, increment constraints are necessary, and the latter can be obtained from partial solutions.
(N; m; m0) is a tuple (C; x; ; r ) of
{ a family of (jump and increment) constraints C = (c1; : : : ; cn), { the -smallest solution x fullling the marking equation of (N; m; m0) and the constraints of C, { a ring sequence 2 T with m[ i and }( ) x, { a remainder r with r = x }( ) and 8t 2 T : (r(t) > 0 =) :m[t i). The vectors x and r are included for convenience only, they can be computed from C, , , and the problem instance.
A full solution is a partial solution (C; x; ; r ) with r = 0. In this case, is a ring sequence solving the reachability problem (with answer ’yes’).
If we obtain a partial solution with r 6= 0 there are not enough tokens on some places to re the transitions in the remainder r. An underapproximation of tokens necessary can be computed from a graph G containing the transitions in r and the undermarked places, an edge from place s to transition t if there are not enough tokens on s to re t, and an edge the other way if ring t increases the token count on s. From any strongly connected component SCC in G without incoming edges (= tokens produced by other components, a source SCC) we compute the minimal number k of tokens needed to activate any of its transitions. Our constraint now states that the number of tokens produced on the component’s places should be increased byPat least that number k. The tokens produced on a place p can be expressed as P t: C(p;t)P>0 C(p; t) x(t) for a solution vectPor x, so tPhe constraint takes the form p2SCC t2=SCC: C(p;t)>0 C(p; t) t k + p2SCC t2=SCC: C(p;t)>0 C(p; t) x(t). Note that we sum up over transitions outside SCC only, as the transitions inside cannot produce tokens until the rst of them gets activated, which is the aim of this constraint.
In our example net from Fig. 1 we start with the solution x = 3a1 + 3a2 + 3‘. None of the transitions can re three times, this leads us to the graph G: y2 ! a2 ! x2 ! ‘ ! s ! a1 ! x2 ! a2. The only source SCC of G consists of just y2 leading to the constraint 1 b2 k + 1 x(b2) = k = 1. Now the smallest solution becomes x0 = 2a1 + 2a2 + b1 + b2 + b3 + 3‘ and only b1 can re as often as wanted. Our constructed graph G0 now has z as its only source SCC, from which we obtain the constraint 1 c1 1 + 1 x0(c1) = 1, leading to x00 = 2a1 + 2a2 + b1 + b2 + b3 + c1 + c2 + 3‘. After the sequence b1c1b2c2b3‘a1 we nd a remainder r = a1 + 2a2 + 2‘ and get again the graph G, but now with a constraint 1 b2 k + 1 x00(b2) = 1 + 1 = 2. After the next solution x000 = a1 + a2 + 2b1 + 2b2 + 2b3 + c1 + c2 + 3‘ with the graph y2 ! a2 ! x2 ! ‘ ! s (a1 not being in the remainder anymore) the constraint is increased to 1 b2 k + 1 x000(b2) = 1 + 2 = 3. We now obtain the nal solution of 3b1 + 3b2 + 3b3 + c1 + c2 + 3‘. Note that the rst step can also be done by a jump a1 < 3, but this is impossible for the second step since x00 x0. 5
Finding maximal ring sequences for a solution x produced by the IP solver to obtain partial solutions can be done by a brute force tree search. The execution time may grow exponentially with the size of the solution, though. Partial order reduction, e.g. the stubborn set method [KSV06], can be applied to reduce the execution time. Other reductions can be thought of; even with stubborn sets a marking may appear more than once, either on a single path (the ring sequence is not minimal) or on permutated paths. Finding such spots allows to avoid going through subtrees unnecessarily.
The algorithm has been implemented in a tool named Sara [Wim10] and tested
well with some small examples and a challenge posed by H. Garavel [Gar03]
in 2003 so far. Four other tools, using dierent approaches, managed to solve
the challenge, with run times from about 10 minutes to more t
Due to the underapproximation of needed tokens when building constraints, our algorithm runs into trouble when the Petri net has high arc weights. A comparison to LoLA [Wol10] suggests an exponential loss with growing arc weights for some specialised examples.
Overall, we have the hope that our implementation is able to compete with other tools using state space exploration or symbolic model checking instead of structure analysis. Of course, more tests are necessary before a stable statement can be made. The algorithm presented here only tries to make a semi-decision for the positive case, but we are working on an extension to also make correct negative semi-decisions in many cases. [BEN10] [CMS06] [Gar03] [Kos82] [KSV06] [Lam92] [Lip76] [May84] [Wim10] [Wol10]