Jurriaan Rot
email: jrot@liacs.nl

Frank De Boer

Marcello Bonsangue
email: marcello@liacs.nl

Unbounded Allocation in Bounded Heaps

des établissements d'enseignement et de recherche français ou étrangers, des laboratoires publics ou privés.

Introduction

In this paper we investigate the interplay between dynamic creation of objects and recursion. To this end we introduce a core programming language which features dynamic object creation, global variables, static scope and recursive methods with local variables, but which does not include (abstract) pointers. In order to focus on the main issue of dynamic object creation in the context of recursion, we further restrict the data types to that of objects. Other finite data domains could have been added without problem, but would have increased the complexity of the model without strengthening our main result.

We first define a concrete operational semantics for our language based on a standard implementation of recursion using a stack. This semantics uses an explicit representation of objects which immediately gives rise to an infinite name space because an unbounded number of objects can be stored on the stack using local variables. Consequently, decidability results for pushdown systems (for which the stack alphabet is finite) and existing model checking techniques of pushdown systems against temporal formulas [START_REF] Bouajjani | Reachability analysis of pushdown automata: Application to model-checking[END_REF] are not applicable.

Our solution is to abstract from the concrete representation of objects by representing states, i.e., assignments of objects to the program variables, symbolically as conjunctions of equations over the program variables, identifying those variables which refer to the same object. In this symbolic setting we show how to describe the basic computation steps, e.g., object allocation, recursive calls and returns, in terms of a strongest postcondition semantics. The resulting symbolic semantics can be modeled formally as a pushdown system with a finite set of control states and a finite stack alphabet. Our main technical result is a rigorous proof of the equivalence between the concrete and the symbolic semantics.

Adding (abstract) pointers however allows to program dynamically linked data structures, like lists or trees, and allows the simulation of a 2-counter machine. As such, reachability is undecidable [START_REF] Minsky | Computation: Finite and Infinite Machines[END_REF] for this extended language. We show in this paper that if a (recursive) program with pointers gives rise to computations in which the number of reachable objects in the heap is bounded a priori, then it can be simulated by a program without pointers. Therefore, in the context of bounded visible heaps, (recursive) programs with pointers are no more expressive than programs without them.

Related work. Our main contribution is a new symbolic semantics and a corresponding direct proof of decidability of a class of recursive programs which feature dynamic creation and unbounded allocation of objects, but do not include (abstract) pointers. The decidability of our core language itself follows from the general result of [START_REF] Bouajjani | Context-Bounded Analysis of Multithreaded Programs with Dynamic Linked Structures[END_REF] for recursive programs with (abstract) pointers which generate only bounded visible heaps. On the other hand, the general result of [START_REF] Bouajjani | Context-Bounded Analysis of Multithreaded Programs with Dynamic Linked Structures[END_REF] concerning pointers can be derived from our basic decidability result by our simulation of programs with pointers. In fact, our simulation shows that restricting to bounded (visible) heaps basically boils down to restricting to programs without pointers! Moreover, the general result of [START_REF] Bouajjani | Context-Bounded Analysis of Multithreaded Programs with Dynamic Linked Structures[END_REF] is based on a complex mechanism for "merging" upon the return of a method the local part of the "old" heap (the heap before the call) and the current heap (see [START_REF] Rot | Interacting via the Heap in the Presence of Recursion[END_REF] for a more extensive discussion). This is because a reuse is required in order to model the semantics as a pushdown system with a finite stack alphabet (as explained above, by means of the local variables an unbounded number of objects can be stacked). In contrast, in the absence of pointers in our strongest postcondition semantics such name clashes are resolved symbolically by a simple substitution of fresh variables. The underlying equational logic then allows for a simple elimination of these implicitly existentially quantified variables.

More recently, [START_REF] Abdulla | Podelsk Push-Down Automata with Gap-Order Constraints[END_REF] introduces an algorithm for reachability in pushdown automata with gap-ordered constraints, a model which allows to represent the behavior of our language. The symbolic semantics introduced in this paper is based on ordinary pushdown systems and therefore we can use standard algorithms for model checking [START_REF] Bouajjani | Reachability analysis of pushdown automata: Application to model-checking[END_REF]. Furthermore, it is similar in spirit to the one used in high level allocation Büchi automata [START_REF] Distefano | Who is Pointing When to Whom?[END_REF] for model checking of a possibly unbounded number of objects with pointers but for a language with a restricted form of recursion (tail recursion) and no block structure. Full recursion, but with a fixed-size number of objects is instead considered in jMoped [START_REF] Esparza | A BDD-based model checker for recursive programs[END_REF], using a pushdown structure to generate an infinite state system. Similar and even stronger restrictions limiting either size of heap and stack, or the number of objects are considered by current model checkers for object-oriented languages, such as Java Path Finder [START_REF] Havelund | Model checking Java programs using Java PathFinder[END_REF], JCAT [START_REF] Demartini | A deadlock detection tool for concurrent Java programs[END_REF], Bandera [START_REF] Corbett | Bandera: Extracting finite-state models from Java source code[END_REF] (possibly combined with the Symbolic Analysis Laboratory model checker [START_REF] Park | Java Model Checking[END_REF]).

Plan of the paper. In Section 2 we introduce the syntax of our language and give an informal description of its semantics. Section 3 provides a concrete execution model using a transition system with infinite states and a symbolic model based on pushdown systems. We end the section by studying the relationship between these two models. In Section 4 we discuss the extension with pointers. Finally, the last section discusses some possible future research and tool development.

A core language for allocation

We introduce a core programming language that focuses on dynamic allocation, global and local variables, and recursive procedures. To simplify the presentation it is restricted to a single data structure, that of objects. Objects can be dynamically allocated and referenced. A program consists of a finite set of procedures, each acting on some global and local state. Procedures can store object references in global or local variables, compare them, and call other procedures.

We assume a finite set of program variables V ranged over by x, y, v, w such that V = G ∪ L, where G is a set of global variables {g 1 , g 2 , . . . , g n } and L is a set of local variables {l 1 , l 2 , . . . , l m }, with G and L disjoint. We often write l for the sequence of all local variables. We assume a distinguished element nil ∈ G, used as a constant to refer to the undefined object. For a finite set P of procedure names {p 0 , . . . , p k }, a program is a set of procedure declarations of the form p i :: B i , where B i , denoting the body of the procedure p i , is a statement defined by the following grammar:

B ::= x := y | x := new | call p | B; B | [x = y]B | [x = y]B | B + B
The language is statically scoped. The assignment statement x := y assigns the reference stored in y (if any) to x. The statement x := new allocates a new object that will be referenced by the program variable x. As for the ordinary assignment, the old value of x is lost. For this reason we will consider only programs in which the variable nil does not appear at the left-hand side of an assignment or allocation statement. Sequential composition B 1 ; B 2 , guarded statements [x = y]B and [x = y]B, and nondeterministic choice B 1 + B 2 have the standard interpretation. Execution of a procedure call call p consists of the execution of the associated body B with its local variables initialized to nil. Upon termination of the body B of a procedure the previous local state (from which the procedure has been called) is restored.

Example 1. As a basic example of storing an unbounded number of objects, consider the procedure p :: l := new; ((call p; g 1 := l) + g 2 := l) A call to p allocates a number of objects not bounded a-priori and stores them in the several copies of the local variable l in the call-stack. The global variable g 2 refers to the last allocated object (or nil), whereas g 1 refers to the first one (or nil). Note that if all variables are initially nil, then g 1 = g 2 eventually holds if and only if the program terminates.

The usual while, skip, if-then-else statements, and more general boolean expressions, can easily be encoded in this sequential setting. Procedures with call-by-value parameters and return values can also be modeled using assignments to global variables.

A concrete and a symbolic semantics

In this section, we introduce a semantics of the programming language which is defined in terms of an explicit representation of objects by natural numbers. This representation allows a simple implementation of object allocation. A program state is a variable assignment s : V -→ N, where 0 is used to represent the "undefined" object, and thus we assume s(nil) = 0. To model allocation we distinguish a global "system" variable cnt which is used as a counter, and is not used by programs. We implicitly assume that s(x) < s(cnt), for every state s and variable x different from cnt. Note that this implies that s(cnt) = 0, as this is the value of nil.

A configuration of a program is a tuple s, S where s is the current program state and S is a stack of statements and stored return states. The current statement to be executed is on the top of the stack. An execution step of a program is a transition from a configuration C to a configuration C , denoted by C -→ C . A computation is a (possibly infinite) sequence C 1 -→ C 2 -→ . . . of execution steps. The possible execution steps are given below. For modeling function updates we use multiple assignments of the form f [x 1 , . . . , x k := y 1 , . . . , y k ], where x i and x j are distinct elements of the domain of f for i = j, and all y i 's are in the codomain of f . It denotes the function mapping x i to y i if i ∈ {1, . . . , k}, and otherwise x is mapped to the old value f (x). The head of a stack is separated from the tail by means of the right-associative operator •: for example, B • S is a stack consisting a statement B and tail S, whereas s • S is a stack consisting a state s as head and tail S.

When an assignment is the current statement to be executed, then the current program state is updated accordingly. The tail of the stack is not changed.

s, x := y • S -→ s[x := s(y)], S
Dynamic allocation is similar to an assignment, but it uses the system variable cnt, which is now increased.

s, x := new • S -→ s[x, cnt := s(cnt), s(cnt) + 1], S
The execution of the sequential composition of two statements updates the stack so that they are executed in the right order.

s, B 1 ; B 2 • S -→ s, B 1 • B 2 • S
Guarded statements are executed only if the current program state satisfy their respective conditions, otherwise they block.

s(x) = s(y) s, [x = y]B • S -→ s, B • S s(x) = s(y) s, [x = y]B • S -→ s, B • S
A non-deterministic choice updates the stack so that only one of the two statements becomes the current one.

s, B i • S -→ C s, B 1 + B 2 • S -→ C (i ∈ {1, 2})
In a procedure call the entire current state is pushed onto the stack so that the local variables can be restored when the procedure returns (we push the entire state only for notational convenience, to avoid irrelevant case distinctions). In the new current state all local variables are set to 0 and the current program on the stack becomes the body of the called procedure.

