Jean-Daniel Boissonnat

Arijit Kunal Dutta

Arijit Ghosh

Sudeshna Kolay

Kernelization of the Subset General Position problem in Geometry

Keywords: 1998 ACM Subject Classification F.2.2 Nonnumerical Algorithms and Problems Incidence Geometry, Kernel Lower bounds, Hyperplanes, Bounded degree polynomials Digital Object Identifier 10 .MFCS.2017.25

In this paper, we consider variants of the Geometric Subset General Position problem. In defining this problem, a geometric subsystem is specified, like a subsystem of lines, hyperplanes or spheres. The input of the problem is a set of n points in R d and a positive integer k. The objective is to find a subset of at least k input points such that this subset is in general position with respect to the specified subsystem. For example, a set of points is in general position with respect to a subsystem of hyperplanes in R d if no d + 1 points lie on the same hyperplane. In this paper, we study the Hyperplane Subset General Position problem under two parameterizations. When parameterized by k then we exhibit a polynomial kernelization for the problem. When parameterized by h = n -k, or the dual parameter, then we exhibit polynomial kernels which are also tight, under standard complexity theoretic assumptions. We can also exhibit similar kernelization results for d-Polynomial Subset General Position, where a vector space of polynomials of degree at most d are specified as the underlying subsystem such that the size of the basis for this vector space is b. The objective is to find a set of at least k input points, or in the dual delete at most h = n -k points, such that no b + 1 points lie on the same polynomial. Notice that this is a generalization of many well-studied geometric variants of the Set Cover problem, such as Circle Subset General Position. We also study general projective variants of these problems. These problems are also related to other geometric problems like Subset Delaunay Triangulation problem.

Introduction

In the geometric subset general position problem, the input is a family of algebraic objects, e.g. lines, circles, hyperplanes, zero set of quadratic functions, and a point set P in R d . The objective is to extract a large subset S of P such that the subset S is in general position with respect to the geometric objects. The definition of general position is different for different families of geometric objects. For the case of hyperplanes in R d , a set S, assume |S| > d, will be in general position with respect to the family of hyperplanes in R d if no more than d points of S lie on a hyperplane. For the case of spheres in R d , a set S with |S| > d + 1, will be in general position with respect to the family of spheres in R d if no more than d + 1 points of S lie on a sphere. In this paper, we will assume that d is a constant. In computational geometry it is generally assumed that the point set is in general position, such as no more than d points lie on a hyperplane in the case of convex hull computation or no more than d + 1 points lie on a sphere for Delaunay triangulation computation (see [START_REF] Berg | Computational geometry[END_REF]). Also, algebraic techniques like simulation of simplicity have been introduced to handle degenerate cases in practice [START_REF] Edelsbrunner | Simulation of Simplicity: A Technique to Cope with Degenerate Cases in Geometric Algorithms[END_REF].

The problem of determining whether a given point set in R d is in general position with respect to family of spheres and family of hyperplanes has been extensively studied in computational geometry. Edelsbrunner, O'Rourke and Seidel [START_REF] Edelsbrunner | Constructing Arrangements of Lines and Hyperplanes with Applications[END_REF] gave an O(n d ) (and O(n d+1 )) space and time complexity algorithm to determine if a point set is in general position with respect to hyperplanes (resp. spheres) in R d . Edelsbrunner and Guibas [START_REF] Edelsbrunner | Topologically Sweeping an Arrangement[END_REF][START_REF] Edelsbrunner | Corrigendum: Topologically Sweeping an Arrangement[END_REF] later improved the space bound to O(n). Erickson and Seidel [START_REF] Erickson | Better Lower Bounds on Detecting Affine and Spherical Degeneracies[END_REF][START_REF] Erickson | Erratum to Better Lower Bounds on Detecting Affine and Spherical Degeneracies[END_REF] showed in the worst case Ω(n d ) (and Ω(n d+1 )) sided queries are required to determine whether a set of n points in R d is in general position with respect to hyperplanes (resp. spheres). We have mentioned a small sample of the papers on this topic and for a more complete picture of this area and the more general problem of arrangement of hyperplanes please refer to the survey by Agarwal and Sharir [START_REF] Agarwal | Arrangements and their applications[END_REF].

More recently, the problem of finding a maximum-cardinality subset of points in general position has been studied in parameterized complexity, approximation algorithm, and combinatorial geometry [START_REF] Froese | Finding Points in General Position[END_REF][START_REF] Payne | On the general position subset selection problem[END_REF][START_REF] Cardinal | General position subsets and independent hyperplanes in d-space[END_REF]. Payne et al. [START_REF] Payne | On the general position subset selection problem[END_REF] and Cardinal [START_REF] Cardinal | General position subsets and independent hyperplanes in d-space[END_REF] gave a non-trivial lower bound on the size of a largest size subset in general position from a point set with bounded coplanarity in R 2 and R d . A point set in R 2 (and R d ) has bounded coplanarity if the number of points from the set that lie on a given plane (or hyperplane) is bounded. Cao [START_REF] Cao | Study on Two Optimization Problems: Line Cover and Maximum Genus Embedding[END_REF] and Froese et al. [START_REF] Froese | Finding Points in General Position[END_REF] studied the geometric subset general position problem in R 2 with respect to lines in R 2 through the lens of parameterized complexity. Cao [START_REF] Cao | Study on Two Optimization Problems: Line Cover and Maximum Genus Embedding[END_REF] also gave an O( √ opt)-factor approximation algorithm for the general position subset selection problem with respect to lines in R 2 .

In this paper we generalize the results of [START_REF] Froese | Finding Points in General Position[END_REF] by studying the kernelization aspect of the following primal problem:

Hyperplane Subset General Position

Parameter: k

Input: An n point set P in R d , for a fixed constant d, and a positive integer k Question: Is there a subset S ⊆ P of size at least k such that S is in general position with respect to hyperplanes in R d ?

We will also study a more general version of the above problem for bounded degree polynomial families (see Section 2 and 3): Therefore, the general position subset selection problems with respect to natural set families like the vector space of spheres, ellipses, etc. are special cases of the d-Polynomial Subset General Position problem. We also study the problems with respect to the dual parameter h = n -k. That is, the problem of Hyperplane Subset General Position or d-Polynomial Subset General Position still have the same input and aim for the same decision problem. However, the parameter for the problem becomes h.

Note that both these problems are NP-hard following from the results of [START_REF] Froese | Finding Points in General Position[END_REF] on Subset General Position in R 2 .

J.-D. Boissonnat, K. Dutta, A. Ghosh and S. Kolay 25:3

Our contribution

In this paper, we exhibit polynomial kernels for Hyperplane Subset General Position in R d . This is a generalization to higher dimensions of the results on kernelization obtained in [START_REF] Froese | Finding Points in General Position[END_REF], with more carefully designed reduction rules to take care of the higher dimension. We further generalize the result with the help of a variant of the Veronese mapping, to obtain polynomial kernels for d-Polynomial Subset General Position in R t , where the bounded degree polynomial family is a vector space of d-degree polynomials. Special cases of the d-Polynomial Subset General Position problem include variants where the polynomial family is that of spheres or quadratic surfaces. Also, Delaunay Subset Selection is a special case of this problem. We further study the general projective variants of these problems. These results are described in Section 3

We also give tight polynomial kernels for Hyperplane Subset General Position in R d parameterized by h, the dual parameter, as described in Section 4. In Section 4, we obtain tight results for the number of elements in a polynomial kernel for Hyperplane Subset General Position in R d . These results are similar to those obtained in [START_REF] Kratsch | Point Line Cover: The Easy Kernel is Essentially Tight[END_REF]. Finally, in Section 5, we are able to generalize this result for certain variants of d-Polynomial Subset General Position.

Preliminaries

Hypergraphs

A set of consecutive integers {1, 2, . . . n} will be written as [n] in short. A hypergraph G is a set system where V (G) denotes the universe and E(G) denotes the family of sets. We refer to the objects in the universe V (G) by either vertices or elements, and each subset of E(G) as a hyperedge. For a hyperedge e ∈ E(G) the set of vertices belonging to e is denoted as

V e . A

General position in Geometry

An i-flat in R d is the affine hull of i + 1 affinely independent points. The dimension of a (possibly infinite) set of points P , denoted as dim(P ), is the minimum i such that the entire set P is contained in an i-flat of R d [START_REF] Langerman | Covering things with things[END_REF]. We use the term hyperplanes interchangeably for (d -1)-flats. A set P of points in R d is said to be in general position with respect to hyperplanes, if for each i-flat, i ≤ d -1, in R d there are at most i + 1 points from P lying on the i-flat.

As described earlier, the Geometric Subset General Position problem, defined on a subsystem of geometric objects, takes as input a set of points P and a positive integer k and determines whether there is a subset of at least k points that are in general position with respect to the specified subsystem of geometric objects. For example, Hyperplane Subset General Position in R d takes in a set of points in R d and a positive integer k and determines whether there is a subset of at least k points that are in general position with respect to hyperplanes in R d .

Similarly, we can define the notion of general position with respect to multivariate polynomials. Given a set {X 1 , X 2 , . . . , X t } of variables, a real multivariate polynomial on these variables is of the form P (X 1 , . . . , X t ) = i1,i2,...,it a i1i2...it j∈[t] X ij j where [t] = {1, . . . , t} and a i1i2...it ∈ R. The set of all real multivariate polynomials in the variables {X 1 , . . . , X t } will be denoted by R[X 1 , X 2 , . . . , X t ]. The degree of such a polynomial P (X 1 , . . . , X t ) is defined as deg(P ) := max{i 1 + i 2 + . . . + i t | a i1i2...it = 0}. A polynomial is said to be a degree d polynomial is its degree is d.

In this paper, we are interested in the set/subsets of polynomials whose degree is bounded by d, for some d ∈ N. In this context we define Poly

