=Paper=
{{Paper
|id=Vol-2424/paper4
|storemode=property
|title=Solving E (φUψ) using the CEGAR Approach
|pdfUrl=https://ceur-ws.org/Vol-2424/paper4.pdf
|volume=Vol-2424
|authors=Torsten Liebke,Karsten Wolf
|dblpUrl=https://dblp.org/rec/conf/apn/LiebkeW19a
}}
==Solving E (φUψ) using the CEGAR Approach==
https://ceur-ws.org/Vol-2424/paper4.pdf
Solving E (φ U ψ) using the CEGAR Approach
Torsten Liebke and Karsten Wolf
Universität Rostock, Institut für Informatik, Germany
{torsten.liebke,karsten.wolf}@uni-rostock.de
Abstract. Petri nets are an established formal method for modelling
and verifying asynchronous, concurrent and distributed systems. To ver-
ify a specification, given as a temporal logic formula, state space methods
often encounter the state space explosion problem. We propose a veri-
fication 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.
Keywords: Petri Nets, Verification, Structural Analysis, CEGAR, ILP.
1 Introduction
Explicit model checking algorithms encounter the state space explosion problem.
A different concept to verify the reachability problem was introduced in [7]
and extended by [4, 3]. This concept is based on the structure of Petri nets
and decreases the state space explosion problem significantly. It transforms the
problem to an integer linear programming (ILP) problem, which runs iteratively
based on counterexample guided abstraction refinement, proposed in [1].
Due to the fact that ILP problems can become infeasible, the CEGAR ap-
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 [5] it is shown that it is beneficial to use specialised routines for com-
mon formulas to increase the number of verifiable problems. We propose two
techniques to solve the CTL queries E(φ U ψ) and (EX)k φ with the CEGAR
approach for Petri nets. Using well known tautologies, also A(φ R ψ) and (AX)k φ
are solvable with these techniques. [5] also shows that only 62.3 % of the E(φ U
ψ)/A(φ R ψ) formulas from the model checking contest 2018 [2] are solved using
the explicit model checker LoLA 2 [8]. This is due to the reason that the on-the-
fly effect has no or very limited impact in some cases, e.g. when φ ∧ ¬ψ holds in
the entire state space. For this case, the CEGAR approach we are introducing
will terminate very quickly, stating that the ILP problem is infeasible.
One drawback is that termination of the introduced approach is not guar-
anteed, which makes the procedure incomplete [7]. Applying it in a portfolio
approach with traditional algorithms, this drawback vanishes.
48 PNSE’19 – Petri Nets and Software Engineering
2 Basic Definitions
We consider place/transition Petri nets.
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
/ F if and only if W ([x, y]) = 0, and an initial marking m0 . A marking is
[x, y] ∈
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 −→ m′ .
t
Every Petri net defines a labeled transition system where the set of mark-
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.
The incidence matrix of a Petri net N is a matrix CN : P ×T −→ Z where, for
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′ . The set of all reachable markings in N starting in m is written as
w
m −
RN (m). The question whether m′ ∈ RN (m) is called the reachability problem.
The feasibility of the Petri net state equation is a necessary condition for a
positive answer to this question.
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.
A realizable T-invariant is a cycle in the state space and will not change the
marking.
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 ni yi , where
b ∈ NT is the base solution and ni ∈ N is the coefficient of the T-invariant
yi ∈ NT [3, 7].
Liebke et.al.: Solving E ( U ) using the CEGAR approach 49
3 Increasing and Decreasing Transitions
Consider a formal sum s = k1 p1 + · · · + kn pn . Every marking m turns this sum
into the integer number vs (m) = k1 m(p1 ) + · · · + kn m(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 = k1 CN (p1 , t) + · · · + kn CN (pn , t).
Lemma 1. For all markings m, m −
→ m′ implies vs (m) + ∆t,s = vs (m′ ).
t
Proof. Apply the Petri net state equation. ⊓
*
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.
Based on Lemma 1, we can identify increasing and decreasing transitions.
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.
The terminology may sound strange at first glance. However, increasing tran-
sitions have the tendency to turn a false proposition into a true one while de-
creasing transitions help turning a true proposition into a false one.
Let p ≤ 0 be an atomic proposition where p is the number of tokens on place
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 −
→ m′ and atomic
t
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′ .
Proof. Regarding 1, we have vs (m) > k and vs (m′ ) ≤ k. By Lemma 1, we
conclude ∆t,s < 0. Regarding 3, we have vs (m) ≥ L (since L is a lower bound).
Hence, vs (m′ ) = vs (m) + ∆t,s ≤ L + ∆t,s and, according to Def. 6, vs (m′ ) ≤ k.
⊓
*
50 PNSE’19 – Petri Nets and Software Engineering
4 CEGAR approach for reachability analysis in Petri nets
Abstraction is a powerful method for verifying systems. It omits irrelevant details
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 [1], which is an overapproximation of the original system
and then iteratively refine the abstraction based on spurious counterexamples.
In our case, the Petri net state equation is the initial abstraction for the
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 reach-
able.
– If the linear system has an unrealizable solution, which is a counterexample,
then the abstraction has to be refined.
If we have an unrealizable solution, then there exists at least one t ∈ T
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 [7].
– 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. !k
– Increment constraints have the form 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.
Adding the two types of constrains to existing solutions we can traverse
through the solution space and check whether the unrealizable solution of our
linear system becomes realizable or whether the ILP problem becomes infeasible.
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:
Liebke et.al.: Solving E ( U ) using the CEGAR approach 51
– Γ is the set of jump and increment constraints. Together with the state equa-
tion 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 [6] can be used to
build a tree of reachable markings, such that for all transitions t ∈ T it holds
that they only occur ℘(w)|t| times. Each path to a leaf represents a maximal
firing sequence of a new partial solution. If a partial solution has an empty
remainder r = 0, it is a full solution and the reachability problem is satisfied.
If no full solution exists, ℘(w) might be realizable by another firing sequence
σ ′ , or by adding a jump constraint to get to a new base solution, or by adding
an increment constraint to get additional tokens for transitions with r(t) > 0.
If all possible partial solutions are explored and no full solution is found, the
reachability problem can not be satisfied.
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 [7].
5 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 − → m′ , with ∃i ∈ N ∀j <
w
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
52 PNSE’19 – Petri Nets and Software Engineering
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.
t0 t1 t2
p0 p1 p2 p3
Fig. 1. The minimal solution for this Petri net and the formula E (p1 > 0) U (p3 > 0)
is t1 t2 . Since t1 is weakly decreasing w.r.t. p1 > 0, the balance constraint adds the
weakly increasing transition t0 to the solution.
As an example, consider Figure 1 and the formula E (p1 > 0) U (p3 > 0).
Note that this formula and every other formula can be rewritten into the required
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 −− → m′ , where m′ satisfies p3 > 0.
t1 t2
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 −− −−→ m′ , to keep p1 > 0 true.
t0 t1 t 2
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.
Proof. Regarding the second claim, we know, based on Definition 6, that only
increasing/decreasing transitions affect si ≤ ki . The offset θi ensures that the
Liebke et.al.: Solving E ( U ) using the CEGAR approach 53
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
t2 t3 t4 (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 proposi-
tions, 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 ap-
proach from [7] and by adding all balance constraints to the initial abstraction
and cutting-off all paths starting in m∗ in the exploration of the solution space,
whenever such a marking m∗ |= ¬φ ∧ ¬ψ is reached.
Proof. In [7] EF ψ is proved. We constantly add jump and increment constraints
to get to a full solution, such that the final marking of this solution satisfies
54 PNSE’19 – Petri Nets and Software Engineering
t0 t1
p0
t2 t3
p1 p2 p3
p4
t4 t5
p5
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
t2 t3 t4 (t5 )
next CEGAR step and provides a full solution, m −−−−−−→ 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 − → mk ∧ mk |= φ. This
w
means there exists a path m −
→ mk with |w| = k transitions in it and mk |= φ.
w
For example for k = 2 this means (EX)2 φ = EX EX φ ⇐⇒ ∃t1 t2 ∈ T 2 :
→ mk ∧ mk |= φ. To solve (EX)k φ, we solve EF φ. In addition to this
t1 t2
m −−
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.
The sum of the number of occurrences of all transitions in the Parikh-vector
℘(w) should exactly be k. To make the proposition true, marking mk , which is
reached after firing k transitions, must satisfy φ.
Liebke et.al.: Solving E ( U ) using the CEGAR approach 55
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 [7] and by adding
the length constraint to the initial abstraction.
Proof. Based on Definition
! 11, m |= (EX) φ ⇐⇒ ∃w ∈ T ∧m −
w
k k
→ m′ ∧m′ |= φ.
The length constraint t∈T ℘(w)|t| = k from Definition 12 ensures that only
solutions ℘(w) of the ILP problem are found, such that the length of the firing
sequence is exactly k and results in the final marking mk |= φ. ⊓
*
7 Conclusion and future work
We proposed two promising techniques to solve E(φ U ψ) and (EX)k φ with the
CEGAR approach for Petri nets.
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
ILP problem to ensure that an atomic proposition is true after firing the entire
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 [8]. LoLA 2 is an explicit
model checker and is every year on the podium of the Model Checking Contest
(MCC) for Petri nets. Once implemented we expect that the proposed approach
will increase the verification performance for this formulas significantly. Espe-
cially in case of a negative result, the procedure will terminate quickly, due to
the fact that the ILP problem will become infeasible. We expect a similar per-
formance increase as it was the case for the CEGAR approach for reachability
analysis, where the performance of LoLA 2 increased from solving under 80 %
to over 90 % in the MCC.
References
1. Edmund M. Clarke, Orna Grumberg, Somesh Jha, Yuan Lu, and Helmut Veith.
Counterexample-guided abstraction refinement. In Computer Aided Verification,
12th International Conference, CAV 2000, Chicago, IL, USA, July 15-19, 2000,
Proceedings, pages 154–169, 2000.
2. Fabrice Kordon et al. The model checking contest (2019). To appear in LNCS
11429.
3. Ákos Hajdu, András Vörös, and Tamás Bartha. New search strategies for the Petri
net CEGAR approach. In Application and Theory of Petri Nets and Concurrency -
36th International Conference, PETRI NETS 2015, Brussels, Belgium, June 21-26,
2015, Proceedings, pages 309–328, 2015.
4. Ákos Hajdu, András Vörös, Tamás Bartha, and Zoltán Mártonka. Extensions to
the CEGAR approach on Petri nets. Acta Cybern., 21(3):401–417, 2014.
5. Torsten Liebke and Karsten Wolf. Relieving the CTL model checker in explicit
verification. Accepted for Application and Theory of Petri Nets and Concurrency -
40th International Conference, PETRI NETS 2019, Aachen, Germany, June 23-28.
56 PNSE’19 – Petri Nets and Software Engineering
6. Karsten Schmidt. Stubborn sets for standard properties. In Application and The-
ory of Petri Nets 1999, 20th International Conference, ICATPN ’99, Williamsburg,
Virginia, USA, June 21-25, 1999, Proceedings, pages 46–65, 1999.
7. Harro Wimmel and Karsten Wolf. Applying CEGAR to the Petri net state equa-
tion. In Tools and Algorithms for the Construction and Analysis of Systems - 17th
International Conference, TACAS 2011, Held as Part of the Joint European Con-
ferences on Theory and Practice of Software, ETAPS 2011, Saarbrücken, Germany,
March 26-April 3, 2011. Proceedings, pages 224–238, 2011.
8. Karsten Wolf. Petri net model checking with LoLA 2. In Application and Theory of
Petri Nets and Concurrency - 39th International Conference, PETRI NETS 2018,
Bratislava, Slovakia, June 24-29, 2018, Proceedings, pages 351–362, 2018.