s, call p i • S -→ s[ l := 0], B i • s • S
Here B i is the body of p i , l denotes the sequence of local variables l 1 , . . . , l m and 0 is a sequence of length m of 0's, where m is the number of local variables.

When the top of the stack is a program state, a procedure return is executed. The local variables are restored using the state stored on the stack.

s, s • S -→ s[ l := s ( l)], S
Again, l denotes the sequence of local variables l 1 , . . . , l m , while s ( l) denotes the sequence of old values s (l 1 ), . . . , s (l m ).

A symbolic semantics

The concrete semantics introduced in the previous section clearly cannot be modeled as a pushdown system because it uses the infinite set of natural numbers to represent objects. However, at any moment of a computation, only finitely many objects are referenced by program variables. In this section we exploit this basic fact and represent a program state symbolically as a finite conjunction of equalities, identifying program variables referring to the same object. Subsequently, we define program steps based on a strongest postcondition calculus, which requires the introduction of fresh global variables for assignments. It suffices to assume a distinct logical variable z for each variable in V . We denote by Var the set of program variables V extended with their logical variables. Note that Var is finite. A symbolic state ϕ is a finite conjunction of equalities as given by the grammar

ϕ ::= x = y | ϕ ∧ ϕ
where x and y range over Var . A symbolic state ϕ gives rise to a relation r(ϕ) ⊆ Var × Var , inductively defined by

r(x = y) = {(x, y)} r(ϕ 1 ∧ ϕ 2 ) = r(ϕ 1 ) ∪ r(ϕ 2 ) .
Next we let r * (ϕ) ⊆ Var × Var denote the reflexive, symmetric and transitive closure of r(ϕ). This way, any symbolic state ϕ gives rise to a partioning of Var . We define ϕ |= x = y if and only if (x, y) ∈ r * (ϕ), and extend it to disequalities by the closed world assumption, i.e., ϕ |= x = y iff ϕ |= x = y.

We describe the effect of a basic statement S on a symbolic state ϕ in terms of its strongest postcondition SP (S, ϕ), i.e., SP (S, ϕ) will be the strongest state formula such that whenever we start from a program state satisfying ϕ (under the obvious satisfaction relation), after executing S the resulting state satisfies SP (S, ϕ). We denote by t[z/x] the syntactic substitution of x in t by a corresponding fresh (logical) variable z.

SP (x := new, ϕ) = ϕ[z/x] SP (x := y, ϕ) = ϕ[z/x] ∧ x = (y[z/x])
Note that z in the above two clauses represents the "old" value of x. In an assignment statement x := y as well as in in a dynamic allocation x := new we have for all variables v, w (syntactically) different from x that ϕ |= v = w if and only if SP (x := y, ϕ) |= v = w. Further, for dynamic allocation, SP (x := new, ϕ) |= x = y if and only if x and y are the same variable (and thus by the closed world assumption SP (x := new, ϕ) |= x = y, for every y different from x).

For procedure calls, we assume without loss of generality that for each global variable g ∈ G there exists a unique local variable g ∈ L which does not occur in the given program. These so-called freeze variables are used to represent locally the global variables before a call. This information is needed to relate logically the state before the call and the return state. In the strongest postcondition of a procedure call we model logically the initialization of the local program variables (thus not the freeze variables) to nil, and the assignment to each freeze variable g of the value of its corresponding global variable g:

SP (call p, ϕ) = ϕ[z/ l] ∧ g∈G (g = g ) ∧ l∈L l = nil ,
where z is a sequence of logical variables corresponding to a sequence l of all local variables appearing in ϕ; z is used to represent the old values of l. L is the set of local variables that are not freeze variables.

To describe the strongest postcondition of the return of a procedure we introduce an auxiliary statement "ret ψ" for each symbolic state ψ. The global variables in ψ thus represent the old values of the global variables before the call. On the other hand, in the current symbolic state ϕ the old equalities between the global variables before the call are represented by their corresponding freeze variables. We can identify these simply by replacing the freeze variables in ϕ and the global variables in ψ by the same logical variables. This explains the main idea underlying the following rule:

SP (ret ψ, ϕ) = ϕ[z/ḡ ][z / l] ∧ ψ[z/ḡ]
where z and z are disjoint sequences of fresh logical variables, ḡ is the sequence of freeze variables and l is the sequence of all local variables. So in ϕ, first the freeze variables are renamed to z, and then the other local variables in ϕ, which are no longer valid, are renamed away into fresh logical variables z .

We use the above postcondition calculus to define a symbolic semantics for our programs. An (abstract) configuration of a program is a pair ϕ, S where ϕ is a symbolic state restricted to the program variables V and S is a stack of statements and symbolic states also restricted to the program variables V . This restriction is justified because logical variables are implicitly existentially quantified and as such can be eliminated (in each step): for any symbolic state ϕ we can construct a formula ϕ ↓ V which only contains variables in V such that r * (ϕ) restricted to V × V equals r * (ϕ ↓ V ). Now for dynamic allocation and assignment statements we lift the strongest postconditions defined above to transitions as follows:

ϕ, B • S -→ SP (B, ϕ) ↓ V , S (1)
where B is either x := new or x := y for some program variables x and y.

The transition rules for sequential composition, non-deterministic choice and guarded statements are similar to the corresponding transition rules in the concrete semantics. As an illustration, we give below the two rules for guarded statements:

ϕ |= x = y ϕ, [x = y]B • S -→ ϕ, B • S ϕ |= x = y ϕ, [x = y]B • S -→ ϕ, B • S (2)
On a procedure call p i , we push the procedure body and current state onto the stack:

ϕ, call p i • S → SP (call p i , ϕ) ↓ V , B i • ϕ • S . (3)
The transition for procedure return is similar to that of an assignment:

ϕ, ψ • S → SP (ret ψ, ϕ) ↓ V , S . (4)
Example 2. As a simple example of a symbolic computation, consider the procedure declaration p :: l := new where l is a local variable. Let g be some global variable. We will consider the execution of the statement call p starting from a symbolic state where g equals l. During the execution of p, l is assigned a new object; however, since l is a local variable, it is restored when the procedure returns, so then we should again have that g is equal to l. We restrict the above definition of the strongest postcondition of a procedure call to the local variable l and some global variable g; then SP (call p, l = g) is

z = g ∧ g = g ∧ l = nil ,
and thus by eliminating the logical variable z we derive the transition step

l = g, call p -→ g = g ∧ l = nil, l := new • l = g .
Next we compute SP (l := new, g = g ∧ l = nil):

g = g ∧ z = nil ,
and again eliminating the logical variable z we now derive the transition

g = g ∧ l = nil, l := new • l = g -→ g = g , l = g .
As above, restricting the above definition of SP (ret l = g, g = g ) to the local variable l and the global variable g, we obtain

g = z ∧ l = z .
Finally, eliminating the logical variable z we arrive at the final transition

g = g , l = g -→ l = g, ,
where indeed l and g are again identified.

The above semantics gives rise to a finite pushdown system. A pushdown system is a triple P = (Q, Γ, ∆) where Q is a finite set of control locations, Γ is a finite stack alphabet, and

∆ ⊆ (Q × Γ ) × (Q × Γ * ) is a finite set of productions.
A transition (q, γ, q , γ) is enabled if control is at location q and γ is at the top of the stack -then control can move to location q by replacing γ by the possible empty word of stack symbols γ.

In our case, for a given program p 1 :: B 1 , . . . , p n :: B n , the set of control locations is given by the set of state formulas restricted to V . In order to define the stack alphabet we introduce the finite set k i=1 cl(B i ) of possible reachable statements where the closure of a statement B, denoted as cl(B), is defined as follows:

cl(A) = {A} cl([x = y]B) = {[x = y]B} ∪ cl(B) cl(B 1 ; B 2 ) = {B 1 ; B 2 } ∪ cl(B 1 ) ∪ cl(B 2 ) cl([x = y]B) = {[x = y]B} ∪ cl(B) cl(B 1 + B 2 ) = {B 1 + B 2 } ∪ cl(B 1 ) ∪ cl(B 2 )
where A is an assignment, an allocation or a procedure call. The stack alphabet Γ is then defined by the union of the abstract state space and the above set of possible reachable statements. Finally, it is straightforward to transform the rules of the above semantics into rules of a pushdown system, simply by removing the common stack tail from the left-and righthand sides. For a pushdown system both the halting problem and reachability are decidable. In fact, it is possible to model check pushdown systems against linear-time or branching-time temporal formulas. For linear-time temporal formulas the complexity is even of the same order as for finite state systems [START_REF] Bouajjani | Reachability analysis of pushdown automata: Application to model-checking[END_REF][START_REF] Esparza | A BDD-based model checker for recursive programs[END_REF].

Correctness of the symbolic semantics

In this section we show that the concrete and the abstract semantics are equivalent. First we identify the relevant properties of the concrete semantics satisfied by any reachable configuration. Basically, (1) on a procedure call, all local variables must be initialized to 0. Thus if an object is referenced by a variable in the current state s and in a stacked state s , then there must be a global variable referencing it in that stacked state s . Moreover (2) the system variable cnt is greater than all objects currently referenced by variables stored somewhere in the stack. Formally this is the content of the next definition. Definition 3. A stack S is proper if either S is the empty stack, or S = B • S for some statement B and proper stack S , or S = s • S for some program state s and proper stack S such that for any state s occurring in S :

(1) s(V ) ∩ s (V ) ⊆ s (G), (2) ∀v ∈ V.s(cnt) > s (v). A configuration s, S is proper if s • S is proper.
Properness is preserved by all computation steps: Lemma 4. If s, S is proper and s, S → s , S then s , S is proper.

For example, the configuration s, p 0 is proper, where p 0 is the main procedure name, and s is the state mapping cnt to 1 and all other variables (including nil) to 0. From the above Lemma, any configuration in a computation starting from this initial one is a proper configuration.

