key: cord-0046611-2tcqmnga
authors: Haddad, Serge; Khmelnitsky, Igor
title: Dynamic Recursive Petri Nets
date: 2020-06-02
journal: Application and Theory of Petri Nets and Concurrency
DOI: 10.1007/978-3-030-51831-8_17
sha: 43df7227f4e89d00bdf510604f03f8b61ee04385
doc_id: 46611
cord_uid: 2tcqmnga

In the early two-thousands, Recursive Petri nets (RPN) have been introduced in order to model distributed planning of multi-agent systems for which counters and recursivity were necessary. While having a great expressive power, RPN suffer two limitations: (1) they do not include more general features for transitions like reset arcs, transfer arcs, etc. (2) the initial marking associated with the recursive “call” only depends on the calling transition and not on the current marking of the caller. Here we introduce Dynamic Recursive Petri nets (DRPN) which address these issues. We show that the standard extensions of Petri nets for which decidability of the coverability problem is preserved are particular cases of DPRN. Then we establish that w.r.t. coverability languages, DRPN are strictly more expressive than RPN. Finally we prove that the coverability problem is still decidable for DRPN.

thread covers one of the final markings, it may perform a cut transition pruning upward closed set Y , denoted min(Y ), is finite and fulfills Y = min(Y ) ↑ . So whenever we handle upward closed sets, they are implicitely defined by their set of minimal elements. -Given any infinite sequence of upward closed sets (Y n ) n∈N ∈ (2 X ) ω where for all n, Y n ⊆ Y n+1 , there exists n 0 such that n∈N Y n = n≤n0 Y n . -Let f be a partial non decreasing function from X to X, f is effective if (1) there is an algorithm that takes as input x ∈ X, decides whether x belongs to the domain of f and, in the positive case, computes f (x) and (2) there is an algorithm that takes as input x ∈ X and computes min(f −1 ({x} ↑ )). -Let F be a finite set of effective functions and Y be an upward closed set. Define Cov(F, Y ) as the smallest set C that contains Y and fulfills

Then Cov(F, Y ) can be computed the following backward exploration:

For instance, coverability in Petri nets can be decided using this backward exploration (see for instance [7] ) and we will apply it in several contexts.

Notation. Let X ⊆ Y be two sets. The mapping Id denotes the identity mapping from X to Y where X and Y should be clear from the context.

Let us introduce dynamic recursive Petri nets (DRPN). Like a Petri net, a DRPN has a set of places P and a set of transitions T partitioned in elementary and abstract transitions (resp. T el and T ab ). A state s of an SRPN is a tree whose vertices are labelled by markings (defined by the mapping M ) and edges are labelled by transitions (defined by the mapping Λ). A transition t may fire in any vertex u provided that the marking of this vertex M (u) belongs to an upward closed set Grd t . If t is elementary then M (u) is updated by applying an effective function Upd t . If t is abstract then (1) a vertex v is created as a child of u with Λ(u, v) = t, (2) marking M (v) is defined by Beg t (M (u)) where Beg t is an effective function, and (3) M (u) is updated by applying an effective function Upd − t ≤ Id. A DRPN is equipped with End, an upward closed set of N P . When for some vertex v, M (v) ∈ End then τ , the cut transition, can be fired whose effect consists to (1) delete the subtree rooted v and (2) when v = r where r denotes the root of the state to update M (u) where u is the parent of v by applying the effective function Upd + t ≥ Id. The state consisting in the empty tree is denoted ⊥. -Upd + = {Upd + t } t∈T ab is a family of effective functions with Upd + t ∈ (N P ) N P ; -For all t ∈ T ab , Upd − t ≤ Id and Id ≤ Upd + t ; -Beg = {Beg t } t∈T ab is a family of effective functions with Beg t ∈ (N P ) Grdt ; -End is an upward closed set of N P .