d [X 1 , . . . , X t ] := {f (X 1 , . . . , X t ) ∈ R[X 1 , X 2 , . . . , X t ] | deg(f ) ≤ d}. Observe that Poly d [X 1 , . . . , X t ] is a vector space over R with the monomials X i1 1 . . . X it t | 0 ≤ t j=1 i j ≤ d as the basis. Notice that X i1 1 . . . X it t | 0 ≤ t j=1 i j ≤ d = d+t d . In d-Polynomial Subset General Position in R t , a subspace F of Poly d [X 1 , . . . , X t ]
is given with a basis {f 1 (X), f 2 (X), . . . , f b (X), 1}, where X = (X 1 , . . . , X t ) and f i (X) ∈ Poly d [X 1 , . . . , X t ], and a set of n points from R t . The objective is to find a subset of points in general position with respect to the vector space of polynomials, i.e., no more than b points from the subset satisfy any equation of the form f (X) := b i=1 λ i f i (X) + λ b+1 = 0, where for each j ∈ {1, . . . , b}, λ j ∈ R and not all the λ j 's can be zero simultaneously.

Veronese mapping

In this paper, one of our strategies for generalizing our results is to convert d-Polynomial Subset General Position in R t to Hyperplane Subset General Position in R b by using a variant of Veronese mapping [START_REF] Matoušek | Lectures on Discrete Geometry[END_REF] from R t → R b . The Veronese mapping of a vector space F of d-degree polynomials will be as the following: Φ F : R t → R b , where for a vector

X = (X 1 , . . . , X t ), Φ F (X) = (f 1 (X), . . . , f b (X)). Observe that if p = (p 1 , . . . , p t ) satisfies the equation f (X) := b i=1 λ i f i (X) + λ b+1 = 0 then, for a vector of variables Z = (Z 1 , . . . , Z b ), Φ F (p) will also satisfy the linear equation b j=1 λ j Z j + λ b+1 = 0.
In other words, for any set of points P in R t and the vector space F, the incidences between P and F and incidences between Φ F (P ) and Poly 1 [Z 1 , . . . , Z b ] (these are hyperplanes in R b ) are preserved under the mapping Φ F . Also, observe that there is a bijection between polynomials in F and hyperplanes in R b .

Parameterized Complexity

The instance of a parameterized problem/language is a pair containing the actual problem instance of size n and a positive integer called a parameter, usually represented as k. The problem is said to be in FPT if there exists an algorithm that solves the problem in f (k)n O (1) time, where f is a computable function. The problem is said to admit a g(k)-sized kernel, if there exists an polynomial time algorithm that converts the actual instance to a reduced instance of size g(k), while preserving the answer. When g is a polynomial function, then the problem is said to admit a polynomial kernel. A reduction rule is a polynomial time procedure that changes a given instance I 1 of a problem Π to another instance I 2 of the same problem Π. We say that the reduction rule is safe when I 1 is a Yes instance of Π if and only if I 2 is a Yes instance. Readers are requested to refer [START_REF] Cygan | Parameterized Algorithms[END_REF] for more details on Parameterized Complexity.

Lower bounds in Parameterized Algorithms

There are several methods of showing lower bounds in parameterized complexity under standard assumptions in complexity theory. One such technique is polynomial parameter transformation. For two parameterized problems Π, Π , a polynomial time algorithm A is called a polynomial parameter transformation (or ppt) from Π to Π if, given an instance 1) . By a result of [START_REF] Bodlaender | Kernel bounds for disjoint cycles and disjoint paths[END_REF], if Π, Π are two parameterized problems such that Π is NP-hard, Π ∈ NP and there exists a polynomial parameter transformation from Π to Π , then, if Π does not admit a polynomial kernel neither does Π .

