Marin Bougeret
email: bougeret@imag.fr

Pierre François Dutot
email: pfdutot@imag.fr

Klaus Jansen

Christina Otte

Denis Trystram
email: trystram@imag.fr

Approximating the non-contiguous Multiple Organization Packing Problem

We present in this paper a 5 /2-approximation algorithm for scheduling rigid jobs on multi-organizations. For a given set of n jobs, the goal is to construct a schedule for N organizations (composed each of m identical processors) minimizing the maximum completion time (makespan). This algorithm runs in O(n(N + log(n)) log(npmax)), where pmax is the maximum processing time of the jobs. It improves the best existing low cost approximation algorithms. Moreover, the proposed analysis can be extended to a more generic approach which suggests different job partitions that could lead to low cost approximation algorithms of ratio better than 5 /2.

Problem statement

In this paper we consider the problem of scheduling rigid jobs on Multi-organizations. An organization is a set of m identical available processors. A job j must be executed on q j processors (sometimes called the degree of parallelism) during p j units of time. The q j processors must be allocated on the same organization. The makespan of the schedule is defined as the maximum finishing time over all the jobs. Given a set of n jobs, the goal is to find a non-overlapping schedule of all the jobs on N organizations while minimizing the makespan.

This problem is closely related to strip packing problems. Indeed, if we add the constraint of using contiguous processors, then scheduling a job j on q j contiguous processors during p j units of time is equivalent to packing a rectangle of width q j and height p j .

Related works. Strip packing, rigid jobs scheduling and Multi-organizations scheduling problems are all strongly N P -hard, and Zhuk [START_REF] Zhuk | Approximate algorithms to pack rectangles into several strips[END_REF] showed that there is no polynomial time approximation algorithm with absolute ratio better than 2 for strip packing.

For Strip Packing problem, Coffman et al. gave in [START_REF] Coffman | Performance bounds for level-oriented two-dimensional packing algorithms[END_REF] an overview about performance bounds for shelf-oriented algorithms as N F DH (Next Fit Decreasing Height) and F F DH (First Fit Decreasing Height). These algorithms have a approximation ratio of 3 and 2.7, respectively. Schiermeyer [START_REF] Schiermeyer | Reverse-fit: A 2-optimal algorithm for packing rectangles[END_REF] and Steinberg [START_REF] Steinberg | A strip-packing algorithm with absolute performance bound 2[END_REF] presented independently an algorithm for Strip Packing with absolute ratio 2. A further important result for the Strip Packing problem is an AFPTAS with additive constant O( 1 /ǫ 2 ) of Kenyon and Rémila [START_REF] Kenyon | A near-optimal solution to a two-dimensional cutting stock problem[END_REF]. This constant was improved by Jansen and Solis-Oba, who presented in [START_REF] Jansen | New approximability results for 2-dimensional packing problems[END_REF] an APTAS with additive constant 1. Concerning the multi-strip packing problem, there is a 2 + ǫ approximation in [START_REF] Ye | On-Line Multiple-Strip Packing[END_REF] whose algorithmic cost is doubly exponential in 1 ǫ . In [START_REF] Bougeret | Approximation algorithm for multiple strip packing[END_REF] we gave a 2 approximation with a large algorithmic cost and an AFPTAS for this problem.

Let us now review the related work about rigid job scheduling. For one organization, the famous List Algorithm for scheduling with resource constraints of Garey and Graham [START_REF] Garey | Bounds for multiprocessor scheduling with resource constraints[END_REF] can be applied (when there is only one resource to share) to schedule rigid jobs, and is then a 2 approximation. The rigid job scheduling problem on multi-organization has been studied with an on-line setting in [START_REF] Schwiegelshohn | Online scheduling in grids[END_REF]. The authors achieved a ratio of 3 without release times (and 5 with release times). Notice that these results do not require the knowledge of the processing times of the jobs. Moreover, the organizations may have a different number of processors. The rigid job scheduling problem on multi-organizations has been extended in [START_REF] Dutot | Approximation algorithms for the multi-organization scheduling problem[END_REF] for the case where the jobs are submitted to local queues on each cluster with the extra constraint that the initial local schedules must not be worsened. The authors provide a 3-approximation.

Generally, the results about rigid job scheduling cannot be adapted to the more constrained contiguous version. To the best of our best knowledge, there is still no (reasonable) α such that for any instance I, Optc(I) ≤ αOptnc(I) (where Optc denotes the contiguous optimal value and Optnc the non-contiguous one). The authors of [START_REF] Dutot | Handbook of Scheduling[END_REF] show that α > 1 by constructing a (rather) simple instance with 8 jobs and 4 machines.

Our contribution. In this paper, we present a 5 2 approximation algorithm for the rigid job scheduling problem on multi-organizations that runs in O(n(N +log(n)) log(np max )), where p max is the maximum processing time of the jobs. Moreover, we suggest how the approach used for the 5 /2-algorithm could extended to get approximation algorithms with better ratio and a low algorithmic cost.

Organization of the Paper. The preliminaries for the 5 /2-approximation are in Section 2. In Section 3.1 to 3.4 we describe how to construct a preallocation of the "big" jobs that fits in the targeted makespan. In Section 4 we show how to turn this preallocation into a compact schedule, and in Section 5 we analyze the complexity of the algorithm. The discussions on the approach are in Section 6.

Principle and definitions

Let us now give some definitions that are used throughout the proofs and the description of the algorithm. We first extend the previous p j and q j notations to Q(X) and P (X) where X is a set of jobs. We also define the surface (sometimes also called the area) of a set of jobs as S(X) = Σ j∈X q j p j . A layer is a set of jobs which are scheduled sequentially on the same organization. The length of a layer Lay is P (Lay), the sum of the processing time of all the jobs in Lay. A shelf is a set of jobs which are scheduled on the same organization, and which start at the same time. Given a shelf sh, the value Q(sh) is called the height of sh. What we call a bin can be seen as a reservation of a certain number of processors (generally m) during a certain amount of time. The algorithm will add some jobs to bins, and given a bin b, we denote by Q(b) the value Σ {j∈b} q j . Given a sequence of bins seq, we denote by Q(seq) the value Σ b∈seq Q(b). These notations are extended in the same way for P and S. In the whole paper, we consider that the sets of jobs used as parameters in the algorithms are modified after the calls.

Let us sketch how 5 /2 algorithm is constructed. Let OP T denote the value of an optimal solution. We target a 5 2 ratio by both ensuring that, for each organization at least half of the processors are used at any time before the starting time of the last job, and that the small jobs (whose processing time is lower than OP T /2 and height lower than m /2) are scheduled at the end. Thus, if the makespan of the final schedule is due to a small job, it is lower than the processing time of the small job plus the starting time of this job, implying a makespan lower than OP T /2 + 2OP T = 5OP T /2. As the optimal value is not known, we use the well known dual approximation technique [START_REF] Hochbaum | A polynomial approximation scheme for scheduling on uniform processors: Using the dual approximation approach[END_REF]. Let w denote the current guess of OP T . The schedule is built in three steps. In the first one we compute a preallocation π 0 of the "big" (p j > w /2 or q j > m /2) jobs. Then we apply a list algorithm which turns π 0 into a "compact" schedule π 1 (see Section 4). Finally, the final schedule π is constructed by adding to π 1 the small remaining jobs using again a list algorithm (see also Section 4).

Let us define the following sets:

• let L H = {j|q j > m /2} be the set of high jobs • let L XL = {j|p j > 3w /4} be the set of extra long jobs • let L L = {j| 3w /4 ≥ p j > w /2} be the set of long jobs

• let L B = (L XL L L ) L H be the set of huge jobs • let I ′ = L H L XL L L
We will prove that either we schedule I with a resulting makespan lower than 5w /2, or w < OP T . Notice that for the sake of simplicity we did not add the "reject" instructions in the algorithm. Thus we consider in all the proof that w ≥ OP T , and it is implicit that if one of the claimed properties is wrong during the execution, the considered w should be rejected. Notice that we only consider the w values such that Q(L XL L L ) ≤ N m and P (L H ) ≤ N w.