Next we give some basic properties of the concrete semantics of the procedure return. Informally, global variables are not affected by a procedure returns, and local variables get the values they had before the procedure call.

Lemma 5. If s, s • S -→ s r , S then for every x, y ∈ V :

1. x, y ∈ G ⇒ (s r (x) = s r (y) iff s(x) = s(y)) 2. x, y ∈ L ⇒ (s r (x) = s r (y) iff s (x) = s (y)) 3. x ∈ G, y ∈ L ⇒ (s r (x) = s r (y) iff s(x) = s (y))
We proceed with the following relevant properties of the symbolic semantics. First we make precise what is the relation between global variables in the caller's state ψ and freeze variables in the callee's state ϕ: freeze variables can be equal if and only if their corresponding global variables were equal in the first place. Definition 6. We define ψ ϕ iff for any two globals g 1 , g 2 ∈ G,

ϕ |= g 1 = g 2 iff ψ |= g 1 = g 2
The definition of properness of abstract configurations is based on the above. Definition 7. A stack S (of symbolic states and statements) is proper if either S is the empty stack, or S = B • S for some statement B and proper stack S , or S = ϕ • S for some symbolic state ϕ and proper stack S such that for the topmost state ϕ occurring in S , if it exists: ϕ ϕ. An abstract configuration ϕ, S is proper if ϕ • S is proper.

Properness of abstract configurations is preserved by all computation steps:

Lemma 8. If ϕ, S is proper and ϕ, S → ϕ , S then ϕ , S is proper.

We state the main properties of the procedure return in the abstract semantics. Lemma 9. If ϕ, ψ • S is proper, and ϕ, ψ • S -→ ϕ r , S then for every x, y ∈ V :

1. x, y ∈ G implies ϕ r |= x = y iff ϕ |= x = y, 2. x, y ∈ L implies ϕ r |= x = y iff ψ |= x = y, 3. x ∈ G, y ∈ L implies ϕ r |= x = y iff ∃g ∈ G s.t. ψ |= y = g and ϕ |= x = g
In order to prove the equivalence between the symbolic semantics and the concrete semantics, we extend the latter so that each procedure body starts with the initialization of the freeze variables to their corresponding global variables. Note that this does not affect the behaviour of a program, since freeze variables by assumption do not occur in it.

Let s be a concrete state, and ϕ a symbolic state. We define s ∼ ϕ if and only if for all variables x, y ∈ V : s(x) = s(y) iff ϕ |= x = y . Next this relation is extended to stacks S of statements and (concrete) program states and stacks S of statements and symbolic states. We define S ∼ S iff S and S are proper stacks, and one of the following cases hold: In our setting a bisimulation is a relation R, between concrete-and abstract configurations, such that for every (C, D) ∈ R: if C -→ C then there is a configuration D such that D -→ D and (C , D ) ∈ R, and vice versa; where C -→ C is a transition between concrete configurations, given by the concrete semantics (augmented with the initialization of freeze variables), and D -→ D is a transition between abstract configurations, given by the symbolic semantics. Our main result states the equivalence between the operational and the symbolic semantics, based on this notion.

Theorem 10. The above relation ∼ between proper configurations is a (strong) bisimulation. Proof. Suppose s, S ∼ ϕ, S . The proof proceeds by cases on top of the stacks, i.e., the program constructs; we only treat the case of procedure return. In this case S = s • S and S = ψ • S for some s and ψ, and there are s r and ϕ r such that s, s • S -→ s r , S and ϕ, ψ • S -→ ϕ r , S Note that we have s ∼ ψ, s ∼ ϕ and S ∼ S by assumption. Further note that we can apply Lemma 9 since by assumption ϕ, S is proper. We must show that s r ∼ ϕ r holds. Let x, y ∈ V . We distinguish three cases:

1. x, y ∈ G (both global variables):

s r (x) = s r (y) iff s(x) = s(y) Lemma 5.1 iff ϕ |= x = y assumption iff ϕ r |= x = y Lemma 9.1 2.
x, y ∈ L (both local variables):

s r (x) = s r (y) iff s (x) = s (y) Lemma 5.2 iff ψ |= x = y assumption iff ϕ r |= x = y Lemma 9.2 3.
x ∈ G and y ∈ L. Recall that we have augmented the concrete semantics with the initialization of the freeze variables. It is easy to see that as a consequence s(g ) = s (g) holds, which we will use below.

s r (x) = s r (y) iff s(x) = s (y) Lemma 5.3 iff ∃g ∈ G.s(x) = s (g) and s (g) = s (y) properness iff ∃g ∈ G.s(x) = s(g ) and s (g) = s (y) above argument iff ∃g ∈ G.ϕ |= x = g and ψ |= g = y assumption iff ϕ |= x = y Lemma 9.3

Adding pointers

In this section we extend our programming language with fields and corresponding updates for modeling linked object structures. In particular we investigate kbounded heaps, in which the number of reachable objects is at most k. This notion is extended to k-bounded programs, in which during execution, the heap is always k-bounded. We show that every k-bounded program P including fields can be rewritten into a program P without fields and equivalent to P . The language of Section 2 is extended with statements x := y.f and x.f := y, where f ranges over a finite set of (pointer) fields F . Note that the only type of field is that of a pointer to another object. Informally, the statement x := y.f is a basic assignment, updating x to point to (the location referred to by) y.f . Field update x.f := y changes to y the field of the object to which x refers via the field f . These two basic operations are sufficient; more general expressions and updates can be encoded. For example, a statement

x := y.f i1 .f i2 .f i3 . . . f i k is encoded as x := y.f i1 ; x := x.f i2 ; x := x.f i3 ; . . . ; x := x.f i k .
To give a semantics to this language we introduce a heap H as a pair s, h of a variable assignment s : V → N such that s(nil) = 0, and a field assignment h : F → (N → N) such that for all f , h(f )(0) = 0. We write H(x) for s(x), and

H(f ) for h(f ).
For a set of variables X we denote with R H (X) ⊆ N the set of objects reachable from these variables in H, defined as the least fixpoint of the equation

R H (X) = {H(x) | x ∈ X} ∪ {H(f )(n) | f ∈ F, n ∈ R H (X)}
We abbreviate R H (V ), where as before V denotes the set of program variables, by R H . We denote an assignment to a variable by H[x := n], a global field update by H[f := ρ] with ρ : N → N s.t. ρ(0) = 0, and local field update by

H[f := ρ[n := m]].
We use the standard notation and definition of simultaneous assignments and updates.

A configuration is a tuple H, Γ where H is a heap and Γ is a stack of statements and heaps. We only give the transitions for dynamic allocation, and for assignments of the form x.f := y and x := y.f . All other transitions are similar to the semantics of the language without fields, and are not repeated here. Again we assume a system variable cnt for the implementation of dynamic allocation. On a dynamic allocation all fields of the new object are set to point to 0.

H, x := new • Γ -→ H[x, cnt := H(cnt), H(cnt) + 1][ f := ρ], Γ
where ρ is a sequence such that ρ i = H(f i )[H(x) := 0]. A field update x.f := y is as follows:

H(x) = H(nil) H, x.f := y • Γ -→ H[f := H(f )[H(x) := H(y)], Γ
Finally an assignment of the form x := y.f is as follows:

H(y) = H(nil) H, x := y.f • Γ -→ H[x := H(f )(H(y))], Γ
It is not hard to see that reachability is undecidable for this language. For instance, we can simulate a 2-counter machine [START_REF] Minsky | Computation: Finite and Infinite Machines[END_REF] by using three variables c 1 , c 2 , t and a single field f . An increment of c i is then implemented as a statement t := new; t.f := c i ; c i := t, a decrement is a simple c i := c i .f and we can test for zero by using a guard [c i = nil]. It is thus not possible to devise, in the same fashion as in Section 3, a precise abstraction of the semantics of our extended language for which reachability is decidable.

In [START_REF] Bouajjani | Context-Bounded Analysis of Multithreaded Programs with Dynamic Linked Structures[END_REF] an abstraction of heaps in terms of isomorphic graphs is given, which is applied in a semantics with the property that reachability is decidable for programs in which every heap is k-bounded for some a priori fixed k.

Definition 11. A heap H is k-bounded if |R H | ≤ k. A computation H 1 , Γ 1 → H 2 , Γ 2 → . . . is k-bounded if |R Hi | is k-bounded for all i. A program P with main procedure p 0 is k-bounded if every computation H 0 , p 0 → . . . is k-bounded, for some initial heap H 0 .
We show that k-bounded programs with fields can be simulated by programs without fields in our basic language. We do so by means of a transformation from k-bounded programs to equivalent programs not containing any fields.

We first show how to represent k-bounded heaps using only plain variable assignments of the form s : V → N. To this end let k be a given bound. The correspondence between a k-bounded heap H and a state s is based on an explicit enumeration of the objects in the visible heap, represented by k global variables 1, . . . , k such that s( ī) = s( j), for i = j. Notice that the undefined object 0 is already represented by the variable nil, and as such we have, in fact, a series nil, 1, . . . , k of k + 1 variables to represent k objects, which will turn out to be of technical convenience. Further, we introduce for each i = 1, . . . , k and field f ∈ F a global variable īf which represents H(f )(s( ī)). Without loss of generality we assume that these variables do not appear in the given program. In the sequel we denote by I the set of global variables 1, . . . , k and by V (P ) the (global and local) variables which do occur in P . We next define when a k-bounded heap H is represented by a variable assignment s, denoted by H ≡ s.

Definition 12. Given a k-bounded heap and a variable assignment s we define H ≡ s by 1. s( ī) = s( j) and s( ī) = 0, for i = j, i = 1, . . . , k and j = 1, . . . , k, 2. for every n ∈ R H (V (P )) s.t. n = 0 there is i = 1, . . . , k such that s( ī) = n, 3. H(f )(s( ī))) = s( īf ), for every i = 1, . . . , k and f ∈ F , 4. H(cnt) = s(cnt).

The actual program transformation now is defined in terms of a function t which takes a k-bounded program P with fields and translates it into an equivalent program t(P ) without fields.

