We propose a technique for checking the dynamic controllability of processes with temporally constrained loops. The temporal control structures t-split and t-loop are adequate concepts for modelling the behaviour of processes dependent on the speed of execution of a process instance. While the run-time semantics of these constructs is straightforward, the assessment of the temporal properties of processes with temporal control structures is complex. Here we propose a procedure for checking the dynamic controllability of processes with temporal loops by mapping them to processes without t-loops, which then can be mapped to CSTNUDs, simple temporal networks with uncertainty and decisions. For CSTNUDs procedures for checking dynamic controllability are available.
An important part of the modelling of processes is to represent their temporal
properties and to model the temporal constraints expressing temporal
requirements and restrictions. Compliance to temporal constraints like deadlines,
reaction times, process durations rank among the most important quality measures
[
Temporal qualities of processes rely on the temporal characteristics of the activities and services they are composed of. These activities might have some degrees of freedom, or some degrees of uncertainty formulated in their temporal descriptions. For an example the time-span needed for executing an activity might range between some minimum and maximum duration, without any control of the actual duration by the process controller. On the other hand, the process controller has to guarantee some temporal properties (like e.g. maximum duration of the whole process) in spite of these uncertainties. Therefore, the notion of controllability rather than satis ability is adequate as correctness criterion for processes with temporal constraints. Satis ability only requires that it is possible to satisfy all constraints, for some durations of the activities and for some ow decisions, however not necessarily for all durations of these activities. Controllability, in contrast, requires that all temporal constraints are ful lled for all durations of invoked activities and for all possible ows.
Checking satis ability, controllability and its less restrictive but more
complex variant dynamic controllability is already well established for basic control
patterns [
As an approach to overcome these problems, the notion of temporal control
structures (temporal splits and temporal loops) for process models was
introduced and their semantics was formally de ned [
Although the operational semantics of temporal control structures is easily
de ned and implemented, algorithms for design time checks of controllability
and dynamic controllability, and for pro-active monitoring of the compliance of
the process execution at runtime turned out to be quite challenging. In [
In this paper we consider the dynamic controllability of processes with
temporal loops. We will introduce a procedure which transforms a process with a
temporal loop to a process without any loop with the property, that the rst
process is dynamically controllable, if and only if the second is dynamically
controllable and thus we can reduce the checking to the already solved case for
processes without temporal loops for which we already proposed e ective
procedures for checking dynamic controllability [
The remainder of this paper is organized as follows: we revisit the de nition of process models with temporal loops and the de nition of their semantics in section 2. In section 3 we discuss dynamic controllability and introduce some process transformations which eliminate temporal loops. The results of these transformations can then be checked for dynamic controllability instead of the original process. Related work (section 4) and conclusions (section 5) complete this paper.
As a basis for the introduction of procedures for checking dynamic
controllability, we rst de ne the process model with temporal control structures. It is
basically the process model in [
We use a simple process metamodel, which focuses on the standard minimum
work ow control patterns [
Time points and duration intervals are represented by natural numbers N. Time is measured in an atomic time unit (chronon), like minutes, hours or days. A point in time marks a point on an increasing time axis and represents the temporal distance to a given reference point, for instance the start of a process.
The maximum process duration is constrained by a deadline, that must not be exceeded. Activity instances start at a certain point in time (start event) and end at a certain point in time (end event). The distance between these two points is the actual execution duration of this activity instance. Contingent activities have a duration between their best-case (fastest) and worst-case (slowest) duration which can only be observed (but not controlled). In the following we regard all activities as contingent.
De nition 1 (Process Graph). A process graph G = (N; E; C; !) with a set of nodes N connected by a set of edges E with set of temporal constraints C and deadline ! forms a directed acyclic graph, where n:type = activity j start j end j xor-split j xor-join j and-split j and-join, which have the usual semantics, or a temporal node with n.type = t-loop j t-split. n:cond is the boolean condition for a node n of type xor split.
n:db is the minimum and n:dw maximum duration of a node n 2 N such that 0 n:db n:dw and n:db; n:dw 2 N.
Each edge (n1; n2) 2 E, n1; n2 2 N; describes a precedence constraint between nodes n1 and n2. The successors and predecessors of a node n are denoted n:Succ = fmj(n; m) 2 Eg and n:P red = fmj(m; n) 2 Eg respectively.
There is exactly one start activity (which has no predecessor) and one end activity (which has no successor). The number of predecessors jn:P redj per nodetype n:type is as follows: 0 for start, 2 for xor join and t join, > 1 for and join, and 1 for all other types. The number of successors jn:Succj per node-type n:type is restricted as follows: 0 for end, 2 for xor split and t split, > 1 for and join, and 1 for all other types.
The variable elapsed represents the distance between the start of the process and a point in time.
A temporal split node n has a threshold n:c where n:c 2 R 0, and a true successor and a false successor.
A temporal loop tl 2 N , tl.type = t-loop has a loop body tl:B = G0 where G0 is a process graph, and a loop condition l:cond = [P ^](elapsed c); c 2 N with the optional predicate P . The duration interval of the loop-body is represented by l:bb and l:bw.
We write tsplit(n,c,u,d) for a t-split node n with threshold c, true successor u and false successor d, and tloop(n,P,c,B) for a t-loop node n with predicate P , threshold c, and loop body B.
C is a set of temporal constraints of type upper- and lower-bound, which we write as ubc(m; n; ), resp. lbc(m; n; ), where m; n are nodes and is a constant. ubc(m; n; ) forces n to start no more than time units after m started; lbc(m; n; ) forces n to start at least time units after m started.
We assume that a process graph is full-blocked (proper nesting of matching pairs). Xor-joins are of type simple merge, i.e. it is not possible that both predecessors will be executed in a single process instance.
Without loss of generality in this paper we only consider the temporal conditions (elapsed c).
A temporal loop tloop(n; P; c; B) iterates over its body as long as the condition is true. A temporal loop's condition speci es an upper bound in addition to a regular loop-condition. The body of a loop is again a process graph and might include temporal control structures. The variable elapsed is always de ned relative to the start node of the process graph.
A t-split node is a special variant of an xor-split node with a temporal condition. Here we currently provide the condition \elapsed n:c", where n:c, the threshold value, is a constant. The operational semantics is as follows: when a t-split node is executed, the condition is evaluated, i.e. the time elapsed since process start is compared to the threshold n:c. If it is below or equal to the threshold, the \T " branch is executed, otherwise, execution continues with the \F " branch. We assume that after starting execution of a t-split its condition is evaluated immediately.
As we have shown in [
To formalize the semantics of the proposed temporal control structures and to reason about the correctness of a given model we now introduce the concepts scenario, schedule, and controllability. In a nutshell: a scenario is a timed instance of process. It is correct, if the time stamps of the start and end events of the activities satisfy all explicit and implicit temporal constraints (an activity starts after termination of its predecessor). A schedule assigns a start and end time intervals to each activity, such that all scenarios are valid if start and end-time are within the bounds de ned in the scenario. A process is controllable, if it admits a correct schedule. The following requires some formal elaboration. This is necessary for being able to check controllability of process models.
In a scenario time stamps for the start and the end are assigned to each node, representing one out of many possible process executions.
De nition 2 (Scenario). A scenario S for a process graph P (N; E; C; !) associates each n 2 N and the body l:B of each t-loop l with two time stamps ts; te 2 N, representing the start time and end time of n respectively. We call (n; ts; te) 2 S a scenario entry.
We de ne a valid scenario as formalization of the conceptual semantics of control ow structures described in Section 2.
De nition 3 (Valid Scenario). A scenario S for a process graph P (N; E; C; !) is valid, i : (1) 8n 2 N : n:ts n:te (2) 8n 2 N; n:type 6= t loop : n:ts + n:db (3) 8(m; n) 2 E; m:type 6= t split : m:te (4) 8n 2 N; t split(n; c; u; d): n:ts c ) n:ts u:ts n:ts > c ) n:ts d:ts (5) 8n 2 N; tloop(n; T rue; c; B); n:ts c:
c < n:te c + n:bw; (6) 8n 2 N; tloop(n; P; c; B); n:ts c:
n:ts c ) n:ts n:te c + n:bw (7) 8ubc(m; n; ) : n:ts m:ts + (8) 8lbc(m; n; ) : m:ts n:ts n:te n:ts n:ts + n:dw
For the new control structures the following must hold: If a temporal loop with the condition (elapsed c) starts before or at c, it will run through the loop body at least until c is reached, plus one nal loop-iteration (worst-case duration of the loop body). The end of the loop is always after the cut-o point c. If the loop starts after c, the loop body will not be executed. If the body of the loop is executed, its last iteration does not start before the beginning of the loop, and it does require at least the minimum duration of the body as distance between start and end of the loop. For the end of the loop we require that it can accommodate all durations of the loop body between best-case and worst-case duration. And nally (6) states that t-loops with the condition P ^ (elapsed c) can nish anytime before c due to the condition P , but they can last until c + duration of the loop body.
An example for a process with one possible valid (valid) scenario, is shown
in Figure 1 [
Traditionally, temporal correctness of a process was discussed with the notions
consistency or satis ability, which require the existence of at least one trace
which meets all temporal constraints. Nevertheless, as several works pointed
out, satis ability is a too weak notion for temporal correctness, since
designers look for stronger guarantees that the violation of temporal constraints can
be avoided. In particular, it is desirable to know at design time, whether all
constraints can be satis ed for all considered circumstances, i.e. for possible
durations and conditions. This need led to the formulation of the notion of
(dynamic) controllability (see [
Time constrained processes with unbounded loops (while loops, repeat-until loops, etc.) can never be dynamically controllable, since the number of iterations and, therefore, the maximum duration of the loop cannot be known at design time or even at run-time before the loop nished. For temporal loops the situation is di erent, as the temporal condition in a t-loop de nes a temporal bound for the duration of a t-loop and hence also limits the number of possible iterations.
For checking, whether a process with t-loops is dynamically controllable, we
follow a model transformation approach [
In the following, we introduce three transformations: the rst is based on an unfolding of the t-loop, which is also the basis for the other 2 transformations, which can be seen as compression of the loop unfolded process and is signi cantly more compact and smaller, while having equivalent dynamic controllability. 3.2
Loop unfolding transforms a process with t-loops to a process without t-loops
with identical behavior (i.e. it admits exactly the same set of traces, resp. the
same set of scenarios). Unfolding of general loops su ers, of course, from the
problem that the number of iterations cannot be known (and may even be
innite). For t-loops we exploit the temporal bound of the loop to terminate the
unfolding procedure. Therefore, the unfolding procedure has to be interleaved
with some temporal calculations. In particular, unfolding has to include the
computation of the earliest possible execution time of nodes, which we represent as
an additional attribute for each node, which will be computed in analogy to the
procedures in [
De nition 4 (earliest execution time). Let P = (N; E; C; !) be a process. For each node n 2 N , the earliest execution time n:e is computed as follows: 1. start:e := 0; 2. for nodes n following a temporal loop with tloop(m; P; c; B): n:e := m:e; 3. for nodes n following a temporal loop with tloop(m; T rue; c; B): n:e := c + 1; 4. for and-join nodes: n:e := max(fm:e + m:dminj(m; n) 2 Eg; 5. for all other nodes: n:e := min(fm:e + m:dminj(m; n) 2 Eg.
We de ne here an elementary transformation step of one elementary unfolding step of one t-loop. The transformation of the whole process is then achieved by the successive application of this elementary transformation step as long as it can be applied, i.e. as long as there is a t-loop in the process.
The elementary transformation step has 2 possible outcomes: if the loop cannot be executed, because the earliest time-point the loop node can be started is after the threshold, then the loop is simply removed. Otherwise, the loop is replaced by an xor-split checking P , nested in its T rue branch a t-split checking the temporal loop condition, and nested within its T rue branch, a copy of the original loop.
Fig. 2 shows a graphical representation of the transformation step in the context of a node A preceding a temporal loop and a node X as immediate successor of the loop. Please note, that according to De nition 1 a loop has exactly one predecessor and exactly 1 successor. XS and XJ represent xorsplit and xor-join, T S and T J denote temporal split and -join. For the formal A de nition of the loop unfold step we use the following shorthand: (a; b; T ) 2 E denotes that b is the T rue successor of a split node a.
follows: Let P = (N; E; C; !) be a process. Let n 2 N with tloop(n; P; c; B). P 0 = (N 0; E0; C0; !) = T 1(P; n) is de ned as: 1. If c < n:e, then n is deleted.
(a) N 0 := N fng; (b) E0 := E f(n; x) 2 E; (y; n) 2 Eg [ f(m; x)j(m; n) 2 E; (n; x) 2 Eg 2. If c n:e, then n is unfolded as follows: (a) N 0 := N [ fXS; XJ; T S; T J; Bg :
XS:type = xor split, XJ:type = xor join, XS:cond = P ,
T S:type = t split, T J:type = t join, B = n:B (b) E0 := E f(n; x) 2 E; (y; n) 2 Eg [ f(y; XS)j(y; n) 2 Eg [ f(XJ; x)j(n; x) 2 Eg [ f(XS; T S; T ); (XS; XJ; F g [ f(T S; B; T ); (T S; T J; F g [ fT J; XJ ); (B; n); (n; T J )g
The rationale for the transformation step is as follows: if the body B of a t-loop n can be entered, it is extracted from the loop block and put in the truebranch of a nesting of xor-split and t-split, which evaluate the same boolean condition, resp. temporal condition of n. This realizes the same semantics as entering one iteration of the loop. A copy of the t-loop following B in the truebranch makes it possible to execute further loop iterations. By iteratively unfolding the t-loop into a nesting of xor-splits and t-splits we obtain a new process model temporally equivalent to the original one, but with all t-loops replaced with the conditional splits.
De nition 6 (Transformation). We de ne the loop-unfolding transformation as follows: Let P = (N; E; C; !) be a process. The loop unfolding transformation T (P ) = P 0 = (N 0; E0; C0; !) is de ned as follows:
If 9n 2 N with tloop(n; P; c; B): P 0 = T (T 1(P; n)). P 0 = P , otherwise. Lemma 1. Let P = (N; E; C; !) be a process. P and T (P ) have the same set of valid scenarios. Proof. It is easy to see that for a tloop(n; P; c; B), a process P and the result of a transformation step T 1(P; n) has the same set of scenarios. The lemma then follows by induction.
With the transformation for loop unfolding we de ned here, we transformed
a process with temporal loops to an equivalent process without temporal loops
(but with temporal splits). For such process, an e ective procedure for checking
the dynamic controllability has been proposed in [
The transformation de ned above generates a series of nested occurrences of the loop body B. For the checking of controllability, howeve,r we do not need all these occurrences of B, since there are no upper- or lower-bound constraints to the loop body admitted. For checking dynamic controllability all we need to know is essentially the possible start and end-times of the loop and thus any temporal restrictions and uncertainties for the adjacent nodes.
Therefore, we present here a much more compact transformation of a temporal loop which is not execution - equivalent to the original process but controllability equivalent.
We rst present the simple transformation for temporally constrained loop without an additional predicate, i.e. a tloop(n; T rue; c; B).
Let P = (N; E; C; !) be a process. Let n 2 N with tloop(n; T rue; c; B). The result of the simple transformation T s(P; n) = P 0 = (N 0; E0; C0; !) is de ned as: 1. N 0 := N [ fT S; T J; B0g, tsplit(T S; c); T J:type = tjoin;
B0:type = activity, B0:dmin = 0; B0:dmax = B:dmax 2. E0 := E [ f(T J; x)j(n; x) 2 Eg [f(x; T S)g f(x; n) 2 Eg [f(T S; T J; F ); (T S; B0; T ); (B0; T J )g 3. C0 := C [ flbc(start; B0:s; c + 1)g
Fig. 3 shows graphically the simple transformation for the case of a t-loop having a condition with P = T rue. The temporal loop tloop(n; T rue; c; B) is replaced by temporal split construct with t-split node T S and t-join node T J . The node T S represents the rst loop split node, T J the last loop-join node. The temporal split node T S has the same temporal conditions as the loop elapsed c. The F alse branch of T S is empty, the T rue branch contains a node B0 which represents the part of the loop body of the last iteration, which is executed after the threshold c. The node B0 is contingent with a minimum duration of 0 and A loop (elapsed ≤ c)
B
X lbc(start, B’.s, c+1)
TS
TJ
X a maximum duration of B:dmax and may not start before or at c expressed by the lower-bound constraint lbc(start; B:s; c + 1).
The rationale for this transformation is follows: (a) If the loop is executed at least once, i.e. the loop condition at least one evaluates to true, i.e. it is executed before the threshold c. This corresponds to executing T S in the transformed graph before the threshold c. In this case, the last iteration starts before or at time-point c and ends after c. The last iteration ends in the fastest case immediately after c, in the slowest case B:dmax after c. This uncertainty is represented by the contingent duration of B0.
(b) If the process arrives at T S after the threshold c, the loop is never executed, and the whole loop is left and the process may continue immediately. Lemma 2. Let P = (N; E; C; !) be a process de nition. Let n 2 N with tloop(n; T rue; c; B) and let P 0 be the result of the simple transformation T s(P; n) = P 0 = (N 0; E0; C0; !). P and P 0 have equivalent sets of valid scenarios. Proof. We consider 2 scenarios as equivalent, if they are identical with the exception that the rst loop-head execution is mapped to the t-split and the last loop-head execution is mapped to the t-join to which the t-loop is mapped to. Then the lemma follows immediately with the rationale detailed above. 3.4
In the case a temporal loop has an additional predicate P , i.e. tloop(n; T rue; c; B) we further have to consider the case where a loop ends before the threshold c, because the predicate P evaluates to F alse.
Fig. 4 shows a graphically the general simple transformation for the case of a t-loop having a an additional condition P .
As in the simple transformation the t-loop is replaced by a t-split structure. While the F alse branch of the t-split is the same, in the general case an Xorstructure (XS, XJ) is inserted into the T rue branch of the t-split. The T rue branch of XS represents the termination of the t-loop because of the temporal condition, and the F alse branch represents the early termination, if P eventually evaluates to F alse. This additional branch contains a dummy activity D with duration 0, as the successor of the loop can be executed without delay. This branch, however can only be nished before or at the threshold c, which is expressed by the upper-bound constraint ubc(start; D:s; c).
A
A
TS Theorem 1. A process model P with temporal loops is dynamically controllable, if each loop body is temporally controllable and the process P = T g(P ) is dynamically controllable.
Proof 1. Proof sketch: The theorem follows from the observation that the process and the transformed process have equivalent sets of valid scenarios.
With this result we now can reduce the checking of the dynamic
controllability of processes with t-loops to checking the dynamic controllability of processes
with t-splits but without t-loops. For these types of processes we already
introduced a checking procedure [
A general overview of time management for work ows, orchestrations, and
business process management and its development over the past 20 years is given in
[
We concentrate here on related work with respect to formulating temporal constraints involving control structures, checking correctness and other temporal properties of process de nitions with such temporal constraints.
BPMN [
[
Controllability and dynamic controllability are the most elaborated notions
of correctness of temporally constrained process de nitions. Recently,
controllability and dynamic controllability for more expressive network models like
Conditional Simple Temporal Network with Uncertainty (CSTNU) provide new
sophisticated means to check the properties of temporally constrained process
de nitions [
Temporal control structures for processes have been introduced in [
Dynamic Controllability has been established as the most suitable criterion for the temporal correctness of process de nitions. However, so far only procedures for acyclic processes have been developed, as processes with loops are by de nition not dynamically controllable. The introduction of temporally constrained loops in process models opens interesting new possibilities for representing temporal constraints in process models with loops. Here we showed how dynamic controllability of processes with temporal loops can e ectively be checked at design time. The proposed procedure relies on a series of transformations of process de nitions with the nal target of mapping a process de nition to simple temporal networks with uncertainty and decisions (CSTNUD), for which procedures for checking dynamic controllability have been proposed. For practical implementations, however, a process model can be directly translated to an equivalent CSTNUD, short-cutting the series of transformations.