We start by providing in Section 3 the three phase algorithm Build P realloc that builds the preallocation π 0 of the jobs of I ′ . We will denote by π i 0 the set of preallocated jobs in organization O i . In phase 1 we preallocate the high jobs. In phase 2 and phase 3 we preallocate the long and extra long jobs by first packing shelves of jobs into bins, and then putting these bins into organizations. An example of a preallocation is depicted Figure 1.

3 Construction of the preallocation

Phase 1

Let N 1 be the number of organizations used in phase 1. In phase 1, the jobs of L H are packed in N 1 organizations. The Create Layer(X, l) procedure creates a layer Lay of length at most l, using a Best Fit (according to the processing times) policy (BFP). Thus, Create Layer(X, l) add at each step the longest job that fits. Thus, phase 1 calls for each organization (until

L H is empty) Create Layer(L H , 5w /2).
Let us introduce some notations. Let Lay i denote the set of jobs scheduled in the layer created in organization O i . Let L 1 XL and L 1 L denote the remaining jobs of L XL and L L after phase 1. Thus, for the moment we have

π i 0 = Lay i for all i ≤ N 1 . Lemma 1 (phase 1). If ∃i 0 < N 1 such that P (π i0 0 ) ≤ 2w then it is straight- forward to pack all the jobs of I ′ . Otherwise, we get ∀i ∈ {1, . . . , N 1 -1}, S(π i 0 ) > wm and N 1 ≤ ⌈ N /2⌉ .
Proof. First let us notice that phase 1 ends, as P (L H ) ≤ N w and P (π i 0 ) > w for every organization where we do not run out of jobs to schedule. We first suppose that ∃i 0 < N 1 such that P (π i0 0 ) ≤ 2w. In this case we just have to prove that it is straightforward to preallocate L XL L L . We proceed by contradiction by supposing that we never ran out of jobs of L XL L L . When the algorithm creates a layer for a organization i, we know due to the BFP order that it will pack at least two jobs of L B , if L B is not empty. The hypothesis implies that during the execution of phase 1, L H \ L B was empty before L B . Thus, for i < N 1 , there is at least two jobs of L B in π i 0 , meaning that ∀i with 1

≤ i < N 1 , Q((L XL L L ) π i 0 ) > m.
Concerning the N -N 1 other organizations, we can create shelves of jobs of L L L XL using a best fit according to the height (BFH), implying that each shelf has a height of at least 2m /3 according to Lemma 2. Packing two shelves in each organization, we get ∀i

> N 1 , Q((L XL L L ) π i 0 ) > 4m /3 > m. Finally, let us check what is scheduled in organization N 1 . If two jobs of L B are scheduled in this organization, then Q((L XL L L ) π N1 0 ) > m. If one job of L B is scheduled, then we create one shelf of jobs of L XL L L , and Q((L XL L L ) π N1 0 ) > m /2 + 2m /3.
If no huge job is scheduled in organization N 1 , we pack as before two shelves of jobs of L XL L L . Thus, if in every case we have

Q((L XL L L ) π N1 0 ) > m. Thus, we get Q((L XL L L )) > N m, which is impossible.
Let us prove the second part of the lemma. First notice that for any

i < N 1 , S(π i 0 ) > 2w m /2 = mw. Moreover, we have 2(N 1 -1)w < Σ N1 i=1 P (π i 0 ) = P (L H ) ≤ N w, implying N 1 ≤ ⌈ N /2⌉.⊓ ⊔
Thus, we now assume until the end of the proof that we are in the second case of Lemma 1 where ∀i ∈ {1, . . . , N 1 -1}, S(π i 0 ) > mw and N 1 ≤ ⌈ N /2⌉.

Phase 2

In phase 2 the jobs of L The procedure P ack Shelf (X, b, f ) creates a shelf sh using the Best Fit (according to the height) policy (BFH), and packs it into bin b. The f parameter represents the available height of b (meaning that b corresponds to f free processors during a certain amount of time), implying of course that Q(sh) ≤ f . Thus P ack Shelf (X, b, f ) adds at each step the highest possible job of X that fits. We assume that the length of the bin is larger than p j , for all j ∈ X.

The procedure GreedyP ack(X, seq) creates for each empty bin b ∈ seq one shelf of jobs of X using P ack Shelf (X, b, m). This procedure returns the last bin in which a shelf has been created. Let us now come back to the description of phase 2.

Depending on the set of jobs already scheduled in O N1 , the Create P adding() procedure creates n binL empty bins of length 3w /4 and n binXL empty bins of length w, which are added in organization O N1 . Let us define for each case how many bins of each type are created by Create P adding():

• If P (Lay N1 ) ∈] 3w /2, 7w /4] then set (n binL , n binXL ) to (1, 0) • If P (Lay N1 ) ∈]w, 3w /2] then set (n binL , n binXL ) to (0, 1) • If P (Lay N1 ) ∈] 3w /4, w] then if Q(L 1 L ) ≥ 5 /4 then set (n binL , n binXL ) to (2, 0) else set (n binL , n binXL ) to (0, 1) • If P (Lay N1 ) ∈] w /2, 3w /4] then set (n binL , n binXL ) to (1, 1) • If P (Lay N1 ) ∈ [0, w /2] then set (n binL , n binXL ) to (0, 2)
Let pad L be a sequence of n binL bins of length 3w /4 and pad XL be a sequence of n binXL bins of length w. Create P adding() returns (pad L , pad XL ). All in all, phase 2 can be described by the following procedure calls:

• Let (pad L , pad XL ) = Create P adding() • GreedyP ack(L 1 XL , pad XL ) • GreedyP ack(L 1 L , pad L ) • GreedyP ack(L 1 L , pad XL ) 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1

Phase 3

