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.
In [
The main problem solved in [
In [
In [
In [
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 [
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 ifxed initial number of durable shared resources will contain a lock (i.e. a deadlock or a liveclock), it sufices 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 free processor
As a basic model of process behaviour we will use labelled transition systems [
A labelled transition system is an ordered triple (, , →− • 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.
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 .
Let (, , →− ) be a labelled transition systems. Let ∈ be a state and let : I → be a finite sequence of events. Sequence can occur in state if 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 if 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.
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 .
In this section we briefly introduce the basic definition of Petri nets [
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 () if () > 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 ∑︀∈ ().
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 diference 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 if 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 (, , →− • is the set of all markings, i.e. the set of all functions from to non-negative integers N, • = ,
• →− ′ if 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 .
A marked Petri net = (, , , , 0) is bounded if 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. [
Corollary 1. A marked Petri net = (, , , , 0) with finite set of places is bounded if the number of markings reachable from 0 in is finite.
We focus on processes, where instances has a unique start and unique correct finish. In literature,
such systems are modeled by workflow nets [
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.
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 ∈ diferent from .
Processes with instances and shared resources will be modeled by Petri nets 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.
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) 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 ∈ .
A
Initial marking of a marked workflow net with static places contains one token in the input place, no tokens in dynamic places diferent 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 diferent from .
In comparison with [
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 ∈ diferent 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 if 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 [
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 if there holds: () = 1, () = 0 for each ∈ diferent 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 if 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 [
• 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 ∈ diferent from such that ′() > (). At the same time from the ifrst 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. □
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 diferent 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.
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 diference and , as a set satisfying ∩ ( ∖ ) = ∅ and ( ∖ ) ∪ = (we define the set diference 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 .
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⟩| if 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 if →− ′. 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}.
reachability net only by the name of transition of the original 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⟩|) ∪ ∪ {}. waiting for memory • = ∪ {, }, 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.
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 .
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.
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.
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.
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.
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 difer 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 ifring 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. □
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.
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.
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 which maximizes the objective function This maximal value is called the bound of critical places .
∑︁ () · () ≤ 0() ∈ ∈ () ≥ 0 ∈ ∑︁ () · () ∈ () = ∑︁ () · ()
∈
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 [
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: If 1() = 0 then there holds:
∑︁ ∈[0⟩|
∑︁ ∈[0⟩| 1() ≤ 1() =
∑︁ ∈[0⟩|
∑︁ ∈[0⟩| 2() 2()
let us call it a bufer , from which firing of transition consumes just one token, while in the initial marking this place get number of tokens, i.e. 0(bufer ) = .
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(bufer ) = () or 0(bufer ) = () one can guarantee that whenever the reachability net has a basic lock then the constrained net has the basic lock difering at most in the marking of the added place bufer . The constrained reachability net with 0(bufer ) = () = () = 4 for the reachability net from Figure 3 is in Figure 7.
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. stop new task begin waiting for memory+processor allocated+settings+processor memory allocated+waiting for processor+settings+memory memory allocated+processor allocated+settings+memory+processor settings save memory allocated+processor allocated+settings ready+memory+processor free processor free memory computation begin computation end task end
out processor dispose memory to disposee+processor to dispose+memory+processor stop new task begin waiting for memory+waiting for processor+settings waiting for memory+processor allocated+settings ready+processor memory allocated+waiting for processor+settings ready+memory waiting for memory+processor allocated+settings+processor memory allocated+waiting for processor+settings+memory memory allocated+processor allocated+settings+memory+processor settings save memory allocated+processor allocated+settings ready+memory+processor free processor free memory computation begin computation end task end
out processor dispose memory to disposee+processor to dispose+memory+processor memory to dispose+processor disposed+memory memory disposed+processor to dispose+processor memory dispose memory disposed+processor disposed stop new task begin waiting for memory+waiting for processor+settings waiting for memory+processor allocated+settings ready+processor memory allocated+waiting for processor+settings ready+memory 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 processor free memory computation begin computation end task end
out processor dispose memory to disposee+processor to dispose+memory+processor memory to dispose+processor disposed+memory memory disposed+processor to dispose+processor memory dispose memory disposed+processor disposed stop new task begin waiting for memory+waiting for processor+settings waiting for memory+processor allocated+settings ready+processor memory allocated+waiting for processor+settings ready+memory 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 processor free memory computation begin computation end task end
out processor dispose memory to disposee+processor to dispose+memory+processor memory to dispose+processor disposed+memory memory disposed+processor to dispose+processor memory dispose memory disposed+processor disposed processor dispose stop new processor allocation memory allocated+processor allocated+settings+memory+processor memory allocated+processor allocated+settings ready+memory+processor free processor free memory computation begin computation end 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