High-level Petri nets (evolutions of low-level Petri nets) are well suitable formalisms to represent complex data, which influence the behavior of distributed, concurrent systems. However, usual verification techniques such as model checking and testing remain an open challenge for both (i.e., low-level and high-level Petri nets) because of the state space explosion problem and test case selection. The contribution of this paper is to propose a technique to improve the model checking and testing of systems modeled using Algebraic Petri nets (a variant of high-level petri nets). To achieve the objective, we propose different slicing algorithms for Algebraic Petri nets. We argue that our slicing algorithms significantly improve the state of the art related to slicing APNs and can also be applied to low-level Petri nets with slight modifications. We exemplify our proposed algorithms through a case study of a car crash management system.
Petri nets are well known low-level formalism for modeling and verifying
distributed, concurrent systems. The major drawback of low-level Petri nets
formalism is their inability to represent complex data, which influences the
behavior of a system. Various evolutions of low-level Petri nets (PNs) have been
created to raise the level of abstraction of PNs. Among others, high-level Petri
nets (HLPNs) raise the level of abstraction of PNs by using complex structured
data [
For the analysis of concurrent and distributed systems (including which are
modeled using PNs or HLPNs) model checking is a common approach, consisting
in verifying a property against all possible states of a system. However, model
checking remains an open challenge for both (PNs & HLPNs) because of 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 [
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. In recent years major advances have been made by either modularizing
the system or by reducing the states to consider (e.g., partial orders, symmetries).
The symbolic model checking partially overcomes this problem by encoding the
state space in a condensed way by using Decision Diagrams and has been
successfully applied to PNs [
One limitation of the proposed slicing algorithms that are designed to
improve the model checking in the literature so far is that most of them are only
applicable to low-level Petri nets. Recently, an algorithm for slicing APNs has
been proposed [
The remaining part of the paper is structured as follows: in section 2, we give formal definitions necessary for the understanding of proposed slicing algorithms. In section 3, different slicing algorithms are presented together with their informal and formal descriptions. In section 4, we discuss related work and we give a comparison with 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 algorithms in section 5. An experimental evaluation of the proposed algorithms is performed in section 6. In section 7, we draw conclusions and discuss future work. 2
Algebraic Petri nets are an evolution of low-level Petri nets. APNs have two
aspects, i.e., the control aspect, which is handled by a Petri net and the data
aspect, which is handled by one or many algebraic abstract data types (AADTs) [
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 ! P fin(⌃ 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), where TOP,asg(p) are algebraic terms (if used “closed” (resp.free) terms to indicate if they are build with sorted variables closed or not), an initial marking m0 assigning a finite multiset over TOP,asg(p) to every place p.
Definition 2. The preset of p 2P is •p = {t 2T |(t, p) 2f } and the postset of p is p• = {t 2T |(p, t) 2f }. The pre and post sets of t 2T defined as: •t = {p 2P |(p, t) 2f } and t• = {p 2P |(t, p) 2f }.
Definition 3. Let m and m0 two markings of APN and t a transition in T then < m, t, m0 > is a valid firing triplet (denoted by m[tim0) iff 1) 8 p 2• t | m(p) (p, t) (i.e., t is enabled by m).
2)8 p 2P | m0(p) = m(p) (p, t) + (t, p). 3
PN slicing is a technique used to syntactically reduce a PN model in such a
way that at best the reduced PN model contains only those parts that may
influence the property the PN model is analyzed for. Considering a property over
a Petri net, we are interested to define a syntactically smaller net that could be
equivalent with respect to the satisfaction of the property of interest. To do so
the slicing technique starts by identifying the places directly concerned by the
property. Those places constitute the slicing criterion. The algorithm then keeps
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. Roughly, we can divide
PN slicing algorithms into two major classes, which are Static Slicing algorithms
and Dynamic Slicing algorithms. An algorithm is said to be static if the initial
markings of places are not considered for building the slice. Only a set of places
is considered as a slicing criterion. The Static Slicing algorithms starts from the
given criterion place and includes all the pre and post set of transitions together
with their incoming places. There may exist sequence of transitions in the sliced
net that are not fireable because their incoming places are initially empty and do
not get markings from any other way. An algorithm is said to be dynamic slicing
algorithm, if the initial markings of places are considered for building the slice.
The slicing criterion will utilize the available information of initial markings
and produce a smaller sliced net. For a given slicing criterion that consists of
[
x t2
x C[] C y initial markings and a set of places for a PN model, we are interested to extract a subnet with those places and transitions of PN model that can contribute to change the marking of criterion place in any execution starting from the initial marking. The sliced net will exclude sequence of transitions in the resultant slice that are not fireable because their incoming places are not initially marked and do not get markings from any other way.
One characteristic of APNs that makes them complex to slice is the use of multiset of algebraic terms over the arcs. In principle, algebraic terms may contain the variables. Even though, we want to reach a syntactically reduced net, its reduction by slicing, needs to determine the possible ground substitutions of these algebraic terms.
We follow [
B 1
bindings are used to instantiate a binding-specific version of the transition. The
resulting unfolded APN model of Fig.1 is shown in the Fig. 2. The transitions
arcs are indexed with the incoming and outgoing values of tokens.
Abstract slicing has been defined as a static slicing algorithm. The objective is to
improve the model checking of APNs. In the previous static algorithm proposed
for APNs, the notions of reading and non-reading transitions are applied to
generate a smaller sliced net. The basic idea of reading and no-reading transitions
was coined by Astrid Rakow in the context of PNs [
Definition 4. (Reading(resp.Non-reading) transitions of APN) Let t 2 T be a transition in an unfolded APN. We call t a reading-transition iff its firing does not change the marking of any place p 2 (•t [ t•) , i.e., iff 8 p 2 (•t [ t•), (p, t) = (t, p). Conversely, we call t a non-reading transition iff (p, t) 6= (t, p).
We extend the existing slicing operators by introducing the notion of neutral transitions and using them with the reading transitions. Informally, a neutral transition consumes and produces the same token from its incoming place to an outgoing place. The cardinality of incoming (resp.) outgoing arcs of a neutral tranistion is strictly equal to one and the cardinality of outgoing arcs from an incoming place of a neutral transition is equal to one as well.
Definition 5. (Neutral transitions of APN) Let t 2T be a transition in an unfolded APN. We call t a neutral-transition iff it consumes token from a place p 2• t and produce the same token to p0 2t•, i.e., t 2T ^ 9 p9 p0/p 2• t ^ p0 2 t• ^ | p•| = 1 ^ | •t| = 1 ^ | t•| = 1 ^ (t, p) = (t, p0).
P1
[
2 t1 Algorithm 1: Abstract slicing algorithm
AbsSlicing(hSP EC, P, T, F, asg, cond, , m 0i, Q){ T 0 { t 2T /9 p 2Q ^ t 2(•p [ p•) ^ (p, t) 6= (t, p)}; P 0 Q [ { •T 0} ; Pdone ; ; while ((9 p 2(P 0 \ Pdone)) do while (9 t 2((•p [ p•) \ T 0) ^ (p, t) 6= (t, p)) do
P 0 P 0 [ { •t};
T 0 T 0 [ { t}; end Pdone
Pdone [ { p}; end while (9 t9 p9 p0/t 2T 0 ^ p 2• t ^ p0 2t• ^ | •t| = 1 ^ | t•| = 1 ^ | p•| = 1 ^ p 62Q ^ p0 62Q ^ (p, t) = (t, p0)) do m(p0) m(p0) [ m(p); while (9 t0 2• p/t0 2T 0 ) do
(p0•, p) (p0•, p0) [ (t0, p); end T 0
P 0 end
T 0 \ {t 2T 0/t 2p• ^ t 2• p0};
P 0 \ {p}; return hSP EC, P 0, T 0, F|P0,T0 , asg|P0 , cond|T0 , |P0,T0 , m0|P0 i; }
In the Abstract slicing algorithm, initially T 0 (representing transitions set of the slice) contains a set of all the pre and post transitions of the given criterion places. Only the non-reading transitions are added to T 0. P0(representing the places set of the slice) contains all the preset places of the transitions in T 0. The algorithm then iteratively adds other preset transitions together with their preset places in the T 0 and P 0. Then the neutral transitions are identified and their pre and post places are merged to one place together with their markings.
Considering the APN-Model shown in fig. 1, let us now apply our proposed algorithm on two example properties (i.e., one from the class of safety properties and one from liveness properties). Informally, we can define the properties: ' 1 : “The values of tokens inside place D are always smaller than 5”. ' 2 : “Eventually place D is not empty”.
Formally, we can specify both properties in the CTL as: ' 1 = AG(8 token 2m(D)/token < 5). ' 2 = AF(|m(D)| =6 ; ).
For both properties, the slicing criterion Q = {D}, as D is the only place concerned by the properties. The resultant sliced net can be observed in fig.4, which is smaller than the original unfolded net (shown in fig.2).
[
B 1
Sliced net for Property ' 1 and ' 2
Let us compare the number of states required to verify the given property without slicing and after applying abstract slicing. In the first column of Table.1, number of states are given that are required to verify the property without slicing and in the second column number of states are given to verify the property by slicing.
The abstract slicing can be applied to low-level Petri nets with slight
modifications. The criteria to build abstract slice for both formalisms (i.e., Algebraic
Petri nets and low-level Petri nets) remain the same. In case of low-level Petri
nets, we do not unfold the net and the slice is built directly. The idea of including
non-reading transitions together with merging of places by identifying neutral
transitions remains the same for both formalisms. (Note: we refer the interested
reader to [
Concerned Slicing Concerned slicing algorithm has been defined as a dynamic slicing algorithm. The objective is to extract a subnet with those places and transitions of the APN model that can contribute to change the markings of a given criterion place in any execution starting from the initial markings. Concerned slicing can be useful in debugging. Consider for instance that the user is analyzing a particular trace of the marked APN model (using a simulation tool) so that erroneous state is reached.
The slicing criterion to build the concerned slice is different as compared to the abstract slicing algorithm. In the concerned slicing algorithm, available P1
[
Algorithm 2: Concerned slicing algorithm
ConcernedSlicing(hSP EC, P, T, F, asg, cond, , m 0i, Q){ T 0 ; ; P 0 Q ; while (•P 6= T 0) do
P 0 P 0 [ • T 0 ;
T 0 T 0 [ • P 0; end T 00 P 00
Starting from the criterion place the algorithm iteratively include all the incoming transitions together with their input places until reaching a fix point. Then starting from the set of initially marked places set the algorithm proceeds further by checking the enabled transitions. Then the post set of places are included in the slice. The algorithm computes the paths that may be followed by the tokens of the initial marking.
Considering the APN-Model shown in fig. 1, let us now take the place D
as criterion and apply our proposed algorithm on it. The resultant sliced
APNModel is shown in the fig. 6. The test input data can be generated for the sliced
APN-model to observe which tokens are coming to the criterion place.
[
To explain the basic idea of program slicing according to Wieser [
The Fig.7(b) shows the sliced program that is obtained by tracing backwards
possible influences on the variables: In the line 7, product is multiplied by i, and
in the line 8, i is incremented too, so we need to keep all the instructions that
impact the value of i. As a result all the computations that do not contribute to
the final value of product have been sliced away (The interested reader can find
more details about the program slicing from [
The first algorithm about Petri net slicing was presented by Chang et al [
Astrid Rakow developed two algorithms for slicing Petri nets i.e., CTL⇤ X
slicing and Safety slicing in [
Khan et al presented a slicing technique for algebraic Petri nets [
We took a small case study from the domain of crisis management systems (car crash management system) for the experimental investigation of the proposed slicing algorithms. 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.
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 in the place Recording
Crisis Data that are Fire and Blockage. 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) of sort sys (It is important to note
that for better readability, we omit $ symbol from the terms over the arcs). The
sendcrisis transition passes a recorded crisis to system for further operations.
All the recorded crises are sent for validation through sendcrisisforvalidation
transitions. Initially, every recoded crisis is set to false. The output arc of validat
ecrisis contains the system(getcrisistype(vcs),true) term which sends
validated crisis to system. The transition assigncrisis has two guards, the 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 execution of a crisis mission based on the wrong reporting can waste both human and physical resources. In principle, it is essential to validate a crisis that it is reported correctly. Another, important threat could be to see the number of superobservers should not exceed from a certain limit. Informally, we can define the properties:
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 = AF(8 crisis 2System|isvalid(crisis) = true). ' 2 = AG(|SuperobserverReady| 2).
In contrast to generate the full state space for the verification of the properties ' 1 and ' 2, we alleviate the state space by applying our proposed algorithm i.e., abstract slicing algorithm. For ' 1and' 2, the criterion places are System and Superobserver Ready. The unfolded car crash APN model is shown in the Fig. 9. The abstract slicing algorithm takes an unfolded car crash APN model and System (an input criterion place) as an input and iteratively builds the sliced net for ' 1. Respectively for ' 2, the algorithm starts from Superobserver Ready(as input criterion place) and builds the slice. The sliced unfolded car crash APN models are shown in the Fig. 10, for the both prperties i.e., ' 1 and ' 2.
Let us compare the number of states required to verify the given property without slicing and after applying abstract slicing. In the first column of Table.2, the number of states are given that are required to verify the property without slicing and in the second column the number of states are given to verify the property by slicing.
Let us take a criterion place (i.e, System) from the car crash APN model and apply our proposed concerned slicing algorithm to find which transitions and places can contribute tokens to that place. It is important to note that, we perform concerned slicing directly on the car crash APN model instead of the unfolded car crash APN model (as discussed in the section 3). The sliced car crash APN-model can be observed in the Fig.11.
Recording Crisis Data
Fire
Fire sendcrisisforvalidationFire
(Fire,false) Fig. 9. The unfolded car crash APN model
sendcrisisforvalidationBlockage
Recording Crisis Data Fire,Fire,Blockage,
Blockage Blockage Fire sendcrisisBlockage sendcrisisFire Blockage Fire
System Superobserver Ready (YK,Fire) (Blockage,true) sendcrisisforvalidationBlockage sobs(Yk,Fire), (NG,Blockage) sobs(NG,Bloc kage) assigncrisis(Blockage,true), (NG,Blockage),((Blockage,true), (NG,Bloackage))
sendcrisisforvalidationFire Fire
Recording Crisis Data In this section, we evaluate our abstract slicing algorithm and compare with existing slicing construction for APNs (Note: We do not include concerned slicing algorithm in the evaluation. As discussed in section 3, concerned slicing algorithm is designed to improve the testing of APN for the first time. We only include slicing algorithm that are designed to improve the model checking). We measure the effect of slicing in terms of savings of the reachable state space, as the size of the state space usually has a strong impact on time and space needed for model checking.
To show that state space could be reduced for practically relevant properties.
We took some specific examples of temporal properties from the different case
studies. Instead of presenting properties for which our method the best one, it is
interesting to see where it gives an average or worst case results. Let us specify
the temporal properties that we are interested to verify on the given APN model.
(Note: we refer the interested reader to [
For the Daily Routine of two Employees and Boss APN model, for example, we are interested to verify that: “Boss has always meeting”. Formally, we can specify the property: ' 1 = AG(N M 6= ; ), where “NM" represents a place not meeting.
For Simple Protocol, for example, we are interested to verify that: “All the packets are transmitted eventually”. Formally, we can specify the property: ' 2 = AF(|P ackT orec| = |P ackT osend|), where “PackTosend and PackTorec" represents places.
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 = AG(RecComp ) AFCompReg), where “RecComp" (resp. CompReg) means “place RecComp (resp. CompReg) is not empty".
For an Insurance claim APN model an interesting property could be to verify that: “Every accepted claim is settled”. Formally, we can specify the property: ' 4 = AG(AC ) AFCS), where “AC" (resp. CS) means “place AC (resp. CS) is not empty".
For a Customer support production system an interesting property could be to verify that: “Number of requests are always less than 10 ”. Formally, we can specify the property: ' 5 = AG(|Requests| < 10).
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: ' 6 = AG(|Buf f er| > 0).
Let us study the results summarized in the table shown in Table. 2, the first column represents the system under observation whereas the second column refers to the property that we are interested to verify. In the third column, total number of states is given based on the initial markings of places. In the fourth column, number of states are given that are required to verify the given property by applying APNslicing. In the fourth column, number of states that are required to verify the given property by applying abstract slicing. The last column represents the number of states that are reduced (in percentage) after applying Abstract slicing algorithm.
We can draw the following conclusions from the evaluation results:
– Abstract slicing often reduces the slice size as compared to APNslicing slice
size. This is due to the inclusion of neutral transition together with
reading transitions. As a result number of states are reduced to verify the given
property, which is an improvement towards model checking. We can observe
Table. 2, a part for property ' 2, there is always an improvement in the
reduction of states. It is important to note that at worst the slice size obtained
after applying abstract slicing is equal to the slice size obtained by applying
APNslicing.
– Reduction can vary with respect to the net structure and markings of the
places (this is true for both abstract slicing and APNslicing). 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.
– It has been empirically proved that in general slicing produces best results
for work-flow nets in [
– Abstract slicing algorithm is a linear time complex. 7
In this work, we have presented two slicing algorithms (i.e., Abstract slicing and Concerned slicing) to improve the verification of systems modeled in the Algebraic Petri nets. The Abstract slicing algorithm has been designed to improve the model checking whereas the Concerned slicing has been designed to improve the testing of APNs. Both the algorithms are linear time complex and significantly improves the model checking and testing of APNs.
As a future work, we are targeting to define more refined slicing constructions in the context of APNs and to implement a tool named SLAPn (i.e., slicing algebraic Petri nets). The objective of SLAPn is to show the practical usability of slicing by implementing the proposed slicing algorithms. The initial strategy to implement SLAPn is to extend the AlPiNA (Algebraic Petri net analyzer) a symbolic model checker. As discussed in the section 3, we are using the same unfolding approach as AlPiNA. Certainly, this will help to reduce the implementation effort. 8
This work has been supported by the National Research Fund, Luxembourg, Project RESIsTANT, ref.PHD-MARP-10.