In phase 3 we first schedule the jobs of L 2 XL using the N 2 = N -N 1 remaining organizations. Then, we schedule the jobs of L 2 L using also this N 2 organizations. Finally, the possibly remaining jobs of L 2 L are added to the last bin used for the extra long jobs. Therefore, let us define the add(X, b) procedure. The add(X, b) procedure packs one or two "small" shelves of jobs of X in the bin b (starting from the top of the bin for the sake of clarity). Notice that, as b will be the last bin used for extra long jobs, the available height (for the jobs of X) in b will be generally lower than m. Here is the description of add(X, b): An example of a call to the add procedure is given in Figure 1 for the case where l = 2. We now define two sequences of bins seq XL and seq L , such that every bin of seq XL (resp. seq L ) will (possibly) contains one shelf of jobs of L 2 XL (resp. L 2 L ). Notice that a free organization can be seen as two bins of length w (and height m), three bins of length 3w /4, or one bin of length w and two bins of length 3w /4. Thus, seq XL is composed of 2(N - All in all, phase 3 can be described by the following procedure calls:

• If the
• Let last = GreedyP ack(L 2 XL , seq XL ) • GreedyP ack(L 2 L , seq L )
• add(L 2 L , last) Let start the analysis of phase 3 with a remark about P ack Shelf (X, b, f ). Lemma 2. Let Sh denote the shelf created by P ack Shelf (X, b, f ). If we know that the k highest jobs of X fit in f , then Q(Sh) > k k+1 f . Proof. Let x be the cardinal of X. Let us assume that q i ≥ q i+1 for 1 ≤ i < x. Let i 0 ≥ k+1 be the first index such that job i 0 is not in Sh. Let a = Σ i0-1 i=1 q i . We have Q(Sh) ≥ a ≥ (i 0 -1)q i0 > (i 0 -1)(fa) leading to a > i0-1 i0 f ≥ k k+1 f .⊓ ⊔ Lemma 3 (phase 3). If there remains an unscheduled job after phase 3, then

S(L 2 XL L 2 L ) > (N 2 + 1 /8)mw. Proof. Let us first suppose that L 2 XL = ∅. Let a XL = 2(N -N 1
) be the number of bins in seq XL . After having filled the first a XL -1 bins (using a width of at least 2 /3 according to Lemma 2), the width of remaining jobs of L 2 XL is strictly larger than m. Thus we get Q(L 2 XL ) > 2m /3(a XL -1) + m = 4m /3N 2 + m /3 and S(L 2 XL ) > (N 2 + 1 /4)mw.

We now suppose that L 2 XL = ∅. In every organization that contains two bins of jobs of L 2 XL , the total scheduled area is strictly larger than 2 × 2m /3 × 3w /4 = wm. In every organization that contains three bins of jobs of L 2 L , the total scheduled area is strictly larger than 3 × 2m /3 × w /2 = wm. We have to consider two cases according to the position of the last bin last (the left side of last may be located at time 0 or w). Let i 0 be the index of the organization that contains last.

In the first case where the left side of last is at time 0, two bins (of length 3w /4 and height m) were created after the bin last in organization O i0 . Then, if the remaining jobs of L 2 L do not fit in last, the total area of the jobs scheduled in organization O i0 is strictly larger than (2 2m /3 + m) w /2 > 7wm /6. Then we just sum the area packed over all the organizations, and get the desired result.

In the second case where the left side of last is at time w (as depicted in Figure 1), the only room in organization O i0 to schedule jobs of L 2 L is in last. In organization O i0 , the area of (extra long) jobs contained in the first bin is strictly larger than wm /2. The add procedure will create two shelves (one next to the other) of jobs of L 2 L in last. Let last ′ and L ′ L be the set of jobs in last and L 2 L respectively, just before the call of the add procedure. If Q(last ′ ) > m /2, and as the remaining jobs of L 2 L don't fit in last, we have that 1) then add creates a first shelf of jobs of L 2

Q(L ′ L ) > m -Q(last ′ ) ′ . This implies S(last ′ L ′ L ) > 3w /4Q(last ′ ) + w /2(m -Q(last) ′ ) > 5wm /8. If Q(last ′ ) ≤ m /2 (see Figure
L of height at least (m-Q(last ′ )) /2, and then tries to pack the remaining jobs in the second shelf. Thus in this case, S(last

′ L ′ L ) > 3w /4Q(last ′ ) + w /2 (m-Q(last ′ )) 2 + m -Q(last ′ ) > 3mw /4.⊓ ⊔

Main algorithm

In this section we recall the overall algorithm that builds the preallocation, and we provide the main proof of the preallocation. Notice that we drop the L i L and L i XL notations for writing the algorithm as we consider that the sets of jobs (used as parameters in the procedures) are modified after the calls.

Algorithm 1 Build Prealloc(I ′ ) Phase 1 [START_REF] Zhuk | Approximate algorithms to pack rectangles into several strips[END_REF] Let i = 0

[2] Let i = i + 1, and let Lay i = Create Layer(L H , 5w /2) Pack Lay i in organization S i from time 0 [START_REF] Schiermeyer | Reverse-fit: A 2-optimal algorithm for packing rectangles[END_REF] Repeat step 3 until L H is empty Phase 2 [START_REF] Steinberg | A strip-packing algorithm with absolute performance bound 2[END_REF] Let (pad L , pad XL ) = Create P adding() [START_REF] Kenyon | A near-optimal solution to a two-dimensional cutting stock problem[END_REF] Let last = GreedyP ack(L XL , pad XL ) [START_REF] Jansen | New approximability results for 2-dimensional packing problems[END_REF] Call GreedyP ack(L L , pad L ) [START_REF] Ye | On-Line Multiple-Strip Packing[END_REF] Call GreedyP ack(L L , pad XL ) Phase 3 [START_REF] Bougeret | Approximation algorithm for multiple strip packing[END_REF] Let seq XL and seq L be defined as described in Section 3.3 [START_REF] Garey | Bounds for multiprocessor scheduling with resource constraints[END_REF] Let last 2 = GreedyP ack(L XL , seq XL )

[10] If last 2 is not null, set last to last 2 [START_REF] Dutot | Approximation algorithms for the multi-organization scheduling problem[END_REF] Call GreedyP ack(L L , seq L ) [START_REF] Dutot | Handbook of Scheduling[END_REF] Call add(L L , last)

Theorem 1. Build P realloc(I ′ ) creates a preallocation π 0 of makespan lower than 5w /2.

Proof. Remind that L 1 XL and L 1 L denote the remaining jobs of L XL and L L after Phase 1. The makespan of the preallocation is by construction lower than 5w /2. We know that according to Lemma 1 phase 1 terminates and the area scheduled in the first N 1 -1 organizations is greater than (N 1 -1)wm. We proceed by contradiction by supposing that L 3 then S(Lay N1 pad 1 XL ) > mw and we conclude with Lemma 3. Otherwise, the N 2 remaining organizations are available for L 1 L . Moreover, remind that in this case the only bin in pad XL will be used for jobs of L L during the call of add. Then, if L 1 L does not fit, we have

Q(L 1 L L 1 XL ) > (2N 2 + 1)m and S(Lay N1 L 1 L L 1 XL ) > mw 2 + N 2 wm + wm 2 = (N 2 + 1)mw.
If w ≥ P (Lay N1 ) > 3 4 w, then S(Lay N1 ) > 3 8 mw and two cases are possible according to the value of

Q(L 1 L ). If Q(L 1 L ) ≥ 5m 4
, CreateP adding creates two bins of length 3 4 w. Then, S(Lay N1 pad L ) > ( 3 8 + 5 8 )mw and we conclude with Lemma 3. Otherwise, if Q(L 1 L ) < 5m 4 , CreateP adding creates one bin pad XL of length w. If Q(pad XL ) (after the call line 5) is larger than 2m 3 then S(Lay N1 pad 1 XL ) > 7 8 mw and we conclude with Lemma 3. Otherwise, jobs of L 1 XL are all scheduled in pad XL . As N 2 ≥ 1, at least three bins are available for L 1 L , which is sufficient given that Q(L 1 L ) < 5m 4 . If 3 4 w ≥ P (Lay N1 ) > 1 2 w, then S(Lay N1 ) > 1 4 mw and CreateP adding creates one bin of length w and one bin of length 3 4 w. If extra long jobs are not scheduled at the end of the algorithm, then S(Lay N1 pad XL ) > 3 4 mw. Since L 2

XL do not fit into N 2 free organizations, we have also S(L 2 XL ) > (N 2 + 1 4 )mw. Thus we conclude that the extra long jobs are successfully scheduled. Let us suppose now that the long jobs are not completely scheduled.

If Q(pad XL ) ≥ 5m 9 then S(Lay N1 pad XL pad L ) > ( 1 4 + 5 12 + 1 3 )mw = mw. Otherwise, let L ′ L
denote the set of remaining jobs of L 1 L just before the call to add. The area scheduled in the N 2 last organizations is larger than the one scheduled in the optimal. If L ′ L does not fit in pad XL during the call to add, then

Q(L 1 XL + L ′ L ) > m and S(Lay N1 pad L pad XL L ′ L ) > ( 1 4 + 1 3 + 1 2 )mw > mw. If 1
2 w > P (Lay N1 ), CreateP adding creates two bins of length w.

If N 1 > 1, then S( N1 i=1 Lay i ) > S( N1-2 i=1 Lay i ) + 5 4 mw > (N 1 -1)mw + 1
4 mw because the first job of Lay N1 does not fit in the previous organization. Thus, if Q(L 1 XL ) > m then we have S( N1 i=1 Lay i pad XL ) > N 1 mw and we conclude with Lemma 3. Otherwise, we have an empty bin in the sequence pad XL and N 2 free organizations available for From now on, we suppose that the preallocation π 0 is built. For each organization O i , π 0 indicates first a (possibly empty) sequence of high jobs j i 1 , . . . , j i xi that have to be scheduled sequentially from time 0. Then, π 0 contains an ordered sequence of shelves Sh i 1 , . . . , Sh i x ′ i . Moreover, the makespan of π 0 is by construction less than 5w /2. Definition 1. Let u i (t) be the utilization of organization O i at time t, i.e. u i (t) is the sum of all the q j for any job j which scheduled on organization i at time t. A schedule is 1 /2 compact if and only if for every organization O i there exists a time t i such that for all t ≤ t i , u i (t) ≥ m /2 and u i restricted to t > t i is not increasing.

L 1 L . Let L ′ L be L 1 L before the call to add. If add does not schedule L ′ L in last then Q(L 1 XL )+Q(L ′ L ) > m and S( N1 i=1 Lay i L 1 XL L ′ L ) > (N 1 -3 4 + 1 3 + 1 2 )mw > N 1 mw. If N 1 ≤
Let us now describe the algorithm LS π0 which turns π 0 into a 1 /2 compact schedule π 1 of I ′ . We first define the procedure Add Asap(X, O i ) which scans organization O i from time 0, and for every time t starts any possible job(s) in X that fit(s) at time t. The LS π0 works as follows: for every organization O i , pack first sequentially the high jobs j i

x for 1 ≤ x ≤ x i and then call Add Asap(Sh x , O i ) for 1 ≤ x ≤ x ′ i .

Lemma 4. The makespan of π 1 is lower than the one of π 0 , and π 1 is 1 /2 compact.

Proof. Let σ i be a schedule in a (single) organization O i (of makespan C i ), let X be a set of jobs and let σ ′ i be the schedule (of makespan C ′ i ) produced by Add Asap(X, O i ). If σ i is 1 /2 compact and if forall j ∈ X, q j ≤ m /2, then σ ′ i is 1 /2 compact. The proof is straightforward by induction on the cardinality of X. Moreover, if X q j ≤ m, then C ′ i ≤ C i + max X p j because in the worst case all the jobs of X only start at time C i . Using these two properties, we prove the lemma for every organization O i by induction on the number of call(s) to Add Asap(Sh x , O i ).⊓ ⊔ Remark 1. Notice that in Lemma 4 we do not take care of the particular structure which occurs when add creates two shelves of jobs of L L as depicted Figure 1. However, it is easy to see that the proof can be adapted. Now that π 1 is built, we add the small remaining jobs (I \ I ′ ) using a list algorithm that scans all the organizations from time 0 and schedules as soon as possible any non scheduled job. Let π denote the obtained schedule.

Theorem 2. The makespan of π is lower than 5w /2.

Proof. The proof is by induction on the cardinal of I \ I ′ . At the beginning, π 1 is 1 /2 compact, as proved in Lemma 4. Each time a job j is scheduled by the list algorithm, the obtained packing remains 1 /2 compact because q j ≤ m 2 . Thus it is clear that π is 1 /2 compact.

Let us assume that the makespan of π is due to a job j ∈ I \ I ′ that starts at time s. As π is 1 /2 compact, this implies that when scheduling job j we had t i ≥ s for any organization i. Thus, we have S(I) > N i=1 ti 2 ≥ N s 2 , implying that s < 2w, and thus that the makespan of π is lower than 5w /2.⊓ ⊔

Complexity

Phase 1 can be implemented in O(N n + n log(n)). Indeed, we first sort the high jobs in non increasing order of their processing times. Then, each layer can be created in O(n). Phase 2 and phase 3 can also be implemented in O(N n + n log(n)) by sorting the long (and extra long) jobs in non increasing order of their required processors. Thus π 0 is constructed in O(N n + n log(n)).

The LS π0 algorithm can be implemented in O(n log(n)). Instead of scanning time by time and organization by organization, this algorithm can be implemented by maintaining a list that contains the set of "currently" scheduled jobs. The list contains 3-tuples (j, t, i) indicating that job j (scheduled on organization i) finishes at time t. Thus, instead of scanning every time from 0 it is sufficient to maintain sorted this list according to the t values (in non decreasing order), and to only consider at every step the first element of the list. Then, it takes O(log(n)) to find a job j 0 in the appropriate shelf that fits at time t, because a shelf can be created as a sorted array. It also takes O(log(n)) to insert the new event corresponding to the end of j 0 in the list.

The last step, which turns π 1 into the final schedule can also be implemented in O(n log(n)) using a similar global list of events. Notice that for any organization O i , there exists a t i such that before t i the utilization is an arbitrary function strictly larger than m /2, and after t i a non increasing after. Scheduling a small job before t i would require additional data structure to handle the complex shape. Thus we do not schedule any small job before t i as it is not necessary for achieving the 5 /2 ratio. Therefore, we only add those events that happen after t i when initializing the global list for this step. To summarize, for this step we only need to sort the small jobs in non increasing order of their required number of processors, and then apply the same global list algorithm.

The binary search on w to find the smallest w which is not rejected can be done in O(log(np max )) as all the processing times can be assumed to be integers. Thus the overall complexity of the 5w /2 approximation is in O(log(np max )n(N + log(n))).

Toward better approximation ratios

In this paper we provided a low cost 5 /2-approximation algorithm using a new approach. We discuss in this section how the proposed approach can be used for reaching better approximation bounds. The approach can be summarized in the two following main steps. The first one consists in constructing a 1 /2 compact schedule π 1 of the big jobs I ′ by creating a pre-allocation π 0 and "compressing" it. Then, the remaining small jobs (I \ I ′ ) are added to π 1 in a second step using the classical list scheduling algorithm LS.

We would like to recall the arguments that make our second step easy to analyze, and see what could be some other promising partitions. In our partition, the second step guaranties a makespan lower than 5w /2 because:

• adding a job j with q j ≤ m /2 to a 1 /2 compact schedule with LS produces another 1 /2 compact schedule, • if the makespan is due to a small job j 0 that starts at time s 0 , then s 0 ≤ 2w (since the schedule is 1 /2 compact), leading to a makespan lower than s 0 + p j0 ≤ 5w /2.

Let us now propose other partitions that could be considered. We could define I ′ = {j|q j > αm i or p j > βw} with appropriate values 0 < α < 1 and 0 < β < 1. Then, the previous steps become:

1. construct a pre-allocation π 0 of I ′ (for instance based on shelves and layers) and make sure that, when compressed using LS π0 , the obtained schedule π 1 is 1α compact (meaning that for every organization, the utilization is greater than 1α, and then it is non-increasing), 2. add the small remaining jobs (I \ I ′ ) using LS.

Thus, the makespan of jobs added in the second step would be bounded by b = ( 11-α + β)w, implying that the makespan of the pre-allocation should also be bounded by b.

For example, we can target a 7 /3 ratio by only studying how to pre-allocate I ′ = {j|q j > mi 2 or p j > w 3 }, or a ratio 2 by studying how to pre-allocate I ′ = {j|q j > mi 3 or p j > w 2 }. Obviously, if the preallocation is built using again shelves and layers, the difficulty will probably arise when merging the different types of jobs (high, extra long or long ones for example), and will may be only need to handle more particular cases.

Let us remark that this technique will not be easy to apply with (contiguous) rectangles, since the property of 1 /2 compactness becomes hard to guarantee.

Fig. 1 .

 1 Fig. 1. An example of pre-allocation

  left side of b is at time w then let l = 2 else let l = 1 • Repeat l times the call P ack Shelf (X, b, m -Q(b)) and pack the created shelves in b.

  N 1 ) bins b 1 , . . . , b 2(N -N1) of length w, considering that we created two bins in each of the organizations {O N1+1 , . . . O N }, starting from O N1+1 . This implies that for all i ≥ 1, bins b 2i-1 and b 2i are in O N1+i . The sequence seq L is composed of 3(N -N 1 ) bins b ′ 1 , . . . , b ′ 3(N -N1) of length 3w /4, considering that we created three bins in each of the organizations {O N1+1 , . . . O N }, from O N to O N1+1 . This implies that for all i ≥ 1, bins b ′ 3i-2 , b ′ 3i-1 and b ′ 3i are in O N -i+1 . Notice that these two sequences are not ordered in the same way.

1 XL L 1 L .⊓ ⊔ 4

 114 1 then we have two bins of length w in each of the N organizations, which is of course sufficient to pack L From the preallocation to the final schedule

1

  XLL1 L are scheduled in organization N 1 by creating shelves according to what is already scheduled in organization N 1 . We denote by L 2 XL and L 2 L the remaining jobs of L 1 XL and L 1 L after phase 2. Let us first define two procedures used for phase 2 and phase 3.

1

  XL L 1L is not empty after Phase 2 and Phase 3, and showing that S(I ′ ) > N mw. We proceed by case analysis according to what is scheduled in O N1 . Recall that the jobs of L 1 L are first scheduled in pad L . If Q(pad L ) is larger than m 2 , then S(Lay N1 pad L ) > 3 4 mw + 1 4 mw = mw. Thus, the total area packed in the first N 1 is strictly larger than N 1 wm. Then, according to Lemma 3, L 2 P (Lay N1 ) > w, then S(Lay N1 ) > 1 2 mw and CreateP adding creates one bin of length w. If Q(pad XL ) is larger than 2m

	If P (Lay N1 ) > 7 4 w, then S(Lay N1 ) > 7 8 mw and CreateP adding doesn't create any bin. If L 1 XL and L 1 L are not completely scheduled by phase 3, then according to Lemma 3 we get S(L 1 XL L 1 L ) > (N 2 + 1 8 )mw. Thus in this case we have S(Lay N1 L 1 L 1 XL If 7 4 w ≥ P (Lay N1 ) > 3 2 w, then S(Lay N1 ) > 3 4 mw and CreateP adding cre-ates one bin of length 3 4 w. XL L 2 L must fit in the N 2 remaining organizations. If Q(pad L ) ≤ m 2 , then the N 2 remaining organizations are available for L 1 XL . Thus, if L 1 XL = ∅ at the end, then S(L 1 XL ) > (N 2 + 1 XL ) > 4 )mw, and S(Lay N1 L 1 (N 2 + 1)mw. If 3 2 w ≥

L ) > (N 2 + 1)mw, implying S(I ′ ) > N mw.

