Petri nets are an established formal method for modelling and verifying asynchronous, concurrent and distributed systems. To verify a specification, given as a temporal logic formula, state space methods often encounter the state space explosion problem. We propose a verification technique to solve the CTL query E (φ U ψ) using the Petri net state equation with a counterexample guided abstraction refinement (CEGAR) approach. The algorithm tries to solve EF ψ, while keeping φ true. Especially in case the property does not hold, the technique often terminates quickly. As a side product we show that (EX)kφ formulas can be solved with the CEGAR approach as well.
and extended by [
proach is especially good to verify negative results. This makes it a valuable complement to explicit model checking algorithms, which are in general good for verifying positive results, due to the on-the-fly effect.
In [
Definition 1 (place/transition net). A place/transition net [P, T, F, W, m0] consists of a finite set P of places, a finite set T of transitions, a set F ⊆ (P × T ) ∪ (T × P ) of arcs, a mapping W : (P × T ) ∪ (T × P ) −→ N where [x, y] ∈/ F if and only if W ([x, y]) = 0, and an initial marking m0. A marking is a mapping m : P −→ N.
Transition t is enabled in marking m if, for all p ∈ P , m(p) ≥ W ([p, t]). Firing an enabled transition in m yields the marking m′ where, for all p, m′(p) = m(p) − W ([p, t]) + W ([t, p]). This is denoted m −→t m′.
ings reachable from m0 form the set of states, m0 is the initial state, and the firing relation just defined forms the labeled transition relation. We restrict our considerations to Petri nets where the related transition system is finite.
all p ∈ P, t ∈ T , CN (p, t) = W (t, p) − W (p, t). The incidence matrix is involved in important and well-known results of Petri net theory.
Definition 2 (Reachability problem). Given is a tuple (N, m, m′) consisting of a Petri net N and two markings m, m′. A marking m′ is reachable from marking m in a Petri net N , if there exists a firing sequence w ∈ T ∗ with m −→w m′. The set of all reachable markings in N starting in m is written as RN (m). The question whether m′ ∈ RN (m) is called the reachability problem.
Proposition 1 (Petri net state equation). Let w ∈ T ∗ be a firing sequence of N , that is, the sequence of labels on a path from some marking m to a marking m′ in the transition system corresponding to N . Then it holds
m + CN · ℘(w) = m′ where ℘(w) is a vector where ℘(w)|t| is the number of occurrences of t in the sequence w.
In the sequel, we shall refer to ℘(w) as the Parikh vector of w.
Definition 3 (T-invariant). A Parikh vector ℘(w) is called a T -invariant if CN · ℘(w) = 0. If the firing sequence w is executable, we call ℘(w) realizable.
Definition 4 (Solution space). The solution of the Petri net state equation
m + CN · ℘(w) = m′ can be written as the sum of a base solution and a period
vector, which is a linear combination of T-invariants: ℘(w) = b + !i niyi, where
b ∈ NT is the base solution and ni ∈ N is the coefficient of the T-invariant
yi ∈ NT [
Consider a formal sum s = k1p1 + · · · + knpn. Every marking m turns this sum into the integer number vs(m) = k1m(p1) + · · · + knm(pn). We can immediately derive from the firing rule of Petri nets: Definition 5 (Delta). Let s be a formal sum and t a transition, then ∆ t,s is defined as ∆ t,s = k1CN (p1, t) + · · · + knCN (pn, t).
Lemma 1. For all markings m, m −→t m′ implies vs(m) + ∆ t,s = vs(m′).
As we assume the transition system to be finite, there is only a finite range of values that vs(m) can take. Call an integer number k a lower bound for formal sum s if, for any reachable marking m, vs(m) ≥ k, and upper bound for s if, for any reachable m, vs(m) ≤ k. There exist several approaches in Petri net theory for computing bounds. As an example, we can solve the following optimisation problem where s is the objective function (to be minimised or maximised) and the state equation serves as side condition. If the problem yields a solution with non-diverging value for the objective function, that value is a lower (resp. upper) bound for s.
Definition 6 (Increasing, decreasing). Given an atomic proposition of the form s ≤ k. Let L be a lower bound and U an upper bound for s. We call transition t w.r.t. the formal sum s: 1. weakly increasing iff ∆ t,s < 0 2. weakly decreasing iff ∆ t,s > 0 3. strongly increasing iff there is an upper bound U for s where ∆ t,s ≤ k − U 4. strongly decreasing iff there is a lower bound L for s where ∆ t,s > k − L.
sitions have the tendency to turn a false proposition into a true one while decreasing transitions help turning a true proposition into a false one.
p in a Petri net. Then all transitions in the preset of p are strongly decreasing. Lemma 2. Consider markings m and m′, transition t with m −→t m′ and atomic proposition s ≤ k. 1. If s ≤ k is false in m and true in m′ then t is weakly increasing w.r.t. s. 2. If s ≤ k is true in m and false in m′ then t is weakly decreasing w.r.t. s. 3. If t is strongly increasing w.r.t. s ≤ k then s ≤ k is true in m′. 4. If t is strongly decreasing w.r.t. s ≤ k then s ≤ k is false in m′.
⊓*
of the system behaviours, to simplify the analysis and verification. Finding the
right abstraction is hard. If it is too coarse, the verification might fail and if it
is too fine, the state space explosion problem might occur. A solution is to use
some initial abstraction [
reachability problem. Solving the state equation is a non-negative integer linear programming problem. The objective function for the ILP problem is the shortest firing sequence of the Parikh vector f (w) = !t∈T ℘(w)|t| leading from the initial marking m to the final marking m′.
The feasibility of this linear system is a necessary condition for reachability, but not a sufficient one. We distinguish between three different situations: – If the linear system is infeasible, the necessary condition is violated and the final marking is not reachable. – If the linear system has a realizable solution, then the final marking is reachable. – If the linear system has an unrealizable solution, which is a counterexample, then the abstraction has to be refined.
which fired less than ℘(w)|t| times. To produces a new solution which avoids the spurious one, we build a refined abstraction using inequalities for the ILP problem.
Definition 7 (Constraints). We define two types of constraints, both being
linear inequalities over transitions [
– Jump constraints have the form |ti| < n, with n ∈ N and ti ∈ T where |ti| represents the firing count of transition t. Using the fact that base solutions are pairwise incomparable, jump constraints intend to generate a new base solution. – Increment constraints have the form !k i=1 ni|ti| ≥ n with ni ∈ Z, n ∈ N, and ti ∈ T . Increment constraints are used to get a new non-base solution, i.e., T-invariants are added, since their interleaving with another sequence w may turn w from unrealizable to realizable.
Definition 8 (Partial solutions). Let N = (P, T, F, W, m) be a Petri net and m′ ∈ RN (m) a reachability problem. A partial solution is a tuple ps = (Γ, ℘(w), σ, r) with: – Γ is the set of jump and increment constraints. Together with the state equation they form the ILP problem. – ℘(w) is the minimal solution fulfilling the ILP problem.
σ – σ is a firing sequence with m −→ and ℘(σ) ≤ ℘(w). – r is the remainder with r = ℘(w) − ℘(σ) and ∀t ∈ T : (r(t) > 0 =⇒ ¬m −σ→t).
Partial solutions are produced during the examination of the solution ℘(w)
of the ILP problem by exploring the state space of N . For this an explicit model
checking algorithm with reachability preserving stubborn sets [
Theorem 1 (Reachability of solutions). If the reachability problem has a
solution, a realizable solution of the state equation can be reached by constantly
appending the minimal solution with constraints [
Solving E (φ U ψ) with the CEGAR approach Definition 9 (E(φ U ψ)). Let N = (P, T, F, W, m) be a Petri net and φ and ψ two propositions. m |= E(φ U ψ) ⇐⇒ ∃w ∈ T ∗ : m −→w m′, with ∃i ∈ N ∀j < i : (mj |= φ) ∧ (mi |= ψ). Which means that in every state along path w, φ is true until a state is reached where ψ is true.
It is well known that EF ψ can be rewritten as E (true U ψ). To solve E(φ U ψ), where φ and ψ are atomic propositions, we solve EF ψ with the CEGAR approach. In addition to this we introduce additional (balance) constraints to keep φ true along the path. Furthermore we cut-off paths in the exploration of partial solutions, whenever states are reached where both φ and ψ are false. Definition 10 (Balance constraints). Given a Petri net N = (P, T, F, W, m) and an atomic proposition φ = s0 ≤ k0 ∧ s1 ≤ k1 ∧ · · · ∧ sn ≤ kn, where si is a formal sum, 0 ≤ i ≤ n and i, k, n ∈ N. Tsi = {t ∈ T |∆ t,si ̸= 0} is the set of transitions which can change the value of si. It contains all weakly/strongly increasing/decreasing transitions w.r.t. to si. We call Tsi,ψ ⊆ Tsi the set of decreasing transitions w.r.t si, which are at the same time increasing w.r.t ψ: Tsi,ψ = {t ∈ Tsi |∆ t,si > 0 ∧ ∆ t,φ < 0}. We define variables δi, which are 0, if Tsi,ψ = ∅ and otherwise are MAX(∆ t,si |t ∈ Tsi,ψ). The δi-offset is the maximum arc weight of all transitions that can change the value of si ≤ ki from true to false and ψ from false to true. Let θi = ki − vsi (m) be the offset, which is the number of tokens that can be consumed from the initial marking and still leave the truth value of si ≤ ki unchanged. We call ∀si : !t∈Ts ∆ t,s ≤ θi + δi balance constraints w.r.t. si and m.
p0 t0
t1 p1 p2 t2 p3
As an example, consider Figure 1 and the formula E (p1 > 0) U (p3 > 0).
s ≤ k-format: E (−p1 ≤ −1) U (−p3 ≤ −1). To satisfy the formula, we check EF p3 > 0, while keeping p1 > 0 true along the path. The minimal solution to the ILP would be the firing vector (t1, t2), m −t−1t→2 m′, where m′ satisfies p3 > 0. But after firing the weakly decreasing transition t1 w.r.t. p1 > 0, a marking m′′ = (p0, p2) is reached that does neither satisfy p3 > 0 nor p1 > 0. To avoid this marking, the balance constraint would add the weakly increasing transition t0 to the solution vector, m −t−0−t1−t→2 m′, to keep p1 > 0 true.
Balance constraints in general ensure that the sum of all increasing and decreasing transitions w.r.t. a formal sum s is smaller than the offset, which is based on the initial marking and the maximal arc weight of all transitions t ∈ Tsi,ψ. In case the offset θi is negative, φ is violated and E(φ U ψ) has the value of ψ. We detect this case in the initial marking, before we compute the balance constraints and can return with a definitive answer directly in the beginning. Balance constraints make sure that φ is not violated and ψ is true in the final marking. The only transitions which are allowed to violate φ are in the set Tsi,ψ and they have also the effect to turn ψ to true. Due this effect, if such transitions exist, they tend to occur at the end of the firing sequence, but not exclusively. We add the balance constraints to our initial abstraction, the state equation and run the CEGAR algorithm for EF ψ.
Lemma 3. Given a Petri net N = (P, T, F, W, m) and formula φ = s0 ≤ k0 ∧ s1 ≤ k1 ∧ · · · ∧ sn ≤ kn, where si is a formal sum and k ∈ N and m |= φ. Adding to the ILP problem all balance constraints for φ and checking that θi ≥ 0, then it is guaranteed that after executing the entire firing sequence given as a solution ℘(w) to the ILP problem that ψ is true. It also ensures that if a complete firing sequence exists, φ is true along the path and is only violated, if at all, in the final marking, where ψ holds.
increasing/decreasing transitions affect si ≤ ki. The offset θi ensures that the truth value of si ≤ ki stays unchanged. The balance constraint ensures that φ is not violated minus the δi-offset, which ensures the possibility of a firing sequence which does not violate φ along the path, until ψ holds.
If the set Tsi,ψ is not empty, the δi-offset based on the maximum of ∆ t,si ensures that transitions are not ignored in the balance constraint that violate φ but also turn ψ to true. The additional offset, which is the maximal arc weight of the transitions in the set, is enough to make sure that only one transition is allowed to fire, with the effect of making φ false and ψ true. We use the maximum, since an arc weight, which is not the maximum, will have a smaller effect and will not change the outcome. Transitions from the set Tsi,ψ can also fire, if they are in a different context, i.e. when they do not turn φ to false.
Theorem 1 ensures that if the complete solution ℘(w) is fired, we get to the final marking m′ which satisfies ψ.
Lemma 3 only ensures that m′ |= ψ, where m′ is the final marking after firing the entire solution ℘(w). But it does not guarantee that intermediate markings satisfy φ. This is due to the fact that also decreasing transitions w.r.t. φ are allowed to fire.
Lemma 4. In the exploration of the solution space cutting off paths in markings m∗, with m∗ |= ¬φ∧¬ψ results in keeping only partial solutions which can become full solutions.
Proof. Based on Definition 9, marking m∗ |= ¬φ ∧ ¬ψ violates the property E(φ U ψ). All paths extending m∗ are also violating E(φ U ψ) and no extension to the path can make the property true. ⊓* ⊓*
Consider, for example, the Petri net in Figure 2 and the formula E (p1 + p2 > 0) U (p3 > 0). The minimal solution to the ILP is (t0, t1). After firing t0, a marking m′ = (p0, p5) is reached that violates p1 + p2 > 0 and p3 > 0. Lemma 4 ensures that this solution is cut off. There are also no increasing transitions we can add to this solution. Using the CEGAR approach, we jump to a new base solution, (t2, t3). But this solution is only a partial solution due to the fact that neither t2 nor t3 can fire. At this point, the CEGAR approach adds the T-invariant (t4, t5) from which tokens can be borrowed. Now we have a full t2t3t4(t5) solution and we get the path m −−−−−−→ m′ which satisfies p1 + p2 > 0 until (p3 > 0) is satisfied.
Theorem 2. Let N = (P, T, F, W, m) be a Petri net and φ, ψ atomic
propositions, with φ = s0 ≤ k0 ∧ s1 ≤ k1 ∧ · · · ∧ sn ≤ kn, where si is a formal sum
and k, n ∈ N and it holds that m |= φ. If E(φ U ψ) has a realizable solution
in the solution space, it can be reached by solving EF ψ using the CEGAR
approach from [
Proof. In [
p3 t1 t3 t5 Fig. 2. For the given Petri net and the formula E (p1 + p2 > 0) U (p3 > 0), the minimal solution (t0, t1) is cut off. With the CEGAR approach we jump to the next base solution (t2, t3), which is only a partial one. The T-invariant (t4, t5) is with the next CEGAR step and provides a full solution, m −t−2t−3−t4−(−t5→) m′. m′ |= ψ. Lemma 3 ensures that we only get solutions, such that after firing the complete solution ℘(w), φ holds. Lemma 4 makes sure that φ is not violated along the path. ⊓* 6
Solving (EX)kφ with the CEGAR approach Definition 11 ((EX)kφ). Given a Petri net N = (P, T, F, W, m), a proposition φ and k ∈ N \ {0}. m |= (EX)kφ ⇐⇒ ∃w ∈ T k ∧ m −→w mk ∧ mk |= φ. This w means there exists a path m −→ mk with |w| = k transitions in it and mk |= φ.
For example for k = 2 this means (EX)2φ = EX EX φ ⇐⇒ ∃t1t2 ∈ T 2 : t1t2 m −−→ mk ∧ mk |= φ. To solve (EX)kφ, we solve EF φ. In addition to this we introduce an additional (length) constraint which ensures that the length of sequence w of the ILP problem solution ℘(w) is equal to k.
Definition 12 (Length constraint). Given a proposition of the form (EX)kφ with k ∈ N\{0} and an atomic proposition φ. We call !t∈T ℘(w)|t| = k a length constraint.
℘(w) should exactly be k. To make the proposition true, marking mk, which is
reached after firing k transitions, must satisfy φ.
Theorem 3. Given a Petri net N = (P, T, F, W, m) and proposition (EX)kφ
with k ∈ N \ {0}. If (EX)kφ has a realizable solution in the solution space, it can
be reached by solving EF φ using the CEGAR approach from [
We proposed two promising techniques to solve E(φ U ψ) and (EX)kφ with the
To solve E(φ U ψ), we solve EF ψ and keep φ true in every state along the path. To keep φ true, we introduced the concept of balance constraints for the
solution vector. Furthermore we used a cut-off criterion to ensure that φ is also true in every state along the path. For solving (EX)kφ we introduced the concept of a length constraint, which makes sure that we only get solutions of length k.
These techniques will be implemented in LoLA 2 [