As discussed above, a state of a DRPN is a labelled tree. One denotes by Des s (v)(respectively Anc s (v)) the set of descendants (respectively ancestors) of v ∈ V in the underlining tree of s (including v itself). If v = r then prd(v) is the parent of v in the tree. Given a U ⊆ V we will denote by Anc s (U ) = ∪ v∈U Anc s (v). The depth of s is the depth of its tree. Given m ∈ N P , s m denotes a tree consisting of a single vertex r with marking M (r) = m. Let us formally define the firing of elementary, abstract and cut transitions.

In this case, its firing leads to the state s = V , M , E , Λ , defined below:

The transition firing is denoted s 

The length of σ, denoted |σ|, is n. The abstract length of σ, denoted |σ| ab , is |{i ≤ n | t i ∈ T ab }|. The depth of σ is the maximal depth of states s 0 , . . . , s n . A closing sequence is a firing sequence that reaches ⊥. Given a firing sequence that includes the firing of an abstract transition t in vertex v creating vertex w and followed later by the cut transition in w, we say that (v, t),

Discussion. The main limitations of the modelling power of DRPN are the requirements that (1) sets like Grd t must be upward closed and (2) functions like Upd t must be monotonic. Despite these limitations, DRPNs include many models like:

-Petri nets (PN) that can be defined without abstract transitions and such that for all t ∈ T , Grd t = {m | m ≥ Pre(t)} and Upd t = Id + C(t) where Pre(t) (resp. C(t)) is the column vector indexed by t of the backward incidence matrix Pre (resp. incidence matrix C). -Affine Petri nets ( [6] ) that can also be defined without abstract transitions and such that for all t ∈ T , there exist a matrix A t ∈ N P ×P and a vector

and Beg t is some constant. Here Post(t) is the column vector indexed by t of the forward incidence matrix Post.

Graphical Representation. For modelling purposes, we equip DRPN with a graphical representation based on net representations. Places (resp. transitions) are depicted by circles (resp. rectangles). However a transition does not have input arcs but only output arcs represented by double-headed arrows and labelled by expressions where a place represents the current value of its marking. The guard of an elementary transition is also represented by a boolean expression inside the rectangle. For instance, the elementary transition t figured below is defined by: Grd t = {m | m(p 1 ) > 2} and Upd t (m) = (m(p 1 ) + m(p 2 )) − → p 1 + m(p 2 ) − → p 2 where − → p denotes the vector defined by − → p [p] = 1 and for all p = p, − → p [p ] = 0.

The rectangle of an abstract transition t is divided into several parts: on the top corner left (−) starts the edges representing Upd − t , on the top center Grd t is represented, on the bottom corner left Beg t is represented, and on the bottom corner right (+) start the edges representing Upd + t . There are no edges for unchanged place markings. For instance, the abstract transition figured below is defined by:

Example 1 (Hiring an assassin). In order to illustrate the modelling capabilities of DRPN, we present an example of distributed planning. The DRPN N Jaqen of Fig. 1 represents the possible behaviour of an assassin hired for a job. The transitions filled in black are Petri net transitions and so are presented with input and output arcs as usual. The assassin is given 3 days (3 tokens in p time ), an advance of 20 bitcoins (20 tokens in p adv ), and is promised to get a reward of 20 bitcoins after the job is done (20 tokens in p reward ). In order to try catching their target he needs to devote one bitcoin and one day of his time. After this day either the assassin is successful (t found ) or fails (t lost ) and needs to spend another day. When successful, the assassin can collect the reward (t collect ). However, the assassin has also another strategy which consists of hiring another assassin by giving him a quarter of his advance money and promise him an equal reward, telling him the number of days left (t hire where f pay (m) = m(p time ) − → p time + 0.5 0.5m(p adv ) − → p adv + 0.5 0.5m(p adv ) − → p reward ). If some hired assassin is successful then he can report his success to the hiring guy by firing the cut transition (due to the specification End). The state presented on the right of Fig. 1 consists of three assassins where the last hired one has killed the target. Observe that as long as a guy has money he can hire several assassins and that even after hiring he can still try to kill the target by himself. 

