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 [1,2], is used.

In the context of WF-nets a crucial correctness criterion is soundness [1,3]. We say that a workflow case execution terminates properly, iff its firing sequence (starting from the initial marking with a single token in the initial place) terminates with a single token in the final place (i.e. there are no "garbage" tokens after the termination). A model is called sound iff a process can terminate properly starting from any reachable marking. Soundness of WF-nets is decidable [1]. Moreover, a number of decidable variations of soundness are established, for example, k-soundness [9], structural soundness [14] and soundness of nested models [11].

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 [5,6] a specific class of WFR-nets with decidable soundness is studied. In [10,13] a more general class of Resource-Constrained Workflow Nets (RCWFnets) is defined. Informally, the authors impose two constraints on resources. First, they require that all resources that are initially available are available again after terminating of all cases. Second, they also require that for any reachable marking, the number of available resources does not override the number of initially available resources.

In [10] it is proven that for RCWF-nets with a single resource type soundness can be effectively checked in polynomial time. In [13] it is proven that soundness is also decidable in general case (by reducing to the home-space problem). 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 [8] we defined a notion of WF-nets with resources (RWF-nets). RWF-nets extend RCWF-nets from [10] in such a way that resources can be generated or consumed during a process execution without any restrictions (cf. [7]). For RWF-nets we defined notions of resources and controlled resources and studied the problem of soundnesspreserving resource replacement (this problem is important for adaptive workflows).

Unfortunately, even sound RWF-nets are not bounded in general, hence existing soundness checking algorithms cannot be applied here. In [8] the decidability of soundness for RFW-nets was declared as an open problem.

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.

Let S be a finite set. A multiset m over a set S is a mapping m : S → Nat, where Nat is the set of natural numbers (including zero), i. e. a multiset may contain several copies of the same element.

For two multisets m, m we write m ⊆ m iff ∀s ∈ S : m(s) ≤ m (s) (the inclusion relation). The sum, the union and the subtraction of two multisets m and m are defined as usual: ∀s ∈ 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.

For a transition t ∈ T an arc (x, t) is called an input arc, and an arc (t, x)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

For a Petri net N by R(N, M 0 ) we denote the set of all markings reachable from its initial marking M 0 .

In Petri nets with resources we divide Petri net places into control and resource ones.

Definition 1. A Petri net with resources is a tuple N = (P c , P r , T, F c , F r ), where -P c is a finite set of control places; -P r is a finite set of resource places,

Note that all transitions are necessarily linked to control places -this guarantees the absence of "uncontrolled" 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(P c ) and r ∈ M(P r ), we write c|r.

Definition 2. For a net N a resource is a multiset over P r . A controlled resource is a multiset over P c ∪ P r .

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. Definition 3. A Petri net with resources N is called a WF-net with resources (RWF-net) iff 1. There is one source place i ∈ P c and one sink place o ∈ P c s. t.

Every node from P c ∪ T is on a path from i to o, and this path consists of nodes from P c ∪ T.

Fig. 2 represents an example of a RWF-net, where resource places r 1 and r 2 are depicted by ovals, resource arcs -by dotted arrows.

Every RWF-net N = (P c , P r , T, F c , F r ) contains its control subnet N c = (P c , T, F c ), which forms a RWF-net with the empty set of resources.

A marked net is a net together with some initial marking.

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 [10]. We do not forbid creating and spending of resources. Thus, in RWF-nets resources may be produced and consumed during a process execution. This implies the possible unboundedness of sound RWF-nets.

The following statement is analogous to Lemma 5 in [10].

Proposition 1. [7] If a marked RWF-net (N, i|r) is sound, then its control subnet N c with the initial marking i is also sound.

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 N c , i. e. C(N ) = R(N c , i). The proof of this proposition is given in the Appendix. ¡ ¢ Fig. 3. RWF-net with a sound control subnet, which is not sound for any resource.

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). 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.

Let N = (P c , P r , T, F c , F r ) be an RWF-net with P r = {p r }, 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.

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 (c 1 , c 2 ) of control states, where c 1 t → c 2 . 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 p r by δ(t), a negative δ(t) means that t is enabled in a state (c|r) iff r(p r ) ≥ |δ(t)|, and that the firing of t decrements the resource by |δ(t)|. Formally,

The value δ(t) is called an effect of t (denoted Eff (t)). Note that for simplicity we exclude loops, when both F r (p r , t) > 0 and F r (t, p r ) > 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:

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. [4]) or, alternatively, a 1-dim Vector Addition System with States (VASS [12]) with a specific workflow structure: one source state, one sink state, and every state is reachable from the source state, as well as the sink is reachable from every state. Note that the control automaton Aut(N ) is behaviorally equivalent to N in the branchingtime semantics.

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:

where denotes the truncated subtraction. 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 → c , such that δ(t) < −r.

Proof. Straightforward, since the control subnet of RWF-net N is sound. Proposition 7. The set of livelocks is finite.

Proof. First note that if (c|r), (c|r + x) ∈ L with x > 0 then L is not a livelock. Indeed, in this case the transition sequence (c|r) σ → (c|r + x) corresponds to a 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. 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 [14].

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 1-dim RWF-net (N, i|r) is sound iff neither deadlocks nor livelocks are reachable 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.

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.

Proof. (⇐) It is sufficient to show that for any (large enough) initial resource r 0 there exists a larger initial resource r 0 + x, such that a deadlock is reachable from (i|r 0 + x).

Consider an arbitrary (large enough) initial resource r 0 s.t.

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 θ = qc 1 . . . c j q be a simple negative cycle with generator q, i.e. Supp(θ) = −Eff (θ). Denote z = s mod Supp(θ) and consider a larger initial resource r 0 + z + Supp(σ).

We have i|r 0 + z + 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.

The number of deadlock states is finite, hence some deadlock state (c|r) is reachable from an infinite number of different initial states (initial resource values).

Every transition sequence σ = t 1 .t 2 . . . . .t n from (i|r 0 ) 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:

Note that this decomposition is not unique: ababa can be considered both as (ab) 2 a 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 r 0 + x * k n−1 and a shorter walk

having the same ending -a deadlock. Now, the new walk σ 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 σ , ending with a suffix θ k τ, where θ is a negative cycle and τ is acyclic. Let θ = c 1 c 2 . . . c i . . . c m c 1 , where c i is a negative generator (from Lemma 2 such c i always exists). The path (c i . . . c m c 1 )τ 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 σ is (c|r), for any suffix φ of σ we have Eff (φ) Supp(φ) ≤ r.

It holds for (c i . . . c n c 1 )τ 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).

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.

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 [3].

Proof of Proposition 1.

The proof is by contradiction. Let (N, i|r) be a sound RWF-net and let the net (N c , i) be not sound. Then there exists a marking c ∈ R(N c , i), such that either the final marking o is not reachable from c, or o ∈ c and c = {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 = {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 c 1 , c 2 ∈ C(N ) we have c 2 = c 1 +c for some c = ∅. From the first statement of this proposition it follows that there exist resources r 1 and r 2 s. t. RWF-nets (N, c 1 |r 1 ) and (N, c 2 |r 2 ) are sound. Then nets (N, c 1 |r 1 +r 2 ) and (N, c 2 |r 1 +r 2 ) are also sound. Thus the final marking o|r is reachable from the marking c 1 |r 1 + r 2 , and (due to monotonicity property of Petri nets) the marking o + c |r is reachable from the larger marking c 2 |r 1 + r 2 -contradiction with the soundness for RWF-net (N, c 2 |r 1 + r 2 ).