For each of the procedures except the initial one, we define t(p i :: B i ) = p i :: t(B i ), where t(B) will be defined by structural induction. We append in front of the initial procedure p 0 :: B 0 a series of allocations and assignments to initialize the representation of the heap: where the for all -construct Π l∈L B is a shorthand for a sequential composition of the statements B l , for l ∈ L, where B l is obtained from B by substituting l for l in B. For a better readability we omit the parenthesis in a for-all construct and assume its scope is clear from the context. The fresh global variables true and false, which are assumed not appear in the given program, will be used to encode boolean values. We proceed to discuss for each of the statements in the language its translation. A simple assignment x := y remains unchanged and the translation of a sequential composition or choice between two statements consists of the sequential composition or choice between the translated statements. Since the conditional statements refer only to plain variables, we simply have

t([x = y]B) = [x = y]t(B).
For an assignment of the form x := y.f , in order to find the variable representation of y.f , we must find the variable ī which represents the object denoted by y.

The variable īf then represents y.f . This search and corresponding assignment is described simply by the following non-deterministic choice:

t(x := y.f ) = Σī ∈I [ ī = y]x := īf .
Note that this "n-ary" non-deterministic choice generalizes binary choice in the usual manner. A field update x.f := y is treated in a similar way:

t(x.f := y) = Σī ∈I [ ī = x] īf := y.
Notice that both for field updates x.f := y and x := y.f , the condition H(x) = H(nil) of the semantic rules are enforced by only considering variables from I, which represent non-null objects.

To simulate a dynamic allocation x := new, we non-deterministically select a variable ī ∈ I which denotes an object that is not reachable from any variables in V (P ). This variable will be (re)used to represent the newly created object assigned to x. Reachability in a k-bounded heap can be implemented by the following statement using for each ī ∈ I a fresh variable īb to indicate that ī is reachable from the variables in X: Further notice that since the undefined object is always reachable by the variable nil, and the heap is k-bounded, there can only be k -1 other reachable objects. So there will always be a representative ī ∈ I of a non-null object which is not reachable, i.e., īb = false after executing the above reachability algorithm. This motivates the following translation of object creation:

t(x := new) = R V (P ) ; Σī ∈I ([ īb = false] ī := new; x := ī; Π f ∈F īf := nil) .
It is worthwhile to note that this translation is based on the reuse of a variable ī ∈ I which in fact can be seen as a canonical representative of those variables which refer to the same object. Finally we consider the case of a procedure call. It is not so difficult to see that upon the return of a procedure call in the translated program some objects which are reachable from the restored local variables may no longer be represented by a global variable ī ∈ I because their representation may have been reused by the creation of new objects. In order to restore the representation of such objects we introduce for each ī ∈ I fresh variables ī ∈ I and ī f , for f ∈ F , which are used to store before the call a copy of the heap (as represented by the variables in I) by the following statement copy = Πī ∈I ( ī := ī; Π f ∈F ī f := īf ) .

After the call we first compute which variables ī ∈ I represent objects which are reachable from the (restored) local variables L(P ) of P in the "old" heap represented by the variables ī ∈ I and ī f , for f ∈ F . Assuming for each variable ī ∈ I an additional fresh variable ī b , this is computed by the statement R L(P ) which is obtained from R L(P ) , as defined above, by replacing simply the variables ī , īf and īb by ī , ī Let =⇒ denote the concrete semantics where the translations of assignments, procedure calls and returns are executed atomically (i.e., in one step).

Theorem 13. Given a program P with fields, let H • Γ ≡ s • S. We have 1. if H, Γ -→ H , Γ then s, S =⇒ s , S , for some s , S such that H • Γ ≡ s • S , and 2. if s, S =⇒ s , S then H, Γ -→ H , Γ , for some H , Γ such that H • Γ ≡ s • S .

Conclusion

The interplay between unbounded allocation of objects and recursion with local variables gives rise to an infinite state space. By representing the state space symbolically, we have shown that reachability, as well as model checking, is decidable. Further, we have shown that adding pointer fields to our core language with the restriction that the number of reachable objects is bounded, does not increase the expressiveness of the language. Our symbolic semantics greatly simplifies the basic mechanism of recursion with local variables in the presence of dynamic object allocation, as is also exemplified by a neat formalization of dynamic deallocation, a feature that is typically problematic in the context of model checking. Consider for example a deallocation statement "del x" that sets x and all of its aliases to nil. Note that this is different from an assignment x := nil, as the latter statement does not affect any alias of x. Symbolically, the effect of a deallocation statement is formalized in terms of its strongest postcondition SP (del x, ϕ) simply as ϕ ∧ x = nil. An equivalent concrete semantics for deallocation is much more complex because the stack may contain variables still referencing deallocated objects and a program has only access to the top of the stack. One way of implementing a concrete semantics of deallocation is by an explicit recording of the deleted objects.

Finally, the symbolic nature of our semantics provides a promising basis for future model checking tool development using, for example, the Maude implementation of rewriting logic.

1 .

 1 S, S are both empty 2. S = B • S and S = B • S for some statement B, and S ∼ S 3. S = s • S , S = ϕ • S , s ∼ ϕ and S ∼ S Finally we lift the relation to proper configurations as follows: s, S ∼ ϕ, S iff s • S ∼ ϕ • S.

p 0 :

 0 : Πī ∈I ( ī := new; Π f ∈F īf := nil; ) true := new; false := new; t(B 0 )

R

  X = Πī ∈I īb := false; Π x∈X Σ k i=1 [ ī = x] īb := true; B k where B denotes the statement Πī ∈I ([ īb = false]skip + [ īb = true]Π f ∈F Σj ∈I [ īf = j] jb := true) and B k denotes the sequential composition of k copies of B. Note that because the visible heap is k-bounded we need to iterate the statement B only k times.

  f and ī b , respectively, for ī ∈ I and f ∈ F . Next we compute by R G(P ) which variables ī ∈ I do not represent objects reachable from the global variables G(P ) of P in the current heap. The statement Rī = b := true; Πj ∈I ([ j = ī ]skip + [ j = ī ]b := false) checks whether the object denoted by ī is already represented by some variable ī ∈ I. If the object denoted by ī is not yet represented the following statement restore = Σj ∈I ([ jb = false] j := ī ; Π f ∈F jf := ī f ; jb := true) restores the representation of ī . Putting the above statements together return = R L(P ) ; R G(P ) ; Πī ∈I Rī ; ([b = false]skip + [b = true]restore) restores upon return the representation of the old local heap by the variables I. Summarizing, we have the following translation of procedure calls: t(call p) = copy; call p; return. In order to state the correctness of the translation in terms of a bisimulation relation we first extend pointwise the (representation) relation H ≡ s to the corresponding stacks: 1. if H ≡ s and Γ ≡ S then H • Γ ≡ s • S, 2. if Γ ≡ S then B • Γ ≡ t(B) • S.

Scientific Research (NWO), CoRE project, dossier number: 612.063.920.

The research of this author has been funded by the Netherlands Organisation for


Elham Ramezani
email: e.ramezani@tue.nl

Natalia Sidorova
email: n.sidorova@tue.nl

Christian Stahl
email: c.stahl@tue.nl

Interval Soundness of Resource-Constrained Workflow Nets: Decidability and Repair

Correctness of workflow design cannot be evaluated by checking the execution for one single instance of the workflow, because instances, even when being independent from the data perspective, depend on each other with respect to the resources they rely on for executing tasks. The resources are shared among the instances of the same workflow; moreover, other workflows can use the same resources. Therefore, we enrich the workflow model with the model of its environment that captures the resource perspective. This allows us to investigate the verification of workflows extended with resources in a more general setting than it was previously done. We focus on the soundness property, which means the ability to terminate properly from any reachable state of the system, for every instance of the system. We show the decision procedure for soundness and how to repair a workflow that is unsound from the resource perspective by synthesizing a controller such that the composition of the workflow and the controller is sound by design.

Introduction

A workflow consists of a set of coordinated tasks describing a flow of work for accomplishing some business process within an organization. The occurrence of those tasks may depend on resources, such as machines, manpower, and raw material. Often, several cases (i.e., instances) of a workflow coexist, and they may all concurrently access the resources. In that sense, the execution of a workflow is similar to executing several threads of a piece of software.

Correctness of classical and resource-constrained workflows has been formalized in terms of the soundness property [START_REF] Aalst | Verification of workflow nets[END_REF][START_REF] Hee | Soundness and separability of workflow nets in the stepwise refinement approach[END_REF]. Soundness guarantees that given a finite number of cases and a number of resources of each type, every case has always the possibility to terminate. As we restrict ourselves to durable resources in this paper-that is, resources that can neither be created nor destroyed-soundness also ensures that the number of resources initially available remains invariant.

The current notion of soundness for resource-constrained workflows assumes a workflow to be executed in isolation. However, workflows increasingly cross organizational boundaries and are usually intertwined. As a consequence, resources are no longer internal for a workflow but shared among different workflows. This, in fact, requires a different way of modeling workflows. To do so, we propose to enrich the workflow model with an environment capturing the resource perspective of the workflow.

The environment is generic in the sense that it can be parameterized, thereby enabling the modeling of relevant instances of practical scenarios. More precisely, the environment allows for borrowing, lending, and permanently adding and removing of resources of each type up to an initially specified number. Moreover, it also creates the cases of the workflow that are to be executed, with the number of cases taken from a specified interval.

We formalize correctness of workflows with shared resources with the notion of interval soundness, as it considers intervals of cases and resources. Interval soundness is defined for the composition of the workflow and the corresponding instance of the generic environment. We show that the verification of soundness reduces to check whether for the workflow it is always possible to terminate in the composition with the environment. The state of the environment can thereby be neglected because several invariant properties hold in the environment model which are necessary for interval soundness. To further support the design of interval-sound workflows, we present an approach for repairing an unsound workflow by synthesizing a controller (if exists) such that the composition of the workflow and the controller is interval sound.

Our contributions can be summarized as follows:

