Some global properties of Petri nets, such as liveness or -boundedness, simply aggregate corresponding properties of the individual nodes. It is recommendable to break down their verification to the individual node-based properties. That investigation can be organized as a portfolio of diferent verification techniques. For Petri nets with symmetric structure, we propose to apply symmetries as a separate portfolio member. This way of applying symmetries difers from the usual use of symmetries as a tool for state space reduction. We discuss some nice advantages of this approach.
We can roughly distinguish three categories of Petri net verification. In structural verification , we detect
patterns in the net topology itself. We may, for instance, enumerate siphons. A siphon is a set of
places such that every transition that has a post-place in , also has a pre-place in . [
We contribute to the third category of verification problems. In particular, we study global properties that aggregate properties of the individual places or transitions of the net. We call such a property an aggregating property. A place is -bounded if, for every reachable marking , () ≤ . The net is -bounded if and only if every place is -bounded. A transition is live if every reachable marking enables a transition sequence that contains . The net is live if and only if every transition is live. That is, properties such as -boundedness and liveness are aggregating. In contrast, properties like reversibility and deadlock-freedom are not aggregating since no appearant separation into properties of individual places or transitions is known.
After setting up our terminology in Section 2, we argue in Section 3 that a node-by-node approach is recommendable for the verification of aggregating global properties. For every individual node, several methods exist to solve the node-based subproblem. These methods can be organized as a verification portfolio. We give examples of suitable portfolios for several aggregating properties. In Section 4, we recall the concept of symmetry. In Section 5, we propose to use symmetries as a separate portfolio member rather than a vehicle for state space reduction. We discuss the particular merits of this approach.
Definition 1 (Petri net). A Petri net = [, , , , 0] consists of a finite set of places, a finite set of transitions, disjoint from , a set of arcs ( ⊆ ( × ) × ( × )), a weight function : ( × ) × ( × ) → N where (, ) = 0 if and only if [, ] ∈/ , and a marking 0, the initial marking. A marking is a mapping : → N.
Definition 2 (Firing rule). Transition is enabled in marking if, for all places , [, ] ∈ implies () ≥ (, ). If is enabled in , may fire and yield marking ′ where, for all places , ′() = () − (, ) + (, ). This firing relation is written as →− ′.
We lift relation→− to transition sequences by setting →− for all markings and the empty sequence , and by setting →− ′′ if and only if there is a marking ′ such that →− ′ and →′− ′′. Transition sequence is enabled in marking if there exists a marking with →− ′.
Definition 3 (Properties).
• Marking ′ is reachable from marking if there is a transition sequence where →− ′. • Place is -bounded if, for all markings reachable from 0, () ≤ . A Petri net is -bounded if all its places are -bounded. • Place is constant if, for all markings reachable from 0, () = 0(). A Petri net has the constant-place property if it contains a constant place. • Transition is quasi-live if there exists a transition sequence such that is enabled in 0. A
Petri net is quasi-live if all its transitions are quasi-live. • Transition is live if, for every marking reachable from 0, there exists a transition sequence such that is enabled in . A Petri net is live if all its transitions are live.
Observe that most properties listed above have a local version (place is . . . , transition is . . . ) and an aggregating version (the Petri net is . . . ). In the sequel, we shall therefore distinguish local standard properties and global standard properties. It is also obvious that answering the local problems for all nodes of a Petri net amounts to a solution of the corresponding global problem.
The global versions of 1-boundedness, constant place, quasi-liveness and liveness have been part of the “global properties” competition in recent model checking contests.
The brute-force approach to verify an aggregating global property is to compute the reachability graph of the Petri nets. The vertices of the graph are the markings reachable from 0, and the edges correspond to the firing relation (considering only single transitions). -boundedness and existence of constant places can be easily verified by inspecting the vertices of a reachability graph. Transition is quasi-live if there is an edge labeled with . Transition is live if every terminal strongly connected component of the reachability graph contains an edge labeled with . A strongly connected component is an equivalence class in the set of markings with respect to the equivalence relation “ is reachable from ′ and ′ is reachable from ”. A strongly connected component is terminal if no other strongly connected component can be reached from it.
Although all standard properties can be analyzed using the reachability graph, its use generally is
infeasible even if it is finite, due to the well-known state explosion problem. State space reduction
techniques may alleviate the state explosion problem to a certain degree, but work much better on
the local version of a standard property than on the global version. This can be explained as follows.
The most powerful state space reduction technique for Petri nets is the stubborn set method [
For these reasons, our tool LoLA [
We can substantially reduce the costs of considering all places or all transitions of the net by considering bycatch. Bycatch means that, when approaching a local problem for one node, we may get suficient information for answering the problem for other nodes. If, for instance, we search for an executable firing sequence that proves some transition to be quasi-live, all members of that sequence, and all members of sequences that have been produced in unsuccessful attempts, are clearly quasi-live. Many properties permit similar bycatch.
The efort for verifying the individual local problems can be reduced by running a portfolio approach that applies diferent verification techniques in parallel. In LoLA, the following verification techniques are used.
First, we may produce a reduced state space using the stubborn set method. There exist specialized
approaches for all local problems mentioned so far. The article [
Random walks (i.e. repeated random execution of firing sequences) may provide information for some local problems. If some sequence contains a transition , is quasi-live. If such a walk enters a marking with more than tokens on a place, this place in not -bounded. If the number of tokens changes on a place, it is not constant. Using only random walks, we can, however, never be sure that a transition is not quasi-live. Similarly, random walks may disprove but never prove -boundedness of a place and they can show that a place is non-constant. For liveness of a transition, random walk do not provide any useful information. We can restrict the set of transitions to choose from to a stubborn set that preserves some local verification problem. This way, we can significantly increase the success rate of the random walk approach. Random walks may also deliver some bycatch similar to state space generation.
A place invariant is a solution of · = 0 where is the incidence matrix of the net holding (, ) = (, ) − (, ). If is a place invariant, we have · = · 0, for all markings reachable from 0. The right hand side of this equation is a constant. Place invariants are mainly used for -boundedness. If we find a place invariant with () = 1 and () ∈ {0, 1} for all other places, such that · 0 ≤ then is -bounded. As a bycatch, all other places with () > 0 are -bounded as well.
The state equation refers to the well-known fact that, for all markings and ′ and transition
sequences , + · Ψ( ) = ′ where Ψ( ) is the -indexed Parikh vector of . In the Parikh
vector, Ψ( )() is the number of occurrences of in . Let be a -indexed vector of variables and
be a -indexed vector of variables. If the integer linear program (LP) 0 + · = , ≥ 0, ≥ 0,
() ≥ 1 is infeasible then is not quasi-live. If the system is feasible and can be arranged into an
executable transition sequence then and all transitions ′ with (′) > 0 are quasi-live. If none of that
happens, we have to rely on the other portfolio members. The state equation can be used for other
local standard properties as well. For -boundedness of place , we replace constraint () ≥ 1 with
() ≥ + 1. For the constant place problem, we operate with two separate LP problems where we
use () ≥ 0() + 1 (resp. () ≤ 0() − 1) instead. According to [
The considerations so far suggest the following portfolios. For -boundedness, we run, for every place , a reduced state space generation, a random walk task, a state equation task and a place invariant task. For quasi-liveness we run, for every transition , a reduced state space generation, a random walk task, and a state equation task. For the constant place problem, we run reduced state space generation, a random walk task, and a state equation task for every place . In fact, we run two copies of each task where one copy checks whether the number of tokens on can be increased while the other one checks whether that number can be decreased. This separation simplifies both the stubborn set generation and the ILP problem to be studied. For liveness, we generate a global reduced state space that preserves all terminal strongly connected components and thus the liveness of all transitions. In addition, we generate separate reduced state spaces for each individual transition.
The portfolio manager takes care that the number of active tasks corresponds to the number of available cores. It also takes care that verification tasks are canceled as soon as some portfolio member was able to find the answer for the same place or transition.
Symmetries have been introduced in [
Definition 4 (Symmetry). and and all places ,
A symmetry is a bijection : ( ∪ ) → ( ∪ ) such that, for all nodes • () ∈ if and only if ∈ (respects node type); • (, ) = ( (), ()) (respects arc relation and weights); • 0() = 0( ()) (respects initial marking).
For a symmetry and a marking , the marking () is defined by ()( ()) = (), for all places .
The identity with () = , for all , is always a symmetry. If is a symmetry, so is − 1, and
for two symmetries 1 and 2, the composition 1 ∘ 2 is a symmetry as well. That is, the set of all
symmetries is a group under composition. A Petri net may have exponentially many symmetries which
can be represented by a generating set with a polynomial number of elements (in the number of nodes
of the net) [
Computing the generating set for the symmetries is closely related to the graph isomorphism problem.
The graph isomorphism is in NP, and until now there is neither a known polynomial algorithm nor a
proof of NP-completeness. Computing generators for the symmetry group amounts to a systematic
search [
This is why the use of symmetries is quite risky in situations where only limited time is available (such as the MCC). The computation of the generating set for the symmetries may take substantial time (as discussed above), and the use of large generating sets in reduced state space generation may also slow down the verification speed. For this reason, the most competitive configuration of LoLA in the MCC does not apply the symmetry reduction in its state space explorations. For state spaces in local verification problems, the use of symmetries for actual state space reduction is even more prohibitive since, for every individual node, the use of a specific subgroup of the symmetries may be required, as explained below.
We call two nodes and equivalent if there is a symmetry holding () = . Accordingly, we
call two markings 1 and 2 equivalent if there is a symmetry with (1) = 2. Both relations
are indeed equivalence relations. A symmetrically reduced reachability graph is permitted to omit
markings if it can be guaranteed that at east one member of its equivalence class is contained. There are
many ways to achieve this [
With the symmetrically reduced graph, we can approach some, but not all global versions of standard properties.
Proposition 1 (Preservation of standard properties under symmetry). Place is -bounded if and only if the symmetrically reduced reachability graph does not contain a markimg where, for some place equivalent to , () > .
Place is constant if and only if, for all markings contained in the reachability graph and all places equivalent to , () = 0().
Transition is quasi-live if the symmetrically reduced reachability graph contains an arc annotated with some transition ′ that is equivalent to .
There is no straightforward way to exhaustively analyse liveness of all transitions using the symmetrically reduced graph. Remember that transition is live if and only if it occurs in every terminal strongly connected component of the unreduced graph. If some transition ′ equivalent to occurs in some terminal strongly connected component of the symmetrically reduced graph, then the corresponding terminal strongly connected components in the unreduced graph may be the same for and ′, or may be diferent (just equivalent). That is why we cannot see whether all transitions occur in all terminal strongly connected components. Only if there is a terminal strongly connected component in the reduced graph that neither contains nor any transition equivalent to , we know that is not live.
We can, however, compute a symmetrically reduced reachability graph to solve some particular local
liveness problem [
We are now proposing an alternative way to benefit from symmetries. We consider the following context. We are verifying an aggregating global standard property by separating it into its local problems, one for each place or transition. These local properties are tackled by a portfolio of verification methods, as discussed above. For the verification, a machine with multiple physical cores is available.
In this context, we may add another thread that runs concurrently to the remaining portfolio. It computes a generating set for the symmetries. Whenever some generator has been found, the equivalence relation on places and transitions is updated. Whenever some portfolio member reports a result for some place or transitions, this result is immediately propagated to all equivalent places or transitions.
This approach has some decisive advantages, compared to state space reduction using symmetries. First, the actual portfolio can start to do its work and does not need to wait until the generating set for the symmetries has been computed. That is, we do not lose too much time for getting the actual verification done. In the worst case, only the computing power of one core is siphoned away from the actual verification. Second, every single generator allows us to reason about equivalent nodes. So symmetries start to take efect long before the computation of the generating set has finished. Third, after having used a generator to update equivalences, the generator does not need to be stored permanently (which is the case for state space reduction as the generators are applied for transforming markings into their small representatives). Fourth, if symmetries are detected, we may skip a large number of local verification tasks since values can be inferred from equivalent nodes. Our tool LoLA has recently been quite successful in the verification of global properties, and we blame the combination of local property verification and our novel symmetry application for that.
For organizing the integration of the symmetries into the regular portfolio, the portfolio manager of our tool has implemented the following communication.
The portfolio manager records the local results and checks whether the global result is determined.
Taking quasi-liveness as an example, the global result is fixed if one transition is reported not to be
quasi-live, or if all transitions have been reported to be quasi-live. The portfolio manager additionally
maintains the equivalence relation. To this end, it uses the data structure of Tarjan’s union/find algorithm
[
The regular tasks ask the portfolio manager for an unsolved node they can process (and have not processed yet), and finally deliver their result (true, false, or inconclusive). That result is then propagated to all nodes that are equivalent to the reported one. The symmetry task is started at the beginning. Whenever it finds a generator of the symmetry group, it reports this generator to the portfolio manager for updating the equivalences. If equivalence classes change, known results are propagated to the new members of the equivalence class. Using this strategy, we can evaluate every global property for the dining philosophers problem with 5 places and 4 transitions by solving only up to 5 local problems. This is a dramatic speed up, especially for large .
We studied the verification of aggregating global properties. The proposed approach has a few similarities to state-of-the-art model checking for Petri nets. For both types of verification tasks, we run a portfolio ofering various verification methods, including methods that strongly benefit from Petri net structure theory. For both types of verification problems, we try to separate the problem into as many as possible subproblems such that solving the subproblems requires less memory.
There are, however, remarkable diferences between model checking and the verification of global properties. The first diference is the sheer number of subproblems we end up with. In model checking, we may be able to rewrite the formula under investigation into a Boolean combination of a few sub-formulas and verify them separately. An aggregating global property can be split into as many subproblems as we have places or transitions in the net. For this reason, we need to squeeze out as much bycatch as possible from the solved subproblems. While the subproblems in model checking tend to be heterogeneous, subproblems for global properties are homogeneous. That is why it is possible to apply symmetries in a diferent manner. Instead of using them for state space reduction, we may apply them to generate additional bycatch by propagating results from solved problem instances to unsolved problem instances.