(x, k) of Π, A outputs in polynomial time an instance (x , k ) of Π such that (x, k) ∈ Π if and only if (x , k ) ∈ Π and k ≤ k O(
We also require a lower bound technique given in [START_REF] Dell | Satisfiability allows no nontrivial sparsification unless the polynomial-time hierarchy collapses[END_REF]. This technique links kernelization to oracle protocols. Definition 2. [START_REF] Dell | Satisfiability allows no nontrivial sparsification unless the polynomial-time hierarchy collapses[END_REF] Given a language L, an oracle communication protocol for L is a two-player communication protocol. The first player gets an input x and can only execute computations taking time polynomial in |x|. The second player is computationally unbounded, but does not know x. At the end of the protocol, the first player has to decide correctly whether x ∈ L. The cost of the protocol is the number of bits of communication from the first player to the second player. Proposition 2.1. [START_REF] Dell | Satisfiability allows no nontrivial sparsification unless the polynomial-time hierarchy collapses[END_REF] Let d ≥ 2 be an integer, and be a positive real number. If co-NP NP/poly, then there is no protocol of cost O(n d-) to decide whether a d-uniform hypergraph on n vertices has a d-hitting set of at most k vertices, even when the first player is co-nondeterministic.

As noted in [START_REF] Dell | Satisfiability allows no nontrivial sparsification unless the polynomial-time hierarchy collapses[END_REF], this implies that for any d ≥ 2 and any positive real number , if co-NP NP/poly, then there is no kernel of size k d-for d-Hitting Set. In general, a lower bound for oracle communication protocols for a parameterized language L gives a lower bound for kernelization for L.

Kernels: size vs number of elements.

In literature, a lower bound on the kernel means the lower bound on the size of the kernel, but not necessarily on the number of input elements in the kernel. Kratsch et. al [START_REF] Kratsch | Point Line Cover: The Easy Kernel is Essentially Tight[END_REF] were one of the first to study lower bounds in terms of the number of input elements in the kernel. They used the results of Dell and Melkebeek [START_REF] Dell | Satisfiability allows no nontrivial sparsification unless the polynomial-time hierarchy collapses[END_REF] along with results in two dimensional geometry to build a new technique to show lower bounds for the number of input elements in a kernel for a problem. In this paper, we have adhered to the general convention by saying that a kernel has a lower bound on its size if it has a lower bound on its representation in bits, while explicitly mentioning the cases where the kernel has a lower bound on the number of input elements.

Kernel Upper Bounds for primal parameter

In this section, we consider the Hyperplane Subset General Position problem in R d parameterized by the primal parameter k. We describe a polynomial kernelization for this problem. This method is similar to that described in [START_REF] Froese | Finding Points in General Position[END_REF]. However, there is an error in the analysis of kernel size in [START_REF] Froese | Finding Points in General Position[END_REF]. Our proof, when restricted to the case of Line Subset General Position problem gives the correct bound on the kernel. We will point out the place where there is an error in [START_REF] Froese | Finding Points in General Position[END_REF], while describing our proof. Moreover, using the well-known Veronese mapping, we can generalize this result to give polynomial kernels for d-Polynomial Subset General Position in R d parameterized by k.

Hyperplane case

First, we consider an easy variant of the Hyperplane Subset General Position problem in R d , where the input point set P is such that for every subset S of P of size less than d, dim(S) = |S| -1. In this case, the i-flats are said to be non-degenerate. In this case, parameterization by k gives us a polynomial kernel by a generalization of the results obtained in [START_REF] Froese | Finding Points in General Position[END_REF]. For the sake of completeness, we describe the kernelization. We apply a reduction rule that bounds the coplanarity of hyperplanes in R d . Proof. We know from Theorem 4 that for a point set of size n and cohyperplanarity , i.e., at most points from the point set can lie on a given hyperplane, such that ≤ √ n, there is a point set in general position of size at least

Reduction

C( n log ) 1/d where C = C(d) is a constant. Thus, when ≤ √ n, if C( n log ) 1/d > k,
we correctly say Yes. Substituting by its upper bound of O(k d ), this equation is true when n ≥ Ω(k d+1 ). When n = O(k d+1 ), then anyway we obtain a kernel of size O(k d+1 ). The remaining case is when > √ n. Then, substituting by its upper bound of O(k d ), we know that n = O(k 2d ). Thus, we obtain the required polynomial kernel. Now we consider the general problem. To design a kernel for the general problem, point subsets lying in lower dimensional flats also have to be kept in mind. The approach is to first reduce the number of points that can lie in a lower dimensional flat before we can employ a strategy similar to the kernelization of Theorem 5. First, we describe a reduction rule such that in the reduced instance, the coplanarity of each i-flat with i ≤ d is bounded by a function of k. This reduction rule is similar to Reduction Rule 1, except that it has to take care of point subsets lying in lower dimensional flats before it considers point subsets lying in hyperplanes of R d .

Reduction Rule 2. Let (P, k) be an instance of Hyperplane Subset General Position parameterized by k. Let i be the smallest integer between 2 and d, auch that there is an (i -1)-flat that contains at least c(d) • k id + 1 points. Then we delete all but c(d)k id points. Here c(d) = 15(d -1) is a constant. Lemma 6. Reduction Rule 2 is safe.

Proof sketch. We prove the correctness of the reduction rule by induction on i. In the base case, suppose i = 2. Suppose there is a line L containing at least c(d)k 4 + 1. Then by the reduction rule, we construct an instance (P , k) such that P is modified to P by deleting all but c(d)k 4 points. We show that P has a k-sized set in general position if and only if P has a k-sized set in general position. Since, P ⊂ P , if P has a k-sized set in general position, so does P .

In the forward direction, suppose P has a k-sized set S in general position. Let P L be the set of points in L ∩ P and P L be the set of points in L ∩ P . By definition of general position, there are Σ j≤d k j flats of dimension at most d that can be formed by the points in S. Consider the intersection of these flats with the line L. Each intersection is of dimension at most 1. That is, if the intersection is not the line L itself, then it is a point in L. Thus there are at most Σ j≤d k j points of intersection. Since, the set S is in general position, at most two points from S lie on L. If there are no points or if all the points in S ∩ L belong to P then S is also a k-sized set in general position for the instance (P , k). Otherwise, suppose there are at most t ≤ 2 points from P L \ P L . The number of intersection points is at most Σ j≤d k j < c(d)k 2d . Thus there is a set Ŝ = {p t |t ≤ 2} on L that are not intersection points. Let S = S \ (P ∩ L) ∪ Ŝ. We show that S is also a set in general position. Consider a flat defined by points from S . If they do not contain points from Ŝ, then they remain non-degenerate flats. Suppose a flat contains points from Ŝ. Also, for the sake of contradiction, suppose the flat is degenerate. If the flat contains all the points in Ŝ then it contains the line L and therefore the points from L ∩ P . Thus, in P the set S was not in general position, which is a contradiction. Now, suppose the flat F contains a single point, say p 1 , from Ŝ. Then the points from F ∩ S were in general position and therefore the flat was either the line L or L ∩ F was an intersection point. This contradicts the fact that p 1 belongs to F , as p 1 is chosen to be a point that is not an intersection point. Thus, S ⊆ P is in general position and of size k. Note that this means that after exhaustive application of this rule all lines contain at most λ 2 = c(d)k 2d points.

The arguments of the other values of i are similar but with more case analysis. The full proof can be found in the full version of this paper. This Reduction Rule is exhaustively applied and in the end the reduced instance is such that for any hyperplane in R d , the coplanarity is O(k d 2 ). Now, we can exhibit a polynomial kernel for Hyperplane Subset General Position in R d parameterized by k. The proof is same as that of Theorem 5, while taking into account that the collinearity bound in this case is O(k d 2 ). Notice that this problem in R 2 is polynomial time solvable, as the problem is equivalent to asking whether the projection of the points on a unit sphere, centered at the origin, equals to at least k points where no two lie on the same line through the origin.

We will apply the following reduction rule to reduce the coplanarity of the hyperplanes passing through the origin.

Reduction Rule 3. Let (P, k) be an instance of Projective Hyperplane Subset General Position parameterized by k. Let i be the smallest integer between 2 and d -1, such that there is an (i -1)-flat passing through the origin that contains at least c (d) • k id + 1 points. Then we delete all but c (d)k i(d-1) points. Here, as in the case with Reduction Rule 2, c (d) is a large constant depending linearly on d.

The correctness of this Reduction Rule is same as the inductive proof of Reduction Rule 2. Applying the above reduction rule exhaustively, as was the case with Hyperplane Subset General Position problem, we will get that any hyperplane passing through the origin has O(k (d-1) 2 ) input points on them. To get a polynomial kernel for the Projective Hyperplane Subset General Position problem we will need the following analogue to Theorem 4 with bounded coplanarity. Then P contains a subset of size Ω

n 2/3 log 1/(d-1)
of points in projective general position.

Proof. The proof of this lemma will use Theorem 4. Without loss of generality we will assume that the hyperplane X 1 = 1, intersects all the lines passing through the origin and one point of P . Let L denotes the set of lines passing through the origin and one point of P . Observe that since for any hyperplane H passing through the origin, |H ∩ P | ≤ , therefore |L| ≥ n . Let P be the set points we get by intersecting lines in L with the hyperplane X 1 = 1. Again observe that |P | ≥ n , and for any (d -2)-hyperplane H contained in the hyperplane X 1 = 1, we have |H ∩ P | ≤ , otherwise we can get a hyperplane passing through origin containing more than points from P . Using the fact that = O n/

and Theorem 4, we get that P contains a subset P 1 of size Ω

n 2/3 log 1/(d-1)
with no more than points from P 1 lying on any (d -2)-dimensional subflat of the hyperplane X 1 = 1. For each point p ∈ P 1 , include in the set P 1 a point p from the set P such that p and p are on the same line passing through the origin. By construction the set P 1 is in projective general position and

|P 1 | = Ω n 2/3 log 1/(d-1)
. Now, using the fact that any hyperplane passing through the origin has O(k (d-1) 2 ) input points on them after application of Reduction Rule 3 and Lemma 8, we can prove the following result in the same way we proved Theorem 7.

Theorem 9. Projective Hyperplane Subset General Position in R d parameterized by k has a kernel of size O(k 3(d-1) 2 ).

Bounded degree polynomials

The following lemma will show the direct connection between the d-Polynomial Subset General Position problem and Hyperplane Subset General Position problem: Lemma 10. Let P be a set of points in R t , and F be a subspace of Poly d [X 1 , . . . , X t ] with a basis {f 1 (X), . . . , f b (X), 1}, where X = (X 1 , . . . , X t ). 1. If P is a set of points in general position with respect to the polynomial family F (defined earlier in the section) then Φ F (P ) (Φ F is defined earlier in Section 2) is a set of points in general position with respect to hyperplanes in R b . 2. Let S = {q 1 , . . . , q } ⊆ Φ F (P ) be a set of points in general position with respect to hyperplanes in R b . Then the set S = {p 1 , . . . , p }, where p i ∈ Φ -1 F (q i ) ∩ P , will be a set of points in general position with respect to F.

Proof. 1. First, observe that it is enough to show that the map Φ F is injective P . In general, the map Φ F need not be an injective mapping on an arbitrary set of n points in R t . However, we show that Φ is injective when restricted to P if P is in general position with respect to F. To reach a contradiction, let Φ F (p 1 ) = Φ F (p 2 ) where p 1 , p 2 ( = p 1 ) ∈ P . Let S ⊆ P be of size b + 1 and p 1 , p 2 ∈ S. Observe that the set Φ F (S) will have less than b + 1 points and this will imply that there exists a hyperplane b i=1 λ i Z i + λ b+1 = 0 on which the set Φ F (S) will lie. But this implies that the polynomial b i=1 λ i f i (X) + λ b+1 = 0 will be satisfied by all the points in S. This is a contradiction to the fact that the point set P is in general position. 2. This result follows directly from the construction of the mapping Φ F .

With the above result and Theorem 7 we get the following theorem. As in the case with Theorem 7 we can also get a projective version of Theorem 11. Let F be a subspace of Poly d [X 1 , . . . , X t ] with basis {f 1 (X), . . . , f b (X)} where X = (X 1 , . . . , X t ) and none of the polynomial functions f i (X) are constants. Then we can define projective analog of the general position problem for polynomial families like F. For a given point set P in R t , a subset S of P will be in general position with respect to F if no more than b -1 points from S lie on any f (X) ∈ F.

Using the same techniques as in the proof of Theorem 7 we will get the following result:

Corollary 12. Projective Polynomial Subset General Position in R t parameterized by k has a kernel of size O(k 3(b-1) 2 ).

Upper bounds for non-vector space families

Observe that we may be interested in getting general position point set with respect to families of polynomials that are not vector spaces of Poly d [X 1 , . . . , X t ]. For example, consider the case of hyperplanes in R t of the following type H := t-1 i=1 λ i X i + X t + β, where λ i 's and β are in R + . One might be interested in getting a general position set in R t with respect to these hyperplanes.

Note that our upper bound on the kernel size in the primal parameter extends to these families as well.

Corollary 13. Let F be a subfamily of Poly

d [X 1 , . . . , X t ] such that there exists polyno- mial functions f 1 (X), . . . , f b (X) in Poly d [X 1 , . . . , X t ] and for any f (X) ∈ F, f (X) = b i=1 λ i f i (X)
where the λ i 's are in R. Subset general position problem with respect to F parameterized by primal parameter k has a kernel of size O(k 3(b-1) 2 ).

4

Tight kernels for hyperplanes in dual parameter Proof Idea. The main idea behind the proof is that the sets P and B satisfying the conditions of Lemma 14 can be generated in a greedy manner from considering large grids. We will first construct the point set P of n points in a greedy manner such that P comes from a large grid and is in general position. After P is constructed, the set B is again greedily constructed, this time using a lower dimensional grid lying in a particular hyperplane.

This transformation from a graph to a point set leads to the following observation. Proof. We state the folklore reduction from Hyperplane Subset General Position in R d to (d + 1)-Hitting Set. Given an instance (P, h) of Hyperplane Subset General Position in R d , we construct the following instance (G, h) of (d + 1)-Hitting Set. Corresponding to each point in P we create a vertex in V (G). For any d + 1 point in P that are coplanar in R d , we create a hyperedge with the corresponding vertices. Consider the vertices in a hyperedge of G. At least one of the corresponding points has to be deleted in order to construct a subset of P that is in general position with respect to hyperplanes in R d . Thus, the set of points deleted correspond to a hitting set of G. Therefore, the reduction is correct.

(d + 1)-Hitting Set has a kernel where the universe size if O(h d ) [START_REF] Van Bevern | Towards optimal and expressive kernelization for d-hitting set[END_REF]. This gives us an O(h d ) kernel for Hyperplane Subset General Position in R d parameterized by the dual parameter.

Lower bounds on elements in a kernel for hyperplanes in dual parameter

In this section, we show that by the method suggested by Dell and Melkebeek [START_REF] Dell | Satisfiability allows no nontrivial sparsification unless the polynomial-time hierarchy collapses[END_REF], we can show a lower bound on the number of points in a polynomial kernel for Hyperplane Subset General Position in R d , for each fixed positive integer d. This result is a direct extension of the results obtained in [START_REF] Kratsch | Point Line Cover: The Easy Kernel is Essentially Tight[END_REF] and [START_REF] Froese | Finding Points in General Position[END_REF].

Bounded degree polynomials and the dual parameter

In this section we discuss about the generalization of Theorems 16 and 17. Note that, for any given point set P with n points, both theorems can be proved for finding a point set of size n -h, h being the dual parameter, if the construction of Lemma 14 can be replicated for a particular family F. In particular, consider a family F of polynomials of degree at most d with basis {f 1 (X), . . . , f b (X), 1}, where X = {X 1 , . . . , X t }. Suppose for each b-uniform hypergraph G with n vertices and m edges it is possible to make a transformation as follows:

1. The points {p 1 , p 2 , . . . , p n } are in general position with respect to F and have bounded representation. 2. Each vertex v i ∈ V (G) is mapped to the point p i ∈ P .

3.

Each hyperedge e j ∈ E(G) is mapped to the point b j ∈ B. 4. For a hyperedge e j ∈ E(G), if there are d points {p i1 , p i2 , . . . , p i b } ∈ P such that b j , p i1 , p i2 , . . . , p i b lie on a polynomial from F, then it must be the case that e j = {p i1 , p i2 , . . . , p i b }. 5. For any set of i ≤ b points of B and b + 1 -i points of P cannot be on any polynomial of F. 6. The points in B are in general position. In other words, no b + 1 points in B can be on any polynomial of F. Let us call such a transformation a good transformation. Then with respect to such a family F, equivalent tight kernelizations for the dual parameter can be given. When F is the family of spheres, then such a construction is possible. Proof. The construction is similar as that of Lemma 14, as we again can construct the sets greedily. The point set P can be extracted from a large enough grid as in the construction given in Lemma 14. The construction of the points in B is also done inductively. Suppose the points of a subset B ⊂ B have already been placed on rational points such that all the necessary conditions are satisfied. Let b e ∈ B \ B . Consider the sphere S e defined by the d-sized point set P e corresponding to the vertices of e ∈ E(G). Consider the family F of spheres formed by (i) a set of any d points in P other than the set P e , (ii) any d points from B , and (iii) a set S of d points with at least one point from P and at least one point from B . The intersection of this family of spheres with S e is a family F of lower dimensional spaces. Since the points in P have bounded representation, so do the intersection spaces. It is possible to determine in polynomial time the arrangement of the lower dimensional intersections on S e [START_REF] Agarwal | Arrangements and their applications[END_REF]. From this arrangement, we select a point with bounded representation that does not belong to any of the lower dimensional flats in F and set the point to b e . The set B ∪ b e again satisfies all the necessary conditions. We continue till all the points in B have been determined. Thus, we construct the required set P B.

Open Problems

One of the major open questions in this area is regarding techniques for showing kernel lower bounds with respect to the primal parameter. Currently, no non-trivial lower bound is known for even Hyperplane Subset General Position in R 2 .

In Section 5, we gave tight lower bounds with respect to the dual parameter under some restricted vector spaces of d-degree polynomials. It will be interesting to understand the problem better for general vector spaces of d-degree polynomials. In fact, it might be useful for both algorithmic as well as combinatorial studies to understand the Geometric Subset General Position in both the primal and dual parameter for families of d-degree polynomials that are not vector spaces or a subset of a vector space. We are interested in studying families that fall outside these frameworks.

General position with respect to spheres is also connected to Delaunay Subset Selection problem where we are given a point set P ⊂ R d as input and the problem is to extract a maximum size subset S of P such that the Delaunay complex Del(S) is a triangulation of the convex hull conv(S) of S. Although the upper bounds for kernelization given in this paper hold for this problem, lower bound questions remain open for both primal and dual parameter.

  d-Polynomial Sub. General Pos. Parameter: k Input: A set P of n points in R d , for a fixed constant d, a bounded degree polynomial family F in R d and a positive integer k Question: Is there a subset S ⊆ P of size at least k such that S is in general position with respect to F in R d ?

Rule 1 .Lemma 3 .Theorem 5 .

 135 Given an instance (P, k) of Hyperplane Subset General Position in R d , if there is a hyperplane H with at least (d -1) k-d d + d points then we delete all the points in H ∩ P and set k = k -d. Reduction Rule 1 is safe. We apply this Reduction Rule exhaustively. In the end, we know that each hyperplane can contain O(k d ) input points. Together with the bound on coplanarity, we will also use the following result by Cardinal et al. [4, Theorem 4.1] to get a kernel. Theorem 4. (Cardinal et al. [4]) Let P be a set of n points in R d with at most cohyperplanar points, where = O( √ n). Then P contains a subset of size Ω (n/ log l) 1/d of points in general position. Hyperplane Subset General Position in R d , parameterized by k and with an input point set where all lower dimensional flats are non-degenerate, has a O(k 2d ) kernel.

Theorem 7 . 7 25: 8

 778 Hyperplane Subset General Position in R d parameterized by k has a kernel of size O(k 2d 2 ). Using the techniques in the proof of Theorem 7 we can also solve the projective version of the general position problem. For a given point set P in R d , S ⊆ P \ {0} is said to be in M F C S 2 0 1 Kernelization of Subset General Position problem projective general position if no more than d -1 points from S lie on a hyperplane in R d that passes through the origin. The parameterized version of the problem is the following: Projective Hyperplane Subset General Position Parameter: k Input: An n point set P in R d , for a fixed constant d, and a positive integer k Question: Is there a subset S ⊆ P of size at least k such that S is in projective general position?

Lemma 8 .

 8 (Projective version of Theorem 4) Let P be a set of n points in R d such that for any hyperplane H passing through the origin, we have |H ∩P | ≤ , where = O(n 1/3 ).

Theorem 11 .

 11 d-Polynomial Subset General Position in R t parameterized by k, has a polynomial kernel of size O(k 2b 2 ). Here b is the size of the basis generating the underlying vector space of polynomials.

Observation 1 .Lemma 15 .

 115 Let G be a d-uniform hypergraph and P B be the set of points in R d corresponding to G. For any maximal set S of points in general position, there is a set of size at least |S| that contains all the points in B. This helps us to design a reduction from d-Hypergraph Independent Set to Hyperplane Subset General Position in R d . There is a many-one reduction from d-Hypergraph Independent Set on d-uniform hypergraphs to Hyperplane Subset General Position in R d . Finally, we are ready to prove the main result. Theorem 16. Hyperplane Subset General Position in R d parameterized by the dual parameter cannot have a kernel of size O(h d-) if co-NP NP/poly. Proof. We give a reduction from d-Hitting Set on d-uniform hypergraphs. Given an instance (G, h) of d-Hitting Set on d-uniform hypergraphs, we consider the equivalent d-Hypergraph Independent Set instance (G, |V (G)| -h). By Lemma 15, we construct an instance (P B, |V (G)| + |E(G)| -h). Note that the transformation is such that |P | = |V (G)| and |B| = |E(G)|. Thus, G has a d-hitting set of size k if and only if G has an independent set of size |V (G)| -h, which by Lemma 15 happens if and only if P B has a point subset of size k = |P B| -h that is in general position with respect to hyperplanes in R d . This means that the dual parameter |P B| -k is equal to h, which is the d-hitting set size in G. This implies the lower bound on the kernel size of Hyperplane Subset General Position in R d parameterized by the dual parameter. We obtain tight polynomial kernels from the following Proposition, derived from a folklore result. Proposition 16.1. Hyperplane Subset General Position in R d parameterized by the dual parameter h has a kernel of size h d .

Theorem 17 .

 17 Hyperplane Subset General Position in R d , parameterized by h, cannot have a kernel with O(h d-) points if co-NP NP/poly.

Corollary 18 .

 18 Given the family of spheres in R d , for each (d + 1)-uniform hypergraph with n vertices and m points there is a good transformation to a set P B of n + m points.

  In this Section, we show that Hyperplane Subset General Position in R d , parameterized by the dual parameter h, cannot have a kernel of size h d-if co-NP NP/poly. We show this result by the standard technique of polynomial parameter transformation. For a fixed d, we reduce the d-Hitting Set problem on d-uniform graphs to the problem of Hyperplane Subset General Position in R d . By Proposition 2.1, this gives us a lower bound for Hyperplane Subset General Position in R d . For the main result, we construct for each positive integer n and each d, a set of n points in R d with some special properties. For every d-uniform hypergraph G in n vertices and m hyperedges, there is a transformation to a set P B = {p 1 , p 2 , . . . , p n } {b 1 , b 2 , . . . , b m } of n + m points in R d that have the following properties: 1. The points {p 1 , p 2 , . . . , p n } are in general position.2. Each vertexv i ∈ V (G) is mapped to the point p i ∈ P . 3. Each hyperedge e j ∈ E(G) is mapped to the point b j ∈ B. 4. For a hyperedge e j ∈ E(G), ifthere are d points {p i1 , p i2 , . . . , p i d } ∈ P such that b j , p i1 , p i2 , . . . , p i d are cohyperplanar, then it must be the case that e j = {v i1 , v i2 , . . . , v i d }. 5. For any set of i ≤ d points of B and d + 1 -i points of P cannot be cohyperplanar. 6. The points in B are in general position. In other words, no d + 1 points in B are cohyperplanar.

	Lemma 14.

M F C S 2 0 1 7


Stefan Pernes
email: stefan.pernes@inria.fr

Laurent Romary
email: laurent.romary@inria.fr

Kara Warburton

TBX in ODD: Schema-agnostic specification and documentation for TermBase eXchange

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

Introduction

TermBase eXchange (TBX), the ISO standard for the representation and interchange of terminological data, is currently undergoing revision and will for the first time formalize overarching structural constraints regarding the definition and validation of dialects and XML styles. To match these requirements, the ODD specification language provides advanced subset selection and constraint specification capabilities covering both structure and content of text encoding formalisms. Following the literate programming methodology, it furthermore allows the definition of integrated resources, which contain formal specifications alongside their prose descriptions and usage examples. This paper first describes the meta-model behind TBX as well as current challenges in the context of its revision. From this follows a description of applicable ODD mechanisms and the design of an ODD architecture, which allows for a complete specification of present-day TBX.

Terminological Markup Framework and TermBase eXchange

Terminology standards have witnessed a long evolution since 1987 when a first pre-SGML format for storage and interchange via magnetic tapes was devised. Published in 2003as ISO 16642 (2003), the Terminological Markup Framework (TMF) marks a pivotal point in the succession of terminology standards as it constitutes a meta structure for terminology encoding which also provides the foundation for the more recent TBX format. TMF specifies a framework designed to provide guidance on the basic principles for representing data recorded in terminological data collections (ibid.). Its aims can be described as twofold (Romary 2001, 2f): (1) as a meta-model for terminological data representation it facilitates the description and comparison of existing interchange formats, and (2) it provides a mechanism for the flexible definition of interchange formats while safeguarding interoperability between them. The specification of such a meta-model thus eases the integration of different terminological databases with each other as well as with other lexical resources. In principle, TMF allows one to describe a potentially infinite set of Terminological Markup Languages (TML). Formally, this flexibility is achieved by describing the various components of terminological databases as either part of the structural skeleton or as data categories. This leads to the four elementary notions of TMF (ibid., 3f):

1. The meta-model: A structural skeleton for terminological entries following a concept-oriented, or onomasiological, view.

2. Information units taken from a Data Category Repository (DCR) as described in ISO 12620 (1999) (a new version is about to be published).

3. Methods and representations: The actual implementation of a TML, combining the structural skeleton with the chosen data categories. This also comprises the mappings between data categories and the vocabularies used to express them (e.g. as an XML element or a database field).

4. A generic mapping tool: A methodology that maps any given TML onto the meta-model. The notion of a generic mapping tool can be replaced by the ODD architecture as proposed in this paper.

As a consequence of these elementary notions, the interoperability between two TMLs is reduced to a comparison of their respective use of data categories.

TermBase eXchange (TBX) as defined by ISO 30042 ( 2008) is precisely an instantiation of the described meta-model alongside a specific selection of data categories. It is a reference implementation of TMF, taking the form of XML (thus its official specification is implemented as XML DTD, RelaxNG, and W3C schemas) and constituting what is nowadays called TBX-Default, or the master TBX dialect. It is designed to support various types of processes involving terminological data, including analysis, descriptive representation, dissemination, and interchange (exchange), in various computer environments (ibid.). TBX is currently undergoing extensive review as ISO CD30042 (2017): It establishes provisions for the specification of official TBX dialects, such as their minimum requirements in terms of structure and data categories. Furthermore, it is targeting increased interoperability by merging the content models of two alternative term information group elements, tig and ntig, into one termSec element. See Figure 1 for a short sample TBX entry (in accordance with the current Community Draft version). Additionally, two markup styles, data categories as tags (DCT) and data categories as attribute values (DCA), are defined. Apart from the need for a modular framework for dialect specification, a consequence of this development is that the specification of TBX itself will profit from tighter control over data categories, their identifiers and values, as well as data type information for these values. As has also been noted in the context of data exchange with Linked Open Data description formalisms such as RDF and OWL, the current specification of TBX does not provide data type description mechanisms in the classical sense, focussing mostly on string values based on W3C XML primitives (cf. Reineke 2014, 7). Thus, the strengths of an ODD architecture as proposed herein are a modular mechanism for the description of TBX dialects and an increased control over data types.

The Text Encoding Initiative and One Document Does it all

The Text Encoding Initiative (TEI) maintains a set of guidelines which have become a de facto standard in the encoding of literary, historical, and linguistics research data. Being established in 1987, the TEI guidelines predate and inform a number of modern web and encoding standards. They comprise close to 500 elements which are organised in functional-thematic modules, classes of shared attributes, and macros for common content models. The broadness and complexity of the TEI is paired with its own specification language that allows for a modular definition of project-specific customizations. One Document Does it all (ODD) is a generic specification language, establishing a separation between the specification of TEI encoding models and current schema languages, be it a XML DTD, a RelaxNG schema, or a W3C schema. Thus, TEI encoding models are essentially agnostic about the choice of a representation language and could also map to formalisms other than XML (Burnard 2013, 13). Furthermore, ODD follows the literate programming paradigm and constitutes a single resource containing formal declarations alongside descriptive prose and examples of usage (Burnard and Rahtz 2004, 3). Figure 2 schematically displays the different aspects of processing ODD files. Formal declarations in ODD concern foremost the key components of the TEI abstract model: elements, attributes, modules, classes, and macros. The last three components serve to reduce the overall systems complexity and allow a coarse-grained selection of characteristics for a TEI customization. Another major simplification stems from a conscious effort to provide uniform levels of description and hence processing allowing components to be added, changed, replaced, or deleted within a given context and at any point in a schema declaration (Burnard and Rahtz 2004, 8). Modifications of this kind can be chained together (ODD chaining), thus making it easy to supplement a broadly specified TEI customization with fine-grained, context-specific modifications. The context specificity of such declarations also allows for a tighter constraint on possible attribute values by means of data typing (Burnard 2013, 10):

The vast majority of attribute values are defined by reference to a data type macro as defined within the ODD system, which are in turn mapped to a W3C Schema data type or to an expression in RELAX NG syntax, thus allowing the ODD system to overlay additional semantics onto such bare data types (see Figure 3, TEI datatypes). Additionally, a further layer of constraint specification can be added using ISO Schematron, making it possible to implement many of the informally expressed rules for good practice, which are typically found in the prose of encoding guidelines.

Description of the TBX in ODD architecture

Prior work has already established an ODD architecture for the ISO 30042 (2008) Basic dialect [START_REF] Romary | TBX goes TEI -Implementing a TBX basic extension for the Text Encoding Initiative guidelines[END_REF]. Furthermore, the TBX specification published in 2008 was actually written in ODD by the core editorial team of the time1 . This approach -a major diversion from conventional ISO authoring practices -was undertaken as case study for the use of ODD to author ISO standards that contain a mixture of prose, machine-readable specifications and sample code, and that require schemas as derivative products. Major changes introduced by the current revision of TBX are a modular framework for the specification of dialects and the implementation of markup styles (DCA vs. DCT). Both requirements can be met via module selection in ODD. A prerequisite for this ODD chaining mechanism is a master ODD file, containing specifications for all core structure elements and permissible data categories (it is equivalent to TBX-Default, the so-called master TBX dialect). Specifying a new TBX dialect in ODD is achieved by selecting modules and classes, or parts thereof, and selecting data categories from the ISO Data Category Repository, which may also extend on the TBX default set of data categories. Using the ODD framework, this dialect can afterwards be transformed into any of the supported schema languages for document validation -which also serve as the official specification of TBX and its dialects. The same approach applies for the validation of one or the other data category style. For example, in order to generate a schema for validating files using only DCA style, one would define a subset of the master ODD that excludes the module TBXDCT and vice versa.

A preliminary overview of the module and class organization is shown in Figure 4. File header elements, core structure, and elements specific to the two markup styles are grouped into modules, while

Conclusion

In this paper we have described the specification of TermBase eXchange (TBX), which is currently undergoing revision as ISO CD30042 (2017), using the ODD specification language. The requirements for this upcoming version of TBX include a system for the derivation of dialects, which need to be verifiably compliant to the core structure and, in the best case, can be defined in a user-friendly, modular fashion. The ODD language provides such a framework and follows a literate programming approach where documentation, usage examples, and formal specifications all reside in one document. Additionally, it is a sustainable approach that does not depend on any specific schema language and is in principle able to map to the data modelling ecosystem of the day -an advantage given the long-term perspective of terminology encoding standards.

Figure 1 :

 1 Figure 1: Example TBX entry in DCT style

Figure 2 :

 2 Figure 2: ODD processing and chaining

Figure 4 :

 4 Figure 4: TBX module and class organization in ODD

Arle Lommel, Alan Melby, and Kara Warburton


Adaine Abdoulwahab

Sidi Ould

Saad Hamady

Effect of Interface Properties on the Electrical Characteristics of InGaN-based Multijunction Solar Cell

Keywords: 1 Sun with AM 1.5G Solar Spectrum.  InGaN Bandgap, Affinity, Effective density of states, Permittivity, Absorption, SRH, Auger and direct recombination, Band discontinuity, Tunneling current, Polarization/Piezoelectric parameters, …: taken from

come

The InGaN ternary alloy has the potentiality to achieve high efficiency solar cells: tunable bandgap in the whole solar spectrum, high absorption coefficient, high stability and radiation tolerance. These very promising characteristics make InGaN potentially ideal for designing and developing next-generation high-efficiency thin films solar cells. However, challenging issues remain to address:

Optimal 3 Figure

 3 Photogeneration and recombination rate distribution and effect of deep defects located in


Vidar Slåtten
email: vidarsl@item.ntnu.no

Peter Herrmann
email: herrmann@item.ntnu.no

Contracts for Multi-instance UML Activities

We present a novel way of encapsulating UML activities using interface contracts, which allows to verify functional properties that depend on the synchronization of parallel instances of software components. Encapsulated UML activities can be reused together with their verification results in SPACE, a model-driven engineering method for reactive systems. Such compositional verification significantly improves the scalability of the method. Employing a small example of a load balancing system, we explain the semantics of the contracts using the temporal logic TLA. Thereafter, we propose a more easily comprehensible graphical notation and clarify that the contracts are able to express the variants of multiplicity that we can encounter using UML activities. Finally, we give the results of verifying some properties of the example system using the TLC model checker.

Introduction

A key to efficient software engineering is the reuse of existing software components that ideally are independently developed and marketed as commercial off-the-shelf (COTS) products. To enable a seamless combination of the components, one needs meaningful descriptions of the component interfaces that specify properties to be kept by both the components themselves and their environments. Due to the tight interaction with their environment, this requirement holds in particular for reactive systems [START_REF] Harel | On the development of reactive systems[END_REF]. To support the reuse of software components for reactive, distributed software systems, we use collaborative building blocks described by multi-partition UML activities, each augmented with an interface contract in the form of a UML state machine [START_REF] Kraemer | Automated Encapsulation of UML Activities for Incremental Development and Verification[END_REF][START_REF] Kraemer | Engineering Support for UML Activities by Automated Model-Checking -An Example[END_REF]. We call these contracts External State Machines (ESMs). The contracts not only enable reuse of problem solutions, but also make for a reuse of verification effort as the user can verify a composed system using only the contracts, which in turn have been verified to be correct abstractions of the underlying solutions. This compositional approach helps to reduce the complexity and state space of the system models significantly [START_REF] Kraemer | Automated Encapsulation of UML Activities for Incremental Development and Verification[END_REF]. The ESMs also help another problem with reuse: It may not always be straightforward to look at a reusable activity and see what it does and how to compose it correctly with the rest of the system. As the ESM only describes behaviour visible to the outside of the block, it aids both these tasks.

ESMs constitute what Beugnard et al. [START_REF] Beugnard | Making Components Contract Aware[END_REF] call synchronization contracts, meaning that they can specify the effect of interleaving operations on a component, not just sequential operations. However, up until now we have been limited to collaborations in which only one instance of each type participates, as the contracts could not support collaborations featuring multiple component instances of the same type. If, for instance, a client request may be routed to one of several servers, we could not express an interface behaviour that permits server S to receive the request only if none of the other servers have received it. In systems that employ load balancing or fault-tolerance mechanisms, however, to specify and guarantee this kind of behaviour is crucial. Thus, compared with the ESMs, we need additional concepts and notation for behavioural interfaces.

Any extension of ESMs should ideally keep a key characteristic of SPACE [START_REF] Kraemer | Tool Support for the Rapid Composition, Analysis and Implementation of Reactive Services[END_REF]: The underlying formalism is hidden to the user. According to Rushby [START_REF] Rushby | Disappearing formal methods[END_REF], this is a key quality of practical development methods. SPACE relies on automatic model checking to verify system models. To mitigate the problem of state-space explosion, we limit our scope to verifying properties dependent only on the control flow of the system designs. While we could very well include data in the model, the model checker would not be able to verify properties dependent on data for realistic systems, as the state space would grow exponentially with every data element we include. Nevertheless, as pointed out in [START_REF] Kraemer | Engineering Support for UML Activities by Automated Model-Checking -An Example[END_REF][START_REF] Kraemer | Tool Support for the Rapid Composition, Analysis and Implementation of Reactive Services[END_REF], also the model checking of just control flows is of great practical help, for single-instance activities.

The ESMs are basically Finite State Machines (FSMs) with special annotations of their transitions. To model multiple entities in a suitable way, we use Extended Finite State Machines (EFSMs) [START_REF] Cheng | Automatic functional test generation using the extended finite state machine model[END_REF] instead, which allow to refer to the indexes of instances in the form of auxiliary variables. The semantics of these Extended ESMs (EESMs) is formalized using the Temporal Logic of Actions, TLA [START_REF] Lamport | The temporal logic of actions[END_REF]. To relieve the software engineer from too much formalism, we further present a more compact graphical notation in the form of UML state machines where statements closer to programming languages are used to describe variable operations.

The next section discusses related work on component contracts, particularly work using UML. Our load balancing example system is presented in Sect. 3. In Sect. 4, we formalize the EESM semantics for many-to-many activities in TLA, and present the graphical notation. We give EESMs for the other types of activities, one-to-one and one-to-many, in Sect. 5. Some results, in particular about the effects on model checking, as well as future work is discussed in Sect. 6, where we also conclude.

Related Work

There are several other works that define a formal semantics for UML activities [START_REF] Eshuis | Symbolic model checking of UML activity diagrams[END_REF][START_REF] Guelfi | A Formal Semantics of Timed Activity Diagrams and its PROMELA Translation[END_REF][START_REF] Storrle | Semantics and Verification of Data Flow in UML 2.0 Activities[END_REF], but neither of them include contracts for use in hierarchical activities. Eshuis [START_REF] Eshuis | Symbolic model checking of UML activity diagrams[END_REF] explicitly argues to leave this concept out, as any hierarchical activity can be represented as a flat one. However, this results in a much bigger state space.

As Beugnard et al. [START_REF] Beugnard | Making Components Contract Aware[END_REF] point out, we can only expect software components to be reused for mission-critical systems if they come with clear instructions on how to be correctly reused and what guarantees they give under those conditions. UML has the concept of Protocol State Machines [START_REF]OMG: Unified Modeling Language: Superstructure[END_REF] to describe the legal communication on a port of a component. Mencl [START_REF] Mencl | Specifying Component Behavior with Port State Machines[END_REF] identifies several shortcomings of these, for example that they do not allow to express dependencies between events on a provided and required interface, nor nesting or interleaving method calls. To remedy this, he proposes Port State Machines, where method calls are split into atomic request and response events. These Port State Machines are restricted to pure control flow, as transition guards are not supported. Bauer and Hennicker [START_REF] Bauer | Views on Behaviour Protocols and Their Semantic Foundation[END_REF] describe their protocol style as a hybrid of control flow and data state. However, they also cannot express the dependency between provided and required interfaces, and they currently lack verification support for whether two components fit together.

The ESMs have similar properties to Port State Machines in that all interface events are atomic, i.e., an operation is split into a request and response event, to allow for expressing nesting and interleaving of operations. They also essentially combine provided and required interfaces in the same contract, hence allowing to express dependencies between them. The EESMs combine this with data state to allow for compact representations of parametrized components and collaborations.

Sanders et al. [START_REF] Sanders | Service Discovery and Component Reuse with Semantic Interfaces[END_REF] present what they call semantic interfaces of service components, both described as finite state machines. These interfaces support both finding complementary components and implementations of an interface, hence also compositional verification. While they provide external interfaces for each local component and then asynchronously couple these to other, possible remote, components, our activity contracts act as internal interfaces that can be synchronously coupled with other local behaviour in the fashion of activity diagrams.

Our approach differs from all the above in that it permits the encapsulation of both local components and distributed collaborations between components, described by single-partition or multi-partition activities respectively. Further, our extended interfaces allow to constrain behaviour based on the state of parallel component instances, giving a powerful abstraction of distributed collaborations.

A Load Balancing Client -Server Example

In SPACE, the main units of composition are collaborative building blocks in the form of UML activities that can automatically be transformed to executable code [START_REF] Kraemer | Tool Support for the Rapid Composition, Analysis and Implementation of Reactive Services[END_REF]. A system specification consists of a special system activity as the outermost block. This system activity can contain any number of inner activities, referenced by call behaviour actions, as well as glue logic between them. (c) Structural view of system example with four clients and two servers Fig. 1: System example: A load balancing client -server system requests via a Router m-n block to a set of servers. Thus, Router m-n is an inner block, its activity depicted in Fig. 1(b). Each activity partition is named in the upper left corner and the bracketed parameter behind the name, a for client and b for server, denotes the number of component instances of this type. While each client only sees one router, each server partition has a/b instances of the router block, as denoted by parameters (1, a/b) after its name and the shade around the server side of the block. This is also illustrated in Fig. 1(c), where we see that each client component only has a single requester sub-component, whereas each server has two responders. Note that the structural view is completely redundant and only serves to illustrate the information in the activities and the EESMs introduced below. The diagonally striped area inside the server partition represents other components of the same type, i.e., other servers. This gives a visual indication that the Router m-n block, in addition to collaborating with clients, also collaborates with other server instances. Each server also makes use of an inner activity called Make Response, which turns requests into responses. We have omitted it in Fig. 1(c), as it is completely local.

It is the job of the Router m-n block in Fig. 1(b) to balance the load so that a single server does not have to serve requests from all clients at the same time. All requesters can send requests to all responders, as illustrated by the full mesh connectivity in Fig. 1(c). Each responder uses the Forward block to forward requests to other responders, if it is currently busy itself. In the structural view, the component of the Forward block is shown as a small nameless rectangle on each responder that can communicate with every other such component. It is important to note that the Router m-n activity encapsulates asynchronous communication between components, while the synchronous interaction between an outer and an inner activity takes place via pins1 linking flows of the two activities. For instance, the block Router m-n is linked with the system activity by the pins reqIn, reqOut, resIn and resOut. Here, reqIn is a start pin initiating an activity instance (really, the corresponding requester instance), whereas resOut is a stop pin terminating the instance. The remaining pins with black background are streaming pins for interacting with active instances.

The semantics of UML activities is similar to Petri-nets, where the state is encoded as tokens resting in token places and then moving along the directed edges to perform a state transition [START_REF]OMG: Unified Modeling Language: Superstructure[END_REF]. In our approach, all behaviour takes place in run-to-completion steps [START_REF] Kraemer | Reactive Semantics for Distributed UML Activities[END_REF]. That is, all token movements are triggered by either receptions of external events (for instance, tokens resting between partitions) or expiration of local timers, and the tokens move until such an event is needed to make progress again.

Initial nodes start the behaviour of each system-level partition instance. They are fired one by one, but we make the assumption that no token will enter a partition before its initial node has fired. The initial node of the server partition can fire at any time, releasing a token into the start pin of the Make Response block. In the client partition, the token emitted from the initial node will enter the Router m-n block via the reqIn pin. Afterwards, it will be forwarded to a server instance and leave the block via pin reqOut, to enter pin req of Make Response. The Make Response block will eventually emit a token via its res pin, and the server partition will choose one of the Router m-n instances to receive it via its resIn pin, as denoted by the select statement [START_REF] Kraemer | Synthesizing components with sessions from collaboration-oriented service specifications[END_REF]. A select statement takes some data carried by the token and uses it to select either among various instances of a local inner block or of remote partitions. The Router m-n block will eventually emit a token through its resOut pin in one of the client partitions, which will follow the edge to the timer on the client side, where the step will stop. Later, the timer will expire, causing it to emit the token so that the client can perform another request. In this example, the timer is simply an abstraction for whatever the client might be doing between receiving a response and sending a new request. The behaviour of the Router m-n block is described in Sect. [START_REF] Eshuis | Symbolic model checking of UML activity diagrams[END_REF].

When we compose a system by creating new activities and reusing existing ones, we want to be able to verify properties of it. Given that SPACE models have a formal semantics [START_REF] Kraemer | Formalizing Collaboration-Oriented Service Specifications using Temporal Logic[END_REF][START_REF] Kraemer | Automated Encapsulation of UML Activities for Incremental Development and Verification[END_REF], we can express them as temporal logic specifications and use a model checker to verify properties automatically. To mitigate the problem of the state space growing exponentially with every stateful element, each activity is abstracted by an External State Machine (ESM), which is a description of the possible ordering of events visible on the activity pins. This allows us to do compositional verification of the system specification: We first verify that the activity and its ESM are consistent, then we only use that ESM when verifying properties for a higher-level or system-level block. Note that verifying the consistency of an ESM and its activity cannot be done automatically for all blocks, as some will constrain their control-flow behaviour according to data stored in the activity tokens. In this case, the model allows all possible behaviours, and the potentially false positives reported by a model checker (that is, error traces that cannot occur in the real system) can be inspected manually, reducing the verification task. A select statement is an example where data constrains the destination of a token.

Figure 2(a) shows the ESM of the local building block Make Response. As discussed in the introduction, the ESM notation has the same expressive power as a finite state machine or Mealy machine [START_REF] Mealy | A Method to Synthesizing Sequential Circuits[END_REF], to be precise. The transition labels correspond to pins, and the slash character separates the transition trigger event, as seen from the perspective of the block, from the effect. Hence, start/ means that the transition is triggered from outside by a token entering pin start and that no tokens will pass any other pins in the same step. The ESM shows that a response is not output until a request has been sent in, and that this will not happen in the same step. Once the non-empty state is reached, further requests may enter and responses may be emitted from the block. Just looking at the ESM, however, we cannot know exactly how many responses will be sent out, as there is no way of knowing if a /res event has caused a transition to the empty state, or if the ESM is still in the non-empty state. This is because there is no way to track the actual number of buffered requests. 2 When verifying properties of a system, such information may sometimes be necessary. For example, if this block was used in a system that sends three requests, we would like to infer from the ESM that exactly three responses can be emitted back out.

Contracts for Multi-instance Activities

To support multi-instance activities, we extend the ESMs to include transition guards, variables, arithmetic and predicate logic. Hence, they are now formally EFSMs [START_REF] Cheng | Automatic functional test generation using the extended finite state machine model[END_REF]. This enables us to specify event constraints that relate to the state of parallel component instances. Moreover, this increases the general expressiveness, so that we are able to better handle the case of the Make Response block.

Figure 2(b) shows the EESM of the Make Response block. We have here added a variable, queue, that tracks the number of requests buffered. To constrain the behaviour based on the queue size, as well as update it, this EESM also contains transition guards in square brackets and variable operations in lined boxes.

Figure 1(b) shows the internal activity of the Router m-n block. A request enters through the reqIn pin of the requester partition and is forwarded to a responder partition. The select statement, along with the fact that there are n responder partitions, tells us that a requester expects to have a choice of responders to communicate with, when forwarding the token. When a token crosses a partition border, the corresponding activity step ends, as remote communication is asynchronous. When the token is received by the responder partition, it is passed on to an inner block, Forward. This block may emit the token directly through its out pin to be passed on through the reqOut pin of Router m-n, or it may forward the token to another responder, if this one is busy already serving a request. 3 When a response token is received via the resIn pin, it is duplicated in the fork node and passed both to pin done and the channel for the originating requester partition.

We now describe the EESM of block Router m-n using the language TLA + of the temporal logic TLA [START_REF] Lamport | The temporal logic of actions[END_REF], as shown in Fig. 3. The TLA + module starts by defining the module name on the first line. The extends keyword states that this module imports the modules Naturals, which defines various arithmetic operators on natural numbers, and MatrixSum, defining operators for summing matrices. The variables of the module are declared using the variables keyword, where req and res represent the requester and responder partitions respectively. Constants are declared by the constants keyword. They are the parameters of the model. When creating the building block Router m-n, we do not know how it will be reused in an enclosing activity. Another developer may choose to put multiple instances in both, one or none of the enclosing partitions. So, we need constants for the number of requesters and responders per enclosing partition instance, as well as the number of enclosing partition instances on each side. Hence, the global number of requesters is really no req * no req encl.

A TLA + specification describes a labelled transition system. This is given as a set of states, a subset of the states that are initial states, a set of actions (labels) and a transition relation describing whether the system can make a transition from one state to another via a given action. The set of initial states

∆ = req.reqIn[e, i] > 0 ∧ ∃ f ∈ 1 . . no res encl, k ∈ 1 . . no res : ∧ res.resIn[f , k ] > 0 ∧ res = [res except ! .reqOut[f , k ] = 0, ! .resIn[f , k ] = 0] ∧ req = [req except ! .reqIn[e, i] = 0]
Fig. 3: TLA + module for the EESM of Router m-n is described by the Init construct. Here, the req and res variables are each given records for their corresponding pins (except pin resOut, see below), which in turn are functions in two dimensions stating whether a token has passed the pin for each requester or responder instance. That is, a requester or responder instance is identified by an enclosing instance number combined with an inner instance number.

Next in the TLA + module follow the actions, which formally are predicates on pairs of states. Variables denoting the state before carrying out an action use their common identifiers while those referring to the state afterwards are given a prime. The action reqIn states that for a requester e, i identified by enclosing instance e and inner instance i , a token can enter pin reqIn only if the given instance has not yet had a token pass through this pin. The next conjunct of the reqIn action says that the values of the req variable will be the same as now, except that the counter for tokens having passed through pin reqIn will be set to 1 for requester e, i . The unchanged keyword states which variables are not changed by an action, as TLA + requires all next-state variable values to be set explicitly.

The reqOut action also represents that a token is only allowed through pin reqOut of responder e, i if it has not already had a token pass through. The second line constrains this further by stating that a token passing event can only happen if the sum of all tokens having passed any reqIn pin is greater than the sum of all tokens having passed any reqOut pin. Hence, this event on responder e, i is constrained by the state of parallel components. Action resIn

«eesm» Router m-n active ∀ i ∈ 1..|requester|: reqIn[i] = 0 ∀ k ∈ 1..|responder|: reqOut[k] = 0 ∧ resIn[k] = 0 active reqIn(i)/ reqIn[i] = 1 ∃ i: reqIn[i] == 0 active /resOut(i) reqIn[i] = 0 reqOut[k] = 0 resIn[k] = 0 ∃ i: reqIn[i] > 0 ∧ ∃ k: resIn[k] > 0 active resIn(i)/ resIn[i] = 1 ∃ i: reqOut[i] > 0 ∧ resIn[i] == 0 active /reqOut(i) reqOut[i] = 1 ∃ i: reqOut[i] == 0 ∧ ∑reqIn[ALL] > ∑reqOut[ALL]
Fig. 4: UML notation for the EESM of Router m-n states that a token may only enter a responder e, i via pin resIn if the same instance has already emitted a token via pin reqOut, but not already sent a response through pin resIn. The resOut action states that a requester e, i can only emit a token through pin resOut if it has received a token through pin reqIn. This is constrained further by requiring there to be a responder f, k , that has received a token through its resIn pin. All counters belonging to requester e, i and responder f, k are then set to 0, to reset their state. As the resOut action also performs the reset, there is no TLA + variable for its corresponding pin.

This behaviour is easier seen looking at the graphical notation in Fig. 4. Here, the style of the transition operations is closer to programming languages like Java. The number of partition instances is denoted |partition name|. We omit the domain of ∃ statements where this is obvious from the context, and the keyword ALL denotes all indexes in a domain. We also omit specifying which partition a pin belongs to if there is only one pin by that name in the activity. The transition from the initial node to the active state represents the Init construct in TLA + , and the remaining transitions represent the actions.

Since we do not model that a token keeps the index of its requester instance as data while located at a server, we cannot fully automatically verify that the activity and EESM for Router m-n are consistent. The model checker finds counterexamples where a response is simply sent to a requester that has not yet issued a request, instead of to a requester that has. What we can verify automatically, however, is that whenever a token is sent back to a requester, the EESM is in a state where the token would be allowed through the resOut pin of at least one of them.

Once a building block is complete, we can reuse it like we have reused Router m-n in our system example from Fig. 1(a). To verify properties of the system, we generate the TLA + module in Fig. 5 (see [START_REF] Kraemer | Engineering Support for UML Activities by Automated Model-Checking -An Example[END_REF]). This module instantiates other modules, namely Router m-n and Make Response. The constants no clients and no servers represent the parameters a and b from the system activity. We express the actions of the system activity as a composition of constraints and operations on the variables of the system activity, and actions of ESMs of the inner activities. Hence, the Init construct not only sets the timer in all client module load sharing system extends Naturals, MatrixSum variables r req, r res, m state, m queue, client, server constants no clients, no servers no res ∆ = no clients ÷ no servers r ∆ = instance router m n with no req ← 1, no req encl ← no clients, no res ← no res, no res encl ← no servers, req ← r req, res ← r res m ∆ = instance make response with no make response ← 1, no enclosing ← no servers, state ← m state, queue ← m queue

Init ∆ = client = [timer → [i ∈ 1 . . no clients → 0], initial → [i ∈ 1 . . no clients → 1]] ∧ server = [initial → [i ∈ 1 . . no servers → 1]] ∧ r ! Init ∧ m ! Init start client(p) ∆ = client.initial[p] = 1 ∧ client = [client except ! .initial[p] = 0] ∧ r ! reqIn(p, 1) ∧ unchanged server , m state, m queue start server (p) ∆ = server .initial[p] = 1 ∧ server = [server except ! .initial[p] = 0] ∧ m ! start(p, 1) ∧ unchanged client, r req, r res r reqOut m req(p, i) ∆ = r ! reqOut(p, i) ∧ m ! req(p, 1) ∧ unchanged client, server m res r resIn(p, i) ∆ = m ! res(p, 1) ∧ r ! resIn(p, i) ∧ unchanged client, server r resOut client timer (p) ∆ = r ! resOut(p, 1) ∧ client.timer [p] = 0 ∧ client = [client except ! .timer [p] = 1] ∧ unchanged server , m
P 1 ∆ = 2(∀ p ∈ 1 . . no servers : m queue[p, 1] ≤ no res) P 2 ∆ = 2
(Sum(r res.reqOut, no servers, no res) ≤ Sum(r req.reqIn, no clients, 1))

P 3 ∆ = 2(∀ p ∈ 1 . . no servers, i ∈ 1 . . no res : (server .initial[p] = 0 ∧ enabled r ! reqOut(p, i)) ⇒ enabled m ! req(p, 1)) P 4 ∆ = 2(∀ p ∈ 1 . . no servers : enabled m ! res(p, 1) ⇒ ∃ i ∈ 1 . . no res : enabled r ! resIn(p, i)) P 5 ∆ = 2(∀ p ∈ 1 . . no clients : enabled r ! resOut(p, 1) ⇒ client.timer [p] = 0)
Fig. 5: TLA + module for the system activity instances to 0 and all initial nodes to 1, but also calls the Init construct of Router m-n and Make Response as shown by r !Init and m!Init. Note also that since this is a system activity, we do not need to add an extra dimension for enclosing partition instances when identifying activity elements like the timer, as it cannot be reused in other activities. For a description of each action, we refer back to Sect. 3.

The whole system specification is written as a single formula Spec

∆ = Init ∧ 2[Next]
vars . This formula states that the transition system has initial states(s) as specified by Init and that every change to the variables listed in vars is done via one of the actions listed in the next-state relation, Next. The box-shaped symbol (2) in front of [Next] is the temporal logic operator always. It means that what follows must be true for every reachable state of the system model.

The small example system of this paper is chosen to allow us to show the formal semantics of the EESMs in TLA + and clarify that they are unambiguous, yet expressive enough for our needs. Therefore, the properties that we can verify for this system might seem rather trivial, but for more complex systems, variations of these properties may be very hard to verify without a formal model. The properties we want to verify are written formally below the horizontal bar in Fig. 5. All the properties can be verified by model checking. See Sect. 6 for further discussion of the results.

P1

The number of requests queued in any Make Response block is at most equal to the number of responders per server, i.e., the inner queue is finite. P2 There are at most as many ongoing requests on the server side as there are on the client side. P3 Whenever a server is started and a responder instance of that server is ready to emit a token through the reqOut pin, the Make Response instance of that server is ready to accept a token through its req pin. P4 Whenever a token can be emitted from the Make Response block of a server, at least one of the responder instances on that server is able to accept it. P5 Whenever a token can be emitted via the resOut pin of a requester instance, the corresponding timer is empty, hence ready to receive a token.

Other Types of Multiplicity

Our formalism for expressing contracts of multi-instance activities also works for one-to-one building blocks without any internal select statements, like Router 1-1 shown in Fig. 6(a). This is a special case, where each requester instance is statically mapped to a responder instance and vice versa. As each binary collaboration cannot have any constraints on its behaviour in terms of the state of parallel instances, we can simplify the EESM as shown in Fig. 7 without loss of information. This is, in fact, the same notation that we have been using already for ESMs of activities with one instance of each type [START_REF] Kraemer | Tool Support for the Rapid Composition, Analysis and Implementation of Reactive Services[END_REF], only augmented with an index i . The difference is that the formal semantics now supports multiple instances globally, instead of requiring such a block to be used in a system with only one instance of each enclosing partition as well.

Router 1-1 responder [1] requester [START_REF] Bauer | Views on Behaviour Protocols and Their Semantic Foundation[END_REF] Finally, we present a one-to-many variation of the router block, Router 1n, where a requester is statically mapped to a set of responders, as shown in Fig. 6(b). 4 This could be used in a setting where each server from Fig. 1(a) has one responder instance per client, so that each client has a choice of any server when issuing a request. When the response is to be routed back, the corresponding requester is already given, due to the static mapping.

The EESM of Router 1-n is shown in Fig. 8. Due to the mapping between requester and responder instances, the notation is a bit more complex than for the other variants. For example, the /reqOut(i) transition states that a token may only leave the reqOut pin through instance i if this has not happened already. The rest of the guard constrains this further by stating that a token passing can only occur if the corresponding requester instance has gotten more tokens through its reqIn pin than the sum of tokens having already passed through pin reqOut in all the responders mapping to that requester. The expression reqIn[responder [i ]] means the value of the reqIn variable for the requester who can be found by mapping responder [i ] to its corresponding requester. Hence, Σ reqOut[requester [responder [i ]][k ]] means the sum of reqOut values for the k different responders found by mapping responder[i] to its requester and then mapping that requester to the set of corresponding responders.

Note that it is the EESM that holds the information on whether there is a constrained static mapping or not. In contrast, the EESM of Router m-n, given in Fig. 4, has no references to any particular parallel instance or set of instances, only to the current instance and the keyword ALL. active /resOut(i)

reqIn[i] = 0 reqOut[k] = 0 resIn[k] = 0 ∃ i: reqIn[i] > 0 ∧ ∃ k ∈ responder[requester[i]]: resIn[k] > 0 «eesm» Router 1-n active ∀ i ∈ 1..|requester|: reqIn[i] = 0 ∀ k ∈ 1..|responder|: reqOut[k] = 0 ∧ resIn[k] = 0 active reqIn(i)/ reqIn[i] = 1 ∃ i: reqIn[i] == 0 active resIn(i)/ resIn[i] = 1 ∃ i: reqOut[i] > 0 ∧ resIn[i] == 0 active /reqOut(i) reqOut[i] = 1 ∃ i: reqOut[i] == 0 ∧ reqIn[responder[i]] > ∑reqOut[requester[responder[i]][k]]

Concluding Remarks

All the properties from Fig. 5 have been verified by the TLC model checker [START_REF] Yu | Model Checking TLA+ Specifications[END_REF], for the parameter values shown in Table 1. 5 Model checking only verifies properties for a model with some exact parameters. It does not say whether those properties will still hold for different parameters. However, if the model changes behaviour with respect to a property for some specific parameter values, it is often when a parameter is changed from 1 to >1, or it is likely due to highly intentional design decisions. Hence, the fundamental problem remains, but it is not always that great in practice.

Given that model checking is automatic, one could say that time is not an issue, as we can just leave a computer at it and check for up to, for example, a thousand instances of each partition. However, as Table 1 shows, the time needed grows exponentially as we increase the number of client instances. The linear increase from server instances comes from the fact that more servers reduce the number of responders per server.

There is a high level of parallelism in our system example. This is also the case for other systems using EESMs that we have verified. Hence, we expect partial order reduction [START_REF] Holzmann | An improvement in formal verification[END_REF] to alleviate the state-space blowup from increasing the number of instances. We therefore plan to also formalize our semantics in Promela, so we can use the Spin [START_REF] Holzmann | The Spin Model Checker, Primer and Reference Manual[END_REF] model checker, which implements partial order reduction. The formalisms are compatible, as there is already work for transforming another TLA derivative, cTLA, into Promela automatically [START_REF] Rothmaier | Analyzing Network Management Effects with Spin and cTLA[END_REF]. For relatively simple blocks, where the contract must be verified for any number of instances, the TLA formalism allows for writing manual refinement proofs as well [START_REF] Lamport | Refinement in state-based formalisms[END_REF].

We already have a tool for generating TLA + from SPACE models [START_REF] Kraemer | Engineering Support for UML Activities by Automated Model-Checking -An Example[END_REF]. This tool greatly reduces the time required to specify systems, and it automatically generates many types of general properties to ensure the well-formedness of SPACE models. We will extend the work with EESMs, outputting Promela specifications as well. To hide the formalism when specifying applicationspecific properties, there is work in progress to express them in UML.

To verify properties like "Every request is eventually responded to", would require adding data to identify each request and adding liveness constraints to the model. Being based on TLA, the formalism can accommodate this quite easily in the form of weak or strong fairness assumptions. The limiting factor is still time needed for model checking.

Having formalized extended ESMs, we are eager to use them in the setting of fault-tolerant systems, where multiple instances of the same type often collaborate to mask failures, and conditions such as a majority of the instances being reachable are often essential to precisely describe the behaviour of a block.

To conclude, contracts encapsulate software components and facilitate both reuse and compositional verification. The SPACE method uses collaborations detailed by UML activities as the unit of reuse. We introduce EESMs, which allow to describe the global behaviour of multi-instance activities, abstracting away internal state, while still having the expressive power to detail when an external event can take place. An example from the load balancing Router m-n block is that a request will only arrive at a server that has free capacity in the form of free responder instances, and only if the number of requests received from all clients is greater than the number of requests forwarded to any server. While the EESMs have a formal semantics in TLA, we give graphical UML state machines as specification tools, so that software engineers themselves need not be experts in temporal logic.

  Figure 1(a) shows the system activity for our example, a set of clients that can send «system» Load Balancing System

Fig. 2 :

 2 Fig. 2: Contracts for the Make Response block

  module router m n extends Naturals, MatrixSum variables req, res constants no req, no res, no req encl, no res enclInit ∆ = ∧ req = [reqIn → [e ∈ 1 . . no req encl, i ∈ 1 . . no req → 0]] ∧ res = [reqOut → [e ∈ 1 . . no res encl, i ∈ 1 . . no res → 0], resIn → [e ∈ 1 . . no res encl, i ∈ 1 . . no res → 0]]reqIn(e, i) ∆ = req.reqIn[e, i] = 0 ∧ req = [req except ! .reqIn[e, i] = 1] ∧ unchanged res reqOut(e, i) ∆ = res.reqOut[e, i] = 0 ∧ Sum(req.reqIn, no req encl, no req) > Sum(res.reqOut, no res encl, no res) ∧ res = [res except ! .reqOut[e, i] = 1] ∧ unchanged req resIn(e, i) ∆ = res.reqOut[e, i] > 0 ∧ res.resIn[e, i] = 0 ∧ res = [res except ! .resIn[e, i] = 1] ∧ unchanged req resOut(e, i)

=

  state, m queue client timer r reqIn(p) ∆ = client.timer [p] = 1 ∧ client = [client except ! .timer [p] = 0] ∧ r ! reqIn(p, 1) ∧ unchanged server , m state, m queue Next ∆ = ∨ ∃ p ∈ 1 . . no clients : start client(p) ∨ ∃ p ∈ 1 . . no servers : start server (p) ∨ ∃ p ∈ 1 . . no servers, i ∈ 1 . . no res : r reqOut m req(p, i) ∨ ∃ p ∈ 1 . . no servers, i ∈ 1 . . no res : m res r resIn(p, i) ∨ ∃ p ∈ 1 . . no clients : r resOut client timer (p) ∨ ∃ p ∈ 1 . . no clients : client timer r reqIn(p) Spec ∆ Init ∧ 2[Next] r req, r res, m state, m queue, client, server

Fig. 6 :Fig. 7 :

 67 Fig. 6: The two other variants of the router activity, with respect to select statements

Fig. 8 :

 8 Fig. 8: UML notation for the ESM of Router 1-n

Table 1 :

 1 Number of states found and time required to verify properties P1-P5

	# of servers →	1	2	3
	# of clients ↓
	1	7 states, < 1 sec
	2	37 states, 1 sec	70 states, 1 sec
	3	241 states, 2 sec		707 states, 3 sec
	4	1713 states, 4 sec	3410 states, 5 sec
	5	12617 states, 9 sec
	6	94513 states, 48 sec 188962 states, 99 sec 283411 states, 155 sec
	7	715001 states, 651 sec

They are really activity parameter nodes when seen from the inner activity itself, but are called pins when an activity is reused via a call behaviour action. We use pins to denote both, to keep it simple.

An ESM could of course track the number of buffered requests in explicit states, up to some finite number, but it would quickly grow syntactically very large.

This behaviour is described by the EESM of the Forward block, which, due to space constraints, we do not show.

In addition, there could naturally be a mirror version of the Router 1-n activity, a Router n-1, but this is also a one-to-many activity.

We are aware that the TLA + specification for the given example can be optimized by only storing the aggregate number of tokens having passed through a pin on any of the responders in a server. However, this optimization would not work if the EESM required two tokens to pass pin reqOut before a token is allowed though pin resIn.