A firing sequence of N Jaqen is presented in Fig. 2 where the vertex who fires the transition is filled in black. The initial assassin first tries to find the target but fails ((r, t lost )), losing one bitcoin and one day. Then he hires another assassin by firing the abstract transition (r, t hire ), losing half of his advance money and creating a new vertex v), where the hired assassin has two days, an advance of five bitcoins and a promised reward of five bitcoins for completing the job (M (v) = 2 − → p time + 5 − → p adv + 5 − → p reward ). This assassin kills the target and collects the reward ((v, t lost ) followed by (v, t collect )). Then using the cut transition he (3, 20, 20, 0) (2, 19, 20, 0) (2, 9, 20, 0) (2, 5, 5, 0) t hire (1, 4, 5, 1) t hire (1, 9, 0, 1) t hire (2, 9, 20 , 1) (2, 29, 0, 1) reports it to his employer ((v, τ )), which removes v and adds one token to p dead in M (r). Finally the original assassin can collect his money by firing t collect .

Ordering States of a DRPN. We now define a quasi-order on the states of a DRPN. Given two states s, s of N we say that s is smaller or equal than s or equivalently that s covers s if (without considering labels) there is a subtree in s isomorphic to s (by some matching) such that (1) given any pair of matched vertices (u, u ), M (u) ≤ M (u ) and (2) given any pair of transitions (t, t ) labelling matched edges, 

We say that s covers s denoted s s if there exists ϕ such that s ϕ s .

Given states s, s , deciding whether s covers s is a necessary condition for designing algorithms related to the coverability relation. So we assume that given a DRPN, for all pairs t, t ∈ T ab one can decide whether Upd + t ≤ Upd + t . This hypothesis is satisfied by all "reasonable" effective functions.

The coverability set Cov(N , s 0 ) is defined as the upward closure of the reachability set: Cov(N , s 0 ) = Reach(N , s 0 ) ↑ . As for recursive Petri nets (see [4] ) this quasi-order is strongly compatible (and even more): for all s ϕ s and s

− −−−− → s 1 and ϕ and ϕ 1 coincide on the intersection of their domain. However this quasi-order is not a well quasi-order (see also [4] ) and thus in order to solve the coverability problem, one cannot apply the backward exploration.

Notation. Let S t be a finite set of states. We call a sequence σ such that s σ − → s s ∈ S t a covering sequence.

Expressiveness of a formalism may be defined by the family of languages that it can generate. In [4] , expressiveness of RPNs was studied using coverability languages. In order to compare RPN and DRPN we need to define coverability languages of DRPNs and so we equip any transition t ∈ T ∪ τ with a label λ(t) ∈ Σ ∪ {ε} where Σ is an alphabet and ε is the empty word of Σ * fulfilling λ(τ ) = ε. The labelling is extended to transition sequences in the usual way. Thus given a labelled marked DRPN (N , s init ) and a finite set of states S t , the coverability language L(N , s init , S t ) is defined by:

i.e. the set of labellings for sequences covering some state s ∈ S t of N . We say

The next proposition is an important ingredient for our expressiveness result (see proof in [8] ). The main idea of this proof consists in considering a PN with enough copies of P and T such that each copy mimicks the behaviour of a vertex in a state of the RPN with height at most B and outgoing degree at most B for every vertex. Additional places and transitions allow to express the child relation between vertices and the existence of the vertices in the current mimicked state of the RPN.

We say that a function f :

