Petri nets and their numerous extensions (or subclasses) are one of the popular traditional formalisms for the speci cation and veri cation of concurrent systems. Furthermore, due to the expressivity of rewriting logic, Maude and its associated analysis tools have been adopted in many recent works for executing and analyzing Petri nets. In this paper, we rst present the existing semantics for the standard Petri nets. Then, we demonstrate the usefulness and the expressivity of the new enhanced semantics |that encodes the sets of tokens in a place by their cardinality | for such type of Petri nets. Thereafter, we show that such semantics can naturally express di erent variants of high-level Petri nets such as Petri nets with inhibitor arcs, variable arc weights, and coloured Petri nets. The distinguishing feature of this semantics is that it facilitates the checking of behavioral properties related to boundedness and liveness via the Maude LTL model checker.
Petri nets were rst introduced in 1962 [
Maude [
In this paper, we propose an enhanced semantics based on a simple, intuitive and structured notation for Petri nets in rewriting logic. While tokens are repeated and not counted in the existing semantics, the number of tokens in a place is recorded in the proposed semantics. This leads to the easiness of speci cation of Petri net models unambiguously. It also accommodates inhibitor arcs, variable arc weights, and thereafter facilitates | since it uses an intentional and reduced notation | the simulation and analysis of both basic and high-level Petri nets by using Maude formal analysis tools.
The rest of the paper is organized as follows: Section 2 presents some necessary concept about Petri nets and rewriting logics. In Section 3, the existing rewriting logic semantics for Petri nets is described. Section 4 presents our proposed semantics, followed by some experimental results in Section 5 to show the relevance of the proposed enhancements. Finally, Section 6 concludes the paper with some perspectives for future work. 2 2.1
In this section, we brie y recall basic notions about Petri nets: both structural and dynamical parts of a Petri nets with the usual associated graphical representation and some of their relevant extensions related to our work. For this purpose, consider the following de nition.
De nition 1 A Petri net is de ned as a 5-tuple N = (P; T; P re; P ost; M0) where: { P : a nite set of places with jP j = n, { T : a nite set of transitions with jT j = m and P \ T = ;, { P re: P T ! N, is the Pre incidence function { P ost: T P ! N, is the Post incidence function { M0: P ! N, function mapping a number of tokens to each p 2 P (so-called initial marking) The structural aspect of a Petri net (see, Figure 1(a)) is extremely simple and it basically consists of a set of places, transitions and directed arcs that connect places with transitions. The places (depicted by circles) represent system states or conditions and may hold a non-negative integer number of tokens, which are represented by black dots. The transitions (depicted by bars) represent the system state changes or events that may occur. The directed arcs (signi ed by arrows) de ne pre-conditions and/or post-conditions for each transition in terms of places.
The set of places linked to a transition t with arcs starting from places are called input places (or preset) is noted by •t = fpjP re(p; t) > 0g, and the set of places linked to a transition t with arcs starting from the transition are called output places (or postset) is noted by t• = fpjP ost(t; p) > 0g. A transition that does not have any input place is called a source transition and a transition that does not have any output place is called a sink transition. An arc may have a given integer value that de nes its weight, i.e., the number of tokens that will be consumed or produced following this arc.
Note that M P re (resp, M P ost) is an n m matrix that is commonly called the pre (resp, post) incidence matrix, where M P re[i; j] = P re(pi; tj ) (resp, M P ost[i; j] = P ost(tj ; pi)). In addition, P re(•; tj ) and P ost(tj ;•) denote all input and output arcs of a transition tj with their weights, i.e., the j-th columns of the MPre and MPost matrices, respectively.
A function Mf : P T ! N is called a marking function that assigns to each place of the Petri net a non-negative integer number of tokens. With the implicit ordering (p1; p2; :::; pn) on the set of places P , a marking M | that describes the Petri net state | can be represented as a column vector M where M [i] (i'th row) contains Mf (pi). Therefore, the dynamical aspect of a Petri net, starting from an arbitrary initial marking, is de ned by the evolution of its marking, i.e., the sequence of markings generated by the set of the red transitions. A transition t may be red at a marking M if : M [i] P re(pi; t) f8 pi 2 •tg Thereafter, ring of a transition t at marking M removes a number of tokens equals P re(pi; t) from each of its input places and puts another number of tokens equals P ost(t; pi) to each place of its output places. In other words, whenever a Petri net is marked with M , its new marking M 0 after ring a transition t, is de ned as follows:
M 0 = M
P re(•; t) + P ost(t;•) A Petri net is said to be \k-bounded " if the number of tokens in all of its places does not exceed a nite number k for any marking reachable from M0. A Petri net is called safe if k = 1, i.e., for all reachable markings, no place of the Petri net has more than one token.
Petri nets have been extended by many researchers. Some of the relevant
extensions related to our work are described below:
{ One of the most widely used extensions is the introduction of inhibitor arcs
[
Maude rewrite system o ers a large number of powerful tools such as: an explicitstate LTL model checker, reachability tool and an inductive theorem prover to facilitate formally verifying systems. 3
Existing Rewriting Logic Semantics for Petri nets
The existing semantics for Petri nets is based on a number of previous works
such as [
The basic sorts needed to describe a Petri net are: place and marking . A marking on a Petri net is viewed as a multiset4 over its set of places, representing (a snap-shot of) a Petri net state and denoting the available tokens (resources) in each place. These elements are de ned as sorts with a subsort relation as follows: sorts Place Marking .
subsort Place < Marking . 4 Mathematically, a multiset (or bag, or mset) is a set-like, unordered collection of elements in which elements are allowed to be repeated. ops C A $ q :-> Place .
Then, the Petri net place's names are declared as operators as follows: Thereafter, the current state (marking) of a Petri net can be de ned with a nite multiset union operator as follows: op null : -> Marking . op : Marking Marking -> Marking [assoc comm id: null] . According to this declaration, we can see that a marking (or partial marking) can be represented by an element of the nite multiset sort Marking and the union of two markings is a new marking. The empty marking is represented by the constant null. In addition, the attribute "assoc" (resp. "comm") is used to declare that the operator is associative (resp. commutative). Finally, the initial marking may also be declared as an operator and then de ned by an equation: op initial :-> Marking .
eq initial = $ $ $ q q q .
In such a declaration, only the names of the places that hold tokens appear in the initial state with an occurrence equal to the number of tokens they contain. 3.2
The evolution of a Petri net is related to the transitions ring. For that, the speci cation of a transition consists of two multisets (termsets), where the rst multiset (marking representing the transition pre-set ) may be replaced with the second one (marking representing the transition post-set ). Therefore, each transition t is described by a labelled rewrite rule with the following syntax: rl [hTransition-Labeli] : hTermset-1i => hTermset-2i .
In such a rule, the Termset-1 (resp. Termset-2) contains only the set of input (resp. output) places of the corresponding transition t, where a place name is repeated in the left-hand or right-hand side of the rule, as many times as the weight of the arc linking the place to the transition t.
In that case, a transition speci ed by a rewrite rule can take place if its lefthand side (Termset-1) matches. Then, the sub-marking is transformed into the right-hand side (Termset-2) of such rule. The process of rewriting will start with a rewrite rule that matches its left-hand side in the initial marking, and stop if no rule matches anymore.
In addition, a sink (resp. source) transition is a special case and its corresponding rewrite rule remains the same and a variable (M, for example) of sort Marking is added to the Termset-2 (resp. Termset-1) and also, used to completely replace the Termset-1 (resp. Termset-2) since it has not a pre-set (resp. post-set ).
Finally, by following the pre-described steps, we give the complete speci cation of the Petri net, presented in Figure 1 (a), as follows: fmod PETRI-NET-SIGNATURE is sorts Place Marking . subsorts Place < Marking . op null : -> Marking . ops C A $ q : -> Place . op __ : Marking Marking -> Marking
[assoc comm id: null] . op initial : -> Marking .
eq initial = $ $ $ q q q . endfm protecting PETRI-NET-SIGNATURE . var M : Marking . rl [add-$] : M => M $ . rl [add-q] : M => M q . rl [buy-C] : $ => C . rl [buy-A] : $ => A q .
rl [change] : q q q q => $ . endm As we can see, in this speci cation, the static part (the signature) of the machine is given in a functional module PETRI-NET-SIGNATURE. This module has been imported in the system module VENDING-MACHINE, in which we add one rule for each transition to complete describing the dynamic part of the vending machine. Notice that the two rules "[add-$]" and "[add-q]" are used to describe the source transitions in the Petri net, and because of that, the rewriting in the module VENDING-MACHINE does not terminate. 4
Proposed Petri net Semantics Based on Rewriting Logic
In the semantics we propose here, our focus is on how to overcome the
abovementioned drawbacks in order to make the speci cation of Petri nets more
natural. It has been found that, according to [
Starting from the fact that places and tokens are two passive and distinguishable components in a Petri net and, therefore, each new proposed semantics for Petri nets has to clearly de ne and distinguish between these two primitive concepts. Thus, we propose to represent a token k that resides in place p as a tuple (p, x) (may also be called pair)5 where p is a place identi er (label) belongs to P (set of places) and x is a variable ranging over non-negative integers that represents the number of occurrences of token k in place p.
Of course, the use of tuple-based notation may seem to be no more than a simple modi cation of the original representation. However, we argue that the use of 5 A pair can only have two values | neither less nor more |. However, a tuple, has almost no semantic limitation on the number of values. a counting-based notation is very bene cial. Intuitively, this notation facilitates the counting of tokens, drops the ambiguity between places and tokens and considerably enhances the description of long Petri net marking (very compact). In addition, this notation will help developers to naturally specify high level Petri nets.
Practically, a tuple is de ned by enclosing two items in angle brackets, separated by a comma <_,_>. The rst item is used to de ne a place by its name (sort : PlaceName) followed by the number of tokens6 it holds (sort : Int)7. On the other hand, the marking8 is consequently de ned as a set of tuples. Mathematically, the elements of a set have no order among them; hence, tuples in a marking do not have any particular order. Thus, the basic sort Marking is used to de ne the marking of a Petri net. In addition, the operator "__" is also used to allow combining (union) two or more tuples and then produce a new set of tuples. The result may be a subset of tuples related to one transition (pre-set and post-set ) or the whole set of tuples describing the global state of the Petri net (marking). The empty marking is represented by the constant "null". Moreover, the attribute "assoc" (resp. "comm") is used to declare that the operator is associative (resp. commutative). Therefore, the corresponding new signature is given as follows: sorts PlaceName Place Marking . subsort Place < Marking . ops C A $ q :-> Placename . op < , > : PlaceName Int -> Place [ctor] . op null : -> Marking . op : Marking Marking -> Marking [assoc comm id: null]. op initial :-> Marking . eq initial = < $,3 > < q,3 > < C,0 > < A,0 > .
The rst advantage of the proposed speci cation is that the test for the number of tokens in a place as well as the speci cation of inhibitor arcs is now possible. Moreover, the declaration of the initial marking in our proposal describes the overall Petri net, including all its places, and is not limited to the places holding tokens. Therefore, this declaration gives a clear snap-shot of the initial marking of the system and one can thereby know all the names of the Petri net places along with the tokens they hold. 4.2
Theoretically, the global state of a Petri net is generally represented by a marking M . Thereafter, when ring a transition t, the change in such a state of the 6 For the sake of simplicity and since tokens are indistinguishable in basic Petri nets, we were only interested in their number in a place. 7 We use the sort Int since the subtraction is not de ned with sort NAT. 8 It is noticed that the Petri net marking in the proposed semantics has the commutative monoidal structure since the set of tuples (p,x) is equipped with an associative binary operation ( ) and an identity element. Petri net occurs at the level of the set of input and output places by removing tokens from the former and adding tokens to the latter. Such evolution can be naturally speci ed in the rewriting logic by rewrite rules. In general, these rules are conditional and a rewrite rule has to be de ned for each transition as follows: crl [hTransition-Labeli] : hLHSi => hRHSi if Cond .
During execution, Maude uses the whole set of tuples given in initial marking and whenever a subset (sub-marking) matches the LHS then that part can be replaced by RHS if the enabling condition9 is veri ed. In fact, the LHS (resp. RHS) describes the state of both the input and output places before (resp. after) ring the transition t, and are de ned as follows:
LHS, RHS = set of tuples(p; x), where p 2 f•t [ t•g In addition and according to the number of input places, a condition | de ned by the expression Cond | can be either a single equation or a conjunction of equations using an associative binary conjunction connective such as: /\ or "and". Consequently, a rewrite rule could be somewhat larger, yet it is considerably more clear | in terms of presentation| than the one in the existing semantics. We now present the complete speci cation of the previous Petri net according to the proposed speci cation. fmod NEW-PETRI-NET-SIGNATURE-1 is protecting INT . sorts PlaceName Place Marking . subsort Place < Marking . ops C A $ q : -> PlaceName . op <_,_> : PlaceName Int -> Place [ctor] . op __ : Marking Marking -> Marking [ctor assoc comm id: null] . ops null initial : -> Marking .
eq initial = < $,3 > < q,3 > < C,0 > < A,0 > . endfm mod NEW-VENDING-MACHINE-1 is inc NEW-PETRI-NET-SIGNATURE-1 . vars x y z : Int . rl [add-$] : < $,x > => < $,x + 1 > . rl [add-q] : < q,x > => < q,x + 1 > . crl [buy-c] : < $,x > < C,y > => < $,x - 1 > < C,y + 1 > if (x > 0) . crl [buy-a] : < $,x > < A,y > < q,z > => < $,x - 1 > < A,y + 1 > < q,z + 1 > if (x > 0) .
crl [change] : < $,x > < q,z > => < $,x + 1 > < q,z - 4 > if (z >= 4) . endm 9 The condition is not needed in the case of a source transition since it is unconditionally enabled and therefore, the corresponding rewrite rule will be unconditional.
In this section, we present the e ectiveness of the proposed rewriting logic-based
semantics for Petri nets. For that, some experimental comparison results have
been presented in order to assess the advantages and evaluate of the performance
of the proposed speci cation compared to the existing ones.
As the proposed semantics use tuples to describe a marking, there is a clear
difference between a place and its tokens. Therefore, a marking will be very clear
and the number of tokens in each place is shown without the need to manually
count them. To show that, let's explore the behavior of our machine from the
given initial marking. For that, we use the command "rewrite"10 (abbreviated
"rew"). For instance, consider the same command "rew [
Existing Semantics Enhanced Semantics
Maude> rewrite [
In order to examine the ability of describing inhibitor arcs, we consider the second machine, presented in Figure 1(b), in which we imply users to not insert more than 4 dollars (resp. 4 quarters) in the coins box before buying something (resp. making change). However, the returned quarters after buying an apple are added without control.
In addition, we have added two places (S1 and S2) to describe the vending machine capacity in delivering items (cake and apple). The capacity of the vending machine is assumed to be 50 items for both cakes and apples. This capacity is declared in the initial state and after delivering all items, the machine has to be re lled (this process is not considered here). 10 It is necessary to determine the upper bound allowed for the number of rule applications when using such commands. Otherwise, in nity is assumed.
An Enhanced Rewriting Logic Based Semantics for High-Level Petri nets 165
In the existing semantics, the number of tokens in a place cannot be naturally obtained and, in order to get it, one can use an additional operator (enclosing the entire marking) such as the usual system-grabbing operator as follows: op f g : Marking -> PN .
Thereafter, one could similarly de ne a second operator as follows: op number : PN Place -> Int . that is simply de ned as: eq number(fM M'g,M) = 1 + number(fM'g,M) . eq number(fM'g,M) = 0 [owise] .
With this new operator, one could describe transitions with inhibitor arcs. For instance, the rules add-$ and add-q could now be written as follows: crl [add-$] : fMg => fM $g if number(fMg,$) < 4 . crl [add-q] : {M} => {M q} if number({M},$) < 4 /\ number({M},q) < 4 .
The speci cation of Petri nets with inhibitor arcs is made naturally due to the proposed representation of places. Therefore, the speci cation of the machine presented in Figure 1(b) is given as follows: fmod NEW-PETRI-NET-SIGNATURE-2 is protecting INT . sorts PlaceName Place Marking . subsort Place < Marking . ops C A $ q S1 S2 : -> PlaceName . op <_,_> : PlaceName Int -> Place [ctor] . op __ : Marking Marking -> Marking [ctor assoc comm id: null] . ops null initial : -> Marking .
eq initial = <$,3> <q,3> <C,0> <A,0> <S1,50> <S2,50> . endfm mod NEW-VENDING-MACHINE-2 is inc NEW-PETRI-NET-SIGNATURE-2 . vars x y z t : Int . crl [add-$] : < $,x > => < $,x + 1 > if (x < 4) . crl [add-q] : < $,x > < q,z > => < $,x > < q,z + 1 > if (z < 4) and (x < 4) . crl [buy-c] : < $,x > < C,y > < S1,z > => < $,x - 1 > < C,y + 1 > < S1,z - 1 > if (x >= 1) and (z >= 1) . crl [buy-a] : < $,x > < A,y > < q,z > < S2,t > => < $,x - 1 > < A,y + 1 > < q,z + 1 > < S2,t - 1 > if (x >= 1) and (t >= 1) .
crl [change] : < $,x > < q,z > => < $,x + 1 > < q,z - 4 > if (z >= 4) . endm In this speci cation, the transitions add-$ and add-q have been described with conditional rewrite rules with the necessary test for the number limit. 5.3
The boundedness testing is possible since our system is terminating. In addition, we already know that the place $ is bounded with 17 because the studied system has a limited number (50) for both cakes and apples. Therefore, we would like to demonstrate the ability to check the correctness of such characteristic. To do so, one can use the reachability tool or Maude LTL model checker11 to look for the existence of a marking where the place $ holds 18 tokens by using the following command.
No solution.
Maude> search in NEW-VENDING-MACHINE-2 : initial =>* M < $,18 > .
states: 714867 rewrites: 15490529 in 4281906278ms cpu (105312ms real)
(3 rewrites/second)
In this result, we can see that the Maude reachability tool did not nd a
solution, which means that the place $ will not have 18 tokens during the system
evolution12. So, such place may be bounded and in order to con rm that, we
have to check if there are some markings where the number of tokens in such
place is equal to 17.
11 Maude LTL model checker cannot be used for the existing semantics without the
additional operator given in Section 5.2. In addition, it would be unsuitable to use
the reachability tool with the existing semantic since the number of tokens have to
be repeated as many as number of tokens to be searched.
12 In this case, we have used the parameter " =>! " for search command in order to
minimize (reduce) the set of solutions to the canonical nal states, i.e., states that
cannot be further rewritten. Otherwise, parameter " =>* " can be used (see [
On the other hand, the LTL model-checker can also be used to check the previous property by de ning the following modules: mod VENDING-MACHINE-2-PREDS is protecting NEW-VENDING-MACHINE-2 . including SATISFACTION . subsort Marking < State . op Bound(_,_) : PlaceName Int -> Prop . var M : Marking . var P : PlaceName . vars x y : Int . ************** PLACE BOUNDEDNESS PROPERTY *************** ceq < P,x > M |= Bound(P,y) = true if x <= y . endm mod VENDING-MACHINE-2-CHECK is inc VENDING-MACHINE-2-PREDS . inc MODEL-CHECKER . inc LTL-SIMPLIFIER . op Place-Bounded(_,_) : PlaceName Int -> Prop . op PN-Bounded(_,_) : PlaceName Int -> Prop . var P : PlaceName . var x : Int .
eq Place-Bounded(P,x) = [](Bound(P,x)) . endm In the following, we give the boundedness veri cation results of places $ and q. Maude> reduce in VENDING-MACHINE-2-CHECK : modelCheck(initial, Bounded($,17)) . rewrites: 16920270 in 48121469397ms cpu (99937ms real) (~ rewrites/second) result Bool: true 5.4
To better understand the notion of Petri nets with \variable arc weights", we
consider the example, given in Figure 2(a), that is inspired by [
In this example, the transitions T1 and T2 are used to control and maintain the marking of the place P1 at a desired level. In this example, the marking shall not be less than 3. Therefore, the transition T1 will be red when the marking of the place P1 is greater than the desired level and a token is added to the place P2. Thereafter, T2 will be enabled and then red to remove the excess of tokens from the place P1 through the weight (M(P1) 3) of the arc (P1, T2). The following code represents the initial marking and the rewrite rules describing the transitions T1 and T2 according to the proposed semantics as given in Section 4. eq initial = <P1,5> <P2,0> <P3,0> . crl [T1] : < P1,x > < P2,0 > => < P1,x > < P2,1 > if (x >= 4) . crl [T2] : < P1,x > < P2,1 > < P3,y > => < P1,3 > < P2,0 > < P3,y + x - 3 > if (x > 3) .
We should note that it is not possible to describe a Petri net with variable arc weights (i.e., produce or remove a variable number of tokens) in the existing semantics neither naturally nor with the additional operator, given in Section 5.2. Thus, for this purpose, one has to explore other alternatives (strategies, loops ...etc). 5.5
To show the extensibility of the proposed semantics for describing colored Petri nets, we consider the model shown in Figure 2(b). The given coloured Petri net has four places P1, P2, P3 and P4 and four colors of tokens that are: Color1 (A), Color2 (B), Color3 (C) and Color4 (D).
Of course, the speci cation of coloured petri nets is also based on tuples as seen in basic Petri nets, possibly de ned with two generic parameters (sorts). The rst parameter speci es the name of the place and the second determines the set of colors within this place. Such a speci cation is given as follows: op < , > : PlaceName ColorSet -> Place .
For that, the set of color within a place need the following declaration: sorts ColorId Color ColorSet . subsort Color<ColorSet . op f g : ColorId Int -> Color . op , : ColorSet ColorSet -> ColorSet .
Thereafter, the list of places and color names of the studied coloured Petri nets must be given. In our example, such declaration is: ops P1 P2 P3 P4 : -> PlaceName . ops A B C D : -> ColorId .
The complete speci cation of the structural aspects of our coloured Petri nets is given as follows: endfm However, such generic speci cation for a coloured Petri net may be inconvenient since it does not preclude the user from constructing erroneous tuples (composed of place's name and colors) that do not belong to the coloured Petri net in study. Therefore, we propose a seconde well-formed signature for a coloured Petri net in which the places of the Petri net have to be decomposed into sets which share the same set of token colors. For instance, the given CPN has three color sets so that, P1 and P4 belong to the same color set ("PlaceNameset1"), P2 belongs to the color set ("PlaceNameset2") and P3 belongs to the color set ("PlaceNameset3").
Subsequently, we de ne each type of place (according to the colors of its tokens) in a separate operator in order to obtain an unambiguous presentation. The corresponding new signature is given as follows: fmod CPN-SIGNATURE is
protecting INT . sorts PlaceNameset1 PlaceNameset2 PlaceNameset3 . sorts Place Marking . subsort Place < Marking . ops P1 P4 : -> PlaceNameset1 . op P2 : -> PlaceNameset2 . op P3 : -> PlaceNameset3 . op <_,A(_) B(_)> : PlaceNameset1 Int Int -> Place . op <_,A(_) C(_)> : PlaceNameset2 Int Int -> Place . op <_,B(_) D(_)> : PlaceNameset3 Int Int -> Place . ops null initial : -> Marking . op _ _ : Marking Marking -> Marking [ctor assoc comm id: null] . eq initial = < P1,A(2) B(1) > < P2,A(1) C(1) > < P3,B(0) D(0) > < P4,
A(0) B(0) > .
endfm
According to that, the behavioral aspects can be given as follows:
mod CPN is
inc CPN-SIGNATURE .
vars x1 x2 x3 y1 y2 y3 z t : Int .
crl [T] : < P1,A(x1) B(y1) > < P2,A(x2) C(z) > < P3,B(y2) D(t) > < P4,A(x3)
B(y3) > => < P1,A(x1 - 1) B(y1 - 1) > < P2,A(x2 - 1) C(z - 1) >
< P3,B(y2 + 2) D(t + 1) > < P4,A(x3 + 1) B(y3 + 1) > if ((x1 >= 1)
and (y1 >= 1) and (x2 >= 1) and (z >= 1)) .
endm
Let us now use the command rewrite to explore the behavior of this CPN.
The result of execution of this speci cation is given as follows:
rewrite [
D(1) > 6
In this paper, a new enhanced semantics, based on a highly structured notation
for Petri nets in rewriting logic, is introduced and compared to the existing one.
The main advantage of both semantics is that the basic paradigm of Petri net
computations (true concurrency involving several non-con icting transitions) is
preserved. However, the proposed semantics is structurally and behaviourally
straightforward and clear, i.e., while tokens are repeated (and not counted) in
the existing at notation, the number of tokens in a place is counted in the
enhanced semantics. In addition, the new semantics facilitates the simulation
and analysis of both basic and high-level Petri nets and deals unambiguously
with variable arc weights, inhibitor arcs, and boundedness testing.
For the future, we intend to exploit the bene ts of the proposed semantics for
the veri cation of models described in terms of extended high-level Petri nets as
parametric and recursive Petri nets [
Foremost, we would like to express our sincere gratitude to Prof. Peter Csaba O lveczky who provided insights and expertise that greatly helped this research. His criticisms were quite constructive and helped to get this work in the current form. Then, this work would not have been possible without the nancial support (PhD scholarship) No:034/PNE/ENS/Spain/13-14 received through the Algerian ministry of higher education and scienti c research.
Finally, we greatly appreciate the support received through the collaborative work undertaken with Laura M Castro at the MADS (Models and Applications of Distributed Systems) research group, A Corun~a University, Spain.