⋆ This work has been supported by DGA-CNRS


Nisansala Yatapanage

Kirsten Winter

Saad Zafar

Slicing Behavior Tree Models for Verification

Program slicing is a reduction technique that removes irrelevant parts of a program automatically, based on dependencies. It is used in the context of documentation to improve the user's understanding as well as for reducing the size of a program when analysing. In this paper we describe an approach for slicing not program code but models of software or systems written in the graphical Behavior Tree language. Our focus is to utilise this reduction technique when model checking Behavior Tree models. Model checking as a fully automated analysis technique is restricted in the size of the model and slicing provides one means to improve on the inherent limitations. We present a Health Information System as a case study. The full model of the system could not be verified due to memory limits. However, our slicing algorithm renders the model to a size for which the model checker terminates. The results nicely demonstrate and quantify the benefits of our approach.

Introduction

Detecting problems early in the software life cycle, in the modelling and design phase, would greatly reduce the costs involved. Formal models of systems allow for rigorous analyses to be conducted. The Behavior Tree graphical modelling language [START_REF] Dromey | From requirements to design: Formalizing the key steps[END_REF][START_REF] Dromey | Genetic design: Amplifying our ability to deal with requirements complexity[END_REF], which has a formal semantics, has been proposed as a support for engineers handling the complexity of large systems. Behavior Tree models maintain a strong connection with the original textual requirements of the system. Behavior Trees can be automatically translated into model checking languages for verification [START_REF] Grunske | An automated failure mode and effect analysis based on high-level design specification with behavior trees[END_REF][START_REF] Grunske | Defining the abstract syntax of visual languages with advanced graph grammars-a case study based on Behavior Trees[END_REF][START_REF] Colvin | Timed behavior trees for failure mode and effects analysis of time-critical systems[END_REF].

