Analysis of Petri Nets with Context-Free Structure Changes
Electronic Communications of the EASST
Volume 71 (2015)
Graph Computation Models
Selected Revised Papers from GCM 2014
Analysis of Petri Nets with
Context-Free Structure Changes
Nils Erik Flick and Björn Engelmann
20 pages
Guest Editors: Rachid Echahed, Annegret Habel, Mohamed Mosbah
Managing Editors: Tiziana Margaria, Julia Padberg, Gabriele Taentzer
ECEASST Home Page: http://www.easst.org/eceasst/ ISSN 1863-2122
http://www.easst.org/eceasst/
ECEASST
Analysis of Petri Nets with
Context-Free Structure Changes
Nils Erik Flick and Björn Engelmann∗
{flick,engelmann}@informatik.uni-oldenburg.de,
https://scare.informatik.uni-oldenburg.de
Carl-von-Ossietzky-Universität, D-26111 Oldenburg
Abstract: Structure-changing Petri nets are Petri nets with transition replacement
rules. In this paper, we investigate the restricted class of structure-changing work-
flow nets and show that two different reachability properties (concrete and abstract
reachability) and word membership in the language of labelled firing sequences are
decidable, while a language-based notion of correctness (containment of the lan-
guage of labelled firing sequences in a regular language) is undecidable.
Keywords: Petri nets, transition replacement, correctness
1 Introduction
Petri nets or place/transition nets [DR98] are system models where resource tokens are moved
around on an immutable underlying structure. They originally lack a notion of structure change
or reconfiguration, but several structure-changing extensions have been formulated. In this paper,
we define Petri nets together with transition replacement rules similar to graph replacement rules
[EEPT06].
Petri nets are popular in the context of workflow modelling [van97], where labelled transitions
correspond to tasks to be executed. An important property of workflow nets is soundness, which
is decidable (in the absence of extra features such as reset arcs), and intuitively means the work-
flow can always terminate correctly and there are no useless transitions. Plain workflow nets,
however, lack the ability of representing dynamic evolution [van01, WRR08].
Structure-changing Petri nets offer a potential solution for dealing with dynamic change in
workflows by combining some advantages of Petri nets and graph grammars. In a structure-
changing Petri net, structure-changing rules interfere with the behaviour of a Petri net. Recon-
figurations occur unpredictably, modelling the influence of an uncontrolled environment, such as
the dynamic addition of a component, or the unexpected complication or iteration of a task.
In detail, the results are decision procedures for
• the firing word problem for 1-safe structure-changing workflow nets
• reachability in structure-changing Petri nets
• abstract reachability in 1-safe structure-changing workflow nets
∗ The work of both authors is supported by the German Research Foundation (DFG), grant GRK 1765 (Research
Training Group System Correctness under Adverse Conditions)
1 / 20 Volume 71 (2015)
mailto:\protect \T1\textbraceleft flick,engelmann\protect \T1\textbraceright @informatik.uni-oldenburg.de
https://scare.informatik.uni-oldenburg.de
Analysis of Petri Nets with Context-Free Structure Changes
and undecidability of the containment of a structure-changing workflow net (labelled firing se-
quence) language in a regular language.
The paper is structured as follows: in Section 2, we introduce structure-changing Petri nets and
workflow nets. In Section 3 we state our decidability and undecidability results. Section 4 draws
parallels to existing work and Section 5 concludes with an outlook.
2 Structure-Changing Petri nets
In this section, we introduce Petri nets in the sense of [DR98, PW02] and extend them to struc-
ture-changing Petri nets as special graph grammars.
Notation. We use −−− and +++ to denote set difference and disjoint set union, respectively, and NNN
for the set of natural numbers including 0. The cardinality of a set X is denoted by |X||X||X|, the length
of a sequence w is also denoted |w||w||w|, and |w|Y|w|Y|w|Y denotes the number of occurrences in w ∈ X∗ of
symbols from Y ⊆ X . The symbol εεε denotes the empty word.
Assumption 1. There are two disjoint alphabets Σ and R of transition labels and rule names,
respectively.
In the following, we introduce structure-changing Petri nets with coloured places. This type
of nets will be used in Section 3.
Definition 1 A net is a tuple (P,T,F−,F+,l,c) where P is a finite set of places, T is a finite
set of transitions with P∩T = /0, F−,F+ : T ×P →N are functions assigning preset and postset
arc multiplicities, respectively, l : T → Σ is the labelling function, c : P → N is the colouring
function. A marked net is a pair N = (N,M), where N is a net and M : P → N is called the
marking of N.
Places and transitions are collectively called items. A net is said to be (strongly) connected,
resp. acyclic, if it is (strongly) connected, resp. acyclic, as a graph, regarding arcs as directed
edges. Isomorphism, denoted N ∼=∼=∼= N′ (resp. N ∼=∼=∼= N′) of (marked) nets means that there are
bijections between the respective place and transition sets that preserve F±, l and c (and M). The
size of a net is |P|+|T|. A connected net with a single transition is a 1-net.
Notation. when F−(t, p) = k, one says there is an arc of weight k from p to t. Likewise, when
F+(t, p) = k, there is an arc of weight k from t to p. We write •t for {p ∈ P | F−(t, p) > 0} and
t• for {p ∈ P | F+(t, p) > 0}. When M(p) = k, it means that p is marked with k tokens. When
c(p) = k, we say that p has colour k. The components of a net named Nx will likewise be named
Px and so on. If there is no subscript, they will be referenced as P and so on. Likewise, the
marked net (Nx,Mx) is usually referred to as Nx. The pictorial representation of nets as graph-
like diagrams is well known, and a translation to graph grammars has been formalised in [Kre81]
and [Cor95].
Selected Revised Papers from GCM 2014 2 / 20
ECEASST
Example 1 (Graphical representation of a marked net; a 1-net:)
a
t0
p0 p1
b
t1
1 1
12
a
Let N be a net. The transition t ∈T is enabled by the marking M iff for all places p, F−(t, p)≤
M(p). The successor marking Mt of M via t is then defined by ∀p ∈ P, (Mt)(p) = M(p)−
F−(t, p)+ F+(t, p), and (N,M)
t⇒ (N,Mt) is called a firing step.
For a sequence u ∈ T∗, the marking Mu is defined recursively as Mε := M and Mau := (Ma)u.
The sequence u is said to be enabled in M iff Mu is defined.
Example 2 (A firing step:)
a a
a
a a
Throughout this paper, all replacement rules are of a simple context-free kind that replace
a single transition by an unmarked net. The adjective context-free is understood in the sense
of hyperedge replacement [Hab92], which is also called context-free replacement. In our case,
transitions correspond to hyperedges.
Definition 2 A (context-free) rule is a tuple (ρ,Nl,Nr) where ρ ∈ R is the rule name, Nl is a
1-net, and Nr is a net with Pl ⊆ Pr, and ∀p ∈ Pl,cl(p) = cr(p) Nl is the left hand side and Nr the
right hand side of the rule.
A match of the 1-net Nl in the net N is a mapping m : Pl ∪{tl}→ P∪T such that m maps the
sole transition tl of Nl to a transition such that ll(m(tl)) = l(tl) and the places pl ∈ Pl to places
in P such that ∀p ∈ Pl,cl(m(p)) = c(p). The notion is extended to matches in marked nets: a
match of Nl in (N,M) is a match of Nl in N. A match of the rule (ρ,Nl,Nr) on a marked net
N is a match of Nl in N. An abstract application, with match m, of ρ to a marked net N is a
pair (N,N′) such that if tl is the transition in Nl , T ′ = T −{m(tl)}+ Tr, P′ = P + (Pr −Pl), M′
coincides with M on the places from P and has value 0 otherwise. The place colours are as in N
and Nr, and
F′±(t, p) =
F±(t, p) t ∈ T, p ∈ P
F±r (t, p) t ∈ Tr, p ∈ (Pr −Pl)
F±r (t, p
′) t ∈ Tr, p = m(p′)
0 otherwise.
N
ρ
⇒N′ or N
ρ,m
⇒ N′ is a replacement step.
Note that we always assume Pr ∪Tr to be disjoint from P∪T in a replacement step (hence
the notation “+” instead of “∪” in the above definition). Formally, in a replacement step Nl and
Nr are replaced with isomorphic copies whose items do not occur in P∪T , and these copies are
3 / 20 Volume 71 (2015)
Analysis of Petri Nets with Context-Free Structure Changes
used in the rule application.1
Remark 1 Given N, ρ and a m, the resulting net N′ is uniquely determined.
Example 3 (A replacement step induced by a rule ρ and a match m:)
0
a
1
c
( )
a
0 1
c
( )
a
0 1
c
( c )
( )
a
0 1
ρ
m
A step is either a firing step or a replacement step. We define four functions for extracting
the information from a step: for a firing step e, let τ(e) := t, λ (e) := l(t), from(e) := (N,M)
and to(e) := (N,M′). For a replacement step, let τ(e) := m(tl), λ (e) := ρ , from(e) := N and
to(e) := N′. The functions to, from, τ and λ canonically extend to sequences.
Definition 3 A structure-changing Petri net is a tuple S = (N,R), where N is a marked net and
R is a finite set of rules.
Remark 2 Every marked net N may be seen as a structure-changing Petri net (N, /0) with empty
rule set, which will be called a static net and by abuse of notation also denoted N. We will not
distinguish between N and (N, /0).
A derivation of length n ∈ N in a structure-changing Petri net S = (N,R) is a pair (ξ ,σ) of
a sequence ξ0...ξn−1 of steps and a sequence σ0...σn of marked nets such that to(ξi) = σi+1,
from(ξi) = σi for all i ∈{1,...,n−1} and N = σ0. We write σ0
ξ
⇒R σn and say that (ξ ,σ) starts
in N = σ0 and ends in σn.
Example 4 (A structure-changing Petri net derivation. The small numbers serve to track places
through the derivation:)
0
a
1
ρ,m
0
a
2
a
1
a
0
a
2
a
1
1 As this causes little confusion in our paper, we will not stress this issue further.
Selected Revised Papers from GCM 2014 4 / 20
ECEASST
Example 5 (Rules for a vending machine which either returns 50 cent pieces or smaller change.
Place colours represent denominations of coins:)
50¢
0 1 0 1
20¢
0 1 0 1
10¢
0 1 0 1
50¢
0 1
)
20¢
20¢
10¢
(
0 1
A marked net N′ is said to be reachable in S from N iff there is a derivation in S that starts in
N and ends in N′. The marked nets reachable in S are also called (reachable) states of S. We
write RS(S) for the set of all reachable states of S. In a static net, instead of derivations one
considers transition sequences, as they uniquely determine derivations. A net, rule or structure-
changing Petri net is k-coloured if the highest colour assigned to any place does not exceed k−1.
A marked net is k-safe if any reachable marking has at most k tokens per place.
Remark 3 Note that the place colouring does not affect the behaviour of the net at all. It will
be used in Section 3 to specify abstract markings.
In the following, we introduce workflow nets [van97], extended by structure-changing rules,
as a special case of structure-changing Petri nets.
Definition 4 A workflow net is a tuple (N, pin, pout) consisting of a net N and a pair of dis-
tinguished places pin, pout ∈ P, the input and output place which have no input respectively no
output arcs, subject to the requirement that adding an extra transition from pout to pin would
render the net strongly connected.
The data (pin, pout) need not be made explicit, since these places are easily seen to be uniquely
determined in a workflow net. Thus we are justified in treating a workflow net as a special net.
The start marking of a workflow net N, i.e. the marking where only pin is marked with one
token and all other places are not marked, is denoted by •N. The end marking where only pout
is marked with exactly one token is denoted by N•. A workflow net N is sound iff from any
marking reachable from •N, N• is reachable, and for each transition t there is some marking M
reachable from •N such that t is enabled in M.
5 / 20 Volume 71 (2015)
Analysis of Petri Nets with Context-Free Structure Changes
Definition 5 A structure-changing workflow net is a structure-changing Petri net S = (N,R)
such that
(1) N is a sound workflow net marked with its start marking.
(2) for every rule (ρ,Nl,Nr) ∈ R, Nl and Nr are sound workflow nets; Nl has two places, one
transition, arc weights 1.
(3) ∑t∈Tr F
+
r (t, pout) = ∑t∈Tr F
−
r (t, pin) =1 and the input (resp. output) place of Nr is pin ( pout ).
Condition (2) implies that only single-input, single-output 1-nets are permitted as left hand
sides. The role of condition (3), which in our opinion does not unduly impact modelling capacity,
is to avoid certain complications that otherwise arise in the analysis. Although the restrictions
rule out markings with multiplicities, it is now possible to create more instances of a subnet
by replacing transitions. Structure-changing workflow nets can still capture situations such as
workflows that undergo complications as they are executed, as in Example 5.
Every reachable state of a structure-changing workflow net is a reachable state of some work-
flow net. A structure-changing workflow net is called acyclic if every reachable state is an acyclic
net. It is called 1-safe if every reachable state is marked with at most one token per place.
3 Analysis of Structure-Changing Workflow Nets
In this section, we define and investigate some decision problems for structure-changing work-
flow nets. We define the derivation language of a structure-changing Petri net and show that
while language containment in a regular language is undecidable, two reachability problems are
decidable, and the firing word problem is decidable at least for structure-changing workflow nets.
We prove a series of lemmata, corresponding to a local Church-Rosser property for graph
grammars [EEPT06], that allow us to equivalently re-arrange derivations, which will be conve-
nient in later proofs.
Lemma 1 (Independence) Given a structure-changing Petri net (N,R), a firing step (N,M) t⇒
(N,M′′) and a replacement step (N,M)
ρ,m
⇒ (N′,M′) for some (ρ,Nl,Nr) ∈ R and match m with
t 6= m(tl), then there is a firing step (N′,M′)
t⇒ (N′,M′′′) and a replacement step (N,M′′)
ρ
⇒
(N′,M′′′) where M′′′(p) takes the value M′′(p) for p ∈ P and 0 for p 6∈ P.
(N,M)
(N′,M′) (N,M′′)
(N′,M′′′)
ρ t
t ρ
Proof. Immediate from Definition 2 and the definition of transition firing.
The result (N′,M′′′) is the same only up to an isomorphism, but this will not really impact
any of the results. In the scope of this section, two derivations (ξ ,σ) and (ξ ′,σ ′) are equivalent
if they are of the same length n and the marked nets σn and σ ′n are isomorphic. Two transition
sequences are said to be equivalent if they are equivalent as derivations. Transition sequences
Selected Revised Papers from GCM 2014 6 / 20
ECEASST
which only differ by a permutation of the steps are easily seen to be equivalent. In a sound
workflow net N, a transition sequence u is said to be terminal when (•N)u = N•.
Lemma 2 (Permuting Steps) If S is a structure-changing Petri net, for every derivation (ξ ,σ)
of length n in S, under any of the conditions given below there is a derivation (ξπ ,σπ ) also
of length n such that σn and (σπ )n are isomorphic, and λ (ξ ) = uabv and λ (ξπ ) = ubav for
some u,v ∈ (R∪Σ)∗ and a,b ∈ (R∪Σ). If λ (ξi) = a and λ (ξi+1) = b, ta = τ(ξi), tb = τ(ξi+1),
from(ξi) = N, to(ξi) = from(ξi+1) = N′ and to(ξi+1) = N′′,
Situation Sufficient condition for transposition
a ∈ Σ,b ∈ Σ •tb ∩ta• = /0
a ∈ Σ,b ∈ R ta 6∈ T −T ′
a ∈ R,b ∈ Σ tb 6∈ T ′−T
a ∈ R,b ∈ R tb 6∈ T ′−T
Proof. a,b ∈ Σ: transitions meeting the requirement can be transposed in an enabled sequence:
in a net N, if Mt1t2 exists and •t2 ∩ t1• = /0, then t2 is enabled in M: all places in •t2 hold at
least as many tokens as in Mt1, and t1 is enabled in Mt2 because ∀p ∈ •t1 ∩•t2 have M(p) ≥
F−(p,t1)+F−(p,t2). By commutativity of addition Mt1t2 = Mt2t1 and hence σ|u|+2 = (σπ )|u|+2.
a ∈ Σ,b ∈ R: b can be applied to σ|u| because rule applicability is independent of the mark-
ing, and by Lemma 1 the same state σ|u|+2 is reached. The condition is necessary to meet the
requirements of Lemma 1: otherwise, ta is not available after the replacement step.
a ∈ R,b ∈ Σ is similar: since the preset of the transition tb is unchanged by the application of
R, tb is enabled in the state σ|u| and Lemma 1 applies.
a,b ∈ R: since only the matched transition is replaced and all others remain unchanged, the
rules can be swapped, yielding an isomorphic result. In this case and the previous one, the
condition is necessary because otherwise the transition tb is not present prior to the event σi.
The homomorphism t 7→ (if t ∈ A then 0 else 1) defines a pre-order wA,BwA,BwA,B on sequences of
(A + B)∗ by comparing the images of sequences under the lexicographic order induced by 0 < 1
on {0,1}∗.
Lemma 3 Given a transition sequence u in a marked net with T = T ′+T ′′, and T ′×T ′′ contains
only pairs (t′,t′′) where •t′′∩ t′• = /0, then any transition sequence that is equivalent to u and
minimal with respect to wT ′,T ′′ is in T ′∗T ′′∗.
Proof. A strictly decreasing step along the lexicographic order is possible as long as Lemma 2
can still be applied to a contiguous subsequence t′′t′, yielding another equivalent transition se-
quence.
Definition 6 A step ei of a derivation (ξ ,σ) causally precedes another step e j, i < j, if either
λ (ξi),λ (ξ j) ∈ Σ and τ(ξi)•∩•τ(ξ j) 6= /0, or λ (ξi) ∈ R,λ (ξ j) ∈ Σ and τ(ξ ) j ∈ codomain(mi) or
λ (ξi),λ (ξ j) ∈ R and τ(ξ ) j ∈ from(ei). The causal dependency relation is the transitive closure
of the causal precedence relation.
Lemma 4 Any derivation (ξ ,σ) equivalent to a given one and minimal with respect to wΣ,R
7 / 20 Volume 71 (2015)
Analysis of Petri Nets with Context-Free Structure Changes
has λ (ξ ) = r0s0...snrn+1 where ∀i,si ∈ Σ,ri ∈ R∗ and if ξi,0...ξi,n = ri, then ξi, j causally precedes
ξi, j+1, and ξi,n causally precedes si+1.
Proof. Analogous to Lemma 3. As long as there is a contiguous subsequence ξiζ ξ j where
λ (ξi) ∈ R, λ (ζ ) ∈ R∗, λ (ξi+1) ∈ Σ and ξi does not causally precede any of ζ ξ j, by induction
over the length of ζ and using Lemma 1, an equivalent but strictly wΣ,R-smaller derivation with
...ζ ξ jξi... can be constructed.
3.1 Firing Word Problem
Definition 7 The firing language of a structure-changing Petri net (N,R) is
F(S) :={ f (w)∈ (Σ∪R)∗ | ∃N′ : N w⇒R N′}
where f is the homomorphism that deletes all letters of R and leaves transition labels Σ un-
changed.
Due to the deleting homomorphism, it is not trivial to see whether a given word w occurs in
the firing language of S.
Problem 1 (Firing word problem).
Given: a structure-changing Petri net S and a word w ∈ Σ∗
Question: w ∈F(S)? Is w contained in the firing language of S?
We leave Problem 1 open and treat the firing word problem for 1-safe structure-changing
workflow nets instead.
Problem 2 (Problem 1 for 1-safe structure-changing workflow nets).
Given: a 1-safe structure-changing workflow net S and a word w ∈ Σ∗
Question: w ∈F(S)? Is w contained in the firing language of S?
The question is decidable for 1-safe structure-changing workflow nets by the following means:
while applying rules, one keeps track of the minimum length of any word in which each transi-
tion could occur (the minimum word length defined below). Rule matches on transitions that can
only be used in words longer than w need not be explored, because under the postulated assump-
tions the minimum word length is non-decreasing under replacement. Rules are only applied
to enabled transitions. The creation of redundant transitions is limited by condition (3) of the
definition of a structure-changing workflow net.
In a static net N = (N,M), let ‖·‖N : T ⇀ N be the partial function assigning to each transition
t of the net the minimum length of any derivation using t. It is undefined if there is no such
derivation, otherwise ‖t‖N = min({|ut| | ut ∈ T∗,∃M′ = Mut}). We call ut with |ut| = ‖t‖N a
minimum-length t-word of N. It contains t exactly once at the end, or a proper prefix would
suffice. Note also that sequences in T∗ rather than label words in Σ∗, are considered. Calculating
‖t‖N might in general not be efficient, but it is in principle possible for all nets.
Selected Revised Papers from GCM 2014 8 / 20
ECEASST
Lemma 5 Let S = (N,R) be a 1-safe structure-changing workflow net. If N ∗⇒N′, and N′
ρ,m
⇒
N′′ is a replacement step using rule (ρ,Nl,Nr), and let t = m(tl). Then each transition t ∈ T ′′−T ′
has ‖t‖N′′ =‖t‖N′−1 +‖t‖(Nr,•Nr) ≥‖t‖N′, and each transition ť ∈ T −{t} has ‖ť‖N′′ ≥‖ť‖N′.
Proof. Let ut be a minimum-length t-word in N and vt a minimum-length t-word in (Nr,•Nr).
Then uvt is a minimum-length t-word in N′.
A transition sequence v ∈ T∗r is enabled in some marking in Nr precisely when it is in the
corresponding marking (mapping the places via m) in N′′ and has the same effect on the places
of Pr −Pl + m(Pl) and no effect on all other places. If u is a transition sequence enabled in M′,
then Lemma 3 guarantees the existence of a transition sequence ũ that can be decomposed as
ũ = uv, where u ∈ T ′∗ and v ∈ (T ′′−T ′)∗. For any such uv, because Mu exists and enables t, ut
is also a possible transition sequence, and furthermore the shortest one containing t.
As to the second statement, let uť be a minimum-length ť-word of N′′. Decomposing u as
u0t0u1...tnun+1 with ui ∈ T ′∗ and ti ∈ T ′′−T ′, there is an equivalent wT ′′−T ′,T ′-minimal enabled
transition sequence ũ = ũ′0s0ũ
′
1s1...ũ
′
m+1 with ũ
′
i ∈ T
′∗, sk ∈ (T ′′−T ′)∗ and s0 ·...·sm = t0 ·...·tn,
and ũ′0 ·...·ũ
′
m+1 = u0 ·...·un+1, and sk is terminal in Nr: assuming the contrary would imply that
any equivalent transition sequence of the form ũ′0s0ũ
′
1s1...ũ
′
m has some sk such that the condition
(•Nr)sk = Nr• is violated. Every transition ti added in the replacement step falls into one of
three sets, which we call start, middle and end. A start transition is one enabled in •Nr. A
end transition is one that has the end place of Nr in its postset. A middle transition is any other
transition of Nr. So if ũ′0s0ũ
′
1s1...ũ
′
m is such a sequence where for some k ∈{0.....m}, (•Nr)sk
differs from Nr• then the first transition of sk+1 (if k < m−1) can neither be a start, nor middle,
nor end transition. The latter two lead to a contradiction with wT ′′−T ′,T ′-minimality, while the
former would contradict 1-safety.
Therefore one can construct a ť-word of N′, namely ˜̃u′′ = ũ′0tũ
′
1...ũ
′
mť, which is in any case at
most as long as uť, thus ‖ť‖N′ ≤‖ť‖N′′
Proposition 1 It is decidable for any 1-safe structure-changing workflow net S and word w∈Σ∗
whether w ∈F(S).
Proof. The idea of the proof was described in the text following the problem description. The
following algorithm decides the question:
1: procedure WORD(N,w)
2: k := |w|
3: St :={N}
4: while w 6= ε do
5: St := EXPLORE(St,k−|w|)
6: aw := w ; a was the first letter, w now contains the rest
7: St :={(N,Ma) | (N,M)∈ St} ; try successor by firing, if defined
8: return St 6= /0
9: procedure EXPLORE(St, j)
10: repeat
11: for all N ∈ St do ; gather relevant successors by replacement
9 / 20 Volume 71 (2015)
Analysis of Petri Nets with Context-Free Structure Changes
12: for all enabled transitions t of N do
13: for all matches m of rules ρ on t do
14: N′ := result of replacement step ; N
ρ,m
⇒ N′
15: if 6 ∃N′′ ∈ St : N′ ∼= j N′′ then
16: add N′ to St
17: until no new states found
18: return St
We prove that the algorithm terminates and outputs the correct answer.
The procedure WORD iterates over w. It is correct, by induction on the length of w: the
induction basis is witnessed by the trivial case of the empty word. Induction hypothesis: for any
j ≤ k ∈ N, the prefix u of w of length j is in the language iff St is not empty. Induction step:
for any derivation (ξ ,σ) with f (λ (ξ )) = au, Lemma 4 yields another derivation (ξ ′,σ ′), with
λ (ξ ′) = zau′, z ∈ R∗ and f (u′) = u, and each step ei (i ≤|z|) causally preceded by the previous.
z1 a1 z2 a2︸ ︷︷ ︸
∈R∗
∈
Σ
︸︷︷︸
∈R∗
∈
Σ
...
...
Each of the replacement steps ei whose corresponding rule names form the z prefix causally
precedes the next; unless |z| = 0, the first transition to be fired, labelled a, is created in the step
e|z|−1. In any of the first |z| steps, the matched transition is enabled. This makes it unnecessary
to ever directly explore the replacement of disabled transitions.
It remains to be seen that the subset of reachable states of S that actually need to be explored
further for the word u is finite: it is always the case that |z|, which may well be 0, can be bounded
from above by a constant depending only on the rules. The reason why the EXPLORE procedure
terminates rests with the comparison that decides whether states are added to St. The comparison
is done according to an equivalence relation ∼= j ( j ∈ N): a pair of marked nets is in ∼= j if they
have the same subnet induced by considering only the transitions that can contribute to words
of length up to j, and the places attached to these. By Lemma 5, minimum word lengths only
increase and therefore all transitions with minimum word length exceeding j can be ignored in
the exploration.
Only a finite number of equivalence classes of ∼= j occur in the application of replacement
steps from R. Let n be the maximum number of items in a right hand side of any rule of R.
Regarding each state as a directed graph whose nodes are the places and transitions, and whose
arcs are directed edges, let d be the function assigning to each item it the length of the shortest
directed path from the place pin to it. Then by induction on the length of the derivation, no rule
application leads to a state which, as a graph, has any node with more than n successors. The
number of items with d up to 2 j is bounded by n2 j. There is a finite number of 1-safe nets with
these properties.
The set of items of N with d up to 2 j clearly includes all transitions t with ‖t‖N ≤ j. Firing
may reduce the minimum word length of any transition by at most 1. This makes it safe to
compare states by ∼= j−1 at the next iteration.
Selected Revised Papers from GCM 2014 10 / 20
ECEASST
3.2 Reachability Problems
In this subsection, before defining abstract reachability we first show that concrete reachability
(without using any abstraction) of a given marked net is decidable. Our construction for deciding
concrete reachability is similar to the unfolding construction used in [BCKK04] in a different
context. The idea is to unfold all possible rule applications until the size of the smallest net
obtained using a new match exceeds the queried N, since the size of the net grows monotonically
with each rule application and the set of rules is finite.
In the construction, for each possible match, the net is extended the same way as in a rule ap-
plication but the matched transitions are preserved. To control the simulation, the rule transitions
and control places take care of disabling or enabling net transitions according to the simulated
rule applications.
Let matchρ (N) ⊆ T × P∗ be the set of all matches of rule ρ on net N, each match being
uniquely determined by target transition and place mapping (we assume here that every left hand
side is equipped with an arbitrary total order on the place set, inducing a bijection between place
mappings and sequences over P).
Construction 1 (k-unfolding). Given a n-coloured structure-changing Petri net (N,R), let N0 be
the net obtained from N by adding new places {pt | t ∈ T} and arcs of weight 1 from each t to its
respective pt and back. The new colour n is chosen for all the pt places. To each item created in
the construction, we assign a history, which is a sequence of steps. All transitions t of N0 have
hist(t) = ε . Items added in a rule application eµ,ρ matching t ∈ Ti will have history hist(t)·eµ,ρ .
For i ≤ k, the set Ti+1 is computed from Ti by disjointly adding, for every match µ of any rule
(ρ,Nl,Nr) ∈ R, the transitions Tr −Tl , and one transition for each match, which we call match
transition: {thist(t)·eµ,ρ | µ ∈ matchρ (Ni)} where eµ,ρ is the replacement step determined by ρ , µ
and Ni.
The set Pi+1 is computed from Pi by disjointly adding, for every match µ of any rule (ρ,Nl,Nr)∈
R, the places of Pr −Pl , and one control place for every right hand side transition: Pctrl = {pt |
t ∈ Ti+1 −Ti,l(t)∈ Σ}.
The arc weights in Ni+1 are as follows:
F±i+1(t, p) =
F±i (t, p) t ∈ Ti, p ∈ Pi
F±r (t, p) t ∈ Tr, p ∈ (Pr −Pl) (∗)
F±r (t, p
′) t ∈ Tr, p = m(p′) (∗)
1 t ∈ Ti + Tr, p = pt
1 t = tx, c(p) = n, hist(p) = xe (F+only)
1 t = txe, c(p) = n, hist(p) = x (F−only)
0 otherwise,
where (∗) applies to items obtained from the same match of a rule (ρ,Nl,Nr), x is any sequence
of steps and e is any step. The pt places are always assigned colour n and the tx transitions are
labelled with the corresponding rule name from R. The marking Mk agrees with M on the places
of N0, has 1 on each pt place and 0 elsewhere. Nk = (Nk,Mk) is the k-unfolding of (N,R).
11 / 20 Volume 71 (2015)
Analysis of Petri Nets with Context-Free Structure Changes
Example 6 (A structure-changing workflow net S = (N,R):)
a
a
,
ρ, a0 1 cb0 1
Example 7 (The 0-unfolding N0 and the 1-unfolding N1 of S, where µ indicates match transitions:)
a
a
a
a
µ µ
cb cb
Let κ′ = κ′(S,NQ) ∈ N be the smallest number such that every marked net N reachable in
any derivation (ξ ,σ) without state cycles (i.e. repetition-free σ ) and with |λ (ξ )|R ≥ κ′ has no
derivation N
∗⇒R (NQ,M) for any M. The number κ′ is well-defined because net size increases
monotonically along any derivation, and only finitely many nets of any given size are reachable.
For the same reason, κ′ can be effectively over-approximated by considering all derivations with
|λ (ξ )|Σ = 0 that produce nets of size at most |PQ|+|TQ|.
Proposition 2 It is decidable whether a given marked net NQ is reachable in a given structure-
changing Petri net S = (N,R).
Proof. The idea is to determine the number κ′(S,NQ) and reduce the question to reachability in
a κ -unfolding Nκ of S for κ ≥ κ′(S,NQ), the Petri net reachability problem being well-known
to be decidable [PW02].
(N̂,M̂) (Nκ ,M)
(N̂′,M̂′) (Nκ ,M′)
strip
ρ or t
strip
tµ or t
We prove a mutual simulation of S and Nκ for any derivation ξ with up to κ rule applications
by induction on the length of ξ . As argued in the definition of κ(S,NQ), no derivation with
|λ (ξ )|R > κ yields NQ. If |λ (ξ )|R ≤ κ , by induction on the length of the derivation, Nκ and S
simulate each other via a mapping strip, defined as follows: the image of (Nκ ,M) is the marked
net N̂ with transitions T̂ ={t ∈ T | M(pt) > 0}, places P̂ = (P−Pctrl)−{p ∈ P |∀t ∈ •p∪ p•,t 6∈
T̂} and F̂−, F̂+, l̂, ĉ are F−, F+, l, c with their domains restricted to P̂, T̂ .
If N̂
x⇒R N̂′, if x ∈ R, and by hypothesis, N̂ = strip(N′′) for N′′ = (Nκ ,M) for some marking,
then Mtx = M′ such that strip(Nκ ,M′) = N̂′: there is a transition tx because all rule matches
for derivations of up to κ rule applications are represented as transitions in Nκ ; the preset of tx
contains exactly the matched transition τ(x) = strip(t̂) for some t̂ ∈ T̂ . This transition is not in T̂ ′.
Selected Revised Papers from GCM 2014 12 / 20
ECEASST
Instead, the items of the right hand side are present in strip(Nκ ,M′), according to the replacement
step x. If x ∈ Σ, then the step is also simulated in strip(N).
If in Nκ , Mtx = M′, then it is easy to see that the images under strip of (Nκ ,M) and (Nκ ,M′)
are related by the replacement step with match µ . If Mt = M′ for a non-match transition, this
corresponds via strip to a firing of that transition.
The simulation faithfully preserves all events in derivations of length up to κ .
Let us now turn our attention to a different notion of reachability, namely reachability of
abstract markings. Since the state space of a structure-changing Petri net can be infinite, to
specify interesting state properties it is insufficient to specify the number of tokens on specific
concrete places. Instead, we fix a finite set of colours and state constraints generically, for all
places of a given colour. The place colours may carry a model-specific meaning, or just encode
structural information about the net. We will therefore introduce a notion of abstract marking: a
multiset that counts the total number of tokens on places of each colour in a structure-changing
Petri net.
A multiset over a finite set S, or S-multiset, is a function S → N. The set of S-multisets is
denoted NS. The singleton multiset mapping a to 1 and everything else to 0 is also written a.
The size |m| of a multiset m is the sum of the values. Multiset addition is component-wise. A
sum ∑x∈m f (x) over a multiset m ∈ NS is defined with multiplicities, ∑x∈S m(x) f (x). Multisets
are compared using the product order, i.e. m ≤ m′ iff ∀s∈S, m(s) ≤ m′(s). In marked nets,
we redefine •t and t• to mean the P-multisets p 7→ F±(t, p) for ± = +,−, respectively. The
definition of enabledness canonically extends to multisets of transitions. For any marked net
N = (N,M), we define the colour abstraction α : N → N to be the function i 7→ ∑p∈c−1(i) M(p).
For k-coloured nets, we restrict the domain of α to 0,...,k−1. The set of images under α of the
reachable states of S is denoted by ARS(S), for abstract reachability set.
If N = (N,M) is a marked net, define a set of multisets over {0,...,k − 1}+ T , the ex-
tended reachability set ER(N), as ER(N) = ARS(N) +{α(m−∑t∈s •t) + s | m ∈ RS(N), s ∈
NT enabled by m}. The set ER(N) is finite if N is a sound workflow net with its start mark-
ing. Intuitively, it represents all snapshots of the net’s state before, after and during possibly
concurrent firing events.
Problem 3 (Abstract reachability).
Given:
a k-coloured structure-changing Petri net S for some k ∈N
q : {0,...,k−1}→N
Question: q ∈RS(S)? Is the abstract marking q reachable?
Given a structure-changing Petri net S = (N,R), we let A(S)A(S)A(S) denote the set that comprises N
and the right hand sides of all rules in R. Let T(S)T(S)T(S) =
⊎
Nw∈A(S) Tw be the set of all transitions
occurring in any right hand side or in the start net. (
⊎
stands for a disjoint union of multiple
sets). For the intuition behind the following proposition, we would like to refer to Figure 1 on
the following page:
Proposition 3 The abstract reachability problem is decidable for 1-safe structure-changing
workflow nets.
13 / 20 Volume 71 (2015)
Analysis of Petri Nets with Context-Free Structure Changes
ER(S)
ER(R0)
x0 + t0
t0 ⇒ R0 x1 + t1
tk ⇒ Rk
...
xk + tk
ER(Rk)
1 2
2 0
3 1 6 3 7 3≤
α
α
xk+1 + tk+1 0 1 6 4 7 36≤
α
sum
α
target
Figure 1: The abstract reachability procedure visualised
Proof. We present an algorithm that, given a structure-changing workflow net S and q ∈ Nk,
decides whether there is any reachable state N ∈RS(S) such that α(N) = q. Let T = T(S).
1: procedure ABSTRREACH(S,q)
2: Queue := ER(N); Visited := /0
3: while Queue not empty do
4: m := pop(Queue)
5: if m = q then
6: return true
7: else
8: if not (|m|> |q| or m|P 6≤ q or m ∈ Visited) then
9: for all t,m′ such that m = t + m′ do
10: for all {µ ∈ matchρ (t) | (ρ,Nl,Nr)∈R} do
11: append(Queue,{m′+ m | m ∈ER(Nr,•Nr}))
12: Visited := Visited∪{m}
13: return false
To explain the algorithm, let us define a multi-rooted directed graph W, in general infinite. Its
nodes are multisets over {0,...,k−1}+ T. The elements of ER(N) are the roots of W. Each
node t + m with t ∈ T has successors x + m where x ∈ ER(Nr) and Nr is the right hand side of a
rule that matches t. Whether a rule can match t can be checked directly from A(S).
Multiset size increases monotonically along the edges due to the fact that the empty marking
cannot be reachable in a sound workflow net. Hence to check for the abstract reachability of q, it
suffices to explore a spanning tree of the prefix of W induced by the nodes of size not exceeding
|q|, of which there are finitely many. Branching is finite due to the finite ER sets of the right
hand side nets. By Kőnig’s Lemma such a tree is finite, hence the search terminates.
Selected Revised Papers from GCM 2014 14 / 20
ECEASST
Besides those with at least one transition, W contains only colour abstractions of reachable
markings: a derivation leading to a suitable marked net can simply be read off a path in W,
because in the case of 1-safe structure-changing workflow net it is immaterial which transition is
replaced, so the abstraction preserves all information needed to construct a suitable derivation.
Also, W contains the colour abstractions of all reachable states, by induction on the number
of replacement steps in a wΣ,R-minimal derivation. As long as no rule is applied, the statement
clearly holds. Suppose that the property holds for any derivation (ξ ,σ) up to a certain length.
Any new replacement step N
ρ
⇒ N′ using a rule ρ must match an activated transition t by the
assumption on the derivation. Any state obtained by replacing t and executing a non-terminal
sequence of transitions in the right hand side has an abstract marking m + m′′, where m + t ∈
ER(N), and m′′ is in the subset of the abstract reachability set of (N′,R) accessible with fewer
replacement steps, by induction hypothesis.
It follows that the algorithm is correct since it explores W until reaching nodes whose size
exceeds |q|, and checks whether q is obtained.
The complexity of the abstract reachability problem is inherited from the corresponding class
of static 1-safe nets. For 1-safe nets in general, reachability is PSPACE-complete whereas it is
just NP-complete for acyclic 1-safe nets [Esp96].
Proposition 4 The abstract reachability problem for acyclic 1-safe structure-changing work-
flow nets is NP-complete.
Proof. It follows from the proof of Proposition 3 that the problem is not only decidable, but
in NP: the answer is positive iff there exists a certain easily checked polynomial-length object,
namely the path through W at most O(|R| · |q|) nodes of length O(|q|) each. NP-hardness is
straightforwardly shown by a reduction from the corresponding problem for acyclic 1-safe nets.
The reachability problem of 1-safe nets can be reduced to the reachability problem of 1-safe
workflow nets (see Figure 2). This reduction goes as follows: for every place in the 1-safe
marked net (N,M0), a complementary place is added; start end place and 2 + 3|P| extra items
are added; the simulation is initialised by filling in the start marking and its complement, and it
can be aborted without producing erroneous runs by emptying the net. Reachability of M from
M0 becomes reachability of the corresponding marking from the start marking of the workflow
net. The workflow net can be seen to be sound. To preserve acyclicity, one removes the com-
plementary places. The reduction of the reachability problem for 1-safe workflow nets to an
abstract reachability problem for the corresponding static 1-safe structure-changing workflow
net is trivial: places are coloured bijectively.
Proposition 5 The abstract reachability problem for 1-safe structure-changing workflow nets
is PSPACE-complete.
Proof. PSPACE-hardness again follows from the corresponding problem for 1-safe nets, the
reduction using the same construction presented above. The procedure proposed in the proof of
Proposition 3 is also easily seen to be in PSPACE because the upper bound on κ is polynomial
in |q| and |R|.
15 / 20 Volume 71 (2015)
Analysis of Petri Nets with Context-Free Structure Changes
pin pout︸ ︷︷ ︸
initialisation of M0
(complementary places)
︷ ︸︸ ︷
simulation of N
(complementary places)︸︷︷︸p1 ︸︷︷︸p2 ︸︷︷︸p3
Figure 2: Reduction from 1-safe nets to 1-safe workflow nets.
As a bonus, W can be used to decide coverability of an abstract marking q, i.e. the question
whether any state N with α(N)≥ q can be reached.
Proposition 6 Coverability of an abstract marking is decidable for 1-safe structure-changing
workflow nets.
Proof. W is the reachability graph of a net with place set {0,...,k −1}+ T and appropriate
transitions that have as preset t ∈ T and postset m, for every m ∈ ER(Nr,•Nr), where Nr is the
right hand side of a rule matching t. Hence coverability is reduced to Petri net coverability, which
is decidable [PW02].
3.3 Containment Problems
In this subsection, we study the inclusion of the firing language of a structure-changing work-
flow net in a given regular language. The motivation is that the regular language can specify all
desirable net behaviour, and the problem is to check whether any undesirable firing sequences
exist or not.
Problem 4 (Containment in Regular Language).
Given:
a regular language L ⊆ Σ∗
a 1-safe structure-changing Petri net S
Question: f (L(S))⊆ L?
It is well known that the emptiness of the intersection of two context-free languages is unde-
cidable.
Proposition 7 (Undecidability of abstract language compliance) Containment of a structure-
changing workflow net language in a regular language is undecidable even when restricted to
acyclic 1-safe structure-changing workflow nets with at most 2 tokens in every reachable state.
Selected Revised Papers from GCM 2014 16 / 20
ECEASST
Proof. By reduction from the emptiness problem for the intersection of two context-free lan-
guages. Let G1 = (V1,T,P1,S1) and G2 = (V2,T,P2,S2) be two context-free grammars in Greibach
normal form. We assume their non-terminal alphabets disjoint w.l.o.g. (V1 ∩V2 = /0).
To distinguish the words from the two grammars, we introduce a second terminal alphabet
T̂ :={â | a ∈ T} and a function dup(ε) := ε,dup(aw) := aâ ·dup(w).
We construct the structure-changing workflow net S(G1,G2) = (N,R1 ∪R2). N is as shown:
S2
s S1 e
For every production X → aX1...Xn in G1, we add a rule replacing a transition labelled X
with a linear sequence of transitions labelled a,X1,...,Xn to R1. For productions in G2, we do
the same, but replace the terminal label a with â and add the rules to R2. Disjointness of non-
terminal alphabets ensures that the rules in Ri are only applicable in the subnet resulting from Si
(for i ∈{1,2}). The words accepted in these subnets hence correspond to those generated by the
respective grammars. Let L be s{aâ | a ∈ T}∗e with {s,e} 6⊆ T . Now,
L(G1)∩L(G2) = /0 ⇔ F(S(G1,G2))⊆ L
L(G1)∩L(G2) = /0 ⇔ F(S(G1,G2))∩L = /0
∃w ∈L(G1)∩L(G2) ⇔ ∃w ∈F(S(G1,G2))∩L
⇒: if w is generated from both G1 and G2, then a derivation for it exists in both grammars. Since
context-free derivations in G1 and G2 can be translated into sequences of rule applications in the
corresponding subnet, there obviously is a reachable net in S(G1,G2) able to accept s·dup(w)e ∈
L.
⇐: All words in L can be written as sdup(w)e for some w ∈ T∗. To also be accepted by
S(G1,G2), there must be a derivation (ξ ,σ) with f (λ (ξ )) = s·dup(w)e. Now, w ∈L(G1), since
w = f (λ (ξ )) and the subsequence of R1-steps in ξ directly corresponds to a derivation in G1. A
symmetric argument holds for G2.
S(G1,G2) is a 1-safe structure-changing workflow net easily seen to have as reachable states
only acyclic nets marked with one or two tokens.
4 Related Work
Petri nets can be extended with structure changes via graph replacement rules, as in [MGH11].
Graph grammars [EEPT06] define replacement steps according to rules that serve to reconfig-
ure the Petri net dynamically and can be mixed with transition firings. Their work, and ours,
is closely related to graph grammars and results from graph replacement such as local Church-
Rosser and concurrency theorems can be adapted, see [EHP+07, MGH11]. We have concen-
trated on Petri net specific aspects such as reachability of markings in this paper. [BCKK04]
uses similar concepts for model checking graph grammars.
Further noteworthy work includes the box calculus [BDH92], recursive Petri nets [HP99], re-
configurable nets [BLO03], open nets [BCE+07]. These extensions are much more general and
17 / 20 Volume 71 (2015)
Analysis of Petri Nets with Context-Free Structure Changes
allow structure changes beyond dynamic transition refinement. Safe nets-in-nets [KH10] and
Hypernets [Mas11] represent a different kind of dynamic structure. With unbounded nesting of
net tokens, it is possible to simulate a 2-counter machine with zero-tests. The notion of activated
transitions and transition refinement are also found in [KR07]. Finally, in [vSV03], a notion of
refinement for workflow nets was investigated, but with different aims.
5 Conclusion
We have introduced structure-changing Petri nets with context-free transition replacement rules
based on graph replacement, and studied a number of decision problems that arose. Suitably
translated, our results apply to many formalisms that add structure changes to Petri nets.
An overview of the results follows. The columns stand for structure-changing Petri nets (scpn)
and structure-changing workflow nets (general, 1-safe, acyclic 1-safe scwn) respectively, “yes”
means decidable, “no” undecidable, “?” unknown):
scpn scwn 1-safe acyclic 1-safe
concrete reachability yes yes yes yes Proposition 2
abstract reachability ? ? yes yes Proposition 3
firing word problem ? ? yes yes Proposition 1
regular specification no no no no Proposition 7
The firing word problem turned out to be nontrivial. Proposition 7 places severe limitations
on the algorithmic analysis of structure-changing Petri nets. Even for systems with a simple
structure and a globally bounded token number, language containment questions are undecidable
due to the possibility of imposing synchronisation on concurrent context-free processes.
Further Topics
(1) Structure-changing nets with arbitrary replacement rules hardly seem to offer promising
analysis methods. It seems most fruitful to investigate classes of nets that behave sufficiently
like the “simple” ones presented here, and on the other hand to apply general analysis methods
known from graph replacement.
(2) Decidable problems for relatively simple subclasses of structure-changing Petri nets and
case studies to evaluate which features are still lacking in order to model real dynamic workflows.
We suspect that not all restrictions are necessary and are working to determine the decidability
boundary more accurately.
(3) In the spirit of system correctness under adverse conditions, would be to turn the reacha-
bility problems into game problems by considering some nontrivial scheduling between the two
kinds of steps, and universal quantification for replacement steps: until now, rule application and
firing cooperate.
Acknowledgements: We would like to thank Annegret Habel and several other SCARE mem-
bers for constructive discussions, and the reviewers for their very constructive remarks.
Selected Revised Papers from GCM 2014 18 / 20
ECEASST
Bibliography
[BCE+07] P. Baldan, A. Corradini, H. Ehrig, R. Heckel, B. König. Bisimilarity and Behaviour-
Preserving Reconfigurations of Open Petri Nets. In Algebra and Coalgebra in Com-
puter Science. LNCS 4624, pp. 126–142. 2007.
[BCKK04] P. Baldan, A. Corradini, B. König, B. König. Verifying a Behavioural Logic for
Graph Transformation Systems. ENTCS 104:5–24, 2004.
[BDH92] E. Best, R. Devillers, J. Hall. The box calculus: A new causal algebra with multi-
label communication. In Advances in Petri Nets. LNCS 609, pp. 21–69. 1992.
[BLO03] E. Badouel, M. Llorens, J. Oliver. Modeling concurrent systems: Reconfigurable
nets. In Proceedings of Int. Conf. on Parallel and Distributed Processing Techniques
and Applications. CSREA Press, 2003.
[Cor95] A. Corradini. Concurrent Computing: from Petri Nets to Graph Grammars.
ENTCS 2, pp. 56–70. Elsevier, 1995.
[DR98] J. Desel, W. Reisig. Place/transition Petri nets. In Lectures on Petri Nets I: Basic
Models. LNCS 1491, pp. 122–173. 1998.
[EEPT06] H. Ehrig, K. Ehrig, U. Prange, G. Taentzer. Fundamentals of Algebraic Graph Trans-
formation. Monographs in Theoretical Computer Science. Springer, 2006.
[EHP+07] H. Ehrig, K. Hoffmann, J. Padberg, U. Prange, C. Ermel. Concurrency in Reconfig-
urable P/T Systems: Independence of net transformations and token firing in recon-
figurable P/T systems. In Proceedings ICATPN. Pp. 104–123. 2007.
[Esp96] J. Esparza. Decidability and Complexity of Petri Net Problems - An Introduction. In
Lectures on Petri Nets I: Basic Models. LNCS 1491, pp. 374–428. 1996.
[Hab92] A. Habel. Hyperedge Replacement: Grammars and Languages. LNCS 643. 1992.
[HP99] S. Haddad, D. Poitrenaud. Theoretical Aspects of Recursive Petri Nets. In Applica-
tion and Theory of Petri Nets. LNCS 1639, pp. 228–247. 1999.
[KH10] M. Köhler-Bußmeier, F. Heitmann. Safeness for object nets. Fundamenta Informat-
icae 101(1):29–43, 2010.
[KR07] M. Köhler, H. Rölke. Web Service Orchestration with Super-Dual Object Nets. In
ICATPN. LNCS 4546, pp. 263–280. 2007.
[Kre81] H.-J. Kreowski. A comparison between Petri-nets and graph grammars. In Graph-
theoretic Concepts in Computer Science. LNCS 100, pp. 306–317. 1981.
[Mas11] M. Mascheroni. Hypernets: a class of hierarchical Petri nets. PhD thesis, Università
degli Studi di Milano-Bicocca, 2011.
19 / 20 Volume 71 (2015)
Analysis of Petri Nets with Context-Free Structure Changes
[MGH11] T. Modica, K. Gabriel, K. Hoffmann. Formalization of Petri Nets with Individual To-
kens as Basis for DPO Net Transformations. In Proceedings PNGT 2010. Electronic
Communications of the EASST 40. 2011.
[PW02] L. Priese, H. Wimmel. Petri-Netze. Springer, 2002.
[van97] W. M. P. van der Aalst. Verification of workflow nets. In Applications and Theory of
Petri Nets. LNCS 1248, pp. 407–426. 1997.
[van01] W. M. P. van der Aalst. Exterminating the Dynamic Change Bug: A Concrete
Approach to Support Workflow Change. Information Sys. Frontiers 3(3):297–317,
2001.
[vSV03] K. van Hee, N. Sidorova, M. Voorhoeve. Soundness and Separability of Workflow
Nets in the Stepwise Refinement Approach. In Applications and Theory of Petri
Nets. LNCS 2679, pp. 337–356. 2003.
[WRR08] B. Weber, M. Reichert, S. Rinderle-Ma. Change Patterns and Change Support Fea-
tures - Enhancing Flexibility in Process-Aware Information Systems. Data and
Knowledge Engineering 66(3):438–466, 2008.
Selected Revised Papers from GCM 2014 20 / 20
Introduction
Structure-Changing Petri nets
Analysis of Structure-Changing Workflow Nets
Firing Word Problem
Reachability Problems
Containment Problems
Related Work
Conclusion