As an immediate consequence of the properties of f , one defines by induction the strictly increasing sequence (α(n)) n∈N : α(0) = 0 and α(n

. Note that α depends on f , but since in the sequel we consider a single arbitrary f , for sake of readability we write α instead of α f . The next proposition establishes that L f is a DRPN coverability language. Indeed the coverability language of the DRPN below (without abstract transitions) such that the initial state consists of a single vertex with one token in p wa and the final state consists of a single vertex with one token in p w b is L f (see the full proof in [8] ). So we will use L f for witnessing that DRPN coverability languages strictly include RPN coverability languages.

The remainder of this section consists in showing that L f is not an RPN coverability language. Let us pick an arbitrary labelled RPN N with an initial state s init , a finite set of states S t such that L f ⊆ L(N , s init , S t ). Let {σ n } n∈N be a family of sequences covering some state of S t such that λ(σ n ) = a α(n) b f (α(n)) where among the possible σ n 's we pick one with the minimal depth and among those with minimal depth one with the minimal length (i.e. min |σ n |). The skeleton of the proof is as follows.

-L f is a not a PN coverability language (Proposition 3 proved in [8] ). Therefore

The following proposition is obtained by an adaptation of a result related to the (non) weak computability of sublinear functions in PN [12] .

Remark 1. In the appendix of [5] Lemma 6 shows that for any RPN language there exists a marked RPN with an initial state consisting of only one vertex. Therefore we will assume in the following that s init consists of a single vertex.

In order to alleviate notations in RPN and to be consistent with the notations of DRPN, for all t ∈ T , we denote Pre(t), Post(t) and C(t) respectively by Pre t , Post t and C t . Given a labelled RPN N and an abstract transition t, we introduce the following languages:

Proof. Let D denote a bound of the depths of the family of {σ n } ∞ n=1 , and let L N denote more concisely L(N , s init , S t ). We are going to build a net N and some L , a B-bounded language of N such that: L f ⊆ L . Due to Proposition 1 and 3, L f L . We stop the construction earlier if we can conclude that L f L N . Otherwise the relation between L and L N will allow us to conclude. We first build an RPN N that fulfills L(N , s init , S t ) = L N as follows. For all t ∈ T ab , one adds places and transitions according to L N (t) and L ⊥ N (t): 

where the y t and x are defined below:

On the one hand L N ⊆ L(N , s init , S t ) since any firing sequence in N can be performed in N . On the other hand, the new transitions are built according to L N (t) and L ⊥ N (t) in such a way that every firing of a new transition can be replaced by a firing of a sequence of transitions with the same produced label. Hence L(N , s init , S t ) = L N . We now show that for N there exists some B, such for all n ∈ N there is a firing sequence σ n in N with |σ n | ab ≤ B and λ (σ n ) = λ(σ n ). Denote by G = max{|V st | | s t ∈ S t }. Pick an arbitrary n ∈ N and denote more explicitely the covering sequence s init σn − − → s ϕ s t ∈ S t . Assume there is an occurrence t ∈ T ab by the vertex u in σ n creating a vertex v. We transform σ n according to whether the firing (u, t) has a matching cut transition (v, τ ) in σ n : The firing (u, t) Does Not Have a Matching Cut. • Otherwise (i.e. a + b + ∩ L N (t) = ∅ and z t = max{m | b m ∈ L N (t)} < ∞), we replace the firing of (u, t) and all firings from Des(v) by:

which will give us a covering sequence σ n such that λ(σ n ) = a b m with ≤ α(n) and m ≥ f (α(n)). If < α(n), and m > f(α(n)) then L f L N and we are done. Otherwise λ (σ n ) = λ (σ n ) and |σ n | ab < |σ n | ab . We can repeat this process until either one concludes that L f L N or there is no more firing of t without a matching cut transition in σ n . The Firing (u, t) Has a Matching Cut.

If there are more than D occurrences of t with a matching cut in σ n then there are two occurrences (w 1 , t) and (w 2 , t) where w 2 is neither a descendent nor an ascendent of w 1 . So one could build a covering sequence σ with i , m i > 0 such that λ(σ) = . . . a 1 b m1 a 2 

Consider m the occurrences of b in σ n produced at the subtree rooted in v then there exists m > m such that one can build a covering sequence σ with m > f(α(n)) + 1 such that

we replace the firing of (u, t) by the sequence below and remove all firings from Des(v),

and obtain a covering sequence σ n such that λ(σ n ) = a b m with ≤ α(n) and m ≥ f (α(n)). If < α(n), and m > f(α(n)) then L f L N and we are done. Otherwise λ (σ n ) = λ (σ n ) and |σ n | ab < |σ n | ab . We can repeat this process until either one concludes that L f L N or there is no more firing of t with a matching cut transition in σ n . If we are not yet done, we have built a sequence σ n with λ (σ n ) = λ (σ n ) and such that |σ n | ab ≤ |T ab |(2D + G). So we choose B = |T ab |(2D + G). In order that for all a b m ∈ L f there is a covering sequence σ with |σ| ab ≤ B, we build N from N . We observe that the definition of α implies that:

Due to the observation about RPN languages, the initial state of N consists of only one vertex, whose initial marking is denoted m ini . So one builds the RPN N with initial marking − → p ini from N as follows.

• Add elementary transitions t a , t run , t ab and places p ini , p run such that:

• For all t ∈ T , we set:

• For any transition t ∈ T with λ (t) = b, we add the transition t ε which is a copy of t with λ (t ε ) = ε. Let a b m ∈ L f . Then there exist n, δ − , δ + such that = α(n) + δ + and m = f (α(n)) − δ − . Let σ n be a covering sequence in N such that λ (σ n ) = a α(n) b f (α(n)) . We define σ a covering sequence of N as follows. σ starts by (r, t a ) δ + (r, t r )(r, t ab ) |σn| . Then σ is completed byσ n whereσ n is obtained from σ n by: -changing δ − occurrences of transitions with label b by their copy; -whenever σ n creates a new vertex v, one inserts (v, t ab ) |σn| firings. Observe that λ (σ) = a b m . Let w be a word. Define w ↓b as the set of words obtained from w by omitting some occurrences of b.

We are now in position to conclude.

Proof. Let N be an RPN with initial state s init and final states S t such that Each of these vertex either may or may not have a matching cut in σ n . We pick two of these vertices v, v (v ∈ Des(v)) such that either both of them have a matching cut or both of them do not. Denote by w and w the labellings of the sequences performed in the subtree rooted in v and v along σ n , we split the proof in two cases:

• Case w = w . We denote by w = the trace of the sequence performed in the subtree rooted in v without the one performed in the subtree rooted in v :

• w = a , for > 0. Then one can build another covering sequence by mimicking the behavior of v from v. But then the trace of the new covering sequence will be a α(n)− b f (α(n)) and since > 0 we get that a α(n)k− b f (α(n)) / ∈ L f , from which we conclude that L f L N . • w = b m , for m > 0. Then one can build another covering sequence by mimicking the behavior of v from v . But then the trace of the new covering sequence will be a α(n) b f (α(n))+m / ∈ L f from which we conclude that L f L N . • w = a b m , for , m > 0. Then one can build a family of covering sequences { σ x } x∈N by mimicking the behavior of v i from v i+1 recursively x times. We would get that λ( σ x ) = a α(n)+x b f (α(n))+xm for any x ∈ N. But that would give us that:

Then one can build another covering sequence with the trace a α(n) b f (α(n)) where we mimic the behavior of v in v. By doing so we get a covering sequence σ n not deeper then σ n but which is shorter then σ n , i.e. |σ n | ≥ |σ n | which is a contradicts to our assumption about σ n .

The coverability problem takes as input a DRPN N , and two states s 0 , s and asks whether there exists a sequence s 0 σ − → s s. Before developing the proof that the coverability problem is decidable let us describe its scheme.

-The algorithm builds a DRPN N by adding elementary transitions to N (Definition 6). The DRPN N is equivalent to N w.r.t. coverability. Furthermore for any firing sequence σ of N , there is an equivalent firing sequence σ of N such that in σ there is no occurrence of an abstract transition followed later by a matching cut step. -The definition of N , is based on several upward closed sets of N P : (1) Endable(N ), the set of markings m such that from s m one can reach ⊥ and (2) for all t ∈ T ab , Closed t the set of markings from which one can fire t and create a vertex whose marking belongs to Endable(N ). So we establish that one can compute these sets (Proposition 6). -Finally we solve the coverability problem (Theorem 3) by a case based analysis of the covering sequence which, depending on the case, is based on either Theorem 1 or Theorem 2.

As announced above, building the following sets is a key ingredient for the decidability of the coverability problem. Due to the properties of , these sets are upward closed.

and for all t ∈ T ab , Closed t is defined by:

Example 2. Consider the DRPN of Fig. 1 . With one token in p time and in p adv one fires t found producing a token in p dead which allows to fire a cut transition. Furthermore firing the abstract transition t hire does not help to reach ⊥ since in the new vertex, the marking of p time is equal to the marking of p time in its parent vertex and the marking p adv is smaller than the markingof p adv in in its parent vertex. Thus Endable(N ) = {p time + p adv } ↑ . The marking of a vertex created by t hire is greater or equal than p time + p adv if in its parent vertex there is at least one token in p time and three tokens in p adv . Thus Closed t hire = {p time + 3p adv } ↑ .

If we are able to compute Endable and thus {Closed t } t∈T ab then we can build a DRPN N which in some sense is equivalent to N . The interest of N is that for any firing sequence σ of N , there is an equivalent firing sequence σ where the firing of an abstract transition t followed later by a matching cut transition can be replaced by the firing of an elementary t − followed later by the firing of another elementary transition t + . So the set of transitions is extended with T r = {t − , t + | t ∈ T ab }. To ensure the sequentiality between these firings, the set of places is extended with P r = {p t | t ∈ T ab } with one token produced (resp. consumed) in p t by t − (resp. t + ). To ensure that the firing of t − is performed when the corresponding firing of t can be matched later by the firing of the cut transition, the guard of t − is the guard of t intersected with Closed t . In order to formally define N and to exhibit relations between states and thus markings of N and N , we introduce the projection Proj from N P to N P where P = P ∪ P r . In addition N el , obtained from N by deleting T ab , allows to track the evolution of the marking of a vertex in N when no firing of abstract transitions occurs in this vertex.

Then N = P , T , Grd, Upd, Upd − , Upd + , Beg, End is a DPRN defined by:

-for all t ∈ T el , all p ∈ P and all p t ∈ P r , Upd t (p) = Upd t (p) • Proj and Upd t (p t ) = p t ; -for all t − ∈ T r , all p ∈ P and all p t ∈ P r , Upd t − (p) = Upd − t (p) • Proj and Upd t (p t ) = p t + 1 t=t ; -for all t + ∈ T r , all p ∈ P and all p t ∈ P r , Upd t + (p) = Upd + t (p) • Proj and Upd t (p t ) = p t − 1 t=t ; -for all t ∈ T ab , all p ∈ P and all p t ∈ P r , 1.

The following lemma states the correspondence between N , N and N el . We extend Proj to states of N by applying it to the marking of vertices and furthermore to sets of states by the standard set extension. In the reverse direction, given a marking m ∈ N P we define m ∈ N P the extended marking with no token in P r . Similary, given s a state of N , we define s a state of N by extending the marking of vertices of s with no token in P r . N be a DRPN and s 0 Proof.

• Let s 0 σ − → N s. Consider successively all t ∈ T ab . Observe that due to the presence of place p t every occurrence of (v, t + ) in σ can be matched with an occurrence of (v, t − ). The unmatched occurrences of (v, t − ) can be omitted since they only produce useless tokens in p t and do not increase the marking of any other place. So we get a new firing sequence s 0

Proj(s * ). We transform this sequence in a sequence s 0 σ − → N Proj(s * ) as follows. For every pair of matching firings (v, t − ), (v, t + ), we substitute to (v, t − ) the firing (v, t) creating the vertex w with an initial m ∈ Endable(N ) due to the guard of t − . Then we substitute to (v, t + ) a sequence s m σm − − → ⊥ applying it to w. The "reverse" direction is immediate since for all t ∈ T ∪ {τ } and all states s and s , s

• Assertion 2 is an immediate consequence of Assertion 1 of the lemma.

• Let s 0 σ − → s be a firing sequence of N . Consider successively all t ∈ T ab and all matching pairs (v, t), (w, τ ) occurring in σ where w is the vertex created by the firing of (v, t). Let σ * be the subsequence of σ of firings in the subtree rooted at w ended by (w, τ ). Then one substitutes to (v, t), the firing (v, t − ) which is fireable as witnessed by σ * and one deletes σ * substituting (w, τ ) by (v, t + ). Iterating this process, one gets the sequence we are looking for.

• Let m ∈ Endable( N ) ∩ t∈T ab p t = 0. Consider a sequence s m σ − → N ⊥. Using Assertion 3, one can assume that in σ, no firing of an abstract transition is matched with a cut transition. Consider (r, t) the firing of an abstract transition in the root occurring in σ. Since it is not matched by a cut transition one can delete it and all the firings in the subtree rooted at the created vertex and still reaches ⊥. Such a sequence is thus a firing sequence of N el . The other direction is immediate since the set of transitions of N el is included in the one of N . and projection, this immediately entails that Closed n [t] ⊆ Closed n+1 [t] . It remains to prove that for all n, Y n and (for all t) Closed n [t] are upward closed and that the while loop terminates. We also prove it by induction on n. Consider the n th iteration of the repeat loop and let us prove the sequence of sets X k at the beginning of iteration k of the while loop is an increasing sequence of upward closed sets. This will establish the termination of this loop. Observe that X 1 = Proj −1 (End) is an upward closed set and that at every iteration X is increased because it is updated by union of some set with itself. Furthermore, X remains an upward closed set since (1) upward closed sets are closed by union, intersection, and inverse of non decreasing mappings. Finally while X ∩ t∈T ab p t = 0 is not upward closed, this is the case for Y n+1 = Proj(X ∩ t∈T ab p t = 0). Thus for every t, Closed n+1 [t] is upward closed. Assume that σ has depth h > 0. So every m in the root from which there is a firing of an abstract transition t belongs to Closed[t ] since the subsequence in the created vertex up to the cut transition has depth strictly less than h. Consider the last iteration of the repeat loop for which such t is added to Closed [t ] . Then either at this iteration m already belongs to Closed[t] or it will be added at the next iteration (which exists since Y is enlarged) due to execution of the while loop. Indeed consider a closing subsequence of σ for a child of the root created by some transition t and substitute the firing of t by t − , delete the closing subsequence and substitute the cut step by the firing of t + in r. Doing this transformation (and ommitting the cut step in r) one obtains a closing firing sequence in N as described above from s Beg(t) (m) . Thus at the beginning of last iteration of the while loop, N = N el . Using Assertion 4 of Lemma 1, one gets that at this end of this iteration, Y = Endable(N ). Theorem 1. The restricted rooted coverability problem is decidable.

Proof. Due to Assertion 1 of Lemma 1, we consider N . Applying Assertion 3 of Lemma 1, the sequence we are looking for, does not create other vertices than the vertices of s since (1) the firing of abstract transitions matched by cut transitions are non necessary in N and (2) those that are not matched decrease the marking of a vertex and create a subtree useless for covering s = (V, E, M, Λ). Then for any vertex v ∈ V , one guesses an order of creation of its children along the sequence σ and for any transition t labelling an edge of E, one guesses a transition t with Upd + t ≥ Upd + t . Observe that there are only a finite number of such guesses and so the algorithm enumerates them. Afterwards the algorithm proceeds bottom-up from the leaves of s to the root.

Let v be a leaf. Then the algorithm computes by backward exploration the upward closed set Cov

Let v be an internal vertex with v 1 , . . . , v n its children enumerated in the guessed order and t 1 , . . . , t n the associated guessed transitions. Then the algorithm computes by backward exploration the upward closed sets Cov n (v), . . . , Cov

By a straightforward induction, one establishes that m ∈ Cov i (v) if and only from vertex v marked by m there is a firing sequence σ = σ i t i+1 σ i+1 . . . t n σ n with for all j, σ j ∈ T * el and such that (1) the marking of v reached by σ is greater or equal than M (v), and (2) for all j > i, from the initial marking of v j one can fire a sequence that builds a tree covering the subtree of s rooted at v i using the guessed transitions and orders of creation. Finally the algorithm returns true if and only if for some guess m 0 ∈ Cov(r) where r is the root of s.

Proof. Let us fix some net N and some state s. As above we substitute N to N but for sake of readability we omit the occurrences of 'ˆ'. Thus one observes that the state s that should cover s can be chosen as a single branch, say Br, leading to a tree s * isomorphic to s. Indeed the firings that would create other branches are useless since they only decrease the markings in Br or in s . (N , s, k+1) . Furthermore the answer to the restricted coverability problem is positive if and only if m 0 ∈ k∈N RC (N , s, k) . So it only remains to show how to compute RC(N , s, k + 1) when one knows RC (N , s, k) . Observe that: N , s, k) )

