Since the state space explosion is a common problem when analysing Petri nets several ways to deal with this problem leading to a smaller { reduced { state space have been invented. One of them is nding symmetries, an equivalence relation on places and transitions of a Petri net, and only evaluating one object from each equivalence class. All other objects in the same class are then known to yield the same information. Finding symmetries by brute force is known to be expensive, it is even unclear if it can be done in polynomial time due to the inclusion of the graph isomorphism problem. While a rst few symmetries need to be found by brute force, later ones might also be generated. We show how to generate new symmetries from known ones e ciently, how to tell if the brute force algorithm enters a branch not containing symmetries, and how to reduce the symmetries themselves to move towards orthogonality.
Tools for state space exploration like LoLA [Wol10] use many techniques to reduce the state space before exploring it to answer a question. This is due to the well-known problem of state space explosion, where the size of the state space can grow exponentially or worse with the size of the system to be analysed. If a system contains components that are indistinguishable from each other (by the structure of the system and the question asked about the system) it is obviously su cient to analyse one such component only. The result can just be mapped to an equivalent component then. A mapping maintaining the relation between components is called a symmetry.
With Petri nets as systems, components are just the places and the transitions. A symmetry therefore maps each place to some place (possibly itself) and likewise for transitions, keeping the edges, i.e. a mapped pair of place and transition has an edge between them if and only if the original pair has that edge. A symmetry is thus not more than a structure-preserving permutation on the places and transitions of a net.
Unluckily, the number of symmetries (the size of the automorphism group) of a Petri net (or any system) can be much larger than the system itself. It is necessary to nd a small set of symmetries (called generator set) from which all other symmetries may be derived. If the components are ordered and numbered (say from 1 to n), a generator set consists of n levels and each level i contains one symmetry for each possible image j of the component i with j i. Components with a number less than i are mapped to themselves. Take the Petri net from Fig. 1 as an example.
p1 t1 p2 t2 p3 t3 p4 t4 p5 t5 p6 t6
If a place pi is mapped to pj then the transition ti is mapped to tj due to the structure of the net (each place has only one successor transition). If we thus use just the number of a place/transition instead of its name, we may obtain the following generators: the identity for level 1, (2 3) and the identity for level 2, (4 5 6), (4 6 5) and the identity for level 3. Only components mapped to di erent components are shown explicitly in this notation, and each one is mapped to the next inside the parentheses (the last to the rst). For level 2 there are two replacement candidates for (2 3): (2 3)(4 5 6) and (2 3)(4 6 5). Any one of these three is su cient. It can be shown (see e.g. [Sch02]) that any symmetry can be written as the composition of some generators gi, one from each level i, by = g1 g2 : : : gn.
While LoLA seems to implement an algorithm (called Re ne*/De ne in [Sch02]) that runs in polynomial time in practical cases, this cannot be guaranteed due to the inclusion of the graph isomorphism problem for which membership in P is unknown. Therefore, it is important to rely on such an algorithm (that builds generators from scratch) as seldom as possible and use already known generators instead to derive new ones when possible. To a certain extent, LoLA already does this by composing generators with themselves, building powers, and checking whether these powers can ll the gaps where generators are still missing. In the following, we show how this can be improved. 2
We assume Petri nets, formally a tuple (P; T; F ) with F : (P T ) [ (T P ) ! N, to be known to the reader. We also expect some knowledge about linear algebra, especially the de nition of a group, and start now by de ning symmetries. De nition 1 (Symmetry). Given a net (P; T; F ), a symmetry is a map : P [ T ! P [ T with (P ) = P , (T ) = T , and F ( (x); (y)) = F (x; y) for all x; y 2 P [ T .
We might also be interested in a (initial or nal) marking m, in which case m( (p)) = m(p) must hold additionally for all p 2 P . A symmetry is written in the style (a11 : : : a1j1 ) : : : (an1 : : : anjn ) where (aim) = ai;(m mod ji)+1.
In the following we assume a xed Petri net N = (P; T; F ), a xed bijection b: P [ T ! fi 2 N j 1 i jP [ T jg and identify the places and transitions of N with their images under b.
De nition 2 (Generator, level, orbit). A symmetry g for level lev(g) = i (1 i jP [ T j) is a symmetry with g(k) = k for all k < i. The number g(i) is called the orbit of g. Each level i also has orbits, numbered from i to jP [ T j. An orbit k of level i is consistent if there is a symmetry g for level lev(g) = i with an orbit g(i) = k, otherwise the orbit is called inconsistent or empty. De ne Gi to be the group of all symmetries for level i (with Gi Gi+1). On the other hand, a generator set G consists of one symmetry, called generator, gij for each level i and each consistent orbit j on that level.
Corollary 1 ([Sch02]). Let G be a generator set. Each symmetry g for level i can be expressed as a consecutive composition of one generator gj 2 G from each level j i.
Corollary 2 ([Sch02]). There is an algorithm Re ne*/De ne taking a level i and an orbit k as input and producing a symmetry g for level i with g(i) = k if such a symmetry exists. Otherwise, the algorithm terminates with the result \inconsistent". 3
Inconsistencies are obviously the worst result that can be obtained from the Rene*/De ne algorithm. They waste time and do not even produce a generator. Once we know of an inconsistent orbit for some level, we may use this information to nd other inconsistent orbits without the Re ne*/De ne algorithm. An equivalence relation for places/transitions can be helpful here.
De nition 3 (Equivalence of components). Let G be a generator set and i some level. For x; y 2 P [ T we de ne an equivalence relation x i y () 9g 2 Gi: g(x) = y.
Note that i being an equivalence relation follows from the fact that Gi is a group with identity, an inverse, and composition as group operation. Lemma 1 (Inheritance). For level i, let k be an inconsistent orbit and n be a consistent orbit. Then, n 6 i k.
Proof. Assume n i k, then there is g 2 Gi with g(n) = k. Let g0 2 G be the generator for level i with g0(i) = n. Then, g(g0(i)) = k and g0 g 2 Gi has the orbit k. A contradiction, as no symmetry g00 for level i with g00(i) = k exists.
Looking from the other side, this means every orbit m with m i k must be inconsistent. It is therefore unnecessary to call the Re ne*/De ne algorithm for orbits equivalent to k. In our example from the introduction, all orbits k > 1 on the rst level are inconsistent, since p1 can only be mapped to itself by any symmetry. If we know that the orbits 2 and 4 are inconsistent, we conclude from the generators (2 3) and (4 5 6) (from levels 2 and 3) that 2 1 3 and 4 1 5 1 6. We save three calls to Re ne*/De ne. 4
LoLA so far takes a newly acquired generator g for level i and calculates the powers g2 = g g, g3, g4, and so on, until gn(i) = i holds. If one of the powers has an orbit for which no symmetry has been found so far, the power is saved as the new gnerator for that orbit. Further powers do not yield anything new as gn+1 has the same orbit as g1 = g.
Instead, we propose building compositions of any new generator with any generator found so far until no new generators are derived anymore. This looks like a losing approach at rst as there are by a linear factor more such products than powers. But note that in the powers approach O(n) (with n = jP [ T j) powers must be calculated until gn(i) = i holds and each composition done also needs O(n) (the size of the map). The powers approach therefore looks quadratic. Lemma 2 (Complexity of product testing). Let g 2 Gi and g0 2 Gj with j i. A test if the composition g g0 leads to an orbit for which no generator has been found so far can be done in O(1).
Proof. We check if there is a generator for level i with orbit g0(g(i)). This takes O(1) time. If there is none, g g0 will be the new generator for level i and orbit g0(g(i)).
Note that this simple test is useless for the powers. We would test and then calculate the composition anyway, independently of the test's result, when we need the next, higher power.
What is important here is that a newly found generator for level i is composed only with generators of a higher level. To guarantee this, the levels have to be lled with generators from highest to lowest. This is the way it is done in LoLA anyway: LoLA uses a recursion from easier to harder problems, and higher levels represent the easier problems (as more elements are mapped to themselves).
If we try to calculate a complexity for our approach and (falsely) assume that the size of a generator set G is roughly equal to jP [ T j we obtain O(n2) tests (for pairs of generators in G) with complexity O(1) each and O(n) compositions with complexity O(n) each. This would suggest a quadratic complexity just like for the powers' calculation. There are examples where the size of the generator set is much higher as well as those where it is much lower than jP [ T j, so the real complexity comparison is much more di cult.
In general, the product approach will produce more new generators in a single call than the powers approach, but this depends on the structure of the automorphism group. If the order of generators (the lowest power yielding the identity) is lower than the number of orbits on some level, it is impossible to ll all orbits in a single call of the powers approach. Since products are iterated, from them the whole subgroup spanned by all known generators could be computed. This can mean an exponential gain compared to the powers, e.g. in groups with pn elements (p prime) where gp is the identity for all symmetries g. By powers at most p 1 new generators can be built from each call to Re ne*/De ne, while with products the group spanned from the known generators increases by a factor of p for each call. 5
Our last optimisation does not deal with the nding of generators but with the size of their representation. While a smaller size might reduce execution times there may be other bene ts. Let two generators g; g0 be orthogonal if g(i) 6= i =) g0(i) = i, then g and g0 can be composed without e ort. The set fi j g(i) 6= ig is called the carrier of g. Conclusions drawn about the carrier of g cannot be in uenced by g0 and are thus valid for g g0. While orthogonality is unreachable in general, we may still try to minimize the carrier of any generator g. Candidates that may have a smaller carrier are easy to nd: Corollary 3. If g is a generator for level i and orbit k and n > 0 is the smallest integer with gn(i) = i, then, from all powers of g, exactly the gjn+1 (for j 2 N) are generators for level i and orbit k.
Take e.g. the cycle representation of one of the generators for the Petri net from Fig. 1: g = (2 3)(4 5 6). If we take g as generator for level 2 and orbit 3 then (2 3) is the orbit cycle of g (it contains level and orbit). Its length is n = 2, i.e. g2(2) = 2. Thus, reduction candidates are g2+1 = (2 3), g4+1 = (2 3)(4 6 5), g6+1 = g1 and so on. Since 2 + 1 = 3 is divisible by the length 3 of the second cycle (4 5 6), this cycle is eliminated in g3 (g3(i) = i for i = 4; 5; 6 and identities are not shown in cycle representation). In general, the following holds. Lemma 3. Let g be a generator with an orbit cycle o = (o0 : : : oi 1) and another cycle c = (c0; : : : ; cm 1). Let k be the greatest divisor of m such that i and k have a greatest common divisor (gcd) of one. Then, in gk+qm (for q 2 N) the cycle c is replaced by k cycles of length m=k and there is no power of g having the same orbit cycle and shorter replacement cycles for c.
Proof. Just note that gk(c(n+`k) mod m) = c(n+(`+1)k) mod m and for ` = mk 1 for the rst time gk(c(n+`k) mod m) = gk(c(n+m k) mod m) = cn+m mod m = cn holds. If we choose k a greater divisor of m, there can be no j such that k divides ji + 1, since the gcd of k and i also divides ji (and not ji + 1). Since a divisor of k also divides k + qm, k + qm = ji + 1 is impossible, i.e. if gcd(i; k) > 1, gk+qm will not preserve the orbit cycle.
Thus, for k + qm = ji + 1 the cycle c is reduced as far as possible and at the same time the orbit cycle stays intact. It is unnecessary though to solve this equation as the proof of lemma 3 already tells us how the cycle c will be modi ed. 6
The approach of building powers of generators can already be optimal, as it happens e.g. with the dining philosophers and reader/writer systems. Experiments for these examples show a worst case slow down of 1 2% in execution times from the powers approach to our new optimisations. This supports our earlier assumption that building products is not (much) slower than building powers.
A good example to show the di erence between old and new approach is the hypercube ECHO [Rei98], a grid-like network with d dimensions and n communicating agents per dimension. The value of detecting inconsistencies can be shown with the nets Ni, where N3 = N from Fig. 1, and each higher index adds a new ring with i places and transitions each. Execution times for computing the symmetries are shown in Table 1.
Theoretical observations and experimental results have shown that nding and using symmetries can be optimised beyond the current state of a airs represented by LoLA. Using products and an equivalence to detect inconsistencies leads to a clear speed up in not already optimal cases. [Sch02] [Wol10]