The reachability graph entirely describes the state space and the transitional dynamics of a place/transition Petri net N . Many challenges in model checking reduce to searching the reachability graph. Therefore, this is a time critical operation deserving elaborate speed-up efforts in every detail. To enumerate the neighborhood of a reached state m is the fundamental subtask during the graph search. It requires to determine exactly the set T (m) of enabled transitions in state m. In the past, we already avoided to compute T (m) from scratch in every reached state m, as not much changes between consecutive states. Instead, we prepared a data structure DI(N ) allowing the production of T (m) by briefly updating T (m0) when migrating from state m0 to m. Although saving up much time during the actual graph search, the preprocessing of DI(N ) has been an unpleasantly costly investment until this point. In this paper, we introduce a new, generally much faster method to compute DI(N ). We implemented it in the award wining model checker LoLA 2 and compared it to the previous approach. In our experiments we used the model checking contest (MCC) as a benchmark. The new method is in almost all cases at least one order of magnitude faster.
In model checking, the main task is to build the, possibly reduced, state space of a place/transition Petri net N . One of the critical points while building the state space, is to determine whether a transition is enabled or not. I.e. in each state the list of enabled transitions, which can lead to new states, must be computed. The aim is to avoid checking in every state every transition for enabledness. To avoid this, we only check the enabledness information of all transitions in the initial state. Then, whenever a fired transition t leads to a new state, we only want to update the enabledness information of transitions that are possibly disabled or enabled by the firing transition t. To this end, in the preprocessing, before building the state space, we compute the look-up data structure DI(N ), which Copyright c 2020 for this paper by its authors. Use permitted under Creative Commons License Attribution 4.0 International (CC BY 4.0). basically is a list of possibly disabled/enabled transitions for each transition firing. The advantage is that the lists of DI(N ) are in general way smaller than all transitions and, thus, faster to process.
The problem of speeding-up the computation of the state space using
enabling tests was already studied more than 25 years ago [
In this work, we introduce a new and faster method for computing DI(N ).
The key to the performance gain is an indexed graph data structure and a
rigorous reduction of costly copying operations. As a sidenote, we like to point
out that this approach is also used to speed up the computation of conflicting
transitions in partial order reduction techniques [
Definition 1 (Place/Transition Net). A place/transition net, P/T net for short, consists of a finite set of places P , a finite set of transitions T where P \ T = ;, a set of arcs F (P T ) [ (T P ), a weight function W : (P T ) [ (T P ) ! N where W (x; y) = 0 if and only if (x; y) 2= F , and an initial marking m0, where a marking is a mapping m : P ! N. For a node x 2 P [ T , x = fy j (y; x) 2 F g and x = fy j (x; y) 2 F g are its pre- resp. post-set.
The behavior of a P/T net is defined by the transition rule. m !t m0.
Definition 2 (Transition rule of a P/T net). Let N = [P; T; F; W; m0] be a P/T net. Transition t 2 T is enabled in marking m if, for all p 2 P , W (p; t) m(p). The set of all enabled transitions in a marking m is denoted as T (m). If t is enabled in m, t can fire, producing a new marking m0 where, for all p 2 P , m0(p) = m(p) W (p; t) + W (t; p). This firing relation is denoted as
Using the transition rule, a P/T net induces the reachability graph, also called the state space of the P/T net. Definition 3 (Reachability graph of a P/T net). The reachability graph (M; E) of a P/T net N has a set of vertices M that comprises all markings that are reachable by any firing sequence from the initial marking of N . Every element m !t m0 of the firing relation (t 2 T ) defines an edge E from m to m0 annotated with t. 3
Preprocessing decreasing and increasing transitions To speed up building the reachability graph, it is very valuable to preprocess the candidate transitions that can become en- or disabled after firing transitions. In fact, if a transition t fires leading from marking m to m0, it may, in the course of this, disable a previously activated transition t0, if t consumes from a place p 2 t\ t0. More precisely, we would like to capture the situation where both, t and t0, are enabled in m, hence, (i) m(p) maxfW (p; t); W (p; t0)g, and where t0 is not enabled in m0, anymore, hence, (ii) W (p; t0) > m0(p) = m(p) W (p; t) + W (t; p). As preprocessing is unaware of the specific markings m and m0, we need to combine (i) and (ii) for the condition
W (p; t0) < maxfW (p; t); W (p; t0)g
W (p; t) + W (t; p): In such a case, we say that t decreases t0 or that t0 is decreased by t and denote this as the binary relation t & t0. In the case of W (p; t) W (p; t0), the decreasing condition reduces to W (t; p) < W (p; t) and, otherwise, it simply becomes W (t; p) < W (p; t0). Taking everything together, we get the following definition: Definition 4 (Decreasing transitions). We call a transition t0 2 T decreased by a transition t, if there exists a place p 2 t \ t0 with W (t; p) < W (p; t) and W (t; p) < W (p; t0) and denote this by t & t0.
On the other hand, if m !t m0, it may also happen that a previously disabled transition t0 becomes enabled in m0, namely if t produces token on a place p 2 t \ t0. In this simpler situation we have 0 < W (p; t0) m0(p) = m(p)
W (p; t) + W (t; p); which leads to the following definition, right away: Definition 5 (Increasing transitions). We call a transition t0 2 T increased by a transition t, if there exists a place p 2 t \ t0 with W (t; p) > W (p; t) and 0 < W (p; t0) and denote this by t % t0.
By breaking down the concepts of decreasing and increasing to binary relations, we are able to describe all information as graphs.
Definition 6 (Decrease and increase graph). If N is a P/T net with transition set T then we call the directed graph D(N ) = (T; &) with node set T and arc set & the decrease graph of N and the directed graph I(N ) = (T; %) with node set T and arc set % the increase graph of N . The pair of decrease- and increase graph is subsequently denoted as DI(N ).
Having preprocessed DI(N ), building the reachability graph of a net N can be sped up. In fact, whenever we traverse an edge m !t m0 from a node m to a new node m0 by firing a transition t, we have to determine the set of reachability arcs that are incident to m0. In other words, this means to compute the set T (m0) of transitions in N that are enabled in m0. However, as we come from m, we are already in possession of T (m) and, probably, the difference between T (m) and T (m0) is not too big. This is where DI(N ) helps us to make just a few updates of T (m) in order to get T (m0). We begin with the decrease graph D(N ) and obtain the neighborhood d(t) of t, which consists of all transitions that may become disabled by firing t. Secondly, we also compute the neighborhood i(t) of t in I(N ) for the transitions that may become enabled after firing t. Afterwards, the job of computing T (m0) reduces to the following update:
T (m0) = T (m)
ft0 2 d(t) j 9p 2 t0 : W (p; t0) > m0(p)g + ft0 2 i(t) j 8p 2 t0 : W (p; t0) m0(p)g As this update considers only the transitions of d(t) [ i(t), which is usually much smaller than the whole T , investing into the computation of DI(N ) pays out.
A second application field of DI(N ) is partial order reduction [
The former computation of the decrease-increase-graph For any ordering p1; p2; : : : ; pn of the places of the net N , we define for every i 2 f0; : : : ; ng the subnet Ni that, while containing all transitions T of N , only consists of the places Pi = fp1; : : : ; pig and the arcs that go between T and Pi. The former approach to the computation of DI(N ) = DI(Nn) is to start with DI(N0) and then consider the place sequence p1; : : : ; pn in order to successively obtain DI(Ni) for all i 2 f1; : : : ; ng.
It is easy to see that DI(Ni+1) is just DI(Ni) plus the edges induced by pi+1. This happens, as the decreasing and the increasing relations between transitions are defined only existentially over the place set. In other words, if DI(Ni) has a &-edge or %-edge, respectively, between two transitions t; t0 then considering an additional place pi+1 cannot revoke the existence of place p 2 fp1; : : : ; pig that justified the aforesaid edge between t; t0. For that reason it makes sense to define & (pi+1) and % (pi+1), the edges of DI(Ni+1) that are additionally introduced by the consideration of p.
Definition 7 (Incremental edges). For all places p of N , the set & (p) = f(t; t0) j W (t; p) < W (p; t); W (t; p) < W (p; t0)g is called decreasing edges of p and the set % (p) = f(t; t0) j W (t; p) > W (p; t); 0 < W (p; t0)g is the increasing edges of p.
The set % (p) can be represented in a very simple way: There are always two transition sets T 0; T 1 T such that % (p) = f(t; t0) j t 2 T 0; t0 2 T 1g. In fact, T 0 = ft j W (t; p) > W (p; t)g and T 1 = p . We capture this property in the following definition.
Definition 8 (Homogenous pair). A pair (T 0; T 1) of transition subsets of T is called %-homogenous if t % t0 for all t 2 T 0 and all t0 2 T 1. This is also denoted as T 0 % T 1. Analogously, it is called &-homogenous if t & t0 for all t 2 T 0 and all t0 2 T 1, which is denoted as T 0 & T 1.
If (T 0; T 1) is exactly the %-homogenous pair of % (p), this is made explicit by writing T 0 %p T 1.
The set & (p), in turn, is generally not describable as a single &-homogenous pair. That is why we used to fall back on the set
&_(p) = f(t; t0) j W (t; p) < W (p; t); 0 < W (p; t0)g: As, obviously, & (p) &_(p), this set is weaker but sufficient for the anticipated purpose. Moreover, T 0 = ft j W (t; p) < W (p; t)g and T 1 = p provide a &_homogenous pair for T 0 &_pT 1, which stands for & _(p) = f(t; t0) j t 2 T 0; t0 2 T 1g. In practice, we almost always have & (p) = &_(p), which justifies this simplification.
The graphs of every DI(Ni) are represented by a list of homogenous pairs each. More precisely, I(Ni) is given by a list of %-homogenous pairs. This basically corresponds to a compressed adjacency list representation, where all transitions t1; t2; : : : with the same adjacency list T 1 are together in T 0 = ft1; t2; : : : g and we get T 0 % T 1.
Therefore, in iteration i + 1, we have to go through all homogenous pairs Tj0 % Tj1 of I(Ni) and make updates according to T 0 %pi+1 T 1 in order to obtain I(Ni+1). More precisely, in I(Ni+1) every pair Tj0 % Tj1 is replaced by the new pairs (Tj0 n T 0) % Tj1
and (Tj0 \ T 0) % (Tj1 [ T 1) unless they are empty.
Equivalently, every graph D(Ni) is implemented as a list of &_-homogenous pairs, which have to be modified according to T 0 &_pi+1 T 1 for the next step D(Ni+1).
In our implementation, we use numbers to represent transitions and keep the pair items Tj0 and Tj1 as ordered lists. This make the computation of Tj0 n T 0, Tj0 \T 0, and Tj1 [T 1 linear time operations, which is fairly efficient. Nevertheless, we are forced to touch every pair, even though most of them are probably not intersected by T 0 or T 1. Hence, in worst case, the computation of DI(N ) takes O(jP j jT j2) time, as, for every place, we need to consider O(jT j) homogenous pairs in DI(Ni) and process each of them in linear time O(jT j). 5
Sped up computation of the decrease-increase-graph In our former approach, a lot of time is wasted in updating the adjacency lists. In every iteration, all lists have to be touched while most of them are not even relevant and, in case of an actual update, many copying operations occur. The speed-up idea is to create a more efficient way of determining the necessary updates. Moreover, in order to omit unnecessarily copying arrays around, the actual creation of adjacency lists is postponed until after the iteration of all places. If we want to build the graph G(N ), which is either I(N ) or D(N ), our new approach works in three steps: 1. For a given ordering p1; : : : ; pn of the places, we generate the corresponding list of homogenous pairs T10 ! T11; T20 ! T21; : : : , where ! stands for % in case of the computation of I(N ), or for & if D(N ) is about to be built. For that matter, we like to point out that the new computation method of D(N ) does not fall back onto &_ but, instead, processes every place into a set of possibly more than one homogenous pair. As the definition of these homogenous pairs is clear at this point, we do not go into the details of their computation in this section. 2. Iterating through the list of homogenous pairs, we progressively create an intermediate directed graph H(N ) = (X; Y; Z; ) on node sets X and Y , directed edges Z (X Y ) [ (Y X), and a partial function : T ! X. This graph means to implicitly encode G(N ). Every node in x 2 X represents a set Tx0 = ft 2 T j (t) = xg of transitions with the same adjacency list. The adjacency between the different nodes of X is realized indirectly. More precisely, every x 2 X defines a compressed adjacency list by the homogenous pair Tx0 ! Tx1 with Tx1 = S(x;y)2Z S(y;x0)2Z ft0 j (t0) = x0g. Altogether, every adjacency list of the target graph G(N ) is represented by one node of X. The efficient computation of H(N ) is detailed below. 3. In the final step, we take H(N ) and extract the compressed adjacency lists of G(N ) according to the definition above. After computing an inverse mapping of function , this is straightforward and does not need further explanation.
The computation of H(N ) works iteratively. We assume that we have computed the list of homogenous pairs T 0
1 ! T11; T20 ! T21; : : : ; Tk0 ! Tk1 from the list of places. Then we start from an empty graph H0(N ) and, step-by-step, integrate every pair Tj0+1 ! Tj1+1 into Hj (N ) to get Hj+1(N ) and, at the end, H(N ) = Hk(N ). Accordingly, every partial solution Hj (N ) encodes a graph Gj (N ) with all the edges of T10 ! T11; : : : ; Tj0 ! Tj1.
Then, when integrating the pair Tj0+1 ! Tj1+1, we firstly have to process all the nodes x1; : : : ; xr; x01; : : : ; x0s 2 X where Tj0 properly intersects Tx0i ; i 2 f1; : : : ; rg or Tj1 properly intersects Tx00 ; i 2 f1; : : : ; sg. More precisely, we have i to make copies x^1; : : : ; x^r; x^01; : : : ; x^0s having the same neighborhoods in Y as the original nodes. Moreover, we need to redefine (t) = x^i for all t 2 T 0 j \ Tx0i and (t0) = x^0i for all t0 2 T 1 j \ Tx00 . This is necessary as, in contrast to the transitions
i Tx0i n Tj0, all elements of Tx^0i will obtain an enhanced neighborhood in Gj+1(N ), namely Tj1+1. Similarly, the transitions of Tx^00 have to be divided from Tx00i n Tj1, i as only they are neighbors of Tj0.
Up to this point, however, Hj+1(N ) still represents Gj(N ) as no edge of Tj0+1 ! Tj1+1 has been included. To this end, we add a new node x 2 X and define for Tx0 = Tj0+1 n (Tx01 [ [ Tx0r ). We also add a new node x0 2 X and define for Tx00 = Tj1+1 n (Tx001 [ [ Tx00s ). Moreover, we add a new node y 2 Y for the connection Tj0+1 ! Tj1+1. To implement this homogenous pair in Gj+1(N ), we, thus, include the edges (x; y) and (x^i; y); i 2 f1; : : : ; rg into Hj+1(N ) as well as all the edges (y; x0) and (y; x^0i); i 2 f1; : : : ; sg.
The reason that computing H(N ) is much faster than our old method, comes from the fact that finding the intersected nodes x1; : : : ; xr; x01; : : : ; x0s does not work by exhaustive search as before. Instead, we just once iterate through the elements t of Tj0+1 and Tj1+1, respectively, and use (t) to get the intersected set. Moreover, having the intersected sets, we do not split entire transition arrays but copy only small amounts of edges between X and Y . But while the computation of H(N ) works in O(jP j jT j) time, the expansion of H(N ) into the compressed form of G(N ) can still take O(jP j jT j2) time in the worst case. However, that the new approach is usually the better one, even with the overhead of the subsequent adjacency list extraction, is demonstrated experimentally in the next section. 6
Both methods discussed in the paper are implemented in our explicit model
checker LoLA 2 [
Experiments were executed on a machine with 32 physical cores running at 2.7 GHz and 1 TB of RAM. All computations were done with no time and memory restrictions. The time was measured with the C++ chrono library using the high resolution clock. We only show experiments where one of the methods needed more than one second. Table 1 lists the results of our experiments. It shows that the new method is in almost all cases at least one order of magnitude faster. Although both methods are asymptotically of the same complexity, it seems that they have different worst case inputs. Our experiments suggest that the ones that slow down the new approach are less frequent in practice than those making the former one slow.
In the remainder of this section, we want to take a closer look at the outcome of our experiments. As Table 1 shows for the decreasing computation, both methods needed less than 1 ms for 29 of all models. In 7 models the former method was faster, whereas in 6 of them the difference amounted to only a couple of milliseconds. In the remaining 64 models the new approach was faster. All in all the new approach needed only 2.86 % of the time compared to the former method. Even if we leave out the biggest outliers the new approach needs less than 10 % of the time.
The picture for the increasing computation is even better. There are 19 models where both methods needed less than 1 ms. In 8 models the former method was faster, but in all of these cases the difference was also only a couple of milliseconds. In the remaining 73 models the new method was faster. All in all the new approach needed only 0.79 % of the time compared to the former method. And if we again leave out the biggest outliers the new approach still needs less than 10 % of the time.
There are only three models, where the new method is slower. In two of them, the difference is only a couple of milliseconds. But for the CloudDeploymentPT-7b model the decrease computation needed more than 38 seconds, while the former approach needed not even one. We thoroughly investigated this case, but we could not find any useful hints, why this model performs completely different than the rest.
Starting from the 2020 edition of the MCC, LoLA 2 will use the new method and with this the model checking performance will increase, since more time is available for the actual verification. Especially in large Petri nets there will be a lot more time available to validate a given specification. The new approach addresses mainly the runtime performance. In the future we also plan to use DI(N ) for the reduction of memory used to save the decreasing and increasing transitions for each transition.