Model checking [START_REF] Baier | Principles of Model Checking[END_REF] is an automated verification technique that exhaustively searches the state space to determine whether or not a given property holds for the system. A major limitation of model checking is what is known as the state explosion problem. It refers to the possibly exponential number of states produced from even a small number of system components. This prevents model checking from being applied to larger systems. The model checker may run out of memory resources before providing a result, or may take a prohibitively large amount of time to solve the verification problem.

This paper describes a technique for reducing Behavior Tree models prior to model checking, in order to reduce the time and memory resources required. We propose using a technique known as slicing [START_REF] Weiser | Program slicing[END_REF], which has been traditionally applied to programs to aid in understanding and debugging (see [START_REF] Tip | A survey of program slicing techniques[END_REF] and [START_REF] Xu | A brief survey of program slicing[END_REF] for comprehensive surveys).

The objective of this technique is to eliminate those parts of the program that are not relevant in the current context. In doing so slicing can significantly reduce the size of the investigated program.

Although most applications of slicing have been programs, slicing has also been applied to specifications. In particular, slices have been created from Z specifications [START_REF] Oda | Specification slicing in formal methods of software development[END_REF][START_REF] Wu | Slicing Z specifications[END_REF], hierarchical state machines in the RSML specification language [START_REF] Heimdahl | Reduction and slicing of heirarchical state machines[END_REF] and Extended Finite State Machines [START_REF] Dorel | Slicing of state-based models[END_REF]. The aim of these approaches is to support understanding.

Slicing in the context of automated analysis aims at eliminating those parts of the model that have no effect on whether the property to be checked is satisfied by the model or not. Thus, the approach requires a new type of slicing criterion which is derived from the property, often given as a temporal logic formula. This criterion may not refer to a specific program statement; instead several statements could be the slicing targets. In [START_REF] Hatcliff | Slicing software for model construction[END_REF], Hatcliff et al. present the foundations of "property-directed" slicing in which formulas given in linear temporal logic (LTL) [START_REF] Emerson | Temporal and modal logic[END_REF] without using the next state operator provide the slicing criteria.

Whereas Hatcliff et al. apply their technique to Java code, other approaches propose slicing for models of software or systems given in, e.g., the SPIN input language Promela [START_REF] Millett | Slicing promela and its applications to model checking, simulation and protocol understanding[END_REF], the SAL language [START_REF] Ganesh | Slicing SAL[END_REF] and timed automata as used by the UPPAAL tool [START_REF] Thrane | Slicing for UPPAAL[END_REF]. Leuschel et al. [START_REF] Leuschel | The MEB and CEB static analysis for CSP specifications[END_REF] apply slicing to CSP models and Brückner and Wehrheim [START_REF] Brückner | Slicing an integrated formal method for verification[END_REF] investigate models written in CSP-OZ-DC, a language that combines Communicating Sequential Processes, Object-Z and Duration Calculus. Each of these approaches caters for the intricacies of the given modelling language. In our approach the characteristics of Behavior Trees define the avenue of how slicing can be defined such that properties are preserved. A major benefit of slicing is that it requires very little computational resources, as the slicing algorithm runs in close to linear time.

We have applied our slicing algorithm to the Behavior Tree model of a Health Information System in order to evaluate its effectiveness. The results are presented in this paper in the following way: Section 2 provides the reader with preliminaries on the Behavior Tree notation and on slicing in general. In Section 3 we define the main ingredients for Behavior Tree slicing. We introduce our case study in Section 4 and present the results of Behavior Tree slicing and the improvements gained when model checking in Section 5. Section 7 summarises and gives an outlook on future work.

Preliminaries

Behavior Trees

The Behavior Tree (BT) notation [START_REF] Dromey | From requirements to design: Formalizing the key steps[END_REF][START_REF] Dromey | Genetic design: Amplifying our ability to deal with requirements complexity[END_REF] is a graphical notation to capture the functional requirements of a system provided in natural language. The strength of the BT notation is two-fold: Firstly, the graphical nature of the notation provides the user with an intuitive understanding of a BT model -an important factor especially for use in industry. Secondly, the process of capturing requirements is performed in a stepwise fashion. That is, single requirements are modelled as single BTs, called individual requirements trees. In a second step these individual requirement trees are composed into one BT, called the integrated requirements tree. Composition of requirements trees is done on the graphical level: an individual requirements tree is merged with a second tree (which can be another individual requirements tree or an already integrated tree) if its root node matches one of the nodes of the second tree. Intuitively, this merging step is based on the matching node providing the point at which the preconditions of the merged requirement trees are satisfied. This structured process provides a successful solution for handling very large requirements specifications [START_REF] Dromey | From requirements to design: Formalizing the key steps[END_REF][START_REF] Wen | From requirements change to design change: A formal path[END_REF].

The syntax of the BT notation comprises nodes and edges. A node can be either a state realisation describing a state change of a component or one of its attributes, or a selection, guard, or event, guarding the control flow within the BT. A node is specialised by its Component name C, Behavior B, Type, and set of Flags.

