Verification of Token-Scaling Models using an Under-Approximation Torsten Liebke and Karsten Wolf Universität Rostock, Institut für Informatik, Germany {torsten.liebke,karsten.wolf}@uni-rostock.de Abstract. In the model checking domain the state explosion problem is the core issue. The cause is usually the sheer size of the model or the cardinality of tokens in the initial state. For the latter, which we call token-scaling models, we propose an under-approximation for reachable states. The idea is to reduce the number of tokens in the initial state and thus reducing the state space. If in the reduced state space a witness path is found, then the witness path can also be executed in the original state space. This method preserves existential temporal properties (ECTL∗ ) using a simulation relation between the reduced and the original state space. Since the cardinality of the initial marking varies from only a few tokens to multi-digit numbers of tokens, we apply heuristics to compute the number of tokens that should be removed. We implemented the new method in the explicit model checker LoLA 2. The experiments, done on the model checking contest benchmark, show that this method can speed up the model checking process and solve additional queries. Keywords: Model Checking · Under-Approximation · Witness Path. 1 Introduction State space explosion is the main issue in the model checking domain. The cause in place/transition Petri nets (P/T net) is usually either the model size itself, or the cardinality of the initial marking, i.e., the number of tokens on the initially marked places is large and thus resulting in a large state space. In this paper we are concerned with the latter one. P/T nets that have a large number of tokens on the initially marked places, are usually scaling over the number of tokens in the initial marking, while the net stays the same. We call such nets token-scaling models. Token-scaling models are widespread in a lot of different fields. E.g., in biochemistry the tokens represent molecules, or in scheduling problems they rep- resent resources. Such a biochemistry example model would be the Angiogenesis model [2], which is part of the model checking contest (MCC) [1]. It consists of 39 places, 64 transitions and 185 arcs and with scaling parameter 25 it results Copyright c 2020 for this paper by its authors. Use permitted under Creative Com- mons License Attribution 4.0 International (CC BY 4.0). 2 Torsten Liebke and Karsten Wolf in over 4.3 · 1019 reachable markings. One example for a scheduling problem would be the RobotManipulation model [5] from the MCC. The structure is even smaller and consists of only 15 places, 11 transitions and 34 arcs and with scaling parameter 10000 this results in over 2.8 · 1033 reachable markings. To combat the state explosion problem on token-scaling models, we introduce an under-approximation for the verification of existentially quantified temporal properties (ECTL∗ ). The idea is to reduce the number of tokens in the initial marking, on places which have more than one token. Due to this the state space is also reduced. If in the reduced state space a witness path is found, then the witness path can also be executed in the original state space. For preserving ECTL∗ formulas a simulation relation [6] between the original and the reduced transition system needs to be established. The cardinality of the initial marking depends on the model and its scaling parameter, which can vary from only a few to multi-digit numbers of tokens. we apply different heuristics to compute how many tokens should be removed from the initial marking. The introduced method works with all specifications were a single path, ei- ther a witness path or a counterexample, is enough to verify the specification. This means next to positive ECTL∗ formulas with a witness path, we can verify ACTL∗ formulas (universal temporal properties) and LTL formulas (linear time logic) which have counterexamples. The downside of the token-scaling verifica- tion is, it is only a sufficient condition and can only provide answers if a witness path or a counterexample exists. If this is not the case, the original state space has to be checked. The upside is that this method uses in the end a normal model checking algorithm, meaning it can be combined with other reduction techniques like symmetries [8] or partial order reduction [3, 7, 9]. We implemented the introduced method in our award winning model check- ing tool LoLA 2 and tested it on the model checking contest (MCC) benchmark. We run the token-scaling verification in parallel to the actual model checking algorithm. The experiments show that the token-scaling method can produce results faster and solve additional queries, which couldn’t be solved before due to the large state space. The paper is organized as follows. We start in Section 2 with a motivational example. In Section 3 we give a brief introduction of the terminology of P/T nets, temporal logic and simulation. Then we introduce our new under-approximation for token-scaling models in Section 4. We continue in Section 5 with the in- troduction of two different heuristics to increase the performance. It follows an experimentally validation of our new approach in Section 6. And we conclude the work in Section 7. 2 Motivational example Figure 2 shows the token-scaling P/T net RobotManipulation [5]. In the MCC the scaling parameter n ∈ N is between 1 and 10000. The initial marking is based on n. The three marked places p_i1, access and r_stopped get the following number of tokens: p_i1 = 2 · n + 1 and access = r_stopped = 2 · n. The model Verification of Token-Scaling Models using an Under-Approximation 3 Fig. 1. RobotManipulation [5] model from the MCC with n = 1. The number of initial tokens is in place p_i1 = 2 · n + 1 and in places access = r_stopped = 2 · n. consists of 15 places, 11 transitions and 34 arcs. Despite its simple structure, the size of the state space for n = 10000 is rather large and results in 2.8 · 1033 reachable markings. We discovered that there are quite a few interesting temporal properties, which are not dependent on the actual number of tokens in the initial marking. The idea is now to reduce the number of tokens on the marked places in the initial marking and therefore reducing the state space. If we find a witness path in the model with a reduced initial marking, then we know the witness path can also be executed in the model with the original initial marking. It follows that if the property under investigation holds with the reduced initial marking, then the property also holds with the original initial marking. For our example model with n = 5000 a simplified specification ϕ from the last edition of the MCC is concerned with the comparison of the cardinality of some places: ϕ = EF(p_rel > p_m AND p_m > p_rdy), i.e., does a path exists, where in a marking finally it holds, that (p_rel > p_m AND p_m > p_rdy). With n = 5000 the places access and r_stopped have 10000 tokens and the place p_i1 has 10001 tokens in the initial marking. We tested this with our model checking tool LoLA 2 [11]. Without partial order reduction LoLA 2 could not verify this property, even after computing the first one billion states. With partial order reduction enabled a witness path consisting of 195006 transitions was found, while the overall computed reachable markings where 250010. Using our new under-approximation we reduced the number of tokens in the initial 4 Torsten Liebke and Karsten Wolf marking of all marked places to 5 tokens. With this, LoLA 2 found a witness path consisting of only 112 transitions, while computing only 159 markings in total. This is with and without partial order reduction enabled. We see the possible speed-up, here three orders of magnitude, using the under-approximation. 3 Terminology 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) ∈ / F , and an initial marking m0 : P → N, where marking is a mapping m : P −→ N. The behaviour of a P/T net is defined by the transition rule. Definition 2 (Transition rule of a P/T net). Let N = [P, T, F, W, m0 ] be a P/T net. Transition t ∈ T is enabled in marking m if, for all p ∈ P , W (p, t) ≤ m(p). If t is enabled in m, t can fire, producing a new marking m0 where, for all p ∈ P , m0 (p) = m(p) − W (p, t) + W (t, p). This firing relation is t denoted as m → − m0 . It can be extended to a marking sequence by the following ε ω t inductive scheme: m − → m (for the empty sequence ε), and m − → m0 ∧ m0 → − ωt m00 =⇒ m −→ m00 (for a sequence ω ∈ T ∗ and a transition t ∈ T ). Using the transition rule, a P/T net induces a transition system, which is also called the reachability graph or the state space of the P/T net. Definition 3 (Labeled Transition System, Reachability Graph). A tran- sition system consists of a set S of states, an initial state s0 ∈ S, and a labelled transition relation E : S × L × S, for some label set L of transitions. The reachability graph of a P/T net is a transition system, where the set of markings, transitively reachable from the initial marking m0 using the transition rule of the P/T net, is the set of states, and the transition rule defines the set of vertices. m0 serves as initial state. A marking m0 is reachable from a marking ω m in a P/T net if there is a marking sequence ω ∈ T ∗ with m − → m0 . We continue with the introduction of the syntax and semantics of the tem- poral logic CT L∗ . We start with the presentation of atomic propositions. Definition 4 (Atomic proposition). Let N = [P, T, F, W, m0 ] be a P/T net. An atomic proposition is one of the constants true and false, or an expression of the shape k1 p1 + · · · + kn pn ≤ k, for some n ∈ N, k1 , . . . , kn , k ∈ Z, and p1 , . . . , pn ∈ P . For a marking Pn m of N , m satisfies proposition k1 p1 +· · ·+kn pn ≤ k if and only if the term i=1 ki m(pi ) actually evaluates to a number less or equal to k. The fact that m satisfies atomic proposition ϕ is denoted by m |= ϕ. Definition 5 (Syntax of CT L∗ ). For a given set of atomic proposition AP , the temporal logic CT L∗ is inductively defined as follows: Verification of Token-Scaling Models using an Under-Approximation 5 – Every ϕ ∈ AP is a state formula; – If ϕ and ψ are state formulas, so are (ϕ ∧ ψ), (ϕ ∨ ψ), and ¬ϕ; – Every state formula is a path formula; – If ϕ and ψ are path formulas, so are (ϕ ∧ ψ), (ϕ ∨ ψ), ¬ϕ, X ϕ, F ϕ, G ϕ, (ϕ U ψ), and (ϕ R ψ); – If ϕ is a path formula then E ϕ and A ϕ are state formulas. We now consider the semantics of the logic CTL∗ with respect to a Kripke structure. A Kripke structure requires every state to have a successor state. Hence, the reachability graph of a P/T net with deadlocks is not a Kripke struc- ture, but can be turned into one, by adding a silent transition from every dead- lock state to itself. Definition 6 (Semantics of CT L∗ ). Let AP be a set of atomic propositions and N a P/T net with its reachability graph T S extended to a Kripke structure. The semantics of CT L∗ is defined by satisfaction relations of a state formula ϕ at a state (i.e., a marking) s, denoted s |= ϕ, and of a path formula ϕ by a path π, denoted π |= ϕ. – for ϕ ∈ AP , let s |= ϕ according to Def. 4; – for a state formula ϕ, π |= ϕ if π = s1 s2 . . . and s1 |= ϕ; – π |= (ϕ ∧ ψ) if π |= ϕ and π |= ψ; s |= (ϕ ∧ ψ) if s |= ϕ and s |= ψ; – π |= ¬ϕ if π 6|= ϕ; s |= ¬ϕ if s 6|= ϕ; – π |= X ϕ for π = s1 s2 . . . if π 0 = s2 s3 . . . and π 0 |= ϕ; – π |= (ϕ U ψ) for π = s1 s2 . . . if, for some i ≥ 1 and πi = si si+1 . . . , πi |= ψ, and for all j (1 ≤ j < i), πj = sj sj+1 and πj |= ϕ; – s |= E ϕ if, for some path π starting in s, π |= ϕ. Let further ϕ ∨ ψ be equivalent to ¬(¬ϕ ∧ ¬ψ), F ϕ to true U ϕ, G ϕ to ¬ F ¬ϕ, ϕ R ψ to ¬(¬ϕ U ¬ψ), and A ϕ to ¬ E ¬ϕ. A Kripke structure satisfies a state formula if its initial state does. It satisfies a path formula if all paths starting in the initial state do. For CT L∗ , several fragments are frequently studied. Definition 7 (Fragments of CT L∗ ). CT L∗ formula ϕ is in – ACTL∗ if ϕ does neither contain E nor ¬; – ECTL∗ if ϕ does neither contain A nor ¬; – CTL if every occurrence of X, F, G, R, U is immediately preceded by an oc- currence of A or E; – LTL ⊂ ACTL∗ if ϕ does neither contain E nor A; And since we have all the equivalences we need to push negations to the level of atomic propositions. Further we know that ECTL∗ properties are preserved if transition systems are related by a simulation relation. 6 Torsten Liebke and Karsten Wolf Definition 8 (Abstraction, Simulation [6]). Let T S1 = [S1 , E1 , s01 ] and T S2 = [S2 , E2 , s02 ] be Kripke structures. A relation σ ⊆ S1 ×S2 is an abstraction relation if, for all atomic propositions ϕ, (s, s0 ) ∈ σ and s |= ϕ implies s0 |= ϕ. Abstraction relation σ is a simulation if (s01 , s02 ) ∈ σ and, for all (s1 , s2 ) ∈ σ and (s1 , t, s01 ) ∈ E1 implies the existence of a state s02 where (s2 , t0 , s02 ) for some label t0 , and (s01 , s02 ) ∈ E2 . Simulation preserves certain temporal logic fragments. Proposition 1 (Simulation preserves ACTL∗ , [4]). Let T S1 = [S1 , E1 , s01 ] and T S2 = [S2 , E2 , s02 ] be Kripke structures. If T S1 simulates T S2 , then – T S1 , s01 |= ϕ implies T S2 , s02 |= ϕ, for any ACTL∗ formula ϕ; – T S2 , s02 |= ϕ implies T S1 , s01 |= ϕ, for any ECTL∗ formula ϕ. Using this, we can find a counterexample for ACTL∗ using an equivalent ECTL∗ formula. Proposition 2 (Counterexample for ACTL∗ ). For every ACTL∗ formula ϕ there exists an ECTL∗ formula ψ s.t. ¬ϕ and ψ are equivalent CTL∗ formulas. 4 Under-approximation for token-scaling models For token-scaling models we propose an under-approximation to reduce the size of the state space. The idea is to reduce the number of tokens on certain places in the initial marking. I.e., the state space is reduced, since fewer tokens are available. The basic concept is to use a threshold of tokens λ ∈ N. The number of tokens on places that contain more than λ tokens in the initial marking, will be reduced to λ tokens. Definition 9 (Reduced initial marking m0r ). Let N = [P, T, F, W, m0 ] be a P/T net and λ ∈ N. In the reduced initial marking m0r it holds for all p ∈ P that m0r (p) = λ if, m0 (p) ≥ λ or m0r = m0 (p) else. We substitute the initial marking m0 of the given P/T net N with the reduced initial marking m0r and verify the property under investigation on the reduced net. Definition 10 (Reduced net Nr ). Let N = [P, T, F, W, m0 ] be a P/T net. We call Nr = N [m0 7→ m0r ] the reduced net, where the initial marking m0 is substituted with the reduced initial marking m0r . With the reduced net, we can now introduce the under-approximation for token-scaling models. Theorem 1 (N simulates Nr ). Let N = [P, T, F, W, m0 ] be a P/T net, with the induced transition system T S = [S, E, s0 ] and Nr = [P, T, F, W, m0r ] the corresponding reduced net, with the induced transition system T Sr = [Sr , Er , s0r ]. It holds that T S simulates T Sr and that T Sr , s0r |= ϕ implies T S, s0 |= ϕ, for any ECTL∗ formula ϕ. Verification of Token-Scaling Models using an Under-Approximation 7 Proof. The existence of the simulation, together with proposition 1 preserve ECTL∗ . Since the new system T Sr is an under-approximation, it holds that the original system T S is relative to the reduced system T Sr an over-approximation. For over-approximation, it is well known (proposition 1), that the simulation preserves ACTL∗ . And with the inversion, which is the under-approximation, the simulation preserves ECTL∗ . t u This approach is able to verify temporal properties in a transition system which have a witness path or a counterexample. Proposition 3. For every ECTL∗ formula ϕ, it holds, if ϕ is true in the reduced net Nr then ϕ is also true in the original net N . For every ACTL∗ formula ϕ and with this also for every LTL formula ϕ, it holds, if ϕ is false in the reduced net Nr then ϕ is also false in the original net N . 5 Heuristics The reduced initial marking has to balance between two objectives. On one hand a small state space is desired and therefore initially marked places should have as few tokens as possible. On the other hand it should have enough tokens to verify the property under investigation. The optimum would be that initially marked places have exactly the number of tokens on it, which are needed to produce the witness path. Since we don’t know this number in advance, we propose two heuristics, to compute the reduced initial marking. We calculate a threshold for the marked places in the initial marking and cut the number of tokens on these places, to the calculated threshold. Largest constant heuristic: Given is a multiplier n ∈ N, we compute the threshold based on the n-times largest constant appearing in the net, meaning the arc weight and the formula. Percentage heuristic: Given is a divisor d ∈ N, the threshold for each place is 1/d-times the original number of tokens. To avoid getting zero tokens on places, we always round up the division. 6 Experimental validation We implemented the introduced method in our explicit model checker LoLA 2 [11]. For evaluating the methods, we used the benchmark provided by the model checking contest 2019 [1]. The benchmark consists of 94 models, which result in 1018 model-instances due to the scaling parameter. As specification we use the formulas provided in the MCC 2019. Although the introduced method works also for LTL and a lot of CTL formulas, we only present the experimental results for reachability queries. The results for LTL and CTL are similar. For each instance, there are 32 reachability formulas: 16 of them are concerned with the cardinality of tokens on places and the other 16 are concerned with the fireability of transitions. 8 Torsten Liebke and Karsten Wolf For our purpose we only choose a subset of the models from the benchmark. We consider only P/T nets, since coloured nets usually scaling over the cardi- nality of places, transitions and arcs. In the MCC coloured nets are mostly safe and if they are not safe they contain only a few tokens on each place. This is also true for their place/transition counterparts, which we therefore also ignore. We also only consider nets which are not safe. Furthermore, we consider only nets, whose initial marking has tokens that can be removed. We also avoid one instance that has in the initial marking, on at least one place, more than 232 tokens. All in all we consider 21 models with 214 instances with 32 formulas for each instance. The total number of checked formulas are 6848. We executed the experiments on our machine Ebro, which has been used for executing parts of the actual MCC in recent years. It has 32 physical cores running at 2.7 GHz and 1 TB of RAM. The operation system used is CentOS Linux 7 (Core). We run our new method in parallel to the actual state space search and a structural method, namely a counterexample guided abstraction re- finement (CEGAR) state equation [10]. Both methods are well developed and already pushed to the limits. From 6848 formulas 5152 formulas were solvable with a witness path or counterexample. The remaining formulas were either solv- able directly in the initial marking or the entire state space had to be searched. There were 122 formulas that could not be solved. Our new method, with the threshold set to 5 tokens, and run in parallel to the other two methods, was able to solve 436 (8.5 %) of the remaining 5152 queries. No additional query from the 122 unsolved ones could be solved. The picture stays more or less the same if we change the threshold to anything between 1 and 10. The largest constant heuristic does not perform very well with multiplier 1 or 2, although increasing the multiplier is improving the performance. The percentage heuristic, on the other hand, performs really well with n set to anything between 3 and 10. With n = 3, the new method could solve 659 (12.8 %) queries. It was even able to solve 8 (6.5 %) queries from the 122 unsolved ones. 7 Conclusion Token-scaling P/T nets tend to have large state spaces, since they have a lot of tokens on the initially marked places. However, there are a lot of interesting specifications, which can be verified with way fewer tokens in the initial mark- ing. We introduced an under-approximation for token-scaling P/T nets. It is a sufficient quick check, that is based on the reduction of tokens on the marked places in the initial marking. The method is applicable whenever a witness path can be found, namely in the class of ECTL∗ formulas, including reachability, or whenever a counterexample can be found, namely in the class of ACTL∗ and LTL formulas. The experiments show that running the token-scaling method in parallel to a full model checking algorithm speeds up the verification pro- cess, which gives in reverse more time to other verification queries. Our new method could solve 9.6 % of all queries in the benchmark, while competing di- rectly against well established methods like the actual state space search and the Verification of Token-Scaling Models using an Under-Approximation 9 CEGAR state equation method. An additional 6.5 % of the queries that could not be solved by any other method were solved by the new method. We also showed that using a good heuristic can increase the performance even more. In the future we are interested in better heuristics using the structural information of the P/T net and involving the formula. References 1. Fabrice Kordon et al. Presentation of the 9th edition of the model checking contest. In Proc. TACAS, LNCS 11429, pages 50–68, 2019. 2. Lucia Napione et al. On the use of stochastic Petri nets in the analysis of signal transduction pathways for angiogenesis process. In Proc. CMSB, LNCS 5688, pages 281–295, 2009. 3. P. Godefroid and P. Wolper. A partial approach to model checking. Inf. Comput., 110(2):305–326, 1994. 4. Orna Grumberg and David E. Long. Model checking and modular verification. In Proc. CONCUR, LNCS 527, pages 250–265, 1991. 5. F. Kordon. RobotManipulation. https://mcc.lip6.fr/pdf/RobotManipulation- form.pdf, 2017. Accessed: 2020-03-01. 6. R. Milner. Communication and Concurrency. Prentice Hall international series in computer science. Prentice Hall, New York, 1989. 7. D. A. Peled. All from one, one for all: on model checking using representatives. In Proc. CAV, LNCS 697, pages 409–423, 1993. 8. Karsten Schmidt. How to calculate symmetries of petri nets. Acta Inf., 36(7):545– 590, 2000. 9. A. Valmari. Stubborn sets for reduced state space generation. In Advances in Petri Nets, LNCS 483, pages 491–515, 1989. 10. H. Wimmel and K. Wolf. Applying CEGAR to the Petri net state equation. Logical Methods in Computer Science, 8(3), 2012. 11. K. Wolf. Petri net model checking with LoLA 2. In Proc. PETRI NETS, LNCS 10877, pages 351–362, 2018.