where the second term of this union can be computed by a backward exploration.

Using the previous theorems, we are now in position to decide the coverability problem.

Proof. Let us fix some net N and states s 0 and s. As above we substitute N to N and omit the occurrences of 'ˆ'. In order to decide the existence of a sequence s 0 σ − → s ϕ s, we consider two cases depending on ϕ(r)

• |ϕ(V s ) ∩ V s0 | ≤ 1. So one guesses a vertex w ∈ V s0 that is the deepest on the branch leading from r to ϕ(r) in s . Then we transform the net (whose current version is in the sequel denoted N ) as follows. We examine bottom-up all the (proper) descendants of w in s 0 as follows.

Let v be such a vertex, u its parent and t the abstract transition labelling the edge (u, v). If M (v) ∈ Endable(N ) then one adds a place p u,v with a token in u and no token elsewhere and an elementary transition t u,v such that Grd tu,v = p u,v > 0 and Upd tu,v = Since there are only a finite number of possible ϕ (more precisely their restriction over s 0 ) the coverability problem is decidable.

The logical view on continuous Petri nets

Reset nets between decidability and undecidability

A recursive model for distributed planning

Coverability and termination in recursive petri nets

Coverability and termination in recursive Petri nets

A well-structured framework for analysing Petri net extensions

Well-structured transition systems everywhere

