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.
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
represent resources. Such a biochemistry example model would be the Angiogenesis
model [
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 [
The introduced method works with all specifications were a single path,
either 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
verification 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 [
We implemented the introduced method in our award winning model checking 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 introduction 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
Figure 2 shows the token-scaling P/T net RobotManipulation [
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 [
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 : P ! N, where marking is a mapping m : P ! N.
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). 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 m !t m0. It can be extended to a marking sequence by the following inductive scheme: m !" m (for the empty sequence "), and m !! m0 ^ m0 !t m00 =) m !!t m00 (for a sequence ! 2 T and a transition t 2 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 transition system consists of a set S of states, an initial state s0 2 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 ! 2 T with m !! m0.
We continue with the introduction of the syntax and semantics of the temporal 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 k1p1 + + knpn k, for some n 2 N, k1; : : : ; kn; k 2 Z, and p1; : : : ; pn 2 P . For a marking m of N , m satisfies proposition k1p1+ +knpn k if and only if the term Pin=1 kim(pi) actually evaluates to a number less or equal to k. The fact that m satisfies atomic proposition ' is denoted by m j= '. Definition 5 (Syntax of CT L ). For a given set of atomic proposition AP , the temporal logic CT L is inductively defined as follows: – Every ' 2 AP is a state formula; – If ' and are state formulas, so are (' ^ ), (' _ – Every state formula is a path formula; – If ' and are path formulas, so are (' ^ ), (' _
(' U ), and (' R ); – If ' is a path formula then E ' and A ' are state formulas. ), and :'; ), :', X ', F ', G ',
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 structure, but can be turned into one, by adding a silent transition from every deadlock 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 j= ', and of a path formula ' by a path , denoted j= '. – for ' 2 AP , let s j= ' according to Def. 4; – for a state formula ', j= ' if = s1s2 : : : and s1 j= '; – j= (' ^ ) if j= ' and j= ; s j= (' ^ ) if s j= ' and s j= ; – j= :' if 6j= '; s j= :' if s 6j= '; – j= X ' for = s1s2 : : : if 0 = s2s3 : : : and 0 j= '; – j= (' U ) for = s1s2 : : : if, for some i 1 and i = sisi+1 : : : , i j= and for all j (1 j < i), j = sj sj+1 and j j= '; – s j= E ' if, for some path starting in s, j= '. 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 occurrence 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.
Definition 8 (Abstraction, Simulation [
Proposition 1 (Simulation preserves ACTL , [
Proposition 2 (Counterexample for ACTL ). For every ACTL formula ' there exists an ECTL formula s.t. :' and are equivalent CTL formulas. 4
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 2 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 2 N. In the reduced initial marking m0r it holds for all p 2 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 j= ' implies T S; s0 j= ', for any ECTL formula '. 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 . tu 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
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 2 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 2 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
We implemented the introduced method in our explicit model checker LoLA
2 [
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 cardinality 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
refinement (CEGAR) state equation [
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 marking. 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 process, 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 directly against well established methods like the actual state space search and the 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.