The Behavior is an identifier (describing a state, an event, or a channel name), or an expression (referring to component attributes). The Type of a BT node can be (c.f., Figure 1 (d-e) an internal event modelling communication and data flow between components within the system, where B specifies an event; the control flow can pass the internal input/output event node when the event occurs (the message is sent), otherwise it is blocked until it occurs; (f-g) an external event modelling communication and data flow between the system and its environment, where B specifies an event; the control flow can pass the external input/output event node when the event occurs (the message is sent), otherwise it is blocked until it occurs.

The control flow of the system is modelled by either a normal or a branching edge. A normal arrowed edge models sequential flow between two steps. If two nodes are connected by a line without an arrow head the two steps occur together atomically. Figure 2 shows the two types of branching edges: concurrent and alternative. Concurrent branching (Figure 2a) models threads running in parallel. As an example the threads in Fig. 2. Branching structures in the BT syntax the figure start with a guard node. The branches, however, can start with any node type. We show only two sub-trees in the branching, although in general there may be more.

In alternative branching (Figure 2b), the control flow follows only one of the branches. Alternative branches can comprise either selections only (for example, as shown in Figure 2b) or only other node types but no selections. Alternative branching over selections operates as a non-deterministic choice over the branches with a satisfied selection condition B i . If none of the selections is satisfied the behaviour terminates. Alternative branching over non-selections behaves like a non-deterministic choice that is unguarded.

Flags in a BT node can specify: (a) a reversion node, marked by ' ˆ', if the node is a leaf node, indicating that the control flow loops back to the closest matching ancestor node (a matching node is a node with the same component name, type and behaviour) and all behaviour started after the matching ancestor node is terminated; (b) a referring node, marked by '=>', indicating that the flow continues from the matching node; (c) a thread kill node, marked by '--', which kills the thread that starts with the matching node, or (d) a synchronisation node, marked by '=', where the control flow waits until all other threads with a matching synchronisation node have reached the synchronisation point.

As described in [START_REF] Zafar | Early validation and verification of a distributed role-based access control model[END_REF], the BT syntax also includes notation for standard set operations, some of which are shown in Figure 3 on page 4 (for a complete description of the syntax see [START_REF] Dromey | Behavior Engineering[END_REF]): Assume C has an attribute S which is a set, then a) models adding element x to S, b) removing element x from S, c) queries the cardinality of S, and d) queries membership of x in S. Union, difference and intersection of two sets S and T can be specified using the following syntax: S := S + T , S := S -T , and S := S >< T .

Fig. 3. Set Operations and Parametrisation of BTs

In addition to standard set operations, the syntax also provides constructs for parameterisation such that a sub-BT is to be performed on all members or one member of a reference set S. Figure 3d) models execution of a sub-tree BT(x) for all members x of set S, and Figure 3e) models execution of BT(x) for some member x of set S (where x is chosen non-deterministically). These constructs are referred to as do-forall and do-forone, respectively. The component name can also be omitted.

Type declarations and other structural information about the system model are captured in a Composition Tree (CT). We do not introduce the notion of CTs here but refer the interested reader to [START_REF] Dromey | Behavior Engineering[END_REF].

The semantics of BTs is formalised in [START_REF] Colvin | A semantics for Behavior Trees[END_REF] using CSP σ [START_REF] Colvin | Csp with hierarchical state[END_REF] which is an extension of CSP with state. An automated translation [START_REF] Grunske | An automated failure mode and effect analysis based on high-level design specification with behavior trees[END_REF][START_REF] Grunske | Defining the abstract syntax of visual languages with advanced graph grammars-a case study based on Behavior Trees[END_REF] provides an interface to the model checker SAL [START_REF] De Moura | SAL 2[END_REF], allowing for fully automated analysis of BT models.

Program Slicing

Program slicing is a technique which removes irrelevant parts of a program based on the dependencies between the program statements. The program is first transformed into a Control Flow Graph (CFG). The nodes in the CFG represent the program statements and the edges correspond to control flow. There is a single entry node and a single exit node for each graph. Branching statements, such as if or while statements, are represented as nodes in the CFG with two successors representing the true and false paths. All other statements are represented as nodes with a single successor. In many approaches to slicing, a structure known as a Program Dependence Graph (PDG) [START_REF] Ottenstein | The program dependence graph in a software development environment[END_REF][START_REF] Ferrante | The program dependence graph and its use in optimization[END_REF] is then created using the CFG. The PDG is a directed graph with vertexes representing program statements and edges representing dependencies, such as control-flow and data dependencies. To determine the set of statements that may directly or indirectly affect a specified criterion, a simple reachability analysis is performed on the graph. The statements that were found to be irrelevant to the criterion can then be removed, producing the slice. The slice will always be a subset of or equal to the original program.

A formal foundation of control dependencies and slicing correctness can be found in the work by Ranganath et al. [START_REF] Ranganath | A new foundation for control dependence and slicing for modern program structures[END_REF].

Slicing of Behavior Trees

Slicing of BTs is performed in a similar manner as program slicing. We utilise this technique to reduce the size of a BT model when applying model checking. Model checking is a fully automated process which, in our case, checks whether a BT model satisfies a given temporal logic property. We assume the property is specified in LT L X [START_REF] Baier | Principles of Model Checking[END_REF], which is linear temporal logic (LTL) [START_REF] Emerson | Temporal and modal logic[END_REF] minus the next step operator X. A slice of a model wrt. a given property is created in such a way that it preserves the property. Assuming this, it suffices to model check the smaller slice instead of the full model.

The first step in the overall slicing process is to create a Behavior Tree Dependence Graph (BTDG) from the given BT. The BTDG indicates all the dependencies that exist between the nodes of the BT. Each BT will have only one general BTDG which is independent of the property to be verified but covers all dependencies between all components and attributes. Therefore this step only needs to be performed once per BT and the resulting BTDG can be used for creating slices for any LT L X property as well as for any other analysis technique that relies on dependency graphs. The set of nodes that are relevant for a specific property are then identified using the BTDG. Finally, these nodes are re-formed into a tree, producing the BT slice for the given property.

Creating the BT Dependence Graph

The BTDG is similar to a Program Dependence Graph [START_REF] Ottenstein | The program dependence graph in a software development environment[END_REF][START_REF] Ferrante | The program dependence graph and its use in optimization[END_REF]. Each node in a BTDG represents a node in the BT and each edge represents a dependency between two nodes. There are several types of dependencies that might be present in a BT, specifically: control, data, interference, synchronisation, message and alternative choice branching dependencies.

A BTDG is created not from the BT directly but from the control flow graph of a BT (CFG-BT). In the context of program slicing, a control flow graph indicates the flow of control between single program statements. A BT is almost a like a control flow graph as it shows the flow of control via sequential and branching edges. However, some parts of the control flow are denoted by boxes rather than edges, e.g. reversion and reference nodes. These have to be replaced by edges linking the predecessor node in the BT with its successor node. Moreover, selection, guard and (internal/external) input event nodes in a BT do not explicitly show the flow of control in the case where this respective condition fails (i.e., the behaviour in the negative case). We add edges to represent these cases: (a) each selection node has an additional outgoing edge to a terminal node representing termination when the selection condition is not satisfied, (b) guard and input event nodes have an additional edge that loops back to itself representing blocking behaviour (i.e., waiting) in the case where the guard or event is not available.

A path in a CFG-BT is a sequence of nodes. Let P ath(p, q) represent the path from node p to node q. If k ∈ P ath(p, q), then k is a node on the path. A path is called maximal if it either terminates (i.e. it has no successors) or contains an infinite loop (this definition was adapted from [START_REF] Ranganath | A new foundation for control dependence and slicing for modern program structures[END_REF]).

We call two nodes p and q matching, denoted as Matching(p, q), if they have the same component name, behavior and type. If Concurrent(p, q) then nodes p and q are in concurrent threads of the CFG-BT. If Alternate(p, q) then nodes p and q are in alternate branches of the same thread of the CFG-BT.

We now define the notion of definition set and reference set for BT nodes which are used to define dependencies between nodes. Intuitively, if a node updates/queries a component or attribute, the component or attribute is a member of the definition/reference set for that node. Assume in the following that C is a component, a and b are attributes of the component, s is a behavior, g is a guard, S and T are sets, x denotes an element of S, and m is a natural number. Based on these preliminary definitions we now define various types of dependencies between BT nodes from which the BTDG is built.