Dynamic recursive Petri nets

Theoretical aspects of recursive petri nets

Modelling and analyzing systems with recursive petri nets

Recursive Petri nets

On functions weakly computable by petri nets and vector addition systems

Nested petri nets: multi-level and recursive systems

Process rewrite systems

Self-modifying nets, a natural extension of Petri nets

We introduced DRPN that extend recursive Petri nets in several directions. We established that w.r.t. coverability languages, this extension is strict and we have established that the coverability problem is still decidable.We plan to define a restriction of DRPN for which reachability would be still decidable as in RPN. Moreover since our algorithm is based on backward explorations and our team has already developed an efficient tool for coverability in PN based on such explorations [1] , we want to adapt it for DRPN.

Closing(N ) Input: N a DRPN /* P = P ∪ {p t | t ∈ T ab }, T el = T el ∪ {t − , t + | t ∈ T ab } */ /* Proj is the projection from N P to N P */ Data: X, oldX subsets of N P ; oldY, Y subset of N P ; t a transition Output: Closed an array indexed by T ab of upward closed sets of N PProof. In the sequel Closed[t] denotes the value of this variable at some execution point. Let us denote N the version of N el built by the algorithm and updated at every iteration of loop of lines 15-23.• Termination. We prove by induction that the sequence of sets Y n and for all t, Closed n [t] at the beginning of iteration n of the repeat loop is an increasing sequence of upward closed sets of N P and N P , respectively. So it must stabilize after a finite number of iterations. Since T is finite this will establish termination of the algorithm. First, for all t,