-A generalization of the model for workflows extended with resources to deal with shared resources; -A notion of correctness considering intervals of instances and resource vectors and two procedures to decide correctness; and -An approach to repair an incorrect workflow based on controller synthesis.

We continue by providing the background in Sect. 2. In Sect. [START_REF] Aalst | Workflow Management: Models, Methods, and Systems[END_REF], we introduce our model of resource-constrained workflow nets, the generic environment for modeling the resource perspective, and define interval soundness. In Sect. 4, we show how interval soundness can be decided, and repairing unsound workflows is studied in Sect. 5. We discuss related work in Sect. 6 and close with a conclusion.

Preliminaries

In this section, we provide the basic notations used in this paper, such as Petri nets and workflow nets.

For two sets P and Q, let P Q denote the disjoint union; writing P Q expresses the implicit assumption that P and Q are disjoint. A multiset or bag m over P is a mapping m : P -→ IN; for example, [p 1 , 2p 2 ] denotes a multiset m with m(p 1 ) = 1, m(p 2 ) = 2, and m(p) = 0 for p ∈ P \ {p 1 , p 2 }. We define operations +, -, =, <, > , ≤, ≥ on multisets in the standard way. We overload the set notation, writing ∅ for the empty multiset and ∈ for the element inclusion. We canonically extend the notion of a multiset over P to supersets Q ⊇ P ; that is, for a mapping m : P -→ IN, we extend m to the multiset m : Q -→ IN so that for all p ∈ Q\P , m(p) = 0. Analogously, a multiset can be restricted to a subset Q ⊆ P . For a mapping m :

P - → IN, the restriction of m to the elements in Q is denoted by m| Q : Q - → IN.
(p, t) ∈ P × T : C(p, t) = W ((t, p)) -W ((p, t)).
For a transition t ∈ T , we define the preset • t and the postset t • of t as the multisets of places where every p ∈ P occurs W ((p, t)) times in • t and W ((t, p)) times in t • . Analogously, we define for a place p ∈ P its preset • p and its postset p • . We also lift pre-and postsets to sets of places and of transitions. A place p is a source place if

• p = ∅ and a sink place if p • = ∅. A transition t ∈ T is enabled at a marking m, denoted by m t -→ , if • t ≤ m.
If t is enabled at m, it can fire, thereby changing the marking m to a marking m = m -• t + t • . The firing of t is denoted by m t -→ m ; that is, t is enabled at m and firing t results in m . Depending on the context, we interpret a marking m of N either as a multiset over P or as a vector from P -→ IN. Firing transitions can be extended to sequences:

m 1 t1 --→ . . . t k-1 ---→ m k is a run of N if for all 0 < i < k, m i ti -→ m i+1 . A marking m is reachable from a marking m if there exists a (possibly empty) run m 1 t1 --→ . . . t k-1 ---→ m k with m = m 1 and m = m k ; for v = t 1 . . . t k-1 , we also write m v -→ m . Marking m is reachable if m N = m.
The set R(m) represents all markings of N that are reachable from m.

A marking m of N is b-bounded for a bound b ∈ IN, if m(p) ≤ b for all p ∈ P . N is bounded if every reachable marking is b-bounded for some b ∈ IN. A transition t ∈ T is live if from every reachable marking m there is a marking m such that t is enabled at m . If all transitions are live, then N is live. A marking m is a home-marking if from every reachable marking we can reach m. A set HS of markings of N is a home-space if for every reachable marking m, there exists a marking m ∈ HS such that m is reachable from m.

A place invariant is a row vector I : P → Q such that I • C = 0. When talking about invariants, we consider markings as vectors.

In the following, we define two composition operators for labeled Petri nets to model asynchronous composition based on place fusion and synchronous parallel composition based on transition fusion. The composition operator ⊕ merges common places of two labeled Petri nets.

Definition 2 (asynchronous composition). Two labeled nets N 1 and N 2 are a-composable if

(Σ 1 ∪ T 1 ) ∩ (Σ 2 ∪ T 2 ) = ∅. The asynchronous composition of two a-composable labeled nets is the labeled net N 1 ⊕ N 2 = P 1 ∪ P 2 , T 1 T 2 , W 1 W 2 , l, Σ 1 Σ 2 and l(t) = l i (t) for t ∈ T i , i = 1, 2.
If N 1 and N 2 are labeled Petri nets with initial markings m N1 and m N2 , then the composition is a labeled Petri net with initial marking m 0 = m N1 + m N2 .

We define a synchronous composition operator where, for each common action a, an a-labeled transition of one labeled Petri net is merged with an a-labeled transition of the other. If there is more than one a-labeled transition in one of the labeled Petri nets, then each of these transitions is merged with a copy of the respective transition of the other labeled Petri net. Definition 3 (synchronous composition). Two labeled nets N 1 and N 2 are s-composable if (P 1 T 1 ) ∩ (P 2 T 2 ) = (Σ 1 ∩ Σ 2 ). The synchronous composition of two s-composable labeled nets is the labeled net N 1 N 2 = P, T, W, l, Σ , where

-P = P 1 P 2 , -T = {t ∈ T 1 ∪ T 2 | l 1 (t) = τ ∨ l 2 (t) = τ }, {(t 1 , t 2 ) ∈ T 1 × T 2 | l 1 (t 1 ) = l 2 (t 2 ) ∧ l 1 (t 1 ) = τ }, -W ((p, t)) =      W i ((p, t)), p ∈ P i , t ∈ T i , l i (t) = τ, i = 1, 2, W i ((p, t i )), p ∈ P i , t = (t 1 , t 2 ), i = 1, 2, 0, otherwise, W ((t, p)) =      W i ((t, p)), p ∈ P i , t ∈ T i , l i (t) = τ, i = 1, 2, W i ((t i , p)), p ∈ P i , t = (t 1 , t 2 ), i = 1, 2, 0, otherwise -l(t) = l i (t), t ∈ T i , i = 1, 2, l 1 (t 1 ), t = (t 1 , t 2 ), -Σ = Σ 1 ∪ Σ 2 .
If N 1 and N 2 are labeled Petri nets with initial markings m N1 and m N2 , then composition yields a labeled Petri net with initial marking m 0 = m N1 + m N2 . The labeled transition system (LTS) TS N = Q, δ, q, Σ of a labeled Petri net N = P, T, W, l, Σ, m N consists of a set Q = R(m N ) of states, a set δ of labeled edges with (q, l(t), q ) ∈ δ iff q t -→ q and q, q ∈ Q, and an initial state q = m N . We define the synchronous product of two labeled transition systems in the standard way: common visible actions are synchronized, all other actions are not. In fact, we have TS N1 N2 and TS N1 TS N2 are isomorph. Definition 4 (synchronous product). The synchronous product of two LTSs TS 1 and TS 2 is the LTS

TS 1 TS 2 = Q 1 × Q 2 , δ, (q 1 , q2 ), Σ 1 ∪ Σ 2 with δ = {((q 1 , q 2 ), x, (q 1 , q 2 )) | (q 1 , x, q 1 ) ∈ δ 1 , (q 2 , x, q 2 ) ∈ δ 2 , x ∈ Σ 1 ∪ Σ 2 } {((q 1 , q 2 ), τ, (q 1 , q 2 )) | (q 1 , τ, q 1 ) ∈ δ 1 } {((q 1 , q 2 ), τ, (q 1 , q 2 )) | (q 2 , τ, q 2 ) ∈ δ 2 }.
Workflow Nets A workflow refers to the automation of processes by an IT infrastructure, in whole or in part [START_REF] Aalst | Workflow Management: Models, Methods, and Systems[END_REF]. Workflows are case-based; that is, every piece of work is executed for a specific case. The workflow definition specifies which tasks need to be executed for a case and in what order. We can model a workflow definition as a (labeled) net, thereby modeling tasks by transitions and conditions by places; the state of a case is captured by a marking of the net. The assumption that a typical workflow has a well-defined starting point and a well-defined ending point imposes syntactic restrictions on Petri nets that result in the following definition of a workflow net [START_REF] Aalst | The Application of Petri Nets to Workflow Management[END_REF].

Definition 5 (WF-net). A labeled net N = P, T, W, l, Σ is a workflow net (WF-net) if it has a nonempty set of transitions, a single source place i, a single sink place f , and every place and every transition is on a path from i to f .

The short-circuited net N s of N is the labeled net obtained from N by adding a transition t s with W ((t, i)) = W ((f, t)) = 1 and l(t s ) = τ .

In the first instance, researchers were interested in workflow correctness with respect to a single case. One of the most established correctness properties of WF-nets is soundness, as introduced by Van der Aalst [START_REF] Aalst | Verification of workflow nets[END_REF] in the context of one case. Soundness guarantees that the workflow has always the possibility to terminate. Later on, multi-instance behavior attracted researchers' attention, where WF-nets are considered as parameterized systems modeling the processing of batches of tasks, as introduced in [START_REF] Hee | Soundness and separability of workflow nets in the stepwise refinement approach[END_REF]. While in classical workflows cases are considered to be independent and the modeling of multiple cases in one WF-net requires the introduction of id tokens, in batch workflows cases are considered to be undistinguishable and mixable (e.g., it does not matter which employee works on which order) and, as a consequence, cases are modeled with undistinguishable black tokens. Under certain conditions on the workflow structure, called separability, the behavior of the WF-net with undistinguishable cases (black tokens) is equivalent (up to trace equivalence) to the behavior of the WFnet with id tokens [START_REF] Hee | Soundness and separability of workflow nets in the stepwise refinement approach[END_REF][START_REF] Best | Separability in conflict-free petri nets[END_REF][START_REF] Best | Separability in persistent petri nets[END_REF]. Moreover, every net with id tokens can be transformed into an up-to-bisimulation-equivalent net with black tokens only [START_REF] Hee | Soundness and separability of workflow nets in the stepwise refinement approach[END_REF][START_REF] Juhás | Instance deadlock: A mystery behind frozen programs[END_REF].