Control dependencies arise if a BT node controls the execution of another node. A node p in a BT is control-dependent on a node q if and only if there are two possible outcomes after executing node p: in one scenario all paths of execution lead to q and in the other scenario, there exists a path on which node q is never executed. This situation occurs when node p is either a guard, a selection or an external input event. For instance, in the case of a selection, if the selection is satisfied then the control flow proceeds to subsequent nodes, but if the selection is not satisfied then the control flow terminates. Thus, the execution of the subsequent nodes are controlled by the selection node. We exclude dependencies between nodes from alternative and concurrent branches as those are handled separately.

Definition 3. (Control Dependency)

For two nodes p and q in a CFG-BT, node q is control-dependent on node p, denoted as p cd -→ q, iff: (i) node p has at least two successors m and n, where NOT(Alternate(m, n)) and NOT(Concurrent(m, n)), (ii) for all maximal paths from node m, node q always occurs and (iii) there exists a maximal path from node n on which node q never occurs.

If a node q in a BT queries the state of a component or attribute, it is data-dependent on any node p that updates the state of that component or attribute. That is, if for a node p a component or attribute c is in REF (p), then p is data-dependent on a node q for which c is a member of DEF (q), assuming c is not re-defined by another node on the path between p and q. This dependency occurs within a single thread as well as between parallel threads. In the latter case it is often also referred to as interference dependence.

These two dependencies are differentiated because interference dependency is intransitive (in contrast to all other dependencies). This results in slices that are not optimal as they contain nodes that are not relevant for the property and could have been sliced away. Krinke in [START_REF] Krinke | Static slicing of threaded programs[END_REF] introduces the notion of threaded witness to determine whether a path in the dependency graph shows a true dependency. In our approach it remains future work to include a strategy for optimising the slicing algorithm that handles this problem.

