In this work we consider modeling of workflow systems with Petri nets. A resource workflow net (RWF-net) is a workflow net, supplied with an additional set of initially marked resource places. Resources can be consumed and/or produced by transitions. We do not constrain neither the intermediate nor final resource markings, hence a net can have an infinite number of different reachable states. An initially marked RWF-net is called sound if it properly terminates and, moreover, adding any extra initial resource does not violate its proper termination. An (unmarked) RWF-net is sound if it is sound for some initial resource. In this paper we prove the decidability of both marked and unmarked soundness for a restricted class of RWF-nets with a single unbounded resource place (1-dim RWF-nets). We present an algorithm for computing the minimal sound resource for a given sound 1-dim RWF-net.
Petri nets constitute a popular formalism for modeling and analysis of distributed
systems. In this paper we consider workflow systems, or, to be more precise,
workflow processes. To model workflow processes a special subclass of Petri nets,
called WF-nets [
In the context of WF-nets a crucial correctness criterion is soundness [
Soundness of WF-nets is decidable [
One of important aspects in workflow development concerns resource management. Resources here is a general notion for executives (people or devices), raw materials, finances, etc. To take resources into account different extensions of a base formalism where introduced, having different versions of soundness criteria.
In [
In [
In all mentioned papers resources are assumed to be permanent, i.e. they are used (blocked) and released later on. Resources are never created, nor destroyed. Hence the process state space is explicitly bounded.
To study a more general case of arbitrary resource transformations (that can
arise, for example, in open and/or adaptive workflow systems), in [
Unfortunately, even sound RWF-nets are not bounded in general, hence
existing soundness checking algorithms cannot be applied here. In [
In this paper we consider a restricted case — RWF-nets with a single resource place (1-dim RWF-nets). One resource type is sufficient for many practical applications (memory or money are typical examples of such resources). Note that 1-dim RWF-nets are, generally speaking, not bounded and hence this case cannot be reduced to finite-state WF-nets with resources, such as RCWF- or WFR-nets.
In this paper we use graph-theoretic properties of RWF-net control automaton to prove decidability of soundness for marked, as well as unmarked 1-dim RWF-nets. We present also an algorithm for computing minimal sound resource for a given sound 1-dim RWF-net.
The paper is organized as follows. In Section 2 basic definitions of multisets and Petri nets are given. In Section 3 we give definitions of sound RWF-nets. In Section 4 the class of 1-dim RWF-nets is defined and studied, algorithms for checking marked soundness, soundness and finding the minimal sound resource are given. Section 5 contains some conclusions. 2
where Nat is the set of natural numbers (including zero), i. e. a multiset may contain several copies of the same element.
inclusion relation). The sum, the union and the subtraction of two multisets m and m0 are defined as usual: ∀s ∈ S : (m + m0)(s) = m(s) + m0(s), (m ∪ m0)(s) = max(m(s), m0(s)), (m − m0)(s) = m(s) m0(s) (where denotes the truncated subtraction). By M(S) we denote the set of all finite multisets over S.
Non-negative integer vectors are often used to encode multisets. Actually, the set of all multisets over finite S is a homomorphic image of Nat|S|.
Let P and T be nonempty disjoint sets of places and transitions and let F : (P × T ) ∪ (T × P ) → Nat. Then N = (P, T, F ) is a Petri net. A marking in a Petri net is a function M : P → Nat, mapping each place to some natural number (possibly zero). Thus a marking may be considered as a multiset over the set of places. Pictorially, P -elements are represented by circles, T -elements by boxes, and the flow relation F by directed arcs. Places may carry tokens represented by filled circles. A current marking M is designated by putting M (p) tokens into each place p ∈ P . Tokens residing in a place are often interpreted as resources of some type consumed or produced by a transition firing. A simple example, where tokens represent molecules of hydrogen, oxygen and water respectively is shown in Fig. 1.
an output arc; the preset •t and the postset t• are defined as the multisets over P such that •t(p) = F (p, t) and t•(p) = F (t, p) for each p ∈ P . A transition t ∈ T is enabled in a marking M iff ∀p ∈ P M (p) ≥ F (p, t). An enabled transition t may fire yielding a new marking M 0 =def M − •t + t•, i. e. M 0(p) = M (p) − F (p, t) +
is reachable from M iff there is a sequence M = M1 → M2 → · · · → Mn = M 0.
its initial marking M0. 3
In Petri nets with resources we divide Petri net places into control and resource ones.
Definition 1. where
A Petri net with resources is a tuple N = (Pc, Pr, T, Fc, Fr), Definition 3. (RWF-net) iff – Pc is a finite set of control places; – Pr is a finite set of resource places, Pc ∩ Pr = ∅; – T is a finite set of transitions, Pc ∩ T = Pr ∩ T = ∅; – Fc : (Pc × T ) ∪ (T × Pc) → Nat is a multiset of control arcs; – Fr : (Pr × T ) ∪ (T × Pr) → Nat is a multiset of resource arcs; – ∀t ∈ T ∃p ∈ Pc : Fc(p, t) + Fc(t, p) > 0 (each transition is incident to some control place).
Note that all transitions are necessarily linked to control places — this guarantees the absence of u“ncontrolled” resource modifications.
A marking in a Petri net with resources is also divided into control and resource parts. For a multiset c + r, where c ∈ M(Pc) and r ∈ M(Pr), we write c|r.
Definition 2. For a net N a resource is a multiset over Pr. A controlled resource is a multiset over Pc ∪ Pr.
Workflow nets (WF-nets) are a special subclass of Petri nets designed for modeling workflow processes. To study resource dependencies in workflow systems we consider WF-nets with resources.
A Petri net with resources N is called a WF-net with resources 1. There is one source place i ∈ Pc and one sink place o ∈ Pc s. t. •i = o• = ∅; 2. Every node from Pc ∪ T is on a path from i to o, and this path consists of nodes from Pc ∪ T.
Definition 4. A marked RWF-net (N, c|r) is called sound iff ∀s ∈ M(Pr), ∀M ∈ R(N, c|r + s) we have: 1. ∃s0 ∈ M(Pr) : o|s0 ∈ R(N, M ); 2. c0|r0 ∈ R(N, M ) ⇒ c0 = o ∨ c0 ∩ o = ∅.
Thus soundness for a RWF-net means that, first, this workflow net can terminate properly from any reachable state, and, additionally, adding any extra resource does not violate the proper termination property.
Note that our definition is substantially different from the definition of sound
RCWF-nets (Resource-Constrained Workflow net) in [
The following statement is analogous to Lemma 5 in [
Proposition 1. [
The proof of this proposition is given in the Appendix.
The converse statement is not true: there may be RWF-nets with sound control subnets, for which sound resources do not exist. An example of such a net is given in Fig. 3.
Let N be a RWF-net. By C(N ) we denote the set of all control markings reachable in Nc, i. e. C(N ) = R(Nc, i).
Proposition 2. [
The proof of this proposition is given in the Appendix.
Further, we call a RWF-net N sound (without indicating any concrete resource) iff a marked RWF-net (N, i|r) is sound with some initial resource r.
From the second statement of Proposition 2 and the well-known Dickson’s lemma we obtain the following Corollary 1. For a sound RWF-net N the set C(N ) of all its reachable control markings is finite.
Note 1. Since the control subnet of a sound RWF-net N is bounded, the set C(N ) can be effectively constructed (e. g. by constructing a coverability tree). Definition 5.
Let N be a RWF-net, c ∈ C(N ). We define: 1. res(c) =def {r ∈ M(Pr) | (N, c|r) is sound} — the set of all sound resources for c; 2. mres(c) =def {r ∈ res(c) | 6 ∃r0 ∈ res(c) : r0 ⊂ r} — the set of all minimal sound resources for c.
Then from Dickson’s Lemma we immediately obtain:
Proposition 3. [
The questions of computability of mres(c) and decidability of soundness for RWF-nets remain open. In the next section positive answers to these two questions are given for a restricted case — RWF-nets with a single resource place. 4
Let N = (Pc, Pr, T, Fc, Fr) be an RWF-net with Pr = {pr}, i.e. with just one resource place. By 1-dim RWF-nets we denote the subclass of RWF-nets with single resources. An example of such a net is given in Fig. 4. In the following sections we consider only 1-dim RWF-nets.
If a control subnet of N is not sound, then N is also not sound. So, we suppose that the control subnet of N is sound, and hence bounded.
Fig. 4. 1-dim RWF-net N1. 4.1
Control automaton It is easy to note that a bounded control subnet can be represented as an equivalent finite automaton (a transition system). This automaton is an oriented graph with two distinguished nodes – a source node i and a sink node o.
In this control automaton states are exactly the elements of C(N ), transitions — transitions of the given net N . But now it will be more convenient to consider a transition t as a pair (c1, c2) of control states, where c1 →t c2. Every transition t of the automaton is labeled by an integer δ(t), defining a “resource effect” of transition firing. A positive δ(t) means that the firing of t increments the marking of a (single) resource place pr by δ(t), a negative δ(t) means that t is enabled in a state (c|r) iff r(pr) ≥ |δ(t)|, and that the firing of t decrements the resource by |δ(t)|. Formally, δ(t) =def −Fr(pr, t) for Fr(pr, t) > 0;
Fr(t, pr) for Fr(t, pr) > 0.
The value δ(t) is called an effect of t (denoted Eff (t)). Note that for simplicity we exclude loops, when both Fr(pr, t) > 0 and Fr(t, pr) > 0; such loops can be simulated by two sequential transitions.
A support of t is the amount of the resource required for a firing of t. It is defined as:
Supp(t) =def
0, δ(t) ≥ 0; |δ(t)|, δ(t) < 0.
Thus, a 1-dim RWF-net N can be transformed into a control automaton
Aut(N ), which can be considered as a one-counter net (e.g. [
PNSE’13 – Petri Nets and Software Engineering
Consider an example depicted in Fig. 5. This is a control automaton for the 1-dim RWF-net from Fig. 4. States are denoted by octagons, labelled with the corresponding control markings of the net. Transitions are labelled with the corresponding names and effects.
A control automaton (a one-counter net) is a digraph with arcs labeled by integers. Recall some basic notion from graph theory.
A walk is an alternating sequence of nodes and arcs, beginning and ending with a node, where each node is incident to both the arc that precedes it and the arc that follows it in the sequence, and where the nodes that precede and follow an arc are the head and the tail of this arc.
We consider only non-empty walks, containing at least one arc.
A walk is closed if its first and last nodes coincide.
A path is a walk where no arcs are repeated (nodes may be repeated). A simple path is a path where no nodes are repeated.
A cycle is a closed path.
A simple cycle is a closed path where no nodes are repeated (except the first/last one).
A walk in a control automaton corresponds to some sequence of firings in 1-dim RWF-net. Now we inductively define an effect and a support of a walk. Intutively,
Let t be a transition and σ a walk, such that the ending node of t is the beginning node of the first transition of σ. Let tσ denote a walk, constructed by linking t and σ. We define:
Eff (tσ) =def Eff (t) + Eff (σ);
Supp(tσ) =def Supp(t) + (Supp(σ)
Eff (t)), where
denotes the truncated subtraction.
A positive (resp., negative) walk is a walk with a positive (resp., negative) effect. Obviously, the effect of a cycle does not depend on a choice of a starting node.
A node q is called a positive generator, iff there exists a simple positive path from q to q (a simple positive cycle) with a zero support.
Lemma 1. Any simple positive cycle contains at least one generator. Proof. Note that without loss of generality we can consider only cycles of even lengths, having alternating positive and negative arcs. Then the proof is straightforward, by induction on the length of a cycle.
A node q is called a negative generator, iff there exists a simple negative path θ from q to q (a simple negative cycle), such that Supp(θ) = −Eff (θ). Lemma 2. Any simple negative cycle contains at least one generator. Proof. Similar to the previous lemma. 4.2
Decidability of soundness for marked nets
denote by N also the control automaton of N , represented as a one-counter net.
initial value of a counter (the single resource place), and R(N, (i|r0)) denotes the set of all reachable states.
sound if and only if it does not always terminate with a final control state o for some larger initial resource r0 + s:
∃(c|r) ∈ R(N, i|r0 + s) such that (o|s0) 6∈ R(N, c|r) for any s0 ∈ Nat. So we consider both two kinds of possible undesirable (not properly terminating) behaviours of a Petri net, namely, deadlocks and livelocks. no transition t ∈ T s.t. (c|r) →t (c0|r0) for some c0, r0.
Definition 6.
A state (c|r) ∈ C(N )×Nat is a deadlock iff c 6= o and there is A finite set L ⊂ C(N )×Nat of states is a livelock iff 1. |L| > 1; 2. for any (c|r), (c0|r0) ∈ L there is a finite transition sequence (c|r) →σ (c0|r0); 3. for any (c|r) ∈ L and t ∈ T s.t. (c|r) →t (c00|r00) we have (c00|r00) ∈ L. σ ∈ T ∗ s.t.
A livelock state is a state that belongs to some livelock.
Proposition 4. If a state (c|r) is a deadlock then for any t ∈ T s.t. c →t c0 we have Supp(t) > r.
Proof. Straightforward.
Note that Prop. 4 implies δ(t) < 0 and hence we can reformulate it: Corollary 2. If a state (c|r) is a deadlock then: 2. r < min{|δ(t)| : c →t c0 for some c0}. 1. ∀t ∈ T s.t. c →t c0 for some c0 we have δ(t) < 0;
So deadlocks can occur (1) just for control states with only negative outgoing transitions; (2) only for a finite number of different resources – when there are no enough resources for firing any of the successor transitions.
Proposition 5. The set of deadlock states is finite.
Proof. The set of “potential deadlock” control states (nodes with only negative outgoing transitions) is finite. For a given “potential deadlock” control state the set of applicable deadlock states (natural numbers smaller than the smallest required resource for a successor transition) is also finite.
Hence, all deadlocks can be detected by checking control states with only negative outgoing transitions.
Now let us consider livelocks.
Proposition 6. If L ⊂ C(N )×Nat is a livelock then there is a state (c|r) ∈ L and a negative transition t ∈ T with c →t c0, such that δ(t) < −r. Proof. Straightforward, since the control subnet of RWF-net N is sound. Proposition 7. The set of livelocks is finite.
positive cycle, that can generate an infinite number of states — a contradiction to the finiteness of livelocks. So, every control state can occur in a given livelock at most once.
Now assume the converse: there are infinitely many livelocks. Then there are infinitely many livelocks with the same set of control states, which differ only in their resource value. Hence, this set includes a livelock with an arbitrarily large resource, and we can take a livelock with a resource big enough to reach the final state o. This implies that o belongs to the livelock — a contradiction with the definition of a livelock.
Thus, all livelocks can be easily detected by checking finite systems of states, closed under transition firings (strongly connected components) and satisfying the property from Prop. 6. "!$#&%(’)+*-,.0/1324653798:<;=6>
V. Bashkin et al.: Soundness of WF Nets with an Unbounded Resource 71
Fig. 6. Modified RWF-net N .
Theorem 1. Soundness is decidable for marked 1-dim RWF-nets.
Proof. The following proof is similar to the proof of decidability of structural
soundness in [
For a given 1-dim RWF-net N construct the modified RWF-net N by adding a new initial place i and two new transitions, as depicted in Fig. 6. The original
in 1-dim RWF-net (N , i|r) (otherwise some large enough initial resource would produce the same undesirable situation in the given net N ).
Since the sets of deadlocks and livelocks are finite and computable, the problem of soundness of a marked 1-dim RWF-net can be reduced to a finite number of instances of a reachability problem for a 1-counter Petri net. This reachability problem is decidable. 4.3
Decidability of soundness for unmarked nets Theorem 1 gives us only a semidecision procedure for soundness of a net. One can check the soundness of a given initial marking, but if the answer is negative, it is not known whether there exists a larger sound marking.
Definition 7. An unmarked RWF-net N is called sound iff (N, i|r) is sound for some resource r.
Corollary 2 gives us only a necessary condition of a deadlock, reachable from some initial marking. Now we prove a stronger theorem, which gives a sufficient and necessary condition for existence of a soundness-violating deadlock (i.e. a deadlock that is reachable from an infinite number of different initial markings). Theorem 2. An unmarked 1-dim RWF-net is not sound with deadlocks iff there exist a deadlock state (c|r), a negative generator q and a simple path q →σ c such that Eff (σ) Supp(σ) ≤ r.
r0 there exists a larger initial resource r0 + x, such that a deadlock is reachable from (i|r0 + x).
Consider an arbitrary (large enough) initial resource r0 s.t.
(i|r0) →τ (q|s) for some path τ and resource s (it is always possible to find such a resource since the control net is sound, and therefore any control state is reachable for some sufficiently large initial resource). Let θ = qc1 . . . cj q be a simple negative cycle with generator q, i.e. Supp(θ) = −Eff (θ). Denote z = s mod Supp(θ) and consider a larger initial resource r0 + z + Supp(σ).
We have i|r0 + z + Supp(σ)
↓ τ q|s + z + Supp(σ)
↓ θ (s+z)/Supp(θ) q|Supp(σ)
↓ σ c|Eff (σ)
Supp(σ) and hence a deadlock.
(⇒) Assume the converse: the net is unsound with a deadlock, but for any given deadlock state, it is impossible to find a negative generator that satisfies the conditions in the theorem.
is reachable from an infinite number of different initial states (initial resource values).
Every transition sequence σ = t1.t2. . . . .tn from (i|r0) to (c|r) corresponds to a walk σ in the control automaton graph. Since there are infinitely many deadlock-generating initial states, the set of corresponding walks is also infinite. Each of these walks can be decomposed into a sequence of alternating simple cycles and acyclic simple paths:
σ = τ1(θ1)k1 τ2(θ2)k2 . . . τn−1(θn−1)kn−1 τn.
Note that this decomposition is not unique: ababa can be considered both as (ab)2a and a(ba)2. To fix ideas, we only consider “decomposition from the right to the left,” so a(ba)2.
Let us show that among these walks there is a walk with a negative last cycle θn−1. Indeed, if the last cycle is positive (or neutral) with an effect x, we can consider a larger initial resource r0 + x ∗ kn−1 and a shorter walk σ0 = τ1(θ1)k1 τ2(θ2)k2 . . . τn−1τn, having the same ending — a deadlock. Now, the new walk σ0 can be decomposed into simple cycles and simple paths, then the last cycle, if it is positive, can be removed by increasing the initial resource, and so on. At the end of this process we will obtain either a walk with a negative “last cycle” or a completely acyclic walk (simple path from i to c). There are only finitely many acyclic paths in the graph, but infinitely many deadlock-generating initial markings (and hence deadlock-generating walks from i to c), so we necessarily obtain a walk with a negative last cycle.
Consider such a deadlock-walk σ00, ending with a suffix θkτ, where θ is a negative cycle and τ is acyclic. Let θ = c1c2 . . . ci . . . cmc1, where ci is a negative generator (from Lemma 2 such ci always exists). The path (ci . . . cmc1)τ is simple (remember that we decompose “from the right to the left” and hence θτ cannot contain cycles other than θ). Since the final state of the whole walk σ00 is (c|r), for any suffix φ of σ00 we have
Eff (φ)
Supp(φ) ≤ r.
It holds for (ci . . . cnc1)τ as well. But this is a simple path that leads from a negative generator to a deadlock control state – Q.E.D.
A result similar to Th. 2 is valid for livelocks: Theorem 3. An unmarked 1-dim RWF-net is not sound with livelocks iff there exist a livelock state (c|r), a negative generator q and a simple path q →σ c such that Eff (σ) Supp(σ) ≤ r.
Proof. Similar to Th. 2.
Corollary 3. Soundness is decidable for unmarked 1-dim RWF-nets. Proof. All simple (negative) cycles can be found by Tarjan algorithm, deadlock and livelock states — by searching for states, satisfiyng Prop. 4 and Prop. 6 respectively. The set of simple paths is finite (and easily computable). 4.4
Computability of a minimal sound resource Now we propose a plain (and hence, may be, not the most effective) algorithm for computing the minimal resource r such that (N, i|r) is sound: one tests soundness for incremented values of r until success. Note that this method can be applied only to sound nets, while soundness of the unmarked net can be checked with the algorithm given in Cor. 3. 5
In this paper we have investigated the soundness property for workflow nets with one (unbounded) resource place. We have proved that soundness is decidable for marked and unmarked nets, and that the minimal sound resource can be effectively computed.
Our decision algorithms use the reduction to the reachability problem for unbounded Petri nets and hence cannot be considered efficient. However, the inefficiency could be unavoidable, since RWF-nets are expressively rather close to ordinary Petri nets (VASS).
Further research will concern decidability of soundness for the general case of RWF-nets. It is also quite interesting to apply some alternative notions of soundness to our infinite-state workflow nets. The so-called relaxed soundness is of a particular interest. Relaxed soundness has been proposed as a weaker than soundness property.
Some other interesting variants of soundness property are k-soundness,
generalized and structural soundness [
The authors would like to thank the anonymous reviewers for their helpful comments.
Proof of Proposition 1.
net (Nc, i) be not sound. Then there exists a marking c ∈ R(Nc, i), such that either the final marking o is not reachable from c, or o ∈ c and c 6= {o}.
Since for the control subnet the control marking c is reachable from the initial marking i via some sequence of firings, we can always take a resource s, sufficiently large to support the same sequence of firings for (N, i|r + s) and to reach the same control state c. If for the control subnet the final state was not reachable from c, then adding resource places can’t make it reachable for the net with resources, i. e. for (N, i|r + s), in contradiction with the soundness of (N, i|r). If, otherwise, o ∈ c and c 6= {o}, then we also obtain a contradiction with the soundness of (N, i|r), since the control state c is reachable for (N, i|r + s). Proof of Proposition 2.
(1) Similarly to the proof of the Proposition 1 we can always take a sufficiently large initial resource r + s.
(2) Suppose this is not true. Assume that for some c1, c2 ∈ C(N ) we have c2 = c1 +c0 for some c0 6= ∅. From the first statement of this proposition it follows that there exist resources r1 and r2 s. t. RWF-nets (N, c1|r1) and (N, c2|r2) are sound. Then nets (N, c1|r1 +r2) and (N, c2|r1 +r2) are also sound. Thus the final marking o|r0 is reachable from the marking c1|r1 + r2, and (due to monotonicity property of Petri nets) the marking o + c0|r0 is reachable from the larger marking c2|r1 + r2 — contradiction with the soundness for RWF-net (N, c2|r1 + r2).