Capturing the correctness notion for batch workflow nets requires the use of the generalized notion of soundness, as proposed in [START_REF] Hee | Soundness and separability of workflow nets in the stepwise refinement approach[END_REF].

Definition 6 (WF-net soundness). Let k ∈ IN. A WF-net N is k-sound if, for every marking m reachable from marking [k • i], we can reach marking [k • f ].
The next definition gives a requirement for the correct design of a workflow that can be checked using structural properties of the net [START_REF] Hee | Generalised soundness of workflow nets is decidable[END_REF]. Nonredundancy of a place p ∈ P guarantees that p can potentially be marked with a token in some reachable marking.

Definition 7. Let N = P, T, W, l, Σ be a WF-net. A place p ∈ P is nonredundant if there exist k ∈ IN and m ∈ IN P such that [k • i] * -→ m ∧ p ∈ m.

Generalizing Resource-Constrained Workflow Nets

We use the notion of resource-constrained workflow nets (RCWF-nets) [START_REF] Hee | Resource-constrained workflow nets[END_REF] to extend the definition of the workflow with resource dependencies of the tasks. The production net of an RCWF-net is a WF-net in its traditional sense, defining the order of task execution, resource places model the resource types used by the workflow, and resource consumption and production are modeled by the arcs from the resource places to the transitions of the production net, and vice versa. Definition 8 (RCWF-net). A labeled net N = P p P r , T, W p W r , l, Σ is a resource-constrained workflow net (RCWF-net) if

-N p = P p , T, W p , l, Σ is a WF-net, the production net of N ; -P p is the set of production places, and P r is the set of resource places; and -W r : (P r × T ) ∪ (T × P r ) -→ IN is the resource weight function.

The short-circuited net N s of N is the labeled net obtained from N by replacing N p with its short-circuit net.

The initial marking m N = [k•i]+R of an RCWF-net N consists of k ∈ IN tokens in place i, specifying the number of cases in the workflow that are concurrently executed, and an initial marking for the set P r of resources places, denoted as a resource vector R ∈ IN Pr .

Example 1. We illustrate the previously introduced concepts using Fig. 1. The nets N 1 and N 2 are RCWF-nets with one resource place r. Arc weights are depicted on the respective arc unless they are equal to 1. Erasing r and its adjacent arcs from N 1 and N 2 yields the (same) production net, a WF-net. This WF-net is k-sound, for any k > 0.

The Generic Environment

To consider RCWF-nets in the setting where the workflow works within some environment that can borrow resources from the workflow or lend more resources to it, we introduce patterns capturing typical behavior of the resource environment. We consider the following actions of the environment: borrowing resources (the borrowed resources are then used by other workflows and they can eventually be returned and made available for the workflow again), lending resources (i.e., making some additional resources temporarily available, and eventually taking them back, when unused by the workflow), permanently removing resources, and permanently adding resources. Actual environments allow for a (possibly empty) subset of these actions.

We define the generic environment, built as a union of generic environments defined for every resource type (i.e., place). All the patterns can be obtained by choosing an appropriate initial marking for the generic environment. The generic environment of a resource place r is captured in Fig. 2(a). The transitions t ↑ r and t ↓ r model permanent addition and removal of resources correspondingly. Their counterparts t↑ r and t↓ r model the decision of the environment not to lend/borrow a certain number of resources, but removing the tokens from places r ↑ and r ↓ . The number of tokens in places r ↑ and r ↓ in the initial marking gives the bounds for the number of resources that can be added and removed, respectively. Clearly, choosing 0 as initial marking of r ↑ and r ↓ makes the corresponding transitions dead, so they might be removed for the corresponding pattern, but for the sake of readability, we prefer to use only the initial marking for configuring the generic environment into a pattern.

r t r - r - t r + r + t r ↑ t r ↓ r1 ↑ r ↓ r1 ↓ r ↑ r -↓ t r ↓ t r ↑ r2 ↑ r2 ↓ (a) Resource environment c t e d t f t c f i e t d (b) Case environment
Transitions t + r and t - r together with places r + and r -model lending and borrowing resources in the following way: The number of tokens in r + and r -in the initial marking corresponds to the number of resources the environment may lend and borrow, respectively. Thus having 0 for the initial marking on r + means that the environment cannot lend any resource of type r. When the resources are borrowed, the marking of r + is increased by the number of borrowed resources, and the firings of t + r will then correspond to returning those resources by the environment.

The initial marking of the places r ↑ , r ↓ , r + , and r -serves thus as the configuration parameter defining the behavior of the environment. In principle, it is possible to elaborate the model further by linking, for example, r ↓ and r -by means of choosing the bound for the total number of resources that can be removed permanently or temporarily. We can model this by introducing the place r -↓ and the arcs depicted by the dashed lines in Fig. 2(a). The same can be done for other configuration components. Variations on the environment construction are also possible by linking the scheme for adding and removing resources for different resource types. We restrict our attention further to the main structure, without linking the configuration components to each other, although the results hold for environments restricted in this way, too.

Since borrowing is temporary-that is, under the fairness assumption, the environment will eventually return the borrowed resources-the choice of the initial marking for r -does not change the set of markings reachable in the composition of the workflow and the environment projected on the workflow places: The workflow can always wait until the environment returns the resources borrowed and then proceed. The same applies to lending resources: The workflow can always wait until the environment will lend it the maximal amount of the resources possible, meaning that the behavior of the composition is defined by r + . The borrowing/lending part of the environment model becomes important when time is taken into consideration, also for transitions t + r and t - r , since borrowing/lending then changes the set of markings reachable in the workflow. Note that also transition t↓ r , decreasing the amount of resources the environment might remove permanently, only has influence on the set of markings reachable in the workflow when we take time into account.

To create cases of the workflow, we add a generic case environment to our generic environment, allowing for an arbitrary number of cases from the interval 2(b) shows the construction. The place c (creation) contains initially k 1 tokens (i.e., the lower bound of cases to be created), the place d (dismissable) contains k 2 -k 1 tokens (i.e., cases that can but do not have to be created), and place e (end) is empty. For every case that is not created, a token is produced in the place e by firing t e . Thus, if all created cases terminate (modeled by a token in f for each case), the place e contains on the termination k 2 tokens. Definition 9 (generic environment). Let N = P p P r , T, W p W r , l, Σ be an RCWF-net. The generic environment of N is a labeled Petri net E such that E and N are a-composable with ((P p P r )∩P E ) = P r {i, f } and E = P E , T E , W, m E , l E , {τ } is defined as

[k 1 , k 2 ], for some k 1 , k 2 ∈ IN, k 1 ≤ k 2 . Figure
-P E = P r P e {i, f, c, d, e} with P e = {r -, r + , r ↑ , r ↓ , r↑ 1 , r↑ 2 , r↓ 1 , r↓ 2 | r ∈ P r }, -T E = {t - r , t + r , t ↑ , t ↓ , t↑ r , t↓ r | r ∈ P r } {t c , t d , t e , t f }, -W ((r -, t - r )) = W ((r, t - r )) = W ((t - r , r + )) = W ((t + r , r -)) = W ((t + r , r)) = W ((r + , t + r )) = W ((r ↑ , t ↑ r )) = W ((t ↑ r , r↑ 2 )) = W ((t ↑ r , r)) = W ((r ↑ , t↑ r )) = W (( t↑ r , r↑ 1 , )) = W ((r ↓ , t ↓ r )) = W ((t ↓ r , r↓ 2 )) = W ((r, t ↓ r )) = W ((r ↓ , t↓ r )) = W (( t↓ r , r↓ 1 , )) = 1 for r ∈ P r and W ((c, t c )) = W ((t c , i)) = W ((d, t d )) = W ((d, t e )) = W ((t d , i)) = W ((t e , e)) = W ((f, t f )) = W ((t f , e)) = 1, -m E (p) =                                            m N (p),
p ∈ P r m - r , p = r -and m - r is the maximal number of resources r the environment can borrow m + r , p = r + and m + r is the maximal number of resources r the environment can lend m ↓ r , p = r ↓ and m ↓ r is the maximal number resources r the environment can remove m ↑ r , p = r ↑ and m ↑ r is the maximal number of resources r the environment can add

k 1 ∈ IN, p = c k 2 -k 1 ∈ IN, p = d
An environment E, m E of N consists of E and a concrete initial marking m E .

Interval Soundness for RCWF-nets with an Environment

We adapt the definition of soundness for WF-nets to RCWF-nets with an environment. Soundness of an RCWF-net N with an environment E, m E guarantees that the underlying production net of N is k-sound, for every k in the interval; that is, also in the presence of resources, a case has always the possibility to terminate. In addition, we put two conditions on the resources: First, all resources that are initially available in N and E are again available when all cases are terminated. Second, at any reachable marking, the number of available resources does not increase the number of initially available resources. These two criteria are a consequence of our restriction to durable resources, because they ensure that no resources are created or removed.

To guarantee the previous conditions, we define four necessary conditions that are captured in the notion of a well-defined composition of N and an arbitrary environment E, m E . The first condition ensures that the production net of N is k-sound, for every k in the interval. The second condition ensures that no resource tokens can be created by the WF-net; that is, for every firing sequence, the number of resource tokens put by N on the resource places does not exceed the number of tokens taken by N from the resource places (meaning that then every reachable marking has a resource vector R ≤ R, unless the environment can add tokens to the resource places). The third condition states that there exists a place invariant for the places c, d and e, guaranteeing that the number of cases remains constant. Likewise, the fourth condition requires that, for every resource place, there exists a place invariant, guaranteeing that the number of resources remains constant.

Definition 10 (well-defined). Let N be an RCWF-net such that the production net of N does not have redundant places. Let E, m E be an environment of N . The composition N ⊕ E is well-defined if the following four properties hold: The absence of redundant places is necessary for applying invariant techniques. The next lemma shows that a well-defined composition is bounded. Lemma 11. Let N be an RCWF-net and E, m E be an environment of N . If N ⊕ E is well-defined, then it is bounded.