The following definition combines data and interference dependency as both notions differ only in one condition: N OT (Concurrent(p, q) for data dependency and Concurrent(p, q) for interference dependency.

Definition 4. (Data and Interference Dependency)

For two nodes p and q in a CFG-BT, node q is data-or interference-dependent on node p, denoted as p dd/id ---→ q, iff:

(i) ∃c ∈ DEF (p) such that c ∈ REF (q) and (ii) ∀k ∈ P ath(p, q), c / ∈ DEF (k).
Message dependence is similar to data dependence. All internal input nodes are message-dependent on internal output nodes with the same message name. (Note that for external input/output nodes we do not have a similar dependency as the sender/receiver of the message is outside the scope to the system (i.e., external).) Definition 5. (Message Dependency) For two nodes p and q in a CFG-BT, node q is message-dependent on node p, denoted as p md --→ q, iff:

(i) T ype(p) = InternalOutput and Behavior(p) = m and (ii) T ype(q) = InternalInput and Behavior(q) = m.

All sets of synchronising nodes are dependent on each other, because each node must wait for all the others before proceeding. Definition 6. (Synchronisation Dependency) For two nodes p and q in a CFG-BT, node q is synchronisation-dependent on node p, denoted as p sd -→ q, iff:

(i) F lag(p) = Synchronisation and F lag(q) = Synchronisation and (ii) M atching(p, q).
For BTs an extra dependency type arises that is not normally found in program slicing. A BT can have alternative choice branching points. At each of these points, each branch is dependent on whether or not the other branches have executed. If one branch executes then all others are terminated. Therefore, there is a dependency between the root nodes of all branches in an alternative branching construct.

Definition 7. (Alternative Dependency)

For two nodes p and q in a CFG-BT, node q is alternative-dependent on node p, denoted as p ad -→ q, iff nodes p and q:

(i) have the same parent node and (ii) are connected by an alternative choice branching point.

Note that synchronisation as well as alternative dependency are symmetrical relations between BT nodes.

Creating the Slice

After the BTDG has been created for a given BT, it can be used to create the slice for any given LT L X property. The slicing criterion consists of all state-realisation nodes which update the state of one of the components or attributes mentioned in the temporal logic property. If we lift the notion of reference set to temporal logic formulas such that for any formula p, REF (p) denotes the set of components and component attributes that are mentioned in p, then the set of nodes building the slicing criterion for p is characterised as

SliceCrit(p) = {n : BT N ode | ∃c ∈ REF (p) • c ∈ DEF (n)}.
Starting from each of these nodes in SliceCrit, the BTDG is traversed in reverse, collecting every node that is encountered via dependency edges. During the traversal we check if a node has been visited already in order to avoid an infinite traversal due to symmetric or circular dependencies. The algorithm is in most cases linear and in the worst, but unrealistic, case quadratic in the number of nodes of the BTDG. Any nodes that were not encountered during the traversals can be removed from the BT, because they are irrelevant for the property.

The final set of relevant nodes is often a disjoint set of sub-trees. These must be re-formed into a tree. Every node that is missing its parent node is joined to its closest remaining ancestor, becoming one of its children. However, if the node was originally part of an alternative or concurrent branch and one or more of the other branches are still present in the tree, then the root nodes of each branch are joined to a blanknode. A blanknode is a place-holder for the concurrent or alternative branching construct of the original BT and is used in order to preserve the structure. The blanknode then becomes a child of the closest remaining ancestor of the branching nodes.

The reversion and reference nodes are then added back to the slice. These nodes represent jumps to other locations in the tree. The nodes are placed at the bottom of the same threads that they belonged to in the original BT. However, if an entire sub-tree no longer exists in the slice, then any reversions/reference nodes in that sub-tree are left out.

If the BT contains do-forall and do-forone nodes, then these are added back to the slice, unless these nodes are no longer relevant. The nodes become obsolete if the subtree below no longer mentions the member of the reference set (i.e., the parameter).

The final slice can only be used in place of the original BT for model checking the desired property if our slicing algorithm, which is based on the above definitions, is correct. We have formally proved the correctness of our approach and summarise the proof idea in the following. Similar to [START_REF] Ranganath | A new foundation for control dependence and slicing for modern program structures[END_REF] we base our proof on the notion that nodes in the slicing criterion of a property p, SliceCrit(p), are observable steps whereas nodes not in the slicing criterion are silent or stuttering steps. The idea of our proof is to show that our algorithm produces a slice that is stuttering-equivalent to the original BT. We base our proof on the theorem on stutter equivalence and LT L X equivalence ([6], chapter 7) which states that for any paths σ 1 , σ 2 and any LT L X formula ϕ (over the same set of atomic propositions) σ 1 = σ 2 =⇒ σ 1 |= ϕ iff σ 2 |= ϕ, where = denotes stuttering equivalence between two paths. That is, if two models are stuttering equivalent we can imply that both of them satisfy or dissatisfy the same properties.

Using these results it suffices in our context to show that for any behaviour in the original BT there exists a stuttering equivalent behaviour in the slice that is generated wrt. a formula ϕ. With the definitions as given in Section 3.1 a proof by contradiction provides the desired result. We assume that there exists an execution trace in the original BT for which there does not exist a stuttering-equivalent trace in the slice. Therefore the trace of the original BT must at some point contain an observable node that is not able to execute at the equivalent point in any of the traces of the slice. However, we have shown that such a node cannot exist according to the definitions of slicing and dependencies. We then assume that the converse is true: that there exists an execution trace in the slice that does not have a stuttering-equivalent trace in the original BT. We have also shown this to be impossible. Thus, a generated slice is always stuttering-equivalent to the original BT.

Case Study: the e-Health System

The e-Health system presented here has been adapted from a real case study presented in [START_REF] Evered | A case study in access control requirements for a health information system[END_REF]. It is based on the automation requirements for an aged care facility. The facility provides accommodation and care for elderly residents. The facility is administered by a manager. The residents are visited by doctors regularly. Managers, residents and doctors can view and edit relevant electronic records. The resident's data is made up of the following elements. (1) At the time of admission the personal details of the residents are entered. These details include basic personal data (name, sex, etc.), medical details (blood group, allergies, etc.) and details of any nominated responsible person.

(2) Before admission a legal agreement must also be signed electronically. (3) A care plan is initiated after he/she has been admitted to the facility. (4) Past medical records are entered by the manager of the facility. After each examination the doctor adds an entry to the medical records of the residents. The doctor can also add private notes to the medical records.

We have created a BT model of the e-Health system. Fig 4 shows an overview of the model, which is too large to be shown in further detail here. The BT describes the behaviour of the nominated responsible people, the managers, the doctors and the residents, each in a separate thread. A responsible person can give consent to add a doctor or sign an agreement on behalf of the patient. A manager can perform various tasks, including adding or viewing a patient's personal details, managing care plans, adding medical records and deleting data. A doctor can view or add medical records if he/she has permission to do so. Doctors, residents and temporary doctors can be added to the various access control lists, thereby granting them access to a patient's files.

In order to provide the reader with an idea of the structure of the tree, a section of the manager thread is shown in greater detail in Figure 5. The manager thread begins with "for all managers", "choose a resident", followed by "choose a data set". At this point there is an alternative choice between each of the possible actions that a manager Fig. 4. Overview of the e-Health System BT can perform. We show only the action of the manager viewing personal details. If the current data belongs to the current resident, then the manager can view the data. The behaviour then reverts to a higher node, to allow managers to perform other actions. A number of access control requirements have been defined for the security of electronic records and to ensure the privacy of the residents. We have formulated these requirements as LTL theorems, shown below. To comply with different regulations, the resident records must be kept for a period of nine years. After the completion of the nine year period the record can be deleted. This requirement is formalised as theorem 1. The LTL operator, G(p), is used to state that p is always true. The second requirement concerns the ability of managers to add medical records. To protect the privacy of the residents, the access to medical records is limited only to the residents themselves or to the nominated doctors. However, the manager is allowed to enter past medical records at the time of admission to the facility. After the admission, the manager is not allowed to add or view the records. The formula states that medical records can only be added by a manager if the patient associated with the data has not yet been admitted. The last property states that a resident can view his/her private notes only if he/she has been assigned to the record's access control list (ViewNotesACL). 5 Slicing the model of the e-Health system

In this section we compare the execution times for model checking the e-Health system BT with the slices for each property listed in Section 4. First, the BTDG for the e-Health system is created, according to the procedure outlined in Section 3. This BTDG is then used for creating each of the slices. The slicing criterion for each case is derived from the variables mentioned in the property. For example, the slicing criterion for theorem 1 is the set {d.deleted, m.state, d.leaveDate | d ∈ data ∧ m ∈ manager}. Starting from each of the state-realisation nodes that involve these components/attributes, the BTDG is traversed in reverse, collecting all relevant nodes. The size of the resulting slices varies depending on the property. The only relevant part for theorem 1 is the manager's behaviour, so a significant proportion of the BT can be sliced away. The other two properties involve several parts of the BT, so the corresponding slices are larger than for theorem 1. For example, theorem 3 involves the set ViewNotesACL. This set is referred to in several places in the resident behaviour thread. However, the set is updated in the doctor behaviour thread, so the validity of the property is dependent on both parts of the BT. Table 1 The e-Health system BT utilises set constructs, so the BT is expanded before model checking. Whenever a do-forall or do-forone node is encountered, its sub-tree is replicated for each element in the set. We have compared the execution times for model checking the original BT vs. the slices, for increasing cardinality of the sets. The results are presented in Table 2. The system maintains sets of doctors, residents, responsible persons, managers, data and logs.

The checks were run on a 1.2GHz UltraSPARC processor with 24GB of RAM, running Solaris 10. The original model could not be verified. Even with only a single user in each set, i.e. the smallest possible model, the model checker ran out of memory before providing a result. However, using the slices, verification was possible. For all three theorems, the model checker provided a result in only seconds when the sets as an initial step prior to applying other reduction techniques. The extent to which slicing can reduce the verification time depends on both the model and the property. The more dependencies that exist between the components in the formula, the larger the slice. Despite this, in many cases slicing can improve the verification time. In particular, in concurrent models it is often the case that each thread represents a separate component that operates independently. In such cases, slicing is very effective as it reduces the parallelism in the model, which is one of the most computationally expensive aspects in model checking. Due to the low cost for applying slicing, it is worthwhile to try it, especially if the model is infeasible for a model checker.

Conclusion

We have developed a method for automatically reducing Behavior Tree models using the slicing. Slices of a BT model can be used for aiding in understanding and also for reducing models prior to verification. The case study we have presented in this paper demonstrates the benefits of slicing a model before model checking. The results show the improvements in execution time and memory usage. This enables the verification of models for which model checking was previously infeasible. Although the shape and size of a slice depend on the property to be checked, the low computational resources needed to compute a slice makes it ideal for aiding in model checking.

For future work, we plan to extend the slicing procedure to enable slicing wrt. full LTL (including X operator) and to explore further optimisations which could produce greater reductions in the model size.

Fig. 1 .

 1 Fig. 1. Different node types of the BT syntax

Definition 1 .

 1 (Definition Set) DEF (n) represents the set of components and attributes defined at node n. Specifically, if n is of the form (a) (state-realisation) C[s] then C ∈ DEF (n), (b) (state-realisation of attributes) C[a := s] then a ∈ DEF (n), (c) (adding/removing an element from a set) C[S := S + x] or C[S := S -x] then S ∈ DEF (n), (d) (union, subtraction, intersection of sets) C[S := S + T] or C[S := S -T] or C[S := S >< T] then S ∈ DEF (n). Definition 2. (Reference Set) Let REF (n) represent the set of components and attributes referenced at node n. Specifically, if n is of the form (a) (selection/guard) C?g? or C???g??? then C ∈ REF (n), (b) (selection/guard over attributes) C?a = exp? or C???a = exp??? where exp is an expression or a behavior, then a ∈ REF (n), (c) (state-realisation of attribute) C[a := f(b)], where f (b) is an expression over b, then b ∈ REF (n), (d) (selection over set predicates) C?x : S? or C?S = {}? or C?|S| ⊲⊳ m? where ⊲⊳ ∈ {=, <, >, <=, >=}, then S ∈ REF (n).

Fig. 5 :

 5 Fig. 5: Manager thread

c) a guard; the control flow can pass the guard when C is in state B if B is a state name, or when the expression B over one of C's attributes is satisfied if B is an ex- pression over the attribute; otherwise it is blocked until the state realisation occurs;

  ) (a) a state realisation, modelling C being in a state if B is a state name, or updating C's attribute if B is an update expression over the attribute; (b) a selection (or condition) on C's state if B is a state name, or a selection on the state of one of C's attributes if B is an expression over the attribute; in both cases, the control flow terminates if the condition is not satisfied; (

  2. Medical records can only be added by the manager if the patient associated with the data has not yet been admitted. ∀d : data, ∀m : managers, G ((d.medicalRecords = added ∧ m.state = addingM edicalRecords) =⇒ d.admitted = f alse) 3. A resident can only view his/her private notes if he/she is in the set ViewNotesACL. ∀d : data, ∀r : residents, G ((d.privateN otes = viewed ∧ r.state = viewingP rivateN otes) =⇒ (r : d.V iewN otesACL)

Table 1 .

 1 lists the number of nodes in each of the slices compared to the original BT. Number of nodes in the original BT and each slice

		Original BT	Slice Th1	Slice Th2	Slice Th3
	No. of nodes	125	36	116	73

contained one element each. As the number of elements were increased, the execution times increased, but a result could still be obtained for most combinations in which there were two elements in one or more of the sets.

The slice for theorem 1 did not contain any nodes involving doctors or responsible persons, so increasing these sets did not affect the execution time. When the number of managers and residents were increased, the execution time increased, reaching 11 seconds with 2 managers and 1-2 minutes with 2 managers and 2 residents. Even with 3 elements in each of the sets a result was obtained in 2 hours.

The size of the slice for theorem 2 is almost the same as the original BT. However, there was still significant improvement in model checking. It was possible to obtain a result with one element in each set in only 71 seconds. With two elements in a set, the execution times varied between 17 minutes for 2 responsible persons and 10.6 hours for 2 doctors. If two sets contained two elements, such as 2 doctors and 2 residents, the model checker ran out of memory.

Model checking the slice for theorem 3 took only 11 seconds for one element in each set and less than 10 minutes for two elements in a set. With 2 elements in each of the user sets, the model was still able to be verified although the execution time reached 18.6 hours.

Discussion

Slicing can be considered to be complementary to other state-space reduction techniques. The low computational cost needed for slicing makes it ideal to be performed