High-level Petri nets make models more concise and readable as compared to low-level Petri nets. However, usual verification techniques such as state space analysis remain an open challenge for both because of state space explosion. The contribution of this paper is to propose an approach for property based reduction of the state space of Algebraic Petri nets (a variant of high-level Petri nets). To achieve the objective, we propose a slicing algorithm for Algebraic Petri nets (APNSlicing). The proposed algorithm can alleviate state space even for certain strongly connected nets. By construction, it is guaranteed that the state space of sliced net is at most as big as the original net. We exemplify our technique through the running case study of car crash management system.
Petri nets (PNs) are a well-known low-level formalism for modeling concurrent
and distributed systems. Various evolutions of PNs have been created, among
others High-level Petri nets (HLPNs), that raise the level of abstraction of PNs
by using complex structured data [
For the analysis of concurrent and distributed systems (including those
modeled using PNs or HLPNs) model checking is a common approach, consisting in
verifying a property against all possible states of a system. A typical drawback of
model checking is its limits with respect to the state space explosion problem: as
systems get moderately complex, completely enumerating their states demands
a growing amount of resources, which in some cases makes model checking
impractical both in terms of time and memory consumption [
As a result, an intense field of research is targeting to find ways to optimize model checking, either by reducing the state space or by improving the performance of model checkers. A technique called PN slicing falls into the first category. It proposes to reduce the state space size by syntactically reducing a PN model, taking only the portion of the model that impacts the properties to be verified. The resultant model will typically have a smaller state space, thus reducing the cost of model checking.
Slicing was defined for the first time in [
One limitation of the cited approaches is that they only apply to low-level PNs. In order to be applied to HLPNs they need to be adapted to take into account data types.
In this work, we propose a slicing algorithm that is adapted to Algebraic Petri nets (APNs, a variant of HLPNs). To the best of our knowledge, there does not exist any algorithm for slicing APNs. The proposed algorithm iteratively builds a subnet from a given APN, according to a slicing criterion that is derived from the property to be verified. The resulting subnet preserves LT L−X properties under weak fairness assumptions.
APN-MODEL REFINING APN-MODEL
UNFOLDING APN-MODEL SLICING UNFOLDED APN-MODEL Fig.1, gives an overview of the proposed approach for slicing based verification of APNs using Process Flowchart. At first, APN-model is unfolded and then by taking property into an account criterion places are extracted. Afterwards, slicing is performed for the criterion places. Subsequently, verification is performed on the sliced unfolded APNs. The user may use the counterexample to refine the APN-model to correct the property.
The rest of the work is structured as follows: we give basic definitions and concepts of the Algebraic Petri nets (APNs) in section 2. Section 3, illustrates the steps of slicing based verification of APN-models shown in Fig.1. Details about the underlying theory and techniques are given for each activity of the process. In the section 4, we discuss related work and a comparison with the existing approaches. A small case study from the domain of crisis management system (a car crash management system) is taken to exemplify the proposed slicing algorithm in section 5. An experimental evaluation of the proposed algorithm is performed in section 6. In the section 7, we draw conclusions and discuss future work concerning to the proposed work. 2
In this section, we give basic formal definitions of algebraic specifications used
in this paper. Formal definitions, propositions, lemmas and theorems are taken
as is or with slight modifications from [
Definition 1. A signature Σ = (S,OP) consists of a set S of sorts, OP = (OPw,s)w∈S∗,s∈S is a (S∗ × S)−sorted set of operation names of OP. For being the empty word, we call OP ,s the set of constant symbols.
disjoint to OP.
A set X of Σ-variables is a family X = (Xs)s∈S of variables set,
The set of terms TOP,s(X) of sort s is inductively defined by: 1. Xs ∪ OP ,s ⊆ TOP,s(X); 2. op(t1, . . . , tn) ∈ TOP,s(X) for op ∈ OPs1,...,sn,s, n ≥ 1 and ti ∈ TOP,si (X) (for i = 1, . . . , n).
The set TOP,s ≡ TOP,s(∅) contains the ground terms of sort s, TOP (X) ≡ Ss∈S TOP,s(X) is the set of Σ-terms over X and TOP ≡ TOP (∅) is the set of Σ-ground terms.
TOP,s(X).
A Σ-equation of sort s over X is a pair (l,r) of terms l, r ∈ Definition 5. An algebraic specification SPEC = ( Σ,E) consists of a signature Σ = (S,OP) and a set E of Σ-equations.
Definition 6. A Σ-algebra A = (SA, OPA) consist of a family SA = (As)s∈S of domains and a family OPA = (Nop)op∈OP of operations Nop : As1 ×. . . Asn → As for op ∈ OPs1...sn,s if op ∈ OP ,s, Nop congruent to an element of As. Definition 7. An assignment of Σ-variables X to a Σ-algebra A is a mapping ass : X → A,with ass(x) ∈ Asiff x ∈ Xs. ass is canonically extended to ass : TOP (X) → A, inductively defined by 1. ass(x) ≡ ass(x) for x ∈ X; 2. ass(c) ≡ Nc for c ∈ OP ,s; 3. ass(op(t1, . . . , tn)) ≡ Nop(ass(t1)), . . . , ass(tn)) for op(t1, . . . , tn) ∈ TOP (X). Definition 8. Let SPEC-algebra is SPEC = (Σ,E) in which all equations in E are valid. Two terms t1 and t2 in TOP (X) are equivalent (t1 ≡E t2) iff for all assignments ass : X → A, ass(t1) = ass(t2).
Definition 9. Let B be a set. A multiset over B is a mapping msB: B → N. B is the empty multiset with msB(x) = 0 for all x ∈ B. A multiset is finite iff {∀b ∈ B | msB(b) 6= 0} is finite.
Definition 10. Let M SB = {msB: B → N} be a set of multisets. The addition function of multisets is denoted by + : M SB × M SB → M SB. Let ms1B, ms2B and ms3B ∈ M SB. (ms1B + ms2B) = ms3B ⇐⇒ ∀b ∈ B, ms3B(b) = ms1B(b) + ms2B(b).
The subtraction function of multisets is denoted by − : M SB ×M SB → M SB. Let ms1B, ms2B and ms3B ∈ M SB. (ms1B − ms2B) = ms3B ⇐⇒ ∀b ∈ B, ms1B(b) ≥ ms2B(b) ⇒ ∀b ∈ B, ms3B(b) = ms1B(b) − ms2B(b). Definition 11. Let M SB = {msB: B → N} be a set of multisets. Let ms1B, ms2B ∈ M SB . We say that ms1B is smaller than or equal to ms2B (denoted by ms1B ≤ ms2B) iff ∀b ∈ B, ms1B(b) ≤ ms2B(b). Further, we say that ms1B 6= ms2B iff ∃b ∈ B, ms1B(b) 6= ms2B(b). Otherwise, ms1B = ms2B.
Definition 12. A marked Algebraic Petri Net AP N =< SP EC, P, T, F, asg, cond, λ, m0 > consist of ◦ an algebraic specification SPEC = ( Σ,E), ◦ P and T are finite and disjoint sets, called places and transitions, resp., ◦ F ⊆ (P × T ) ∪ (T × P ), the elements of which are called arcs, ◦ a sort assignment asg : P → S, ◦ a function, cond : T → Pfin(Σ − equation), assigning to each transition a finite set of equational conditions.
◦ an arc inscription function λ assigning to every (p,t) or (t,p) in F a finite multiset over TOP,asg(p),
◦ an initial marking m0 assigning a finite multiset over TOP,asg(p) to every place p.
Definition 13. The preset of p ∈ P is •p = {t ∈ T |(t, p) ∈ F } and the postset of p is p• = {t ∈ T |(p, t) ∈ F }. The pre and post sets of t ∈ T defined as: •t = {p ∈ P |(p, t) ∈ F } and t• = {p ∈ P |(t, p) ∈ F }.
over TOP,asg(p).
A marking m of an APN assigns to every place p ∈ P a multiset Definition 15. An occurrence mode is a ground substitution of cond(t), m(p), λ(p, t) and λ(t, p) where p ∈ P, t ∈ T . Obviously, ground substitutions are the syntactical representations of assignments.
Definition 16. A transition t ∈ T of an APN is enabled in an occurrence mode at a marking m iff for all p in P with (p,t) ∈ F, λ(p, t) ≤ m(p). If a transition t is enabled in an occurrence mode at a marking m, then t may occur returning the marking m0, where for all p ∈ P, m0(p) = m(p) − λ(p, t) + λ(t, p). We write m[tim0 in this case.
Definition 17. A firing sequence σ of a marked APN is maximal iff either σ is of infinite length or 6 ∃t ∈ T : m0([σti), where |σ| ∈ (N ∪ {∞}).
Definition 18. Let σ = t1, t2 . . . be an infinite firing sequence of APN with mi[ti+1imi+1, ∀i, 0 ≤ i. σ permanently enables t ∈ T iff ∃i, 0 ≤ i : ∀j, i ≤ j : mj [ti. 3
One characteristic of APNs that makes them complex to model check is the use
of variables on arcs. Computing variable bindings at runtime is extremely costly.
AlPiNA (a symbolic model checker for Algebraic Petri nets) allows the user to
define partial algebraic unfolding and presumed bounds for infinite domains [
The basic idea of the slicing algorithm is to start by identifying which places in the unfolded APN model are directly concerned by a property. These places constitute the slicing criterion. The algorithm will then take all the transitions that create or consume tokens from the criterion places, plus all the places that are pre-condition for those transitions. This step is iteratively repeated for the latter places, until reaching a fixed point.
We refine the slicing construction by distinguishing between reading and
non-reading transitions. The conception of reading and non-reading transitions
is some what similar notion introduced in [
Due to partial unfolding, there could be some domains that are not unfolded. For some cases, we are still able to identify non-reading transitions even if domains are not unfolded. If for example, we have a case where the multiplicities or cardinalities of terms in λ(p, t), λ(t, p)are different then we can immediately state λ(p, t) 6= λ(t, p). But for some cases, we don’t have such a clear indication of the inequality between λ(p, t) and λ(t, p), for example, in the Fig.2, we see that λ(p, t) = 1 + y and λ(t, p) = 2 + x (defined over naturals). Both terms has the same multiplicity and cardinality, so we need to know for which values of the variables it would be a non-reading transition. In general, the evaluation of terms to check their equality for all the values is undecidable. For this particular case, we would like to have a set of constraints from the user. Informally, a constraints set denoted by CS, is a set of propositional formulas, predicate formulas or any other logical formulas for certain specific values of variable assignements, describing the conditions under which we can evaluate terms to be equal or not. Consequently, constrains set CS will help to identify under which cases the transitions can be treated as non-reading.
A function eval : TOP,s(X) × TOP,s(X) × CS → Bool is used to evaluate the equivalence of terms based on the constraint set. Let us take the same terms shown over the arcs in Fig.2, term1 = 1 + y, term2 = 2 + x and a constraint set CS = {∃y, x ∈ (0, . . . , 2)|y = x + 1} . It is important to note that we are not unfolding the domain but evaluating the terms for some specific values provided by user to identify reading and non-reading transitions. Of course, the user can provide sparse values too. Let us evaluate the terms term1 and term2 based on the constraints set CS provided. For all those values of x, y for which we get eval function result true are considered to be reading transitions and rest of them are non-reading transitions. It is also important to note that we include this step during the unfolding. The resulting unfolded AP N will contain only non-reading transitions for the unfolded domains as shown in Fig.3.
The algorithm proposed in this article assumes that such an unfolding takes place before the slicing. Since this is a step that is involved in the model checking activity anyway, we do not consider this assumption to be adding to the complexity of the algorithm. In this section, we will make an extremely simple example of how the slicing algorithm works, starting from an APN, unfolding it and slicing it. 0…10
P 1+1 1+0 1+1 1+2 1+0 1+1 1+2 1+0 1+2 1+1 2+1 t1,1 2+0 t0,0 2+0 t0,1 2+0 t0,2 2+1 2+1
2+1 2+2 2+2 2+2 t1,0 t1,1 t1,2 t2,0 t2,2 t2,1 Fig. 4 shows an APN model. All places and all variables over the arcs are of sort naturals (defined in the algebraic specification of the model, and representing the N set).
Since the N domain is infinite (or anyway extremely large even in its finite
computer implementations), it is clear that it is impractical to unfold this net
by considering all possible bindings of the variables to all possible values in N.
However, given the initial marking of the APN and its structure it is easy to
see that none of the terms on the arcs (and none of the tokens in the places)
will ever assume any natural value above 3. For this reason, following [
A
B x
y
z
proceeds in three steps. First, the data domains of the variables are unfolded up
to the presumed bound. Second, variable bindings are computed, and only that
satisfy the transition guards are kept. Third, the computed bindings are used
to instantiate a binding-specific version of the transition. The resulting unfolded
APN for this APN model is shown in Fig. 5. The transitions arcs are indexed
with the incoming and outgoing values of tokens. A complete explanation of
the unfolding algorithm, and in particular the existence of the tokens 4 and 5
between transition t23, t42, t43 and place C, F is rather complex and out of the
scope of this article. The interested reader can find details about the partial
unfolding in [
The slicing algorithm starts with an unfolded APN and a slicing criterion Q ⊆ P .
Let Q ⊆ P a non empty set called slicing criterion. We can build a slice for an unfolded APN based on Q, using following algorithm:
end Algorithm 1: APN slicing algorithm
APNSlicing(hSP EC, P, T, F, asg, cond, λ, m0i, Q){ T 0 = {t ∈ T | ∃p ∈ Q : t ∈ (•p ∪ p•) : λ(p, t) 6= λ(t, p)}; P 0 = Q ∪ {•T 0} ; Pdone = ∅ ; while ((∃p ∈ (P 0 \ Pdone)) do while (∃t ∈ (•p ∪ p•) \ T 0) : λ(p, t) 6= λ(t, p)) do
P 0 = P 0 ∪ {•t};
T 0 = T 0 ∪ {t}; end
Pdone = Pdone ∪ {p}; return hSP EC, P 0, T 0, F|P0,T0 , asg|P0 , cond|T0 , λ|P0,T0 , m0|P0 i; }
Initially, T 0 (representing transitions set of the slice) contains set of all pre and post transitions of the given criterion place. Only non-reading transitions are added to T 0 set. And P0(representing places set of the slice) contains all preset places of transitions in T 0. The algorithm then iteratively adds other preset transitions together with their preset places in T 0 and P 0. Remark that the APNSlicing algorithm has linear time complexity.
Considering the APN-Model shown in fig. 4, let us now take an example property and apply our proposed algorithm on it. Informally, we can define the property: “The values of tokens inside place D are always smaller than 5”.
Formally, we can specify the property in LTL as G(∀tokens ∈ D|tokens < 5).
For this property, the slicing criterion Q = {D}, as D is the only place concerned
by the property. Therefore, the application of APNSlicing(UnfoldedAPN, D)
returns SlicedUnfoldedAPN (shown in Fig. 6), which is smaller than the original
UnfoldedAPN shown in Fig. 5).
[
A 1 t11 23 t12 t13
Transitions t31,1, t31,2, t31,3, t31,3, t32,1, t32,2, t32,3, t33,1, t33,2, t33,3, t51,1, t51,2, t51,3, t52,1, t52,2, t52,3, t53,1, t53,2, t53,3, and places C, E, F, G has been sliced away. The proposed algorithm determines a slice for any given criterion Q ⊆ P and always terminates. It is important to note that the reduction of net size depends on the structure of the net and on the size and position of the slicing criterion within the net.
[
scope(a) = {a} for a ∈ A; scope(⊗ϕ) = scope(ϕ) with ⊗ ∈ {¬, X}; scope(ϕ1 ⊗ ϕ2) = scope(ϕ1) ∪ scope(ϕ2) with ⊗ ∈ {∧, U }.
Definition 21. Let N be a marked APN. Let N 0 be its sliced net for a slicing criterion Q ⊆ P . Let σ = t1t2t3 . . .be a firing sequence of N and m i the markings with mi[ti+1imi+1, ∀i, 0 ≤ i < |σ|. σ is slice-fair w.r.t N 0 iff either σ is finite and m|σ| does not enable any transition t ∈ T 0;
or σ is infinite and if it permanently enables some t ∈ T 0, it then fires infinitely often some transition of T 0 (which may or may not be the same as t). Slice-fairness is a very weak fairness notion. Weak fairness determines that every transition t ∈ T of a system, if permanently enabled, has to be fired infinitely often, slice-fairness concerns only the transitions of the slice, not of the entire system net and if a transition t ∈ T of the slice is permanently enabled, some transitions of the slice are required to fire infinitely often but not necessarily t. Definition 22. Let N be a marked APN and ϕ an LTL formula. N |= ϕ slicefairly iff every slice-fair (not necessarily maximal) firing sequence of σ |= ϕ. Definition 23. Let N and N 0 be two marked Algebraic Petri nets with T 0 ⊆ T and P 0 ⊆ P . We define the function: slice (N,N0) ∈ [(T ∗ ∪ T w) → (T 0∗ ∪ T 0w)] ∪ [N|P | → N|P 0|] such that a finite or infinite sequence of transitions σ is mapped onto the transition sequence σ0 with σ0 being derived from σ by omitting every transition t ∈ T \ T 0. A marking m of N is projected onto the marking m0 of N 0 with m0 = m |p0 .
The function slice is used to project markings and firing sequences of a net N onto the markings and firing sequences of its slices.
Proposition 1. Let N be a marked APN. Let N 0 be its sliced net for a slicing criterion Q ⊆ P . Let σ be a weakly fair firing sequence of N. σ is slice fair with respect to N 0.
Proof. Let us assume, σ is not slice-fair. In case σ is finite this means that m|σ|[ti for a transition t ∈ T 0. In case σ is infinite, there is permanently enabled transition t ∈ T 0 but all transitions of T 0 are fired finitely often including t. So both cases contradict the assumption that σ is weakly fair.
Lemma 1. Let N be a marked APN and let N 0 be its sliced net for a slicing criterion Q ⊆ P . The coefficients cij of the incidence matrix equal to zero for all places pi ∈ P 0 and transitions tj ∈ T \ T 0.
Proof. Let N 0 be its sliced net for a slicing criterion Q ⊆ P . A transition t ∈ T is also an element of T 0 ⊆ T , if it is a non-reading transition of a place p ∈ P 0. Thus a transition t ∈ T \ T 0 either is not connected to a place p ∈ P 0 or it is a reading transition. Lemma 2. Let N be a marked APN and let N 0 be its sliced net for a slicing criterion Q ⊆ P . Let m be a marking of N and m0 be a marking of N 0 with m0 = m |p0 . m[ti ⇔ m0[ti, ∀t ∈ T 0.
Proof. Let N 0 be its sliced net for a slicing criterion Q ⊆ P . Since a transition t ∈ T 0 has the same preset places in N and N 0 by the slicing algorithm AP N Slicing, m0 = m |p0 implies m[ti ⇐⇒ m0[ti.
Every firing sequence σ of N projected onto the transitions of T 0 is also a firing sequence of slice net N 0. The resulting markings m and m0 assign the same number of tokens to places p0 ⊆ P . mll+1|P0 = m0l |P 0 .
Proposition 2. Let N be a marked APN and let N 0 be its sliced net for a slicing criterion Q ⊆ P . Let σ be a firing sequence of N and let m be a marking of N . m0[σim ⇒ m0 |p0 [slice(σ)im |p0 .
Proof. We prove this Proposition by induction over the length l of σ. Let N be a marked APN, σ be a firing sequence of N .
l = 0: In this case slice(σ) equals . Thus the initial marking of N and N 0 is generated by firing . By defintion 23 and the slicing algorithm AP N Slicing, m00 = m0 |p0
l → l + 1 : Let σ be a firing sequence of length l and ml be a marking of N with m0[σiml. Let tl+1 be a transition in T and ml+1 a marking of N such that ml[tl+1iml+1. By induction hypothesis, m00[slice(σ)im0k with ml |p0 = m0k. If tl+1 is an element of T 0, it follows by Lemma 2, that m0k enables tl+1, since ml enables tl+1. The resulting marking m0k+1 is determined by m0k+1(Pi0) = m0k(Pi0) + ci l+1, ∀pi ∈ P 0 and ml+1 is determined by ml+1(i) = ml(i) + ci l+1, ∀pi ∈ P 0.
Since ml|P0 = m0k, it thus follows that mll+1|P0 = m0k+1. If tl+1 is an element of t ∈ T \ T 0, then it must be a reading transition for all p ∈ P ; slice(σ) = slice(σtl+1) and thus m00[slice(σtl+1)im0k a transition t ∈ T \ T 0 can not change the marking of on any place p ∈ P 0. By Lemma 1 and the resultant markings, A firing sequence σ0 of the slice net N 0 is also a firing sequence of N . The resulting markings of σ0 on N and N 0, respectively assigns the same markings to places p ∈ P 0.
Proposition 3. Let N be a marked APN and let N 0 be its sliced net for a slicing criterion Q ⊆ P . Let σ0 be a firing sequence of N 0 and let m0 be a marking of N 0.
m00[σ0im0 ⇒ ∃m ∈ N|P | : m0 = ml|P0 ∧ m0[σ0im.
Proof. We prove this Proposition by induction over the length l of σ0.
l = 0: The empty firing sequence generates the marking m0 on N and the marking m00, which is defined as m0|P0 , on N 0, by definition 23.
l → l + 1: Let σ0 = t1 . . . tl+1 be firing sequence of N 0 with length l + 1. Let m0l and m0l+1 be markings of N 0 such that m00[t1 . . . tlim0l[tl+1im0l+1. Let ml be the marking of N with m0[t1 . . . tliml and ml|P0 = m0l, which exists according to the induction hypothesis. Lemma 2, ml enables tl+1. The marking ml+1 satisfies ml+1(Pi) = ml(Pi) + ci l+1, ∀pi ∈ P 0 and m0l+1 satisfies m0l+1(Pi) = m0l(Pi) + ci l+1, ∀si ∈ P 0. With ml|P0 = m0l, it follows that (ml+1 |P 0 ) is equal to m0l+1. Proposition 4. Let N be a marked APN and let φ be an LT Lx formula such that scope(φ) ⊆ P . Let N 0 be its sliced net for a slicing criterion Q ⊆ P where Q = scope(φ). Let σ be a firing sequence of N . Let us denote the sequence of markings by M(σ). Then, M(σ) |= φ ⇔ M(slice(σ)) |= φ.
Proof. We prove this Proposition by induction on the structure of φ. Let σ = t1t2 . . . and slice(σ) be σ0 = t01t02 . . .. Let M(σ) = m0m1 . . . and M(σ0) = m00m01 . . ..
φ = true: In this case nothing needs to be shown. φ = ¬ψ, φ = ψ1 ∧ ψ2: Since the satisfiability of φ depends on the initial marking of scope(φ) only and scope(φ) ⊆ P 0 ⊆ P , both directions hold.
φ = ψ1U ψ2: We assume that M(σ0) |= ψ1U ψ2. We can divide up σ0 such that σ0 = σ10σ20 with m0|σ10|m0|σ10|+1 . . . |= ψ2 and ∀i, 0 ≤ i < |σ10| : m0im0i+1 . . . |= ψ1. There are transition sequences σ1 and σ2 such that σ = σ1σ2, slice(σ1) = σ10, slice(σ2) = σ20 and σ1 does not end with a transition t ∈ T \ T 0.
By proposition 2, it follows that m0|σ10| = (m|σ1| |P 0 ). Since m0|σ10|m0|σ10|+1 . . . |= ψ2, m|σ1|m|σ1|+1 . . . |= ψ2 by induction hypothesis. Let % be a prefix of σ1 such that |%| < |σ1|. Let %0 be slice(%). The firing sequence % truncates at least one transition t ∈ T 0, consequently |%0| < |σ10|. Since m0|%01|m0|%01|+1 . . . |= ψ1, m % m|%|+1 . . . |= ψ1 by the induction hypothesis. Analogously, it can be | | shown that M(σ) |= ψ1U ψ2 implies M(σ0) |= ψ1U ψ2.
Proposition 5. Let N be a marked APN and let N 0 be its sliced net for a slicing criterion Q ⊆ P . Let σ0 be a maximal firing sequence of N 0. σ0 is a slice-fair firing sequence of N .
Proof. Let σ0 = t1t2 . . .. Let m0i be the marking of N 0, such that m0i[ti+1im0i+1, ∀i, 0 ≤ i < |σ0|. By Proposition 3 σ0 is a firing sequence of N . Let mi be the marking of N , such that mi[ti+1imi+1, ∀i, 0 ≤ i < |σ0|. In case σ0 is finite, m0|σ0| does not enable any transitions t0 ∈ T 0.
By Lemma 2, m|σ0| does not enable any transition T 0 ∈ T 0 , If σ0 is infinite it obviously fires infinitely often a transition t0 ∈ T 0 and thus is slice-fair. Proposition 6. Let N be a marked APN and let N 0 be its sliced net for a slicing criterion Q ⊆ P . Slice(σ) is maximal firing sequence of N 0.
Proof. Let σ = t1t2 . . . with mi[ti+1imi+1, ∀i, 0 ≤ i < |σ|. By Proposition 2, slice(σ) is a firing sequence of N 0. Let slice(σ) be σ0 = t01t02 . . . with m0i[t0i+1im0i+1, ∀i, 0 ≤ i < |σ|. Let us assume σ0 is not a maximal firing sequence of N 0. Thus σ0 is finite and there is a transition t0 ∈ T 0 with m0|σ0|[t0i. Let σ1 be the smallest prefix of σ such that slice(σ1) equals σ0.
By Proposition 2 (m|σ1| |P 0 = m0|σ0|. By Lemma 2, and the state equation it follows, that (m|σ1| |P 0 = m0|σ0|+1 = . . .. So t0 stays enabled for all markings mj with |σ1| ≤ j ≤ |σ| but is fired finitely many times only. This is a contradiction to the assumption that σ is slice-fair.
Theorem 1. Let N be a marked APN and let φ be an LTL formula such that scope(φ) ⊆ P . Let N 0 be its sliced net for a slicing criterion Q ⊆ P . Let Ψ be an LT L−X formula with scope(Ψ ) ⊆ P .
N |= φ slice-fairly ⇒ N 0 |= φ, for an LTL formula φ.
N |= Ψ slice-fairly ⇐ N 0 |= Ψ , for an LT L−X formula Ψ .
Proof. We first show “ N |= φ slice-fairly ⇒ N 0 |= φ ”. Let us assume that N |= φ slice-fairly holds. Let σ0 be a maximal firing sequence of N 0. Since σ0 is a slice-fair firing sequence of N by Proposition 5 M(σ0) |= φ. Let us now assume N 0 |= Ψ . Let σ be a slice-fair firing sequence of N . By Proposition 6, slice(σ) is maximal firing sequence of N 0 and thus satisfies Ψ . By Proposition 4, it follows that σ satisfies Ψ.
Verification is possible under interleaving semantics if we assume slice-fairness. A firing sequence σ is fair w.r.t T 0 , if σ is either maximal and if σ eventually permanently enables a t0 ∈ T 0, a transition t ∈ T 0 will be fired infinitely often, t may not equal t0. Unfolded APN |= ϕ fairly w.r.t. T 0 holds if all fair firings sequences of N, more precisely, their corresponding traces satisfy ϕ. 4
Slicing is a technique used to reduce a model syntactically. The reduced model
contains only those parts that may affect the property the model is analyzed for.
Slicing Petri nets is gaining much attention in the recent years [
Astrid Rakow developed two flavors of Petri net slicing, CT L∗−X slicing and
Safety slicing in [
We notice that all the constructions are limited to low-level Petri nets. The
main difference between High-level and low-level Petri net is that in high-level
Petri nets tokens are no longer black dots, but complex structured data. Whereas
in case of low-level Petri nets, all (black) tokens correspond to the same data
object. The idea of reading and non-reading transitions introduced in [
Slice CTL*-X
Preserving all CTL*-X properties assuming a weak Properties are about token fairness assumption count only Designed for Low-level
Petri net Preserving safety properties Properties are about token only count only
Designed for Low-level
Petri net
Preserving all LTL-X properties assuming a weak Properties are about token fairness assumption count and token values Designed for High-level
Petri net (APNs)
Fig. 7. A comparison between APNSlicing, CT L∗−X and Safety slicing 5
We took a small case study from the domain of crisis management systems (car crash management system) for the experimental investigation of the proposed approach. In a car crash management system (CCMS); reports on a car crash are received and validated, and a Superobserver (i.e., an emergency response team) is assigned to manage each crash.
Recording Crisis Data [system($cd,false)]
The APN Model can be observed in Fig. 8, it represents the semantics of the
operation of a car crash management system. This behavioral model contains
labeled places and transitions. There are two tokens of type Fire and Blockage in
place Recording Crisis Data. These tokens are used to mention which type of data
has been recorded. The input arc of transition sendcrisis takes the cd variable
as an input from the place Recording Crisis Data and the output arc contains
term system(cd,false) of sort sys. Initially, every recoded crisis is set to false. The
sendcrisis transition passes recorded crisis to system for further operations. The
output arc of validatecrisis contains system(getcrisistype(sy),true) term which
sends validated crisis to system. The transition assigncrisis has two guards, first
one is isvalid(sy)=true that enables to block invalid crisis reporting to be
executed for the mission and the second one is isvalid(sob,getcrisestype(sy))=true
which is used to block invalid Superobserver (a skilled person for handling crisis
situation) to execute the crisis mission. The Superobserver YK will be assigned
to handle Fire situation only. The transition assigncrisis contains two input arcs
with sob and sy variables and the output arc contains term assigncrisis(sob,sy)
of sort crisis. The output arc of transition sendreport contains term rp(ec). This
enables to send a report about the executed crisis mission. We refer the interested
reader to [
An important safety threat, which we will take into an account in this case study is that the invalid crisis reporting can be hazardous. The invalid crisis reporting is the situation that results from a wrongly reported crisis. The exsendcrisisFire,(Fire,false)
Fire Recording Crisis Data
Fire,Blockage ecution of crisis mission based on the wrong reporting can waste both human and physical resources. In principle, it is essential to validate the crisis that it is reported correctly. Another, important threat could be to see the number of crisis that can be sent to place System should not exceed from a certain limit. Informally, we can define the properties: ϕ1 : All the crisis inside place System are validated eventually. ϕ2 : Place System never contains more than two crisis.
Formally we can specify the properties as, let Crises be a set representing recorded crisis in car crash management system. Let isvalid : Crises → BOOL, is a function used to validate the recorded crisis.
ϕ1 = F(∀crisis ∈ Crises|isvalid(crisis) = true) ϕ2 = G(|Crises| ≤ 2)
In contrast to generate the complete state space for the verification of ϕ1 and ϕ2, we alleviate the state space by applying our proposed algorithm. For both ϕ1, ϕ2 LTL formulas, scope(ϕ1 ∧ ϕ2) ⊆ Q. The criterion place(s) for both properties is System.
The unfolded car crash APN model is shown in Fig. 9. The slicing algorithm APNSlicing(Unfolded car crash APN model,System) takes the unfolded car crash APN model and System (an input criterion place) as an input and iteratively builds a sliced net. The sliced unfolded car crash APN model is shown in Fig. 10, places named ExecutedCrisis and ExecutedCrisisreporting together with transition named sendreport are sliced away. From the initial marking of Car Crash APN Model 36 states are reachable, whereas sliced car crash APN model has 27 reachable states. The resultant sub net is sufficient to verify both properties (see proof in Theorem 1). 6
In this section, we evaluate our slicing algorithm with the existing benchmark case studies. We measure the effect of slicing in terms of savings of the reachable sendcrisisFire,(Fire,false)
Fire state space, as the size of the state space usually has a strong impact on time and space needed for model checking. Instead of presenting case studies where our methods work best, it is equally interesting to see where it gives an average or worst case results, so that we will present a comparative evaluation on the benchmark case studies.
To evaluate our approach, we made the follwing assumptions: – Evaluation procedure is independent of the temporal properties. In general, it is not feasible to determine which places correspond to the interesting properties. Therefore, we generated slices for each place in the given APN model (later, we take some specific temporal properties about the APN models under observation) . –
We abandoned the initially marked places (we follow [
Let us study the results summarized in the table.1, the first column shows different APNs models under observation. Based on the initial markings, total number of states is shown in the second column. Best reduction and average reduction (shown in the third and fourth column) refers to the biggest and an average achievable reduction in the state space among all possible properties. In the fifth column total number of places is given, for the properties related to these places, our slicing does not reduce the number of states. Finally, the structure of APN models under observation is given. Results clearly indicate the significance of slicing; the proposed APNSlicing algorithm can alleviate the state space even for some strongly connected nets.
To show that the state space could be reduced for the practically relevant properties. Let us take some specific examples of the temporal properties from the APN models shown in table.2 and compare the reduction in terms of states by applying the APNSlicing algorithm. For the Daily Routine of two Employees and Boss APN model, for an example, we are interested to verify that: “Every time the boss does not schedule a meeting, he will be at home eventually” . Formally, we can specify the property:
ϕ1 = G(N M ⇒ FB1), where “NM" (resp. B1) means “place NM (resp. B1) is not empty".
For a Producer Consumer APN model an interesting property could be to verify that: “Buffer place is never empty” . Formally, we can specify the property: ϕ2 = G(|Buf f er| > 0).
And for a Complaint Handling APN model, we are interested to verify: “All the registered complaints are collected eventually” . Formally, we can specify the property:
ϕ3 = G(RecComp ⇒ FCompReg), where “RecComp" (resp. CompReg) means “place RecComp (resp. CompReg) is not empty".
Let us study the results summarized in the table shown in table. 2, the first column represents the system under observation whereas in the second column total number of states are given based on the initially marked places. The third column refers the property that we are looking for the verification. In the fourth column, places are given that are considered as criterion places, and for those places slices are generated. The fifth column represents the number of states that are reduced (in percentage) after applying APNSlicing algorithm.
We can draw the following conclusions from the evaluation results such as: – The choice of the place can have an important influence on the reduction effects (As the basic idea of slicing is to start from the criterion place and iteratively include all the non-reading transitions together with their input places. The less non-reading transitions attached to the criterion place, the more reduction is possible). – Reduction can vary with respect to the net structure and markings of the places (The slicing refers to the part of a net that concerns to the property, remaining part may have more places and transitions that increase the overall number of states. If slicing removes parts of the net that expose highly concurrent behavior, the savings may be huge and if the slicing removes dead parts of the net, in which transitions are never enabled then there is no effect on the state space). – For certain strongly connected nets slicing may produce a reduced number of states (For all the strongly connected nets that contain reading transitions slicing can produce noteworthy reductions). – Slicing produces best results for not strongly connected nets (By definition work-flow nets are not strongly connected and since they model work flows, slicing can effectively reduce such nets). 7
In this work, we developed an Algebraic Petri net reduction approach to alleviate the state space explosion problem for model checking. The proposed work is based on slicing. The presented slicing algorithm (APNSlicing ) for Algebraic Petri net guarantees that by construction the state space of sliced net is at most as big as the original net. We showed that the slice allow verification and falsification if Algebraic Petri net is slice fair. Our results show that slicing can help to alleviate the state space explosion problem of Algebraic Petri net model checking.
The future work has twofold objectives; first to implement the proposed
slicing construction in AlPiNA (Algebraic Petri net analyzer) a symbolic model
checker [