1. The production net of N is k-sound, for all m E (c) ≤ k ≤ m E (c) + m E (d). 2. ∀x ∈ Z Z T : (C • x)| Pp {e} ≥ 0 implies (C • x)| Pr ≤ 0.
Proof. Boundedness of the resource environment follows from Definitions 10(2),( 4) and of the case environment from Definition 10(3). The latter argument and Definition 10(1), which implies boundedness of the production net, implies boundedness of N .

For a well-defined composition N ⊕ E, we can define interval soundness, which is a more general variant of the soundness notion as defined in [START_REF] Hee | Soundness of resourceconstrained workflow nets[END_REF][START_REF] Barkaoui | Workflow Soundness Verification Based on Structure Theory of Petri Nets[END_REF].

Definition 12 (interval soundness).

Let N be an RCWF-net and E, m E be an en-

vironment of N such that N ⊕ E is well-defined. Then, N is sound with E, m E if for all m ∈ R(m N ⊕E ) : m * -→ m such that m (e) = m E (c) + m E (d). If m E is not relevant, we say N is interval sound.
Definition 12 captures at least the following relevant instances of interval soundness:

-(k, R)-soundness [START_REF] Hee | Soundness of resourceconstrained workflow nets[END_REF][START_REF] Barkaoui | Workflow Soundness Verification Based on Structure Theory of Petri Nets[END_REF] (i.e., we consider a fixed number k of cases and a fixed resource vector R) if m E (p) = 0, for all p ∈ P e {d} and m E (r) = R(r), for all r ∈ P r ; up-to (k, [R, R + ])-soundness (i.e., (k, R )-soundness for all R ≤ R ≤ R + but the initial resource vector R can be increased up to R + at runtime) if m E (d) = 0 and m E (r ↓ ) = 0, for all r ∈ P r and m E (r

↑ ) = R + (r) -R(r), m E (r) = R(r) for all r ∈ P r ; -down-to (k, [R -, R])-soundness (i.e., (k, R )-soundness for all R -≤ R ≤ R but the initial resource vector R can be reduced down to R -at runtime) if m E (d) = 0 and m E (r ↑ ) = 0, for all r ∈ P r and m E (r ↓ ) = R(r) -R -(r), m E (r) = R(r)
for all r ∈ P r ; up-to, down-to (k, [R -, R + ])-soundness (i.e., (k, R)-soundness for all R -≤ R ≤ R + but the initial resource vector R can be reduced down to R -or increased up to

R + at runtime) if m E (d) = 0 and m E (r ↑ ) = R + (r) -R(r), m E (r ↓ ) = R(r) -R -(r), m E (r) = R(r).
We now relate the previous variants of interval soundness, thereby generalizing them from a fixed number k of cases to an interval [k 1 , k 2 ] of cases.

Lemma 13. For any RCWF-net N and

k 1 , k 2 ∈ IN with k 1 ≤ k 2 , we have 1. N is ([k 1 , k 2 ], R )-sound for all R ≤ R ≤ R + iff N is up-to ([k 1 , k 2 ], [R, R + ])- sound. 2. N is down-to ([k 1 , k 2 ], [R -, R])-sound implies N is ([k 1 , k 2 ], R )-sound for all R -≤ R ≤ R. 3. Let R = R + . N is down-to ([k 1 , k 2 ], [R -, R])-sound iff N is up-to, down-to ([k 1 , k 2 ], [R -, R + ])-sound.
Proof (Sketch). It suffices to prove the three statements for k, k 1 ≤ k ≤ k 2 .

(1) ⇒: Let m 0 be the initial marking for (k, R )-soundness with R = R + and m 0 be the initial marking for up-to (k, [R, R + ])-soundness. Clearly, we have

m 0 | Pr ≥ m 0 | Pr . Let m 0 σ -→ m .
Then by the monotonicity of the firing rule and construction of E, we have m 0 σ| T N ----→ m and m| Pr ≥ m| Pr . Thus, if we consider the projection of markings to N , then every marking that is reachable for up-to (k, [R, R + ])-soundness is also reachable for (k, R )-soundness.

⇐: Any resource vector R within the interval can be reached by firing transitions t ↑ r , for all r ∈ P r . Then, every run in the composition for (k, R )-soundness can be replayed in the net for up-to (k, [R, R + ])-soundness.

(2) Similar argumentation as in the reverse implication of ( 1), but this time transitions t ↓ r and t↓ r have to be fired. (3) ⇒: Similar argumentation as for the implication of (1). ⇐: Use argumentation in (2) to decrease the resource vector to R.

The next lemma gives a necessary condition for interval soundness, thereby justifying the restriction to well-defined compositions of N and E. Lemma 14 (necessary condition). Let N be an RCWF-net and E, m E be an environment of N . If N is sound with E, m E , then N ⊕ E is well-defined.

Proof. (1) k-soundness of the production net of N follows from [START_REF] Hee | Resource-constrained workflow nets[END_REF]Cor. 4.1].

(2) Follows from [START_REF] Hee | Resource-constrained workflow nets[END_REF]Thm. 4.4].

(3) Existence of an invariant I follows from [START_REF] Hee | Resource-constrained workflow nets[END_REF]Thm. 4.8] and by the construction of E, we have I + (c + d + e) is also an invariant.

(4) By [START_REF] Hee | Resource-constrained workflow nets[END_REF]Thm. 4.8], a resource invariant exists for all r ∈ P r . Moreover, we have the following invariant: r + r -+ 2r

+ + 2r ↑ + 2r ↑ 1 + r↑ 2 + r ↓ + r↓ 1 + 2r ↓ 2
, for r ∈ P r . So the sum of these two invariants is the resource invariant we are looking for.

Example 2. Consider the RCWF-net N 1 in Fig. 1(a) and its environment E (see Fig. 4(a) for the entire composition). The production net of N 1 is k-sound, for k > 0, and i + p + q + f + c + d + e is a place invariant in the production net. Furthermore, no resource token is created in N 1 , and r +p+2q +r -+2r + +2r ↑ +2r ↑ 1 + r↑

2 +r ↓ + r↓ 1 +2r ↓ 2
an invariant for resource place r. Thus, N 1 ⊕ E is well-defined. For the same reason, N 2 ⊕ E is well-defined. However, N 1 is not (k, R)-sound for all k = R(r). For example, for k = r = 2, firing transition t twice yields a deadlock [2 • p]. In contrast, N 2 is (k, R)-sound for R(r) > 1 and any k. This example exemplifies that well-definedness is only a necessary condition for interval soundness.

Deciding Interval Soundness

Definition 12 (interval soundness) gives an immediate decision procedure:

An RCWF- net N is sound with E, m E if the set {m | m(e) = m E (c) + m E (d)} of markings is a home-space in N ⊕ E or respectively m = [(m E (c) + m E (d))
• e] is a home-marking in the projection of reachable markings of N ⊕ E to the places of N .

Theorem 15 (decision I). Let N be an RCWF-net and E, m E be an environment of

N such that N ⊕ E is well-defined. Then, N is sound with E, m E if the set {m | m(e) = m E (c) + m E (d)} of markings is a home-space in N ⊕ E.
Note that we have one decision algorithm, for every instance of interval soundness. As checking a home-space property is decidable [START_REF] Escrig | Decidability of home space property[END_REF], we can conclude: Theorem 16 (decidability). Let N be an RCWF-net and E, m E be an environment of N . Checking whether N is sound with E, m E is decidable.

In the literature, soundness is often reduced to showing that the short-circuited (RC)WF-net is live and bounded. The reduction works if the transition t s consumes all k cases from the place f and produces k tokens on the place i. Figure 3 illustrates this. The drawback of this construction is that it requires to check a different net for every k. As we consider N with an environment, we propose the following generic reduction to liveness and boundedness: Theorem 17 (decision II). Let N be an RCWF-net and E, m E be an environment of N such that N ⊕ E is well-defined. Let E s be obtained from E by adding a transition t s with W ((e, t s )) = X(c) + X(d), W ((t s , d)) = X(d), and W ((t s , c)) = X(c). Then, N is sound with E, m E iff all transitions T N {t s } of N ⊕ E s are live. Fig. 3. The RCWF-net N is not (3, 1)-sound: The firing sequence t1t2t4t1 yields the marking [2 • f, p1] which is a deadlock. Nevertheless, the short-circuited net of N is bounded and live. However, if the transition ts consumes all k cases from the place f and produces k token on the place i, then the short-circuited net of N is not live.

Proof. ⇒: As N does not have redundant places, it does not have dead transitions in its production net and t s is not dead either, so we conclude that all transitions in T N {t s } are live.

⇐: From liveness of the transition t s , we conclude that it is always possible to reach a marking m with m(e) ≥ m E (c) + m E (d). The number of tokens in e at m cannot be greater than m E (c) + m E (d) by the invariant in Definition 10(3). Moreover, all places of the production net N p of N are unmarked in m by the k-soundness of N p . Firing t s at m yields m where the places c and d contain the same number of tokens as in the initial marking m Z . Because of the invariants covering all places of E (Definition 10(3) and ( 4)), we conclude that m is reachable from m Z . Hence, markings m are a homespace in N ⊕ E s , and N is sound with E, m E .

Example 3. Using Theorem 17, we can show that the RCWF-net N 1 is not (k, R)sound whereas the RCWF-net N 2 is.

Repairing Interval Unsound RCWF-Nets

In the previous section, we presented an algorithm to decide interval soundness of an RCWF-net N . However, designing an interval-sound workflow or adjusting a workflow if some functionality or the environment has been changed is a nontrivial and errorprone task even for experienced process designers. In order to support process designers, we introduce an approach to repair an interval-unsound RCWF-net N if possible so that interval soundness is achieved by design. Clearly, the repaired workflow should be seen as a suggestion to the process designer rather than the ultimate solution.

Requiring the composition N ⊕ E to be well-defined reduces the cause of unsoundness to a deadlock or a livelock due to the lack of resources during the production process (see Lemma 11). To repair an RCWF-net N , we therefore propose to automatically construct a controller C that controls those transitions of N that produce tokens on or consume tokens from a resource place. This way, we control the order in which certain tasks may occur and prevent the workflow from getting stuck.

