=Paper=
{{Paper
|id=Vol-3167/paper6
|storemode=property
|title=Deadlocks and Livelocks in Resource Constrained Workflow Nets
|pdfUrl=https://ceur-ws.org/Vol-3167/paper6.pdf
|volume=Vol-3167
|authors=Gabriel Juhás,Ana Juhásova,Tomáš Kováčik
|dblpUrl=https://dblp.org/rec/conf/apn/JuhasJK22
}}
==Deadlocks and Livelocks in Resource Constrained Workflow Nets==
https://ceur-ws.org/Vol-3167/paper6.pdf
Deadlocks and livelocks in resource constrained
workflow nets
Gabriel Juhás1 , Ana Juhásová2 and Tomáš Kováčik1
1
Faculty of Electrical Engineering and Information Technology, Slovak University of Technology in Bratislava,
Ilkovičova 3, 812 19 Bratislava, Slovakia
2
BIREGAL s.r.o. Klincová 37/B, 821 08 Bratislava, Slovakia
Abstract
The paper is presenting a method for detection of locks (both deadlocks and livelocks) in discrete event
systems with shared resources and multiple instances modeled by resource constrained workflow nets.
We consider that multiple instances with determined initial state and a correct final state are running
in workflow nets. We consider workflow processes, in which instances can share several types of
resources, with instances neither creating nor destroying shared resources. It means, that instances
can use resources but the used resources are returned at the latest by the correct finish of the instance.
Such resources are said to be durable. Examples of durable resources include resources of information
systems, such as memory and processors or employees in roles in an organizational structure. We
consider processes, which have enough resources to execute a single instance, such processes are said to
be sound. A lock is a state of the process, where several instances are running but because of the lack
of shared resources not all running instances can finish properly. The main result of the paper is the
theorem stating that in sound workflow processes with several types of shared durable resources for
given initial number of resources and an arbitrary unbounded number of running instances it is enough
to test locks for a finite bounded number of instances, with the upper bound indicated.
Keywords
Petri net, Deadlock, Livelock, Resource constrained workflow net
1. Introduction
In [1] authors work with workflow processes with instances, in which instances share common
resources. The processes are modeled by resource constrained workflow nets, where shared
resources are modeled by so called static places. Except shared resources, instances are inde-
pendent. Shared resources considered in [1] are durable, i.e. the resources are neither created
nor destroyed by instances. Resources in information systems, such as memory, processors,
i/o ports are typical examples of durable resources. Similarly, employees in particular roles
considered by workflow processes can represent an example of durable resources.
The main problem solved in [1] is the problem of correct finish of all instances of a workflow
process with shared durable resources. The problem is solved for processes with one type of
durable resources. The method from [1] decides whether there is a number of shared resources
The Workshop Algorithms & Theories for the Analysis of Event Data (ATAED 2022): A Satellite Event of the 43rd
International Conference on Application and Theory of Petri Nets and Concurrency, June 19 - 24, 2022, Bergen, Norway
$ gabriel.juhas@stuba.sk (G. Juhás); ana.juhasova@biregal.sk (A. Juhásová); tomas_kovacik@stuba.sk (T. Kováčik)
0000-0001-8302-5112 (G. Juhás); 0000-0003-3157-8609 (T. Kováčik)
© 2022 Copyright for this paper by its authors. Use permitted under Creative Commons License Attribution 4.0 International (CC BY 4.0).
CEUR Workshop Proceedings (CEUR-WS.org)
such that for this number of resources and any greater number of resources any number of
instances can be correctly finished. If the answer is true, then the workflow process is according
to [1] called sound.
In [2] authors solve the soundness problem for several subclasses of resource constrained
workflow nets. In [3] four necessary conditions of soundness of resource constrained workflow
nets based on structural analysis are presented.
In [4, 5] we defined a technique based on a constructor and a runtime net to detect instance
deadlocks of resource constrained workflow nets (called workflow nets with static places) for
a fixed number of durable resources and an arbitrary number of instances. However, method
from [4] did not work for livelocks.
In [6, 7] authors using a technique based on constructor and using a transformed net from
[4] (called production net in [6, 7]) proved that the soundness problem for resource constrained
workflow nets which are sound for one instance, is decidable even for the case where resources
are not durable. The proof is based on the reduction to the home space problem of Petri nets,
which was proved to be decidable in [8]. At the same time, the papers [6, 7] prove that in general,
i.e. if the soundness for one instance is not required and the resources does not necessarily need
to be durable, the problem of soundness in resource constrained workflow nets is undecidable.
In [9] authors using the constructor from [4] proved, that if the nets are sound for one case, then
the soundness problem is decidable even if the instances are not independent (the investigated
net corresponding to our runtime net is not serializable). For more about serializability see
e.g. [10, 11]. Paper [9] extends an unsuccessful attempt to prove decidability of soundness for
resource constrained workflow nets presented in [12]. In the proof of results from [9] authors
again used reduction to home space problem of Petri nets. As it is written at the end of the
paper [9], soundness of resource constrained workflow nets is decidable, but up to now there
is no effective algorithm, because the algorithm proposed in [9] requires the test of general
reachability in possibly unbounded Petri nets [13, 14, 15, 16, 17]. The similar argument can be
found at the end of original paper solving home space problem [8].
There are workflow processes, which for some fixed initial number of shared resources can
correctly finish any number of instances, but for some greater number of shared resources
the same process cannot finish for some number of instances running in parallel. Thus, such
processes are not sound according to the definition of [1, 9]. An example of such a not sound
process is on Figure 1, which can finish any number of instances for the given number of shared
resources in static places free key, free memory, free processor. However, adding any number of
resources to the static place free key will cause that the process may deadlock for the number
of instances greater than 3. In general, once the number of resources in the place free key is
smaller than the sum of free resources in places free memory and free processor, then the process
will have no deadlock, otherwise it will contain a deadlock for any number of instances greater
of equal the sum of shared resources in places free memory and free processor.
In this work we will prove, that in order to decide, whether the workflow process with
arbitrary finite number of resource types and arbitrary unbounded number of instances with
fixed initial number of durable shared resources will contain a lock (i.e. a deadlock or a liveclock),
it suffices to check the existence of locks for bounded number of instances. We also will show
how to compute such upper bounds.
free key
key
free memory
waiting for memory memory allocation memory allocated memory memory to dispose memory dispose memory disposed
in task begin computation begin computation computation end task end out
waiting for processor processor allocation processor allocated processor processor to dispose processor dispose processor disposed
free processor
Figure 1: A marked remembering workflow net with static places, modeling allocation of memory
units and processors to computing tasks with possibility to constrain the number of tasks, which can be
executed in parallel.
2. Labelled transition systems
As a basic model of process behaviour we will use labelled transition systems [18, 19].
Definition 1 (Labelled transition system).
A labelled transition system is an ordered triple (𝑆, 𝐸, −→), where
• 𝑆 is a set of states,
• 𝐸 is a set of events,
• −→⊆ 𝑆 × 𝐸 × 𝑆 is a transition relation.
𝑒
The fact, that (𝑠, 𝑒, 𝑠′ ) belongs to −→ is referred as 𝑠 −→ 𝑠′ .
We will use labelled transition systems that have determined an initial state from which any
other state is reachable.
To define reachability of states, we first define the notion of a sequence and the notion of an
index set.
Definition 2 (Index set).
Index set I is a subset of positive integers satisfying: if a positive integer 𝑖 belongs to the index set I,
then any positive integer smaller than 𝑖 belongs to the index set I. If I is a finite nonempty set with
the maximum 𝑛, then the number 𝑛 is referred as 𝑚𝑎𝑥I . If I is the empty set, then 𝑚𝑎𝑥I = 0.
Definition 3 (Sequence).
Let I be an index set and 𝑆 be a set. Then a function 𝛼 : I → 𝑆 associating an element 𝛼(𝑖) from
the set 𝑆 to each index 𝑖 from the index set I, is called a sequence of elements from the set 𝑆. If I is
a finite set, then we say that 𝛼 is finite sequence with length 𝑚𝑎𝑥I . Especially, if I is the empty set,
then we say that 𝛼 is the empty sequence. If I is equal to the set of all positive integers, then we say
that 𝛼 is an infinite sequence.
For illustration, consider a sequence of characters 𝛼 = 𝑎𝑏𝑏𝑎 from the set of characters
𝑆 = {𝑎, 𝑏}. Intuitively, we understand that it is a finite sequence with length 4. In accordance
with Definition 2 we use the index set I = {1, 2, 3, 4}. The sequences 𝛼 is formalized as follows:
𝛼(1) = 𝑎, 𝛼(2) = 𝑏, 𝛼(3) = 𝑏 a 𝛼(4) = 𝑎, i.e. the first element of the sequence 𝛼 is character
𝑎, the second element is 𝑏, the third element is again 𝑏 a the fourth element is character 𝑎.
Definition 4 (Occurrence sequence, reachability).
Let (𝑆, 𝐸, −→) be a labelled transition systems. Let 𝑠 ∈ 𝑆 be a state and let 𝜖 : I → 𝐸 be a finite
sequence of events. Sequence 𝜖 can occur in state 𝑠 iff there exists a function 𝜎 : I ∪ {0} → 𝑆
𝜖(𝑖)
such that 𝜎(0) = 𝑠 and for each positive integer 𝑖 ∈ I: 𝜎(𝑖 − 1) −→ 𝜎(𝑖). The occurrence of the
sequence 𝜖 in the state 𝑠 leads to the state 𝜎(𝑚𝑎𝑥I ).
A state 𝑠′ ∈ 𝑆 is reachable from a state 𝑠 iff there is an occurrence sequence 𝜖, which leads from
𝑠 to 𝑠′ .
The fact that a finite sequence 𝜖 can occur in 𝑠 and its occurrence leads to 𝑠′ is referred as
𝜖
𝑠 −→ 𝑠′ .
Remember, that according to Definition 4 for any state 𝑠 we have: the empty sequence can
occur in 𝑠 and its occurrence leads to 𝑠, i.e. 𝑠 is self-reachable by occurrence of the empty
sequence.
Definition 5 (Pointed labelled transition system).
A pointed labelled transitions system is an ordered quadruple (𝑆, 𝐸, −→, 𝑞), where (𝑆, 𝐸, −→) is
a labelled transition system and 𝑞 ∈ 𝑆 is its initial state, while for each state 𝑠 ∈ 𝑆 there holds
that 𝑠 is reachable from 𝑞.
3. Petri nets
In this section we briefly introduce the basic definition of Petri nets [20, 21, 22, 23, 24, 25].
Definition 6 (Petri net).
A Petri net is an ordered quadruple (𝑃, 𝑇, 𝐼, 𝑂), where:
• 𝑃 is a set of places
• 𝑇 is a set of transitions
• 𝑃 ∩𝑇 =∅
• 𝐼 : 𝑃 × 𝑇 → N is an input function, where N stands for the set of non-negative integers.
• 𝑂 : 𝑃 × 𝑇 → N is an output function.
A state of a Petri net is given by a marking.
Definition 7 (Marking).
Let 𝑃 𝑁 = (𝑃, 𝑇, 𝐼, 𝑂) be a Petri net. A function 𝑚 : 𝑃 → N attaching a non-negative integer to
each place is called a marking of Petri net 𝑃 𝑁 . The value 𝑚(𝑝) defines the number∑︀of tokens in a
place 𝑝 ∈ 𝑃 . A marking will be written in form of a sum of marking of places, i.e. 𝑝∈𝑃 𝑚(𝑝)𝑝.
The set of places, for which 𝑚(𝑝) is greater than zero, is called the support of marking 𝑚 and is
denoted by 𝑠𝑢𝑝(𝑚), formally for each 𝑝 ∈ 𝑃 there holds that 𝑝 belongs to 𝑠𝑢𝑝(𝑚) iff 𝑚(𝑝) > 0.
Places can be understood as types of tokens. As an example, if a set of places is given by
𝑃 = {𝑎, 𝑏, 𝑐}, we have three types of tokens, tokens of type 𝑎, tokens of type 𝑏 and tokens of
type 𝑐. Consider a marking 𝑚 : 𝑃 → N such that 𝑚(𝑎) = 2, 𝑚(𝑏) = 0 and finally 𝑚(𝑐) = 1. It
means, that the marking expresses a state with two tokens of type 𝑎, no tokens of type 𝑏 and
one token of type 𝑐, which will be expressed by expression 2𝑎 + 0𝑏 + 1𝑐, or more simply by
expression
∑︀ 2𝑎 + 𝑐 (i.e. two tokens of type 𝑎 and a token of type 𝑐), generally by expression
𝑝∈𝑃 𝑚(𝑝)𝑝.
The fact, that for markings 𝑚 and 𝑚′ there holds 𝑚(𝑝) ≤ 𝑚′ (𝑝) for each 𝑝 ∈ 𝑃 , is denoted
by 𝑚 ≤ 𝑚′ . Further, 𝑚 < 𝑚′ , respectively 𝑚′ > 𝑚 denotes the fact that 𝑚 ≤ 𝑚′ and there
exists 𝑝 ∈ 𝑃 such that 𝑚(𝑝) < 𝑚′ (𝑝). If 𝑚 < 𝑚′ , we say that 𝑚 is smaller than 𝑚′ , and 𝑚′ is
greater than 𝑚, respectively. The sum of two markings 𝑚 a 𝑚′ is marking 𝑚 + 𝑚′ such that
(𝑚 + 𝑚′ )(𝑝) = 𝑚(𝑝) + 𝑚′ (𝑝) for each 𝑝 ∈ 𝑃 . If 𝑚 ≤ 𝑚′ , then the difference of markings 𝑚′ a
𝑚 is given by marking 𝑚′ − 𝑚 such that (𝑚′ − 𝑚)(𝑝) = 𝑚′ (𝑝) − 𝑚(𝑝) for each 𝑝 ∈ 𝑃 .
Dynamics of a Petri net is given by firing of transitions.
Definition 8 (Transition firing).
Let 𝑃 𝑁 = (𝑃, 𝑇, 𝐼, 𝑂) be a Petri net. Let 𝑚 : 𝑃 → N be a marking and 𝑡 ∈ 𝑇 be a transition
of the net 𝑃 𝑁 . Transition 𝑡 is enabled to fire in marking 𝑚 iff for each 𝑝 ∈ 𝑃 there holds:
𝑚(𝑝) ≥ 𝐼(𝑝, 𝑡).
If transition 𝑡 is enabled to fire in marking 𝑚, then its firing in 𝑚 leads to marking 𝑚′ such that
for each 𝑝 ∈ 𝑃 there holds: 𝑚′ (𝑝) = 𝑚(𝑝) − 𝐼(𝑝, 𝑡) + 𝑂(𝑝, 𝑡).
We will consider that a Petri net has initial marking. A Petri net together with an initial
marking will be referred as marked Petri net.
Definition 9 (Marked Petri net).
A marked Petri net is an ordered quintuple 𝑀 𝑃 𝑁 = (𝑃, 𝑇, 𝐼, 𝑂, 𝑚0 ), where 𝑃 𝑁 = (𝑃, 𝑇, 𝐼, 𝑂)
is a Petri net and 𝑚0 is a marking of 𝑃 𝑁 called initial marking.
Graphically places are depicted as circles, markings of places by number of tokens inside
of places, transitions are depicted as squares. Enabled transitions are filled (by green color).
Non-zero value of input function 𝐼(𝑝, 𝑡) is expressed by an arrow from place 𝑝 to transition
𝑡, while the value greater than one is written by the arc. Non-zero value of output function
𝑂(𝑝, 𝑡), is expressed by an arrow from transition 𝑡 to place 𝑝, while the value greater than one is
written by the arc. These non-zero values will be referred as weights of arcs. All Petri nets used
in this work where modelled in an online Petri net editor, accessible at www.petriflow.com.
Petri nets defines a labelled transition system in a natural way by firing enabled transitions.
Definition 10 (Reachability graph of a Petri net).
Let 𝑃 𝑁 = (𝑃, 𝑇, 𝐼, 𝑂) be a Petri net. A labelled transition system (𝑆, 𝐸, −→), where
• 𝑆 is the set of all markings, i.e. the set of all functions from 𝑃 to non-negative integers N,
• 𝐸 = 𝑇,
𝑡
• 𝑚 −→ 𝑚′ iff transition 𝑡 is enabled to fire in marking 𝑚 and firing of 𝑡 in 𝑚 leads to
marking 𝑚′ ,
is called reachability graph of Petri net 𝑃 𝑁 .
We also define reachability graphs of marked Petri nets.
Definition 11. (Reachability graph of a marked Petri Net)
Let 𝑀 𝑃 𝑁 = (𝑃, 𝑇, 𝐼, 𝑂, 𝑚0 ) be a marked Petri net. Let (𝑆, 𝐸, −→) be reachability graph
of Petri net 𝑃 𝑁 = (𝑃, 𝑇, 𝐼, 𝑂). Let [𝑚0 ⟩ denote the set of all markings reachable from 𝑚0
in reachability graph of Petri net 𝑃 𝑁 . Then pointed labelled transition system ([𝑚0 ⟩, 𝐸, −→
∩([𝑚0 ⟩ × 𝐸 × [𝑚0 ⟩), 𝑚0 ) is called reachability graph of marked Petri net 𝑀 𝑃 𝑁 . If sequence
𝜖 can occur in 𝑚 and its occurrence in 𝑚 leads to 𝑚′ in the reachability graph of 𝑀 𝑃 𝑁 , then
we say that sequence 𝜖 is enabled to fire in marking 𝑚 in net 𝑀 𝑃 𝑁 and its firing in 𝑚 leads to
the marking 𝑚′ in net 𝑀 𝑃 𝑁 . We also say that marking 𝑚′ is reachable from marking 𝑚 in the
marked Petri net 𝑀 𝑃 𝑁 .
Definition 12 (Boundedness).
A marked Petri net 𝑀 𝑃 𝑁 = (𝑃, 𝑇, 𝐼, 𝑂, 𝑚0 ) is bounded iff there exists a function 𝑏 : 𝑃 → N,
such that for each marking 𝑚 reachable from 𝑚0 in 𝑀 𝑃 𝑁 there holds: 𝑚 ≤ 𝑏. Function 𝑏 is
called the bound of net 𝑀 𝑃 𝑁 .
In the case that a marked Petri net has finitely many places is the boundedness equivalent
with the finiteness of the number of reachable markings. For more results on boundedness see
e.g. [26, 27, 28].
Corollary 1. A marked Petri net 𝑀 𝑃 𝑁 = (𝑃, 𝑇, 𝐼, 𝑂, 𝑚0 ) with finite set of places is bounded
iff the number of markings reachable from 𝑚0 in 𝑀 𝑃 𝑁 is finite.
4. Workflow nets
We focus on processes, where instances has a unique start and unique correct finish. In literature,
such systems are modeled by workflow nets [29, 30, 31, 32].
Definition 13 (Workflow net).
A workflow net is a Petri net 𝑃 𝑁 = (𝑃, 𝑇, 𝐼, 𝑂) with finite number of places and transitions in
which there exists a unique place 𝑖𝑛 ∈ 𝑃 and a unique place 𝑜𝑢𝑡 ∈ 𝑃 such that
• for each 𝑡 ∈ 𝑇 there holds 𝑂(𝑖𝑛, 𝑡) = 0 and there exists such 𝑡 ∈ 𝑇 that 𝐼(𝑖𝑛, 𝑡) ̸= 0,
• for each 𝑡 ∈ 𝑇 there holds 𝐼(𝑜𝑢𝑡, 𝑡) = 0 and there exists such 𝑡 ∈ 𝑇 that 𝑂(𝑜𝑢𝑡, 𝑡) ̸= 0.
Place 𝑖𝑛 is called input place of workflow net 𝑃 𝑁 and place 𝑜𝑢𝑡 is called output place of workflow
net 𝑃 𝑁 .
A marked workflow net is a workflow net with a special initial marking, in which only the
input place is marked.
Definition 14 (Marked workflow net).
A marked workflow net is a marked Petri net 𝑀 𝑃 𝑁 = (𝑃, 𝑇, 𝐼, 𝑂, 𝑚0 ), where 𝑃 𝑁 = (𝑃, 𝑇, 𝐼, 𝑂)
is a workflow net and 𝑚0 = 𝑖𝑛, i.e. 𝑚0 (𝑖𝑛) = 1 and 𝑚0 (𝑝) = 0 for each 𝑝 ∈ 𝑃 different from 𝑖𝑛.
5. Petri nets and workflow nets with static places
Processes with instances and shared resources will be modeled by Petri nets with static places
[4, 5]. Static places inspired by static variables in Java will model shared resources. Petri nets
with static places were inspired by workflow nets with static places originally defined in papers
[33, 1, 3] under the name resource constrained workflow nets.
Definition 15 (Petri net with static places).
Petri net with static places is a quintuple 𝑃 𝑁 𝑆 = (𝐷, 𝑆, 𝑇, 𝐼, 𝑂), where
• 𝐷 is a set of dynamic places
• 𝑆 is a set of static places
• 𝐷∩𝑆 =∅
• 𝑃 𝑁 = (𝑃 = 𝐷 ∪ 𝑆, 𝑇, 𝐼, 𝑂) is a Petri net.
Static places will be depicted by dashed circles.
Definition 16. (Marked Petri net with static places)
Marked Petri net with static places is a sextuple 𝑀 𝑃 𝑁 𝑆 = (𝐷, 𝑆, 𝑇, 𝐼, 𝑂, 𝑚0 ), where
• 𝑃 𝑁 𝑆 = (𝐷, 𝑆, 𝑇, 𝐼, 𝑂) is a Petri net with static places
• 𝑀 𝑃 𝑁 = (𝑃 = 𝐷 ∪ 𝑆, 𝑇, 𝐼, 𝑂, 𝑚0 ) is marked Petri net.
We say that a transition is enabled to fire in a marked Petri net with static places 𝑀 𝑃 𝑁 𝑆 if it is
enabled to fire in marked Petri net 𝑀 𝑃 𝑁 . A reachability graph of a marked Petri net with static
places 𝑀 𝑃 𝑁 𝑆 is the reachability graph of marked Petri net 𝑀 𝑃 𝑁 . All notion defined for marked
Petri net 𝑀 𝑃 𝑁 will analogously used for marked Petri net with static places 𝑀 𝑃 𝑁 𝑆.
Definition 17. (Workflow net with static places/resource constrained workflow net) A
workflow net with static places, also called resource constrained workflow net, is a Petri net with
static places 𝑊 = (𝐷, 𝑆, 𝑇, 𝐼, 𝑂), where 𝑃 𝑁 = (𝑃 = 𝐷 ∪ 𝑆, 𝑇, 𝐼, 𝑂) is a workflow net such
that 𝑖𝑛 ∈ 𝐷 and 𝑜𝑢𝑡 ∈ 𝐷.
Initial marking of a marked workflow net with static places contains one token in the input
place, no tokens in dynamic places different from the input place and any number of tokens
representing shared resources in static places.
Definition 18. (Marked workflow net with static places)
A marked workflow net with static places is a sextuple 𝑀 𝑊 = (𝐷, 𝑆, 𝑇, 𝐼, 𝑂, 𝑚0 ), where
• 𝑊 = (𝐷, 𝑆, 𝑇, 𝐼, 𝑂) is a workflow net with static places
• 𝑚0 is initial marking such that 𝑚(𝑖𝑛) = 1 and 𝑚(𝑑) = 0 for each dynamic place 𝑑 ∈ 𝐷,
which is different from 𝑖𝑛.
In comparison with [33, 1, 3] we formalize durable resources via (weak) complementary
places [34] of static places.
Definition 19. (Remembering workflow net with static places)
Let 𝑊 = (𝐷, 𝑆, 𝑇, 𝐼, 𝑂) be such workflow net with static places, that for each places 𝑠 ∈ 𝑆 there
exists a unique (weak)complementary place 𝑑𝑠 ∈ 𝐷 different from 𝑖𝑛 and 𝑜𝑢𝑡, which for each
𝑡 ∈ 𝑇 satisfies 𝐼(𝑑𝑠 , 𝑡) − 𝑂(𝑑𝑠 , 𝑡) = 𝑂(𝑠, 𝑡) − 𝐼(𝑠, 𝑡). Workflow net 𝑊 is called remembering
workflow net with static places. The set of all complementary places of static places is denoted by
𝐷𝑆 .
The equality 𝐼(𝑑𝑠 , 𝑡) − 𝑂(𝑑𝑠 , 𝑡) = 𝑂(𝑠, 𝑡) − 𝐼(𝑠, 𝑡) in a marked remembering workflow net
with static places implies that in case that 𝑂(𝑠, 𝑡)−𝐼(𝑠, 𝑡) = 0, we also have 𝐼(𝑑𝑠 , 𝑡)−𝑂(𝑑𝑠 , 𝑡) =
0. It means, that firing any transition may create a token in a complementary place 𝑑𝑠 of a
static place 𝑠 iff it consumes a token from the static place 𝑠. Because in any initial marking
the complementary place 𝑑𝑠 is empty, we get that the sum of tokens in a static place 𝑠 and its
complementary place 𝑑𝑠 equals 𝑚0 (𝑠).
Corollary 2. Let 𝑀 𝑊 = (𝐷, 𝑆, 𝑇, 𝐼, 𝑂, 𝑚0 ) be a marked remembering workflow net with static
places. Let 𝑠 ∈ 𝑆 be a static place and let 𝑑𝑠 ∈ 𝐷𝑆 be its complementary place. Then for each
marking 𝑚 reachable from 𝑚0 there holds: 𝑚(𝑠) + 𝑚(𝑑𝑠 ) = 𝑚0 (𝑠) and therefore 𝑚(𝑠) ≤ 𝑚0 (𝑠).
1-soundness of a marked workflow net with static places is defined analogously to soundness
of workflow nets in [32] as the ability to finish correctly a single instance.
Definition 20. (Final marking of marked workflow net with static places)
Let 𝑀 𝑊 = (𝐷, 𝑆, 𝑇, 𝐼, 𝑂, 𝑚0 ) be a marked workflow net with static places. A marking 𝑚𝑓
of net 𝑀 𝑊 reachable from 𝑚0 is called a final marking of 𝑀 𝑊 iff there holds: 𝑚𝑓 (𝑜𝑢𝑡) = 1,
𝑚𝑓 (𝑑) = 0 for each 𝑑 ∈ 𝐷 different from 𝑜𝑢𝑡.
Definition 21. (1-soundness of marked workflow net with static places)
Let 𝑀 𝑊 = (𝐷, 𝑆, 𝑇, 𝐼, 𝑂, 𝑚0 ) be a marked workflow net with static places and let 𝑜𝑢𝑡 ∈ 𝑃
denote the output place. Marked workflow net with static places 𝑀 𝑊 is 1-sound iff for each
marking 𝑚 reachable from 𝑚0 there holds:
• there exists a final marking 𝑚𝑓 of net 𝑀 𝑊 , which is reachable from marking 𝑚,
• if 𝑚(𝑜𝑢𝑡) ≥ 1 then 𝑚 is a final marking of net 𝑀 𝑊 .
For marked remembering workflow nets with static places we have:
Corollary 3. Let 𝑀 𝑊 = (𝐷, 𝑆, 𝑇, 𝐼, 𝑂, 𝑚0 ) be a marked remembering workflow net with static
places and let 𝑚𝑓 be a final marking of 𝑀 𝑊 . Then 𝑚𝑓 (𝑠) = 𝑚0 (𝑠) for each 𝑠 ∈ 𝑆 and therefore
𝑚𝑓 is a unique final marking of 𝑀 𝑊 .
For 1-sound marked remembering workflow nets with static places we get:
Lemma 1. If a marked remembering workflow net with static places is 1-sound then the number
of its reachable markings is finite, i.e. the net is bounded.
Proof. Let the number of markings reachable from 𝑚0 is not finite. According to Dickson’s
lemma [35], let 𝑚 and 𝑚′ are markings reachable from 𝑚0 such that 𝑚 < 𝑚′ . From definition
of 1-soundness we get that 𝑚′ (𝑜𝑢𝑡) = 1 or 𝑚′ (𝑜𝑢𝑡) = 0 and 𝑚(𝑜𝑢𝑡) = 1 or 𝑚(𝑜𝑢𝑡) = 0.
Because 𝑚 < 𝑚′ , we also get 𝑚(𝑠) ≤ 𝑚′ (𝑠) for each 𝑠 ∈ 𝑆.
• The combination 𝑚′ (𝑜𝑢𝑡) = 1 and 𝑚(𝑜𝑢𝑡) = 1 means that 𝑚′ = 𝑚𝑓 = 𝑚, what
contradicts that 𝑚 < 𝑚′ .
• The combination 𝑚′ (𝑜𝑢𝑡) = 0 and 𝑚(𝑜𝑢𝑡) = 1 is in contradiction with 𝑚 < 𝑚′ .
• The combination 𝑚′ (𝑜𝑢𝑡) = 1 and 𝑚(𝑜𝑢𝑡) = 0 means that 𝑚′ = 𝑚𝑓 . Assuming that
𝑚𝑓 > 𝑚 we get 𝑚(𝑑) = 0 for each 𝑑 ∈ 𝐷). From first item of 1-soundness we further
get that 𝑚𝑓 is reachable from 𝑚 by firing of a sequence of transitions. From definition of
transition firing it is clear that whenever a sequence is enabled to fire from a marking, it
is enabled to fire from any greater marking, and therefore also from 𝑚𝑓 . Because firing
of that sequence leads from 𝑚 to 𝑚𝑓 , its firing from 𝑚𝑓 leads to the marking 𝑚′′ such
that 𝑚′′ (𝑜𝑢𝑡) = 𝑚𝑓 (𝑜𝑢𝑡) + (𝑚𝑓 (𝑜𝑢𝑡) − 𝑚(𝑜𝑢𝑡)), i.e. 𝑚′′ (𝑜𝑢𝑡) = 1 + (1 − 0)) = 2,
what contradicts with the second item of 1-soundness implying that for each marking
𝑚′′ reachable from 𝑚0 there holds 𝑚′′ (𝑜𝑢𝑡) ≤ 1.
• The combination 𝑚′ (𝑜𝑢𝑡) = 0 a 𝑚(𝑜𝑢𝑡) = 0 means by assumption 𝑚 < 𝑚′ , that there
exists 𝑝 ∈ 𝑃 different from 𝑜𝑢𝑡 such that 𝑚′ (𝑝) > 𝑚(𝑝). At the same time from the
first item of 1-soundness we get that 𝑚𝑓 is reachable from 𝑚 by firing a sequence of
transitions. From definition of transition firing it is clear that whenever a sequence
is enabled to fire from a marking, it is enabled to fire from any greater marking, and
therefore also from 𝑚′ . Because firing of that sequence leads from 𝑚 to 𝑚𝑓 , its firing from
𝑚′ leads to the marking 𝑚′′ = 𝑚′ + (𝑚𝑓 − 𝑚). Because 𝑚′ (𝑜𝑢𝑡) = 0 and 𝑚(𝑜𝑢𝑡) = 0,
we get 𝑚′′ (𝑜𝑢𝑡) = 1. At the same time 𝑚′ (𝑝) > 𝑚(𝑝). If 𝑝 ∈ 𝐷, we get 𝑚′′ (𝑝) > 0,
what contradicts the second item of 1-soundness. If 𝑝 ∈ 𝑆, we get 𝑚′′ (𝑝) > 𝑚𝑓 (𝑝), what
contradicts Corollaries 2 a 3.
It means that if a marked remembering workflow net with static places is 1-sound, then the
number of its reachable markings is finite and therefore the net is bounded. □
6. Reachability nets
In order to investigate the ability to finish properly arbitrary number of instances running in
parallel, we need to find a net, which will simulate the runtime environment with copies of a
dynamic part of a workflow net for each instance sharing just static places. Such a net should
prohibit the mixing of tokens from different copies. In other words, the net simulating the
runtime environment should separate reachable markings of dynamic places of instances. One
possible way to reach this goal is to use the reachability graph of the original workflow net as
an inspiration.
First we will define some basic notions which will be further used to define such so called
reachability net.
Definition 22 (Notation).
Let 𝑃 be a set, let 𝐴 be a set and let 𝐷 be a set such that 𝐷 ⊆ 𝑃 . Let 𝑚 : 𝑃 → 𝐴 be a function.
Let 𝑚|𝐷 denote restriction of 𝑚 to 𝐷, i.e. 𝑚|𝐷 : 𝐷 → 𝐴 such that 𝑚|𝐷(𝑑) = 𝑚(𝑑) for each
𝑑 ∈ 𝐷. Let 𝑆 be a set such that 𝑆 ⊆ 𝑃 , and let 𝐷 ∩ 𝑆 = ∅ (𝐷 a 𝑆 are disjoint), then we denote
𝑚|𝐷 ∪ 𝑚|𝑆 = 𝑚|(𝐷 ∪ 𝑆). Let us denote by 𝑃 ∖ 𝐷 the set difference 𝑃 and 𝐷, as a set satisfying
𝐷 ∩ (𝑃 ∖ 𝐷) = ∅ and (𝑃 ∖ 𝐷) ∪ 𝐷 = 𝑃 (we define the set difference only for the case that 𝐷 is a
subset of 𝑃 ). Let [𝑃 → 𝐴] denote the set of all functions from 𝑃 to 𝐴. For 𝐴 being a finite set, let
|𝐴| denote the number of elements of 𝐴.
Definition 23 (Set of reachable D-markings).
Let 𝑀 𝑃 𝑁 = (𝑃, 𝑇, 𝐼, 𝑂, 𝑚0 ) be a marked Petri net. Let 𝐷 be a subset of places, i.e. 𝐷 ⊆ 𝑃 .
Let 𝑚 be a marking of 𝑀 𝑃 𝑁 . Then function 𝑚|𝐷 is called a D-marking. By symbol [𝑚0 ⟩|𝐷 we
denote the set of all D-markings 𝑤 satisfying: 𝑤 ∈ [𝑚0 ⟩|𝐷 iff there exists such 𝑚 ∈ [𝑚0 ⟩ that
𝑤 = 𝑚|𝐷. It means that symbol [𝑚0 ⟩|𝐷 denotes the set of all D-markings 𝑚|𝐷 such that 𝑚 is
reachable from 𝑚0 . We also say that [𝑚0 ⟩|𝐷 denote the set of all D-markings reachable from
initial D-marking 𝑚0 |𝐷 in 𝑀 𝑃 𝑁 .
Each reachable D-marking 𝑚|𝐷 from [𝑚0 ⟩|𝐷 of the original workflow net will become to be
a place in reachability net. In addition, static places of the original workflow net will be static
places of reachability net. Elements of transition relation (𝑚, 𝑡, 𝑚′ ) z −→ of the reachability
graph of original workflow net will be used to create transitions of the reachability net. A
triple (𝑚|𝐷, 𝑡, 𝑚′ |𝐷) ∈ ([𝑚0 ⟩|𝐷) × 𝑇 × ([𝑚0 ⟩|𝐷) will be a transition of the reachability net iff
𝑡
𝑚 −→ 𝑚′ . A transition (𝑚|𝐷, 𝑡, 𝑚′ |𝐷) of the reachability net will consume exactly one token
from the place 𝑚|𝐷 of the reachability net and it will produce exactly one token in place 𝑚′ |𝐷 of
the reachability net. Arcs and their weights between static places and transition (𝑚|𝐷, 𝑡, 𝑚′ |𝐷)
of the reachability net will be identical with arcs between static places and transition 𝑡 of the
original net. Finally, we add a constructor consisting of two transitions {𝑛𝑒𝑤, 𝑠𝑡𝑜𝑝} and one
place {source}.
In graphical expression of reachability nets, we will label transition (𝑚|𝐷, 𝑡, 𝑚′ |𝐷) of the
reachability net only by the name of transition 𝑡 of the original net.
Definition 24 (Reachability net).
Let 𝑀 𝑊 = (𝐷, 𝑆, 𝑇, 𝐼, 𝑂, 𝑚0 ) be a marked workflow net with static places and let 𝑛𝑒𝑤, 𝑠𝑡𝑜𝑝
and 𝑠𝑜𝑢𝑟𝑐𝑒 denote elements satisfying {𝑛𝑒𝑤, 𝑠𝑡𝑜𝑝, 𝑠𝑜𝑢𝑟𝑐𝑒} ∩ (𝐷 ∪ 𝑆 ∪ 𝑇 ) = ∅. Reachability
net of the net 𝑀 𝑊 is the marked Petri net 𝑀 𝑃 𝑁 = (𝑃 𝑟 , 𝑇 𝑟 , 𝐼 𝑟 , 𝑂𝑟 , 𝑚𝑟0 ), where
• 𝑃 𝑟 = ([𝑚0 ⟩|𝐷) ∪ 𝑆 ∪ {𝑠𝑜𝑢𝑟𝑐𝑒}.
free memory
waiting for memory memory allocation memory allocated memory memory to dispose memory dispose memory disposed
settings save settings settings open
in task begin settings ready computation begin computation computation end task end out
waiting for processor processor allocation processor allocated processor processor to dispose processor dispose processor disposed
free processor
Figure 2: A 1-sound marked remembering workflow net with static places, modeling allocation of mem-
ory units and processors to computing tasks with possibility to change the setting for the computation.
• 𝑇 𝑟 = 𝑇 𝑎 ∪ {𝑛𝑒𝑤, 𝑠𝑡𝑜𝑝}, where 𝑇 𝑎 is the set of all triples (𝑥, 𝑡, 𝑦) ∈ ([𝑚0 ⟩|𝐷) × 𝑇 ×
([𝑚0 ⟩|𝐷), for which there exists a triple (𝑚, 𝑡, 𝑚′ ) ∈ [𝑚0 ⟩ × 𝑇 × [𝑚0 ⟩, such that 𝑥 = 𝑚|𝐷,
𝑡
𝑦 = 𝑚′ |𝐷 and 𝑚 −→ 𝑚′ , i.e. the transitions of the reachability net are 𝑛𝑒𝑤 a 𝑠𝑡𝑜𝑝 and
such triples (𝑥, 𝑡, 𝑦), where 𝑥 a 𝑦 are D-markings and 𝑡 is enabled to fire in marking 𝑚 in
𝑀 𝑊 and its firing leads to 𝑚′ in 𝑀 𝑊 , while 𝑥 = 𝑚|𝐷 and 𝑦 = 𝑚′ |𝐷.
• 𝐼 𝑟 (𝑥, (𝑥, 𝑡, 𝑦)) = 1 for each (𝑥, 𝑡, 𝑦) ∈ 𝑇 𝑎
• 𝐼 𝑟 (𝑠𝑜𝑢𝑟𝑐𝑒, 𝑛𝑒𝑤) = 1 and 𝐼 𝑟 (𝑠𝑜𝑢𝑟𝑐𝑒, 𝑠𝑡𝑜𝑝) = 1, i.e. constructor 𝑛𝑒𝑤 is enabled to fire
only in a marking with a token in place 𝑠𝑜𝑢𝑟𝑐𝑒, similarly 𝑠𝑡𝑜𝑝
• 𝐼 𝑟 (𝑠, (𝑥, 𝑡, 𝑦)) = 𝐼(𝑠, 𝑡) for each 𝑠 ∈ 𝑆, (𝑥, 𝑡, 𝑦) ∈ 𝑇 𝑎 , i.e. arcs from static places to copies
of transitions are copied
• 𝑂𝑟 ((𝑥, 𝑡, 𝑦), 𝑦) = 1 for each (𝑥, 𝑡, 𝑦) ∈ 𝑇 𝑎
• 𝑂𝑟 (𝑖𝑛, 𝑛𝑒𝑤) = 1 and 𝑂𝑟 (𝑠𝑜𝑢𝑟𝑐𝑒, 𝑛𝑒𝑤) = 1, i.e. firing of constructor 𝑛𝑒𝑤 creates a token
in place 𝑖𝑛 and returns a token to place 𝑠𝑜𝑢𝑟𝑐𝑒 (remember that from Definition 18 we get
𝑖𝑛 = 𝑚0 |𝐷)
• 𝑂𝑟 (𝑠, (𝑥, 𝑡, 𝑦)) = 𝑂(𝑠, 𝑡) for each 𝑠 ∈ 𝑆, (𝑥, 𝑡, 𝑦) ∈ 𝑇 𝑎 , i.e. arcs from copies of transitions
to static places are copied
• 𝐼 𝑟 (𝑝, 𝑡) = 0 a 𝑂𝑟 (𝑝, 𝑡) = 0 for each other pairs (𝑝, 𝑡) ∈ (𝑃 𝑟 × 𝑇 𝑟 )
• 𝑚𝑟0 (𝑠𝑜𝑢𝑟𝑐𝑒) = 1, 𝑚𝑟0 |𝑆 = 𝑚0 |𝑆 a 𝑚𝑟0 (𝑥) = 0 for each 𝑥 ∈ [𝑚0 ⟩|𝐷, i.e. in the initial
marking is one token in place 𝑠𝑜𝑢𝑟𝑐𝑒, tokens in static places are copied and places of the
reachability net equal to reachable D-markings of the net 𝑀 𝑊 are empty.
To illustrate a reachability net, we will consider the net in Figure 2
Existence of the complementary places of static places in remembering workflow net implies
following result:
Corollary 4. Let 𝑀 𝑊 = (𝐷, 𝑆, 𝑇, 𝐼, 𝑂, 𝑚0 ) be a marked remembering workflow net with static
places. Then for each two markings 𝑚 and 𝑚′ from [𝑚0 ⟩ there holds: if 𝑚|𝐷 = 𝑚′ |𝐷 then 𝑚 = 𝑚′ .
Corollary 5. Let 𝑀 𝑊 = (𝐷, 𝑆, 𝑇, 𝐼, 𝑂, 𝑚0 ) be a 1-sound marked remembering workflow net
with static places. Then its reachability net 𝑀 𝑃 𝑁 = (𝑃 𝑟 , 𝑇 𝑟 , 𝐼 𝑟 , 𝑂𝑟 , 𝑚𝑟0 ) has a finite number of
places 𝑃 𝑟 and a finite number of transitions 𝑇 𝑟 .
Places in the reachability net of remembering net represent states of the instance, including
information how many tokens from static places are used by the instance. Each token in a place
of the reachability net represent an instance in the corresponding state. The number of tokens
in a place of the reachability net determine how many instances are in that state. Thus, marking
of the reachability net determines how many instances are in states represented by single places
of the reachability net.
Definition 25 (Final marking of a reachability net).
Let 𝑀 𝑊 = (𝐷, 𝑆, 𝑇, 𝐼, 𝑂, 𝑚0 ) be a marked workflow net with static places and let a marked
Petri net 𝑀 𝑃 𝑁 = (𝑃 𝑟 , 𝑇 𝑟 , 𝐼 𝑟 , 𝑂𝑟 , 𝑚𝑟0 ) be the reachability net of the net 𝑀 𝑊 . A marking 𝑚𝑟𝑓 of
the reachability net 𝑀 𝑃 𝑁 reachable from 𝑚𝑟0 , is called a final marking of 𝑀 𝑃 𝑁 , if 𝑚𝑟𝑓 (𝑥) = 0
for each 𝑥 ∈ 𝑃 𝑟 ∖ (𝑆 ∪ {𝑜𝑢𝑡}) (where 𝑜𝑢𝑡 denotes in accordance with the introduced notation the
reachable D-marking given by function 1 · 𝑜𝑢𝑡 from 𝐷 to N).
A lock of the reachability net is defined as a marking, from which no final marking is reachable.
Definition 26. (Lock, deadlock and livelock of a reachability net)
Let 𝑀 𝑊 = (𝐷, 𝑆, 𝑇, 𝐼, 𝑂, 𝑚0 ) be a marked workflow net with static places and let a marked
Petri net 𝑀 𝑃 𝑁 = (𝑃 𝑟 , 𝑇 𝑟 , 𝐼 𝑟 , 𝑂𝑟 , 𝑚𝑟0 ) be the reachability net of the net 𝑀 𝑊 . A marking 𝑚𝑟
of the reachability net 𝑀 𝑃 𝑁 reachable from the initial marking 𝑚𝑟0 , is called a lock, if from 𝑚𝑟
no final marking of the reachability net 𝑀 𝑃 𝑁 is reachable. If no transition of the reachability net
𝑀 𝑃 𝑁 is enabled to fire in a lock 𝑚𝑟 , then it is called a deadlock of 𝑀 𝑃 𝑁 , otherwise it is called a
livelock of 𝑀 𝑃 𝑁 .
7. Basic locks of a reachability net
Following result, which is implied directly by the construction of the reachability net is important
for detection of locks of reachability nets.
Lemma 2. Let 𝑀 𝑊 = (𝐷, 𝑆, 𝑇, 𝐼, 𝑂, 𝑚0 ) be a 1-sound marked remembering workflow net
with static places and let a marked Petri net 𝑀 𝑃 𝑁 = (𝑃 𝑟 , 𝑇 𝑟 , 𝐼 𝑟 , 𝑂𝑟 , 𝑚𝑟0 ) be the reachability
net of the net 𝑀 𝑊 . Let marking 𝑚𝑟1 be reachable from 𝑚𝑟0 in the reachability net 𝑀 𝑃 𝑁 . Then
for arbitrary marking 𝑤 : (𝑃 𝑟 ∖ 𝑆) → N satisfying 𝑚𝑟1 |(𝑃 𝑟 ∖ 𝑆) > 𝑤 there exists such marking
𝑚𝑟2 reachable from 𝑚𝑟0 in 𝑀 𝑃 𝑁 , that 𝑚𝑟2 |(𝑃 𝑟 ∖ 𝑆) = 𝑤.
In the following definition we will divide the places of the reachability net according to the
fact, whether they represent states, in which resources from static places are used.
Definition 27 (Places with resources).
Let 𝑀 𝑊 = (𝐷, 𝑆, 𝑇, 𝐼, 𝑂, 𝑚0 ) be a 1-sound marked remembering workflow net with static places
and let a marked Petri net 𝑀 𝑃 𝑁 = (𝑃 𝑟 , 𝑇 𝑟 , 𝐼 𝑟 , 𝑂𝑟 , 𝑚𝑟0 ) be the reachability net of the net 𝑀 𝑊 .
• A place 𝑥 ∈ 𝑃 𝑟 ∖ 𝑆 of the reachability net is called a place without resource 𝑠 for 𝑠 ∈ 𝑆
if either 𝑥 = 𝑠𝑜𝑢𝑟𝑐𝑒 or for the complementary places 𝑑𝑠 ∈ 𝐷𝑆 of place 𝑠 there holds
𝑥(𝑑𝑠 ) = 0.
• The set of all places without resource 𝑠 is denoted by 𝐵𝑠𝑟 .
• If place 𝑥 ∈ 𝑃 𝑟 ∖ 𝑆 of the reachability net is a place without resource for each 𝑠 ∈ 𝑆, we
call it simply a place without resources.
• The set of all places without resources is denoted by 𝐵 𝑟 .
• A place 𝑥 ∈ 𝑃 𝑟 ∖ 𝑆 of the reachability net is called place with resource 𝑠 for 𝑠 ∈ 𝑆 if for
the complementary place 𝑑𝑠 ∈ 𝐷𝑆 of 𝑠 there holds 𝑥(𝑑𝑠 ) > 0. The set of all places with
resource 𝑠 is denoted by 𝑍𝑠𝑟 .
• If for a place 𝑥 ∈ 𝑃 𝑟 ∖ 𝑆 of the reachability net there is 𝑠 ∈ 𝑆 such that 𝑥 is a place with
resource 𝑠, then we call it simply a place with resources.
• The set of all places with resources is denoted by 𝑍 𝑟 .
• For a place 𝑥 ∈ 𝑍 𝑟 of the reachability net we denote by symbol 𝑍(𝑥) the set of such 𝑠 ∈ 𝑆,
for which 𝑥 ∈ 𝑍𝑠𝑟 .
Similarly as states, we divide the transitions of the reachability net for those, that need tokens
from static places to be enabled to fire and those, that do not need tokens from static places. We
will divide the places according to the fact, whether there is a transition, which moves a token
from a place with resources and at the same time it requires resources.
Definition 28. (Transitions requiring resources, critical places)
Let 𝑀 𝑊 = (𝐷, 𝑆, 𝑇, 𝐼, 𝑂, 𝑚0 ) be a 1-sound marked remembering workflow net with static places
and let a marked Petri net 𝑀 𝑃 𝑁 = (𝑃 𝑟 , 𝑇 𝑟 , 𝐼 𝑟 , 𝑂𝑟 , 𝑚𝑟0 ) be the reachability net of the net 𝑀 𝑊 .
• A transition (𝑥, 𝑡, 𝑦) ∈ 𝑇 𝑎 is called a transition requiring resources if 𝐼(𝑠, 𝑡) > 0 for some
𝑠 ∈ 𝑆.
• If for a place with resources 𝑥 ∈ 𝑍 𝑟 there holds that there is a transition (𝑥, 𝑡, 𝑦) ∈ 𝑇 𝑎
requiring resources, then 𝑥is called a critical place of the reachability net 𝑀 𝑃 𝑁 .
• The set of all critical places is denoted by 𝐾 𝑟 .
On Figure 3 there is the reachability net of the 1-sound marked remembering workflow net
with static places from Figure 2.
The set of places without resources 𝐵 𝑟 in the reachability net on Figure 3 is given by six
places: by place source, by place in, by place waiting for memory + waiting for processor + settings
ready, by place waiting for memory + waiting for processor + settings, by place memory disposed
+ processor disposed and by the place out.
The set of places with resources 𝑍 𝑟 is given by ten places, two of which are critical.
First critical place of the reachability net is its place waiting for memory + processor allocated
+ settings ready + processor. Second critical place of the reachability net is its place memory
allocated + waiting for processor + settings ready + memory.
On Figure 4 there is a livelock of the process for ten instances.
Corollary 6. Let 𝑀 𝑊 = (𝐷, 𝑆, 𝑇, 𝐼, 𝑂, 𝑚0 ) be a 1-sound marked remembering workflow net
with static places and let a marked Petri net 𝑀 𝑃 𝑁 = (𝑃 𝑟 , 𝑇 𝑟 , 𝐼 𝑟 , 𝑂𝑟 , 𝑚𝑟0 ) be the reachability
net of the net 𝑀 𝑊 . Let 𝑠 ∈ 𝑆 be a static place and let 𝑑𝑠 ∈ 𝐷𝑆 be
∑︀ its complementary place. Then
for each marking 𝑚𝑟 reachable from 𝑚𝑟0 there holds 𝑚𝑟 (𝑠) + 𝑥∈𝑍𝑠𝑟 𝑚𝑟 (𝑥) · 𝑥(𝑑𝑠 ) = 𝑚0 (𝑠),
and therefore 𝑚𝑟 (𝑠) ≤ 𝑚𝑟0 (𝑠) = 𝑚0 (𝑠).
Another important result is given as follows:
Lemma 3. Let 𝑀 𝑊 = (𝐷, 𝑆, 𝑇, 𝐼, 𝑂, 𝑚0 ) be a 1-sound marked remembering workflow net
with static places and let a marked Petri net 𝑀 𝑃 𝑁 = (𝑃 𝑟 , 𝑇 𝑟 , 𝐼 𝑟 , 𝑂𝑟 , 𝑚𝑟0 ) be the reachability
net of the net 𝑀 𝑊 . Then for arbitrary marking 𝑚𝑟1 reachable from 𝑚𝑟0 in the reachability net
there exists a marking 𝑚𝑟2 reachable from 𝑚𝑟1 such that 𝑚𝑟2 (𝑥) = 0 for each 𝑥 ∈ 𝑍 𝑟 ∖ 𝐾 𝑟 .
Proof. We show, that if a token is in a place 𝑥 ∈ 𝑍 𝑟 ∖ 𝐾 𝑟 , we can move that token to a
places without resources from 𝐵 𝑟 , or to a critical place from 𝐾 𝑟 . Repeating the procedure we
can set to zero all places 𝑥 ∈ 𝑍 𝑟 ∖ 𝐾 𝑟 . Because the original remembering workflow net is
1-sound, from each 𝑥 ∈ 𝑍 𝑟 ⊆ [𝑚0 ⟩|𝐷 is in original workflow net reachable a final marking
𝑜𝑢𝑡 ∪ 𝑚0 |𝑆. It means, that for each place 𝑥 ∈ 𝑍 𝑟 ∖ 𝐾 𝑟 there exists a finite sequence 𝜖 : I → 𝑇 a
𝜎 : I ∪ {0} → [𝑚0 ⟩|𝐷 such that 𝜎(0) = 𝑥, (𝜎(𝑖 − 1), 𝜖(𝑖), 𝜎(𝑖)) ∈ 𝑇 𝑎 for each positive integer
𝑖 ∈ I and 𝜎(𝑚𝑎𝑥I ) = 𝑜𝑢𝑡. Let 𝛼 : I → 𝑇 𝑎 be a sequence of transitions from 𝑇 𝑎 such that
𝛼(𝑖) = (𝜎(𝑖 − 1), 𝜖(𝑖), 𝜎(𝑖)) for 𝑖 ∈ I.
• Let no transition 𝛼(𝑖), where 𝑖 ∈ I, is a transition requiring resources. Then sequence 𝛼 is
enabled to fire in any marking of the reachability net 𝑚𝑟1 ∈ [𝑚𝑟0 ⟩ satisfying 𝑚1 (𝑥) > 0 and
its firing leads to marking 𝑚𝑟2 , such that 𝑚𝑟2 (𝑥) = 𝑚𝑟1 (𝑥)−1 and 𝑚𝑟2 (𝑜𝑢𝑡) = 𝑚𝑟1 (𝑜𝑢𝑡)+1,
i.e. firing of sequence 𝛼 moves a token from a place with resources 𝑥 of the reachability
net to the place without resources 𝑜𝑢𝑡 of the rechability net.
• Let there is an 𝑖 ∈ I such that transition 𝛼(𝑖) is a transition requiring resources. Let 𝑖 be
the smallest index, for which 𝛼(𝑖) is a transitions requiring resources. Because 𝑥 is not a
critical place, 𝑖 ≥ 2.
– Let 𝜎(𝑖 − 1) ∈ 𝐵 𝑟 , i.e. 𝜎(𝑖 − 1) is a place without resources. Then sequence
𝛼|{1, . . . , 𝑖 − 1} is enabled to fire in each marking of the reachability net 𝑚1 ∈ [𝑚𝑟0 ⟩
satisfying 𝑚𝑟1 (𝑥) > 0 and its firing leads to marking 𝑚𝑟2 , such that 𝑚𝑟2 (𝑥) =
𝑚𝑟1 (𝑥) − 1 and 𝑚𝑟2 (𝜎(𝑖 − 1)) = 𝑚𝑟1 (𝜎(𝑖 − 1)) + 1, i.e. firing of sequence 𝛼 moves
a token from place 𝑥 of the reachability net to a place without resources 𝜎(𝑖 − 1) of
the reachability net.
– Let 𝜎(𝑖 − 1) ∈ 𝑍 𝑟 , i.e. 𝜎(𝑖 − 1) is a place with resources. Because 𝛼(𝑖) = (𝜎(𝑖 −
1), 𝜖(𝑖), 𝜎(𝑖)) is a transition requiring resources, 𝜎(𝑖 − 1) ∈ 𝐾 𝑟 , i.e. 𝜎(𝑖 − 1) is a
critical place. Then sequence 𝛼|{1, . . . , 𝑖 − 1} is enabled to fire in each marking of
the rechability net 𝑚𝑟1 ∈ [𝑚𝑟0 ⟩ satisfying 𝑚1 (𝑥) > 0 and its firing leads to marking
𝑚𝑟2 , such that 𝑚𝑟2 (𝑥) = 𝑚𝑟1 (𝑥) − 1 and 𝑚𝑟2 (𝜎(𝑖 − 1)) = 𝑚𝑟1 (𝜎(𝑖 − 1)) + 1, i.e. firing
of sequence 𝛼 moves a token from place 𝑥 of the reachability net to a critical place
𝜎(𝑖 − 1) of the reachability net.
□
If we apply the result of Lemma 3 to locks, we get that from each lock of the reachability net
we can reach a lock, in which from all places with resources only critical places are marked.
These locks are called critical locks.
Definition 29 (Critical locks of a reachability net).
Let 𝑀 𝑊 = (𝐷, 𝑆, 𝑇, 𝐼, 𝑂, 𝑚0 ) be a 1-sound marked remembering workflow net with static
places and let a marked Petri net 𝑀 𝑃 𝑁 = (𝑃 𝑟 , 𝑇 𝑟 , 𝐼 𝑟 , 𝑂𝑟 , 𝑚𝑟0 ) be the reachability net of the net
𝑀 𝑊 . Then a lock 𝑚𝑟 , such that 𝑚𝑟 (𝑥) = 0 for each 𝑥 ∈ 𝑍 𝑟 ∖ 𝐾 𝑟 , is called a critical lock of the
reachability net.
Corollary 7. Let 𝑀 𝑊 = (𝐷, 𝑆, 𝑇, 𝐼, 𝑂, 𝑚0 ) be a 1-sound marked remembering workflow net
with static places and let a marked Petri net 𝑀 𝑃 𝑁 = (𝑃 𝑟 , 𝑇 𝑟 , 𝐼 𝑟 , 𝑂𝑟 , 𝑚𝑟0 ) be the reachability
net of the net 𝑀 𝑊 . Then there holds: if an arbitrary marking 𝑚𝑟1 reachable from 𝑚𝑟0 in the
reachability net is a lock, then there exists a critical lock 𝑚𝑟2 reachable from 𝑚𝑟1 .
The lock in Figure 4 is not a critical lock, because the place with resources waiting for memory
+ processor allocated + settings + processor and the place with resources memory allocated +
waiting for processor + settings + memory are not empty. These places with resources are not
critical places of the reachability net.
From marking in Figure 4 the marking in Figure 5 is reachable. The marking in Figure 5 is a
critical lock.
A special set of critical lock are those locks, for which no other places except critical places
and static places are marked. Such lock are called basic locks.
Definition 30 (Basic locks of a reachability net).
Let 𝑀 𝑊 = (𝐷, 𝑆, 𝑇, 𝐼, 𝑂, 𝑚0 ) be a 1-sound marked remembering workflow net with static places
and let a marked Petri net 𝑀 𝑃 𝑁 = (𝑃 𝑟 , 𝑇 𝑟 , 𝐼 𝑟 , 𝑂𝑟 , 𝑚𝑟0 ) be the reachability net of the net 𝑀 𝑊 .
Then a critical lock 𝑚𝑟 , such that 𝑚𝑟 (𝑥) = 0 for each place without resources 𝑥 ∈ 𝐵 𝑟 , is called a
basic lock of the reachability net.
The following results states, that if 𝑚𝑟1 is a critical lock, then marking 𝑚𝑟2 created from 𝑚𝑟1
by removing all tokens from all places without resources, is reachable from z 𝑚𝑟0 and therefore
it is a basic lock of the reachability net.
Lemma 4. Let 𝑀 𝑊 = (𝐷, 𝑆, 𝑇, 𝐼, 𝑂, 𝑚0 ) be a 1-sound marked remembering workflow net
with static places and let a marked Petri net 𝑀 𝑃 𝑁 = (𝑃 𝑟 , 𝑇 𝑟 , 𝐼 𝑟 , 𝑂𝑟 , 𝑚𝑟0 ) be the reachability
net of the net 𝑀 𝑊 . Then there holds: if an arbitrary marking 𝑚𝑟1 reachable from 𝑚𝑟0 in the
reachability net is a critical lock but not a basic lock, then 𝑚𝑟2 , such that 𝑚𝑟2 (𝑥) = 𝑚𝑟1 (𝑥) for each
place with resources 𝑥 ∈ 𝑍 𝑟 and 𝑚𝑟2 (𝑥) = 0 for each place without resources 𝑥 ∈ 𝐵 𝑟 , is a basic
lock of the reachability net.
Proof. According to Lemma 2, 𝑚𝑟2 is reachable from 𝑚𝑟0 . Assume, that 𝑚𝑟2 is not a basic lock.
Because 𝑚𝑟1 is a critical lock, 𝑚𝑟2 (𝑥) = 0 for each 𝑥 ∈ 𝑍 𝑟 ∖ 𝐾 𝑟 , i.e. 𝑚𝑟2 satisfies the condition of
critical locks. Because 𝑚𝑟2 (𝑥) = 0 for each place without resources 𝑥 ∈ 𝐵 𝑟 , 𝑚𝑟2 satisfies also the
condition of basic locks. It means, that 𝑚𝑟2 is not a lock. Then there is a sequence of transitions
𝛽 enabled to fire in 𝑚𝑟2 , such that its firing leads to a final marking 𝑚𝑟𝑓 , where 𝑚𝑟𝑓 |𝑆 = 𝑚𝑟0 |𝑆.
Because 𝑚𝑟2 (𝑥) = 𝑚𝑟1 (𝑥) for each place with resources 𝑥 ∈ 𝑍 𝑟 , i.e. in non-static places of
the reachability net differ 𝑚𝑟2 and 𝑚𝑟1 only in marking of places without resources, there also
holds that 𝑚𝑟2 |𝑆 = 𝑚𝑟1 |𝑆, i.e. the markings of static places of 𝑚𝑟2 and 𝑚𝑟1 are equal. Then the
sequence 𝛽 is enabled to fire also in 𝑚𝑟1 and its firing leads to 𝑚𝑟3 such that 𝑚𝑟3 |𝑍 𝑟 = 0 and
𝑚𝑟3 |𝑆 = 𝑚𝑟0 |𝑆.
Because original net 𝑀 𝑊 is 1-sound, (similarly as in the proof of Lemma 3) from each
𝑥 ∈ 𝐵 𝑟 ⊆ [𝑚0 ⟩|𝐷 is in 𝑀 𝑊 reachable the final marking 𝑜𝑢𝑡 ∪ 𝑚0 |𝑆 of 𝑀 𝑊 . It means, that
for each place 𝑥 ∈ 𝐵 𝑟 there is a finite sequence 𝜖 : I → 𝑇 a 𝜎 : I ∪ {0} → [𝑚0 ⟩|𝐷 such that
𝜎(0) = 𝑥, (𝜎(𝑖 − 1), 𝜖(𝑖), 𝜎(𝑖)) ∈ 𝑇 𝑎 for each finite positive integer 𝑖 ∈ I and 𝜎(𝑚𝑎𝑥I ) = 𝑜𝑢𝑡.
Let 𝛼 : I → 𝑇 𝑎 be the sequence of transitions from 𝑇 𝑎 such that 𝛼(𝑖) = (𝜎(𝑖−1), 𝜖(𝑖), 𝜎(𝑖)) for
𝑖 ∈ I. Sequence 𝛼 is enabled to fire in each marking of the reachability net 𝑚𝑟1 ∈ [𝑚𝑟0 ⟩ satisfying
𝑚1 (𝑥) > 0 and 𝑚𝑟1 |𝑆 = 𝑚𝑟0 |𝑆 and its firing leads to marking 𝑚𝑟4 , where 𝑚𝑟4 (𝑥) = 𝑚𝑟1 (𝑥)−1 and
𝑚𝑟4 (𝑜𝑢𝑡) = 𝑚𝑟1 (𝑜𝑢𝑡) + 1, i.e. firing of sequence 𝛼 moves a token from a place without resources
𝑥 of the reachability net to a place without resources 𝑜𝑢𝑡 of the reachability net, and also
𝑚𝑟4 |𝑍 𝑟 = 0, 𝑚𝑟4 |𝐵 𝑟 ∖ {𝑥, 𝑜𝑢𝑡} = 𝑚𝑟1 |𝐵 𝑟 ∖ {𝑥, 𝑜𝑢𝑡} a 𝑚𝑟4 |𝑆 = 𝑚𝑟1 |𝑆 = 𝑚𝑟0 |𝑆. By repeating the
firing of sequence 𝛼 we get marking 𝑚𝑟5 , where 𝑚𝑟5 (𝑥) = 0 and 𝑚𝑟5 (𝑜𝑢𝑡) = 𝑚𝑟1 (𝑜𝑢𝑡) + 𝑚𝑟1 (𝑥),
i.e. 𝑚𝑟1 (𝑥)-times repeated firing of sequence 𝛼 moves all 𝑚𝑟1 (𝑥) tokens from place without
resources 𝑥 of the reachability net to the place without resources 𝑜𝑢𝑡 of the reachability net,
and also 𝑚𝑟5 |𝑍 𝑟 = 0, 𝑚𝑟5 |𝐵 𝑟 ∖ {𝑥, 𝑜𝑢𝑡} = 𝑚𝑟1 |𝐵 𝑟 ∖ {𝑥, 𝑜𝑢𝑡} and 𝑚𝑟5 |𝑆 = 𝑚𝑟1 |𝑆 = 𝑚𝑟0 |𝑆. By
repeating the procedure for such 𝑥 ∈ 𝐵 𝑟 that marking of 𝑥 is not zero, we get a marking 𝑚𝑟𝑓
such that 𝑚𝑟𝑓 |((𝐵𝑟 ∖ {𝑜𝑢𝑡}) ∪ 𝑍 𝑟 ) = 0 and 𝑚𝑟𝑓 |𝑆 = 𝑚𝑟0 |𝑆, i.e. we get a final marking of the
reachability net. This contradicts with the assumption that 𝑚1 is a critical lock. □
By application of Lemma 4 on critical lock from Figure 5 we get the reachable basic lock in
Figure 6.
Altogether, we get the following main result.
Theorem 1. Let 𝑀 𝑊 = (𝐷, 𝑆, 𝑇, 𝐼, 𝑂, 𝑚0 ) be a 1-sound marked remembering workflow net
with static places and let a marked Petri net 𝑀 𝑃 𝑁 = (𝑃 𝑟 , 𝑇 𝑟 , 𝐼 𝑟 , 𝑂𝑟 , 𝑚𝑟0 ) be the reachability
net of the net 𝑀 𝑊 . Then there holds: if there exists a lock 𝑚𝑟1 , then there exists a basic lock 𝑚𝑟2 .
We also get:
Corollary 8. Let 𝑀 𝑊 = (𝐷, 𝑆, 𝑇, 𝐼, 𝑂, 𝑚0 ) be a 1-sound marked remembering workflow net
with static places and let a marked Petri net 𝑀 𝑃 𝑁 = (𝑃 𝑟 , 𝑇 𝑟 , 𝐼 𝑟 , 𝑂𝑟 , 𝑚𝑟0 ) be the reachability
net of the net 𝑀 𝑊 . If the reachability net has no critical places, then it has no locks.
Critical places are bounded in the reachability net, and therefore basic locks are bounded, i.e.
there are finitely many basic locks.
Definition 31 (Simple bound of critical places).
Let 𝑀 𝑊 = (𝐷, 𝑆, 𝑇, 𝐼, 𝑂, 𝑚0 ) be a 1-sound marked remembering workflow net with static
places and let a marked Petri net 𝑀 𝑃 𝑁 = (𝑃 𝑟 , 𝑇 𝑟 , 𝐼 𝑟 , 𝑂𝑟 , 𝑚𝑟0 ) be the reachability net of the
net 𝑀 𝑊 . Let 𝑘 ∈ 𝐾 𝑟 be a critical place. Let 𝑠 ∈ 𝑍(𝑘) and let 𝑑𝑠 ∈ 𝐷𝑆 be the complementary
place of 𝑠. Denote 𝑝𝑏(𝑘, 𝑠) = 𝑚0 (𝑠) ÷ 𝑘(𝑑𝑠 ), where symbol ÷ denotes integer division. Denote
𝑠𝑏𝑜𝑢𝑛𝑑(𝑘) = min𝑠∈𝑍(𝑘) 𝑝𝑏(𝑘, 𝑠) the minimum of values 𝑝𝑏(𝑘, 𝑠) for 𝑠 ∈ 𝑍(𝑘). The values
𝑠𝑏𝑜𝑢𝑛𝑑(𝑘) is called the simple bound of a critical place 𝑘. The sum of values
∑︁
𝑠𝑏𝑜𝑢𝑛𝑑(𝐾 𝑟 ) = 𝑠𝑏𝑜𝑢𝑛𝑑(𝑘)
𝑘∈𝐾 𝑟
is called the simple bound of critical places 𝐾 𝑟 .
Corollary 9. Let 𝑀 𝑊 = (𝐷, 𝑆, 𝑇, 𝐼, 𝑂, 𝑚0 ) be a 1-sound marked remembering workflow net
with static places and let a marked Petri net 𝑀 𝑃 𝑁 = (𝑃 𝑟 , 𝑇 𝑟 , 𝐼 𝑟 , 𝑂𝑟 , 𝑚𝑟0 ) be the reachability
net of the net 𝑀 𝑊 . Let 𝑚𝑟 be an arbitrary marking of the reachability net reachable from 𝑚𝑟0 .
For each critical place 𝑘 ∈ 𝐾 𝑟 there holds 𝑚𝑟 (𝑘) ≤ 𝑠𝑏𝑜𝑢𝑛𝑑(𝑘), i.e. the number of tokens in
any
∑︀ reachable marking 𝑚𝑟 does not exceed the simple bound of a critical place. There holds that
𝑟 𝑟 𝑟
𝑘∈𝐾 𝑟 𝑚 (𝑘) ≤ 𝑠𝑏𝑜𝑢𝑛𝑑(𝐾 ). In addition, 𝑠𝑏𝑜𝑢𝑛𝑑(𝐾 ) ≥ 1.
More exact upper bound of the number of tokens in critical places can be computed as a
solution of the following integer linear programming problem.
Definition 32 (Bound of critical places).
Let 𝑀 𝑊 = (𝐷, 𝑆, 𝑇, 𝐼, 𝑂, 𝑚0 ) be a 1-sound marked remembering workflow net with static places
and let a marked Petri net 𝑀 𝑃 𝑁 = (𝑃 𝑟 , 𝑇 𝑟 , 𝐼 𝑟 , 𝑂𝑟 , 𝑚𝑟0 ) be the reachability net of the net 𝑀 𝑊 .
Let 𝑦 : 𝐾 𝑟 → N be an integer solution of the linear inequality system
∑︁
𝑘(𝑑𝑠 ) · 𝑦(𝑘) ≤ 𝑚0 (𝑠) 𝑓 𝑜𝑟 𝑠 ∈ 𝑆
𝑘∈𝐾 𝑟
𝑦(𝑘) ≥ 0 𝑓 𝑜𝑟 𝑘 ∈ 𝐾 𝑟
which maximizes the objective function
∑︁
𝑘(𝑑𝑠 ) · 𝑦(𝑘)
𝑘∈𝐾 𝑟
This maximal value ∑︁
𝑏𝑜𝑢𝑛𝑑(𝐾 𝑟 ) = 𝑘(𝑑𝑠 ) · 𝑦(𝑘)
𝑘∈𝐾 𝑟
is called the bound of critical places 𝐾 𝑟 .
From the formulation of the integer linear programming problem we get the following result.
Corollary 10. Let 𝑀 𝑊 = (𝐷, 𝑆, 𝑇, 𝐼, 𝑂, 𝑚0 ) be a 1-sound marked remembering workflow net
with static places and let a marked Petri net 𝑀 𝑃 𝑁 = (𝑃 𝑟 , 𝑇 𝑟 , 𝐼 𝑟 , 𝑂𝑟 , 𝑚𝑟0 ) be the reachability
net of the net 𝑀 𝑊 . ∑︀Let 𝑚𝑟 be an arbitrary marking of the reachability net reachable from
𝑚0 . Then there holds 𝑘∈𝐾 𝑟 𝑚𝑟 (𝑘) ≤ 𝑏𝑜𝑢𝑛𝑑(𝐾 𝑟 ). Moreover, there holds that 𝑠𝑏𝑜𝑢𝑛𝑑(𝐾 𝑟 ) ≥
𝑟
𝑏𝑜𝑢𝑛𝑑(𝐾 𝑟 ).
Methods for solving the integer linear programming problems can be found e.g. in [36].
For the reachability net in Figure 4 of the 1-sound marked remembering workflow net with
static places from Figure 2 we get 𝑠𝑏𝑜𝑢𝑛𝑑(𝐾 𝑟 ) = 𝑏𝑜𝑢𝑛𝑑(𝐾 𝑟 ) = 4.
From definition of the reachability net we get the following result.
Lemma 5. Let 𝑀 𝑊 = (𝐷, 𝑆, 𝑇, 𝐼, 𝑂, 𝑚0 ) be a 1-sound marked remembering workflow net
with static places and let a marked Petri net 𝑀 𝑃 𝑁 = (𝑃 𝑟 , 𝑇 𝑟 , 𝐼 𝑟 , 𝑂𝑟 , 𝑚𝑟0 ) be the reachability
net of the net 𝑀 𝑊 . Let 𝑚𝑟1 be an arbitrary marking of the reachability net reachable from 𝑚𝑟0 .
Then for each marking 𝑚𝑟2 reachable from 𝑚𝑟1 there holds:
∑︁ ∑︁
𝑚𝑟1 (𝑥) ≤ 𝑚𝑟2 (𝑥)
𝑥∈[𝑚0 ⟩|𝐷 𝑥∈[𝑚0 ⟩|𝐷
If 𝑚𝑟1 (𝑠𝑜𝑢𝑟𝑐𝑒) = 0 then there holds:
∑︁ ∑︁
𝑚𝑟1 (𝑥) = 𝑚𝑟2 (𝑥)
𝑥∈[𝑚0 ⟩|𝐷 𝑥∈[𝑚0 ⟩|𝐷
Consider a constrained reachability net for a given positive integer 𝑛 ∈ Z by adding a place,
let us call it a buffer, from which firing of transition 𝑛𝑒𝑤 consumes just one token, while in the
initial marking this place get 𝑛 number of tokens, i.e. 𝑚𝑟0 (buffer) = 𝑛.
Such constrained reachability net preserves all the reachable markings for which the sum of
tokens in places from [𝑚0 ⟩|𝐷 does not exceed 𝑛. It also preserves the firing of all transitions
from 𝑇 𝑎 in these markings. The transition 𝑛𝑒𝑤 is enabled to fire in such a net exactly 𝑛-times.
Such net is bounded and represent the running of at most 𝑛 instances in parallel. Basic locks in
such a constrained net can be defined analogously as for the reachability net without constraints,
just allowing non zero marking of 𝑏𝑢𝑓 𝑓 𝑒𝑟.
If one set the initial value 𝑚𝑟0 (buffer) = 𝑠𝑏𝑜𝑢𝑛𝑑(𝐾 𝑟 ) or 𝑚𝑟0 (buffer) = 𝑏𝑜𝑢𝑛𝑑(𝐾 𝑟 ) one can
guarantee that whenever the reachability net has a basic lock then the constrained net has
the basic lock differing at most in the marking of the added place buffer. The constrained
reachability net with 𝑚𝑟0 (buffer) = 𝑠𝑏𝑜𝑢𝑛𝑑(𝐾 𝑟 ) = 𝑏𝑜𝑢𝑛𝑑(𝐾 𝑟 ) = 4 for the reachability net
from Figure 3 is in Figure 7.
8. Conclusion
We have investigated workflow processes with independent instances, which share durable
resources. We have considered the fixed number of resources and arbitrary number of instances.
We modeled such nets by so called 1-sound marked remembering workflow nets with static
places, which are in fact resource constrained workflow nets sound for one instance. We have
shown that detection of deadlocks and livelocks of such processes can be reduced to detection
of basic locks of the constrained bounded reachability nets of 1-sound marked remembering
workflow nets with static places.
One of the main aims of the further research is to find out how to synthesize a minimally
restrictive completion of a net which has deadlocks or livelock in order to avoid them. Another
aim of the further research is to determine the set of initial markings of static places, i.e. to
determine the number of resources, needed to avoid the deadlock and livelocks.
References
[1] K. Hee, A. Serebrenik, N. Sidorova, M. Voorhoeve, Soundness of resource-constrained
workflow nets, in: Applications and Theory of Petri nets, LNCS, volume 3536, Springer,
Berlin, Heidelberg, 2005, pp. 250–267. doi:10.1007/11494744_15.
[2] K. Barkaoui, R. Ben Ayed, Z. Sbai, Workflow soundness verification based on structure
theory of Petri nets, International Journal of Computing and Information Sciences 5 (2007)
51–61.
[3] K. Hee, N. Sidorova, M. Voorhoeve, Resource-constrained workflow nets., Fundamenta
Informaticae 71 (2006) 243–257.
[4] G. Juhás, I. Kazlov, A. Juhásová, Instance deadlock: A mystery behind frozen programs, in:
Applications and Theory of Petri Nets, LNCS, volume 6128, Springer, Berlin, Heidelberg,
2010, pp. 1–17. doi:10.1007/978-3-642-13675-7_1.
[5] A. Juhásová, G. Juhás, Soundess of resource constrained workflow nets is decidable., Petri
Net Newsletter. (2009) 3–6.
[6] M. Martos-Salgado, F. Rosa-Velardo, Dynamic soundness in resource-constrained workflow
nets, in: Formal Techniques for Distributed Systems, LNCS, volume 6722, Springer, Berlin,
Heidelberg, 2011, pp. 259–273. doi:10.1007/978-3-642-21461-5_17.
[7] M. R. Martos Salgado, Verification of priced and timed extensions of Petri Nets with
multiple instances., Ph.D. thesis, 2016.
[8] D. F. Escrig, C. Johnen, Decidability of home space property, in: LRI Report, volume 503,
Université Paris-Sud, 1989, pp. 1–25.
[9] N. Sidorova, C. Stahl, Soundness for resource-constrained workflow nets is decidable, IEEE
Transactions on Systems, Man, and Cybernetics: Systems 43 (2013) 724–729. doi:10.1109/
TSMCA.2012.2210415.
[10] K. Hee, N. Sidorova, M. Voorhoeve, Soundness and separability of workflow nets in the
stepwise refinement approach, in: Applications and Theory of Petri nets, LNCS, volume
2679, Springer, Berlin, Heidelberg, 2003, pp. 337–356. doi:10.1007/3-540-44919-1_22.
[11] E. Best, P. Darondeau, Separability in persistent petri nets, Fundamenta Informaticae 113
(2011) 179–203.
[12] F. L. Tiplea, C. Bocaneala, Decidability results for soundness criteria of resource-
constrained workflow nets, IEEE Transactions on Systems, Man, and Cybernetics - Part A:
Systems and Humans 42 (2012) 238–249. doi:10.1109/TSMCA.2011.2147310.
[13] E. Mayr, Persistence of vector replacement systems is decidable, Acta Informatica 15
(1981) 309–318. URL: https://doi.org/10.1007/BF00289268. doi:10.1007/BF00289268.
[14] S. R. Kosaraju, Decidability of reachability in vector addition systems (preliminary version),
in: Proceedings of the Fourteenth Annual ACM Symposium on Theory of Computing,
STOC ’82, Association for Computing Machinery, New York, NY, USA, 1982, p. 267–281.
doi:10.1145/800070.802201.
[15] E. W. Mayr, An algorithm for the general Petri net reachability problem, SIAM Journal on
computing 13 (1984) 441–460.
[16] J. Lambert, A structure to decide reachability in Petri nets, Theoretical Computer Science
99 (1992) 79–104. doi:https://doi.org/10.1016/0304-3975(92)90173-D.
[17] J. Leroux, Vector addition system reachability problem: A short self-contained proof, ACM
SIGPLAN Notices 46 (2011) 307–316. doi:10.1145/1925844.1926421.
[18] R. Keller, Formal verification of parallel programs, Communications of the ACM 19 (1976)
371–384. doi:10.1145/360248.360251.
[19] G. Winskel, M. Nielsen, Models for Concurrency, Oxford University Press, Inc., USA, 1995,
p. 1–148.
[20] R. M. Karp, R. E. Miller, Parallel program schemata, Journal of Computer and System
Sciences 3 (1969).
[21] T. Murata, Petri nets: Properties, analysis and applications, Proceedings of the IEEE 77
(1989) 541–580. doi:10.1109/5.24143.
[22] J. L. Peterson, Petri nets, ACM Computing Surveys 9 (1977) 223–252. doi:10.1145/
356698.356702.
[23] W. Reisig, A Primer in Petri Net Design, Springer, Berlin, Heidelberg, 1992.
[24] J. Desel, W. Reisig, Place/transition Petri nets, in: Lectures on Petri Nets I: Basic Models:
Advances in Petri Nets, LNCS, volume 1491, Springer, Berlin, Heidelberg, 1998, pp. 122–173.
doi:10.1007/3-540-65306-6_15.
[25] J. Desel, G. Juhás, What is a Petri net? An informal answer for an informed reader,
in: Unifying Petri Nets, Advances in Petri Nets, LNCS, volume 2128, Springer, Berlin,
Heidelberg, 2001, pp. 1–25. doi:10.1007/3-540-45541-8_1.
[26] R. Lipton, The reachability problem is exponential-space hard, in: Technical Report,
volume 62, Department of Computer Science, Yale University, 1976.
[27] C. Rackoff, The covering and boundedness problems for vector addition systems, Theoret-
ical Compututer Science 6 (1978) 223–231. doi:10.1016/0304-3975(78)90036-1.
[28] L. E. Rosier, H.-C. Yen, A multiparameter analysis of the boundedness problem for vector
addition systems, Journal of Computer and System Sciences 32 (1986) 105–135. doi:https:
//doi.org/10.1016/0022-0000(86)90006-1.
[29] W. M. P. van der Aalst, Three good reasons for using a Petri-net-based workflow manage-
ment system, in: Information and Process Integration in Enterprises, Springer US, Boston,
MA, 1998, pp. 161–182. doi:10.1007/978-1-4615-5499-8_10.
[30] W. M. P. van der Aalst, Verification of workflow nets, in: Application and Theory
of Petri Nets 1997, Springer Berlin Heidelberg, Berlin, Heidelberg, 1997, pp. 407–426.
doi:10.1007/3-540-63139-9_48.
[31] W. M. P. van der Aalst, The application of Petri nets to workflow management, Journal of
Circuits, Systems, and Computers 8 (1998) 21–66. doi:10.1142/S0218126698000043.
[32] W. Van Der Aalst, K. M. Van Hee, K. van Hee, Workflow management: models, methods,
and systems, The MIT Press, Cambridge, Massachusetts, 2002.
[33] K. Barkaoui, L. Petrucci, Structural analysis of workflow nets with shared ressources, in:
Workflow Management: Net-based Concepts, Models, Techniques and Tools (WFM’98).
Computing science reports, volume 9807, TU Eindhoven, 1998, pp. 82–95.
[34] R. Devillers, The semantics of capacities in P/T nets, in: Advances in Petri Nets 1989,
Springer, Berlin, Heidelberg, 1990, pp. 128–150. doi:10.1007/3-540-52494-0_28.
[35] D. Figueira, S. Figueira, S. Schmitz, P. Schnoebelen, Ackermannian and primitive-recursive
bounds with Dickson’s lemma, in: 2011 IEEE 26th Annual Symposium on Logic in
Computer Science, 2011, pp. 269–278. doi:10.1109/LICS.2011.39.
[36] A. Schrijver, Theory of Linear and Integer Programming, John Wiley, 1986.
stop source new in
task begin
processor allocation waiting for memory+waiting for processor+settings ready memory allocation
settings save settings open
waiting for memory+processor allocated+settings ready+processor memory allocated+waiting for processor+settings ready+memory
waiting for memory+waiting for processor+settings
settings save settings open settings save settings open
waiting for memory+processor allocated+settings+processor memory allocated+waiting for processor+settings+memory
memory allocated+processor allocated+settings+memory+processor
settings save settings open
memory allocation processor allocation
memory allocated+processor allocated+settings ready+memory+processor
free memory
free processor
computation begin
computation+memory+processor
computation end
processor dispose memory to disposee+processor to dispose+memory+processor memory dispose
memory to dispose+processor disposed+memory memory disposed+processor to dispose+processor
memory dispose memory disposed+processor disposed processor dispose
task end
out
Figure 3: The reachability net of the 1-sound marked remembering workflow net with static places
from Figure 2
stop source new in
task begin
processor allocation waiting for memory+waiting for processor+settings ready memory allocation
settings save settings open
waiting for memory+processor allocated+settings ready+processor memory allocated+waiting for processor+settings ready+memory
waiting for memory+waiting for processor+settings
settings save settings open settings save settings open
waiting for memory+processor allocated+settings+processor memory allocated+waiting for processor+settings+memory
memory allocated+processor allocated+settings+memory+processor
settings save settings open
memory allocation processor allocation
memory allocated+processor allocated+settings ready+memory+processor
free memory
free processor
computation begin
computation+memory+processor
computation end
processor dispose memory to disposee+processor to dispose+memory+processor memory dispose
memory to dispose+processor disposed+memory memory disposed+processor to dispose+processor
memory dispose memory disposed+processor disposed processor dispose
task end
out
Figure 4: The reachability net of the 1-sound marked remembering workflow net with static places
from Figure 2 in a livelock for ten instances
stop source new in
task begin
processor allocation waiting for memory+waiting for processor+settings ready memory allocation
settings save settings open
waiting for memory+processor allocated+settings ready+processor memory allocated+waiting for processor+settings ready+memory
waiting for memory+waiting for processor+settings
settings save settings open settings save settings open
waiting for memory+processor allocated+settings+processor memory allocated+waiting for processor+settings+memory
memory allocated+processor allocated+settings+memory+processor
settings save settings open
memory allocation processor allocation
memory allocated+processor allocated+settings ready+memory+processor
free memory
free processor
computation begin
computation+memory+processor
computation end
processor dispose memory to disposee+processor to dispose+memory+processor memory dispose
memory to dispose+processor disposed+memory memory disposed+processor to dispose+processor
memory dispose memory disposed+processor disposed processor dispose
task end
out
Figure 5: The reachability net of the 1-sound marked remembering workflow net with static places
from Figure 2 in a critical livelock for ten instances
stop source new in
task begin
processor allocation waiting for memory+waiting for processor+settings ready memory allocation
settings save settings open
waiting for memory+processor allocated+settings ready+processor memory allocated+waiting for processor+settings ready+memory
waiting for memory+waiting for processor+settings
settings save settings open settings save settings open
waiting for memory+processor allocated+settings+processor memory allocated+waiting for processor+settings+memory
memory allocated+processor allocated+settings+memory+processor
settings save settings open
memory allocation processor allocation
memory allocated+processor allocated+settings ready+memory+processor
free memory
free processor
computation begin
computation+memory+processor
computation end
processor dispose memory to disposee+processor to dispose+memory+processor memory dispose
memory to dispose+processor disposed+memory memory disposed+processor to dispose+processor
memory dispose memory disposed+processor disposed processor dispose
task end
out
Figure 6: The reachability net of the 1-sound marked remembering workflow net with static places
from Figure 2 in a basic livelock for four instances
stop source new in
buffer task begin
processor allocation waiting for memory+waiting for processor+settings ready memory allocation
settings save settings open
waiting for memory+processor allocated+settings ready+processor memory allocated+waiting for processor+settings ready+memory
waiting for memory+waiting for processor+settings
settings save settings open settings save settings open
waiting for memory+processor allocated+settings+processor memory allocated+waiting for processor+settings+memory
memory allocated+processor allocated+settings+memory+processor
settings save settings open
memory allocation processor allocation
memory allocated+processor allocated+settings ready+memory+processor
free memory
free processor
computation begin
computation+memory+processor
computation end
processor dispose memory to disposee+processor to dispose+memory+processor memory dispose
memory to dispose+processor disposed+memory memory disposed+processor to dispose+processor
memory dispose memory disposed+processor disposed processor dispose
task end
out
Figure 7: 𝑛-constrained bounded reachability net of the reachability net from Figure 3 for 𝑛 =
𝑠𝑏𝑜𝑢𝑛𝑑(𝐾 𝑟 ) = 𝑏𝑜𝑢𝑛𝑑(𝐾 𝑟 ) = 4