Technically, a controller is a labeled Petri net C and will be composed with N ⊕ E by merging transitions of N only. These merged transitions of N are then controlled by C in the composition. Another technicality that we leave out in the following is ensuring that the nodes of E and C are pairwise disjoint.

Definition 18 (controller, repairable). Let N be an RCWF-net and E, m E be an environment of N . A labeled Petri net C is a controller of N ⊕ E if C and N are s-composable and replacing Z in Definition 12 with C N ⊕ E yields soundness of N with E, m E . If there exists a controller of N ⊕ E, then N ⊕ E is repairable.

The following algorithm synthesizes a controller of N ⊕ E. It takes the state space of N and the environment E as its input, and it outputs an LTS which can, in a next step, be easily transformed into a labeled Petri net.

Definition 19 (controller construction). Let N be an RCWF-net and and E, m E be an environment of N such that Z = N ⊕ E is well-defined and has a finite state space. Let Σ ⊆ Σ N be the set of synchronized actions, and let TS Z = Q Z , δ Z , qZ , Σ be the LTS of Z after relabeling all actions x ∈ Σ N \ Σ to τ . Define a sequence of LTSs TS i , i = 0, 1, . . . inductively as follows:

Base : TS 0 = Q 0 , δ 0 , Q 0 , Σ with -Q 0 = 2 Q Z , -δ 0 = {(Q, x, Q ) ∈ Q 0 × Σ × Q 0 | Q = {q Z | ∃q Z ∈ Q : q Z τ * xτ * ----→ q Z }}, -Q 0 = {q Z | qZ τ * --→ q Z }. Step : TS i+1 = Q i+1 , δ i+1 , Q 0 , Σ with -Q i+1 = Q i \ {Q ∈ Q i | ∃(q Z , Q) ∈ TS Z TS i : (q Z , Q) * -→ (q Z , Q ) ∧ q Z | {e} = k 1 + k 2 } 1 , -δ i+1 = δ i ∩ (Q i+1 × Σ × Q i+1 ).
Let j be the smallest number with TS j = TS j+1 . If Q 0 ∈ Q j , then the corresponding labeled Petri net C of TS j is a controller of N ⊕ E.

The construction of C allows some level of flexibility: We do not assume all transitions of N to be controllable as we restrict the set of labels of TS j in the construction to a subset Σ of the alphabet Σ N . That way, we take into account that not all tasks in a workflow can be controlled. We assume the nodes of C and E to be pairwise disjoint; that is, the controller cannot control actions of the environment. (If one would find it possible to control actions of the environment, we could adapt our construction by labeling certain transitions of E and adding those actions to the alphabet of C.)

Note that C is not necessarily a WF-net, because it may have more than one sink place; thus, the composition N C is not an RCWF-net but a labeled Petri net.

Our main result of this section is that a composition N ⊕ E is repairable if and only if the algorithm in Definition 19 outputs an LTS with at least one state.

Theorem 20 (justification). Let N be an RCWF-net, E, m E be an environment of N , and C be the labeled Petri net constructed according to Definition 19. Then, C exists iff N ⊕ E is repairable.

The verification of soundness for RCWF-nets has been investigated by many researchers. On the one hand, interval soundness is a more restrictive instance compared to soundness in [START_REF] Sidorova | Soundness for resource-constrained workflow nets is decidable[END_REF][START_REF] Hee | Soundness of resourceconstrained workflow nets[END_REF][START_REF] Barkaoui | Workflow Soundness Verification Based on Structure Theory of Petri Nets[END_REF], as we assume the number of cases and resources to be fixed within an interval. On the other hand, it is more general because we assume resources to be shared among workflows rather than internal to a workflow. We incorporated this in our model by enriching the model of RCWF-nets as proposed in [START_REF] Barkaoui | Structural Analysis of Workflow Nets with Shared Ressources[END_REF][START_REF] Hee | Soundness of resourceconstrained workflow nets[END_REF] with a generic environment modeling the resource perspective of a WF-net. Moreover, we are neither restricted to one resource type as [START_REF] Hee | Soundness of resourceconstrained workflow nets[END_REF] nor to certain subclasses of WF-nets as [START_REF] Barkaoui | Workflow Soundness Verification Based on Structure Theory of Petri Nets[END_REF]. Resource problems with an unbounded number of resource items have been studied in [START_REF] Brázdil | Reachability games on extended vector addition systems with states[END_REF].

RCWF-nets can be seen as parameterized (or multi-threaded) systems with two parameters: the number of cases to be executed and the number of available resources. Verification of parameterized systems is a popular topic, but must approaches investigate safety properties with unbounded parameters (e.g., [START_REF] Kaiser | Dynamic cutoff detection in parameterized concurrent programs[END_REF]) whereas we assume fixed bounds but consider with soundness a liveness property. A resource interface in [START_REF] Chakrabarti | Resource interfaces[END_REF] defines a safety property over the resources for open system; we defined the generic environment E and hence deal with a closed system. There also exist extensions of the temporal logics CTL and ATL to reason about resources [START_REF] Bulling | Expressing properties of resource-bounded systems: The logics rtl * and rtl[END_REF][START_REF] Alechina | Resource-bounded alternating-time temporal logic[END_REF]. Although the problem instances considered in this paper can be expressed in terms of those logics, verification would require to check the system for all parameters.

Our approach to repair unsound workflows is based on classical controller synthesis [START_REF] Ramadge | Supervisory control of a class of discrete event processes[END_REF] and has been defined for Petri nets and soundness in [START_REF] Wolf | Does my service have partners?[END_REF]. For an overview of Petri net-based controller synthesis approaches, we refer to [START_REF] Li | Deadlock control of automated manufacturing systems based on petri nets-a literature review[END_REF]. Most of these works focus on the net structure and properties different from soundness; moreover, the main application are manufacturing systems where one tries to construct a scheduler. In contrast, we construct a controller such that the net is robust and thus sound.

Conclusion

We investigated the correctness of workflows with shared resources, called interval soundness. To do so, we proposed to enrich the workflow model with a generic environment capturing the resource perspective. An instance of this generic environment models a specific environment that specifies an interval of workflow instances to be created and available resources for each resource type. The generic environment generalizes the existing workflow model extended with resources and captures environments of practical relevance. To decide interval soundness for every instance of the generic environment, we presented two decision procedures, both using invariant properties of the environment. Furthermore, we showed a way to support the design of correct workflows by automatically synthesizing a controller such that the composition of the workflow and the controller is interval sound.

In ongoing work, we are interested in determining a smallest resource vector (based on given requirements) that guarantees soundness. Likewise, we aim at determining the largest resource vector that guarantees soundness or proving that increasing some resource vector does not influence the soundness result. Constructing more specific controllers by assigning costs to transitions is another direction of future work.

Definition 1 (

 1 labeled Petri net). A net N = P, T, W consists of a finite set P of places, a finite set T of transitions such that P and T are disjoint, and a weight function W : (P × T ) (T × P ) -→ IN. A labeled net N = P, T, W, l, Σ is a net P, T, W together with an alphabet Σ of actions and a labeling function l : T → Σ {τ }, where τ represents an invisible, internal action. A (labeled) Petri net N, m N is a (labeled) net N together with an initial marking m N , where a marking m : P -→ IN is a distribution of tokens over the places. The incidence matrix C of N is defined by ∀

Fig. 1 .

 1 Fig. 1. Example of an unsound and a sound RCWF-net.

Fig. 2 .

 2 Fig.2. Generic resource environment for the resource place r and case environment for a workflow with initial place i and final place f .

3 .

 3 There exists a place invariant I p such that I p (c) = I p (d) = I p (e) = 1 and, for all p ∈ P E \ {c, d, e}, I p (p ) = 0. 4. For each r ∈ P r , there exists a place invariant I r satisfying I r (c) = I r (d) = I r (e) = 0, I r (r) = 1, and ∀r ∈ P r \ {r} : I r (r ) = 0.

For the sake of readability, we see the state q Z as its corresponding marking in Z.

) for N1 ⊕ E, assuming an initial marking [3 • i, 3 • r, r ↓ ] (i.e., the transition t c has been fired three times) for purposes of simplification. The state Q2 contains a deadlock and will be removed in one of the iterations.

Proof. ⇒: Suppose C is a controller of N ⊕ E. As TS 0 is the largest structure, there must be a largest i such that there exists a simulation relation of (the state space) of C by TS i . If there is no simulation relation of C by TS i+1 , then (N ⊕ E) C must violate soundness because this is the reason for removing further states from TS i .

⇐: The construction of TS j and thus of C terminates because finiteness of TS Z ensures that TS 0 is also finite and only removes states and transitions from TS 0 when constructing TS j . If the resulting TS j is nonempty, it must be a controller of N ⊕ E because all reasons not to be a controller have been erased: We removed all states from which N cannot reach a final state and we iteratively check this. So, Definition 19 yields the most permissive controller of N ⊕ E. Other, more specific controllers that have less behavior can also be constructed, for example, by assigning costs to each transition in N and constructing a controller that has the least cost.

Example 4. Figure 4 illustrates the controller construction for N 1 ⊕ E. For the sake of readability, we keep the size of each controller state (i.e., the number of markings N 1 ⊕E can be in) small by choosing [3•i, 3•r, r ↓ ] to be the initial marking of N 1 ⊕Ethe state space of the controller remains the same. Initially, N 1 ⊕ E can be in any of the three markings of the initial state Q 0 of TS . Firing the transition t, yields the three markings depicted in the state Q 1 of TS . The state Q 2 (depicted by a dashed frame) is removed in one of the iterations of the construction, because the marking [i, 2 • p, r↓ 2 ] is a deadlock and no final marking. The complete LTS TS , the controller, has 12 states and realizes tu(tv + vt)u(tv + vt)uv. Composing the resulting labeled Petri net C of TS with N 1 ⊕ E yields a sound net C N 1 ⊕ C. Note that the composition operator requires one copy for each occurrence of the transition t, u, and v in C.