Pierre Genevès
email: pierre.geneves@inria.fr

Nabil Layaïda
email: nabil.layaida@inria.fr

Christine Vanoirbeek
email: christine.vanoirbeek@epfl.ch

XQTC: A Static Type-Checker for XQuery Using Backward Type Inference

Keywords: Web development, Static analysis, XQuery, Debugging Développement web, analyse statique, XQuery, débogage

We present a novel technique and a tool for static type-checking of XQuery programs. The tool looks for errors in the program by jointly analyzing the source code of the program, input and output schemas that respectively describe the sets of documents admissible as input and as output of the program. The crux and the novelty of our results reside in the joint use of backward type inference and a two-way logic to represent inferred tree type portions. This allowed us to design and implement a type-checker for XQuery which is more precise and supports a larger XQuery fragment compared to the approaches previously proposed in the literature; in particular compared to the only few actually implemented static type-checkers such as the one in Galax [6]. The whole system uses compilers and a satisfiability solver for deciding containment for two-way regular tree expressions. Our tool takes an XQuery program and two schemas S in and S out as input. If the program is found incorrect, then it automatically generates a counter-example valid w.r.t. S in and such that the program produces an invalid output w.r.t S out . This counter-example can be used by the programmer to fix the program.

Introduction

One of the most essential tasks in web engineering consists in extracting and then transforming data for generating output (for display or for further processing). Since the inception of XML, dedicated programming languages such as XSLT and XQuery were designed specifically to deal with such transformations. Several research papers have studied the properties of these languages in order to better understand the difficulty they introduce and to master their inherent complexity. In particular, the problem of finding errors statically is of primary importance. Errors can be easily introduced because transformations involve complex information extraction via powerful query languages such as XPath combined with imperative style statements (the so-called FLWOR expressions) containing instructions such as conditionals, loops, etc. combined with data producing instructions. Furthermore, data given as input or expected as output may additionally be constrained by some type (schema). This makes errors even harder to detect since types are specified independently and provided externally to the program. This led W3C, the standard body in charge of defining the XQuery language [START_REF] Boag | XQuery 1.0: An XML query language[END_REF], to include a type system in the specification [START_REF] Draper | XQuery 1.0 and XPath 2.0 formal semantics[END_REF]. This type system allows type information to be effectively propagated to corresponding instructions in the program with the aim of detecting errors at compile time. The ultimate benefit of such analysis is to avoid unexpected runtime errors by proving statically that the program is correct for all input documents. This has performance implications since programs proved correct do not need to validate their output dynamically. The process of detecting errors at compile-time, known as static type checking, typically involves two main operations: type inference and type containment test. The containment test consists in checking that the program produces an XML output which is consistent with the expected output type when applied to a document which is valid with respect to the input type. This is done by comparing the inferred type with the expected type. Effective algorithms for testing containment between types have been developed in the literature [START_REF] Hosoya | Regular expression types for XML[END_REF]. They are typically based on tree automata containment, and they proved effective in practice. Type inference is often tricky for expressive languages and constitutes the central problem in type checking transformations.

Forward Type Inference and its Limitations

The vast majority of works in the literature perform forward type inference. Forward type inference consists in calculating the type describing the actual program output, based on the analysis of the program and the input type. This analysis consists in applying typing rules repeatedly to each program statement and combining the results so that the analysis of the entire program yields a single and global inferred output type. This approach is intuitive since the program produces its output in a top-down fashion, and grammars also describe constraints in a top-down forward-only fashion with respect to the parent-child relationship. However, this approach has some fundamental and intrinsic limitations. Notably, one revealing limitation is the lack of support for backward XPath axes. This is a fundamental limitation because the typical forward inference process navigates in the input tree grammar, using child or descendant axes in order to infer an output type. This navigation in a type is possible (and relatively easy) since tree grammars descriptions are forward-only. However, navigating backward in a tree grammar is very difficult to achieve and to model because there is no guarantee that the target nodes correspond to non-terminals of the (forward-only) grammar. This is why forward type inference is intrinsically tied to forward XPath axes.

Lack of support of backward XPath axes. Backward XPath axes such as parent or ancestor are commonly used in XQuery programs found in practice. Even more remarkably, frequent patterns such as child::a[position()=1] (used to pick the first element in a sequence) happen to be syntactic sugars for expressions involving backward axes. For example, the above pattern is a shorthand for: child::a[not(preceding-sibling::a)].

More generally, this lack of support is unfortunate since one of the main arguments in favor of using languages such as XQuery (or XSLT 1 ) concerns their ability to rely on the full power of XPath, which constitutes the essential core around which those languages are built.

Concretely, current type systems abstract over backward axes by inferring the type "any" (no constraint at all) as soon as a backward axis such as parent or preceding-sibling is found in the program. This gross approximation leads to unsound type-checkers in the context of forward type inference. This is because the inferred type is much less constrained than it would need to be. Therefore, the final containment check between the inferred type and the expected type will more likely fail. An important consequence is that type-checkers based on this approach will report many false errors for correct programs. Reporting false negatives is problematic because of the useless time spent in debugging a correct program.

Backward Type Inference and its Advantages

In this paper we propose another, fundamentally different approach based on backward type inference. Backward type inference consists in inferring the input type modeling the set of admissible input documents so that the program generates a valid output. For this purpose, the analysis uses the program and an expected type as output. Once the inferred input type is obtained, a containment check is performed to test whether this inferred type is included in the input type for documents actually given as input to the program. We claim that this approach offers several decisive advantages that we briefly review below.

Inferring exact constraints for the for loop. One of the main advantages concerns the typing of a problematic XQuery statement: the "for $v in e 1 return e 2 " loop. In the context of forward type inference, typing precisely the for loop amounts to inferring information on how many times the return part e 2 will be executed. The W3C type system, designed to have a polynomial complexity, infers an approximate type.

For example, consider for $v in $db desc::n return $v where the input type and the expected output type are both b, c, b * . The W3C type inference yields (b | c) * . As highlighted by Colazzo and Sartiani [START_REF] Colazzo | Precision and complexity of XQuery type inference[END_REF], this is a gross approximation which is obviously not contained in b, c, b * . The type-checker will thus raise an error while the program is perfectly correct. Colazzo and Sartiani go further and propose another type-system, designed to be more precise (for an exponential complexity). Basically, they perform a case analysis on e 1 expression in order to infer some more precise information on how many times the return clause e 2 will be executed. In the same manner, we could recursively perform more sub-decomposition in order to generate even more precise information (at the cost of an even greater complexity). At some point, one has to choose a trade-off between complexity and precision (necessarily approximate).

Backward type inference brings a radically different perspective to solve this problem. It allows to completely overcome this difficulty by reading the output type and basically copying selected portions of the output type to the inferred input type. A major advantage of looking at the for loop the other way around is that it permits to completely avoid approximation. Using backward type inference, we can type the for loop in an exact manner without any additional cost. For the above example, b, c, b * is directly (and linearly) inferred as input. 1 XSLT can be compiled into XQuery [START_REF] Fokoue | Compiling XSLT 2.0 into XQuery 1.0[END_REF].

Inria

Supporting backward navigation. Another decisive advantage of our approach is that we can infer all structural constraints induced by backward and recursive navigation, and transfer them precisely in the inferred input type. This is a crucial part of our contribution, further explained in Sections 3.3 and 3.2.

Sound type-checkers even with approximation. In both forward and backward type inferences, obviously at some point, one has to choose a trade-off between precision and complexity. However, this choice has a fundamentally different price in each technique. Backward type inference offers a decisive advantage here: an approximation in the inference process will always preserve containment and therefore soundness, unlike in the forward type inference approach. Approximations in the forward type inference introduce false negatives (as in the example above). The less precise is the inferred output type, the greater is the number of false negatives reported. In contrast, approximation in the backward type inference case lead to less errors detected but all of those reported will be real ones. Therefore, we believe that performance/precision trade-offs are much more relevant in the backward type inference.

Contribution

The contribution of our paper is threefold:

• we propose the joint use of backward type inference and a two-way logic as the best technique for the static type-checking of XQuery;

• we present the first algorithm and tool that implement this approach;

• we obtain more precision in type-checking than in previous approaches and we support a larger fragment of XQuery (notably we are the first to provide the support of backward XPath axes);

The crux of our results relies on the use of a two-way logic to represent inferred tree type portions during the process of backward type inference. This logic provides a succinct notation for regular tree types containing constraints expressed in both upward and downward directions.

Programming with XQuery

Consider the following XQuery sample program: This program operates on an instance of a catalog of products whose type is defined by the XML schema given in Figure 1. This type corresponds to a set of products containing Book and CD elements. The program aims at generating an XML data flow, corresponding to a catalog of products containing only CompactDisc information. The program output is expected to be valid against the target XML schema given in Figure 2. At first sight, the program seems correct. First it traverses all CD in the input document ranged over $cd (line 2). For each of them, it extracts its ProductNo information using a backward navigation to the Product element (line 4). However, a careful analysis shows that this simple example contains two errors: i) it generates an unexpected element (Sleeve) and ii) the order of elements do not conform to the targeted schema. The goal of the present paper is to detect this kind of errors automatically.

XQuery Programs

The XQuery fragment we consider in this paper is given by the abstract syntax shown in Figure 3, where axis ∈ {child, desc, parent, anc, psibl, nsibl}. This fragment is equipped with the main control statements (for loops, conditionals, let binders) as well as backward, forward and recursive navigation performed by XPath expressions.

We distinguish variables ($v ) bound by for loops from variables ($v) bound by let expressions. The former are bound to non-empty trees, whereas the latter are bound to arbitrary (and possibly empty) forests.

XQuery Types

As a model for XQuery types, we consider the class of regular tree languages that capture most of the DTDs, XML Schemas, and Relax NG schemas found in practice, with the additional benefit that this class is closed under set-theoretic operations. Furthermore, operations such as containment are decidable.

The usual grammar for XQuery types which is typically considered in the literature is given in Figure 4. This grammar actually defines context-free grammars (for which containment is known to be undecidable). Some additional constraints must be applied on this grammar for it to define regular tree grammars (the typical additional restriction is that every occurrence of a recursive variable must either be guarded or must occur in tail). Furthermore, this grammar contains syntactic sugar (i.e. constructions that can be expressed in terms of others, such as t? = t | ()).

In the present paper, we consider regular tree types from another slightly different (yet equivalent) perspective. We consider the abstract syntax over binary trees, shown in Figure 5. Considering regular tree types through this abstract syntax offers three advantages: first, this grammar already incorporates intrinsically the aforementioned restriction so that it exactly defines regular tree grammars (there is no need for further restriction). Second, this grammar uses fewer constructions which reduces case analyses and in particular the number of inference rules presented in Section 3.3. Third, it makes explicit, through a let binder, recursion which may occur in types. Finally, those advantages come at no cost since unranked trees can be modeled as binary trees without loss of generality, owing to a bijective mapping between unranked and binary trees [START_REF] Genevès | Efficient static analysis of XML paths and types[END_REF].

In the rest of the paper, we rely on the widely known "first-child" and "next-sibling" metaphor [START_REF] Genevès | Efficient static analysis of XML paths and types[END_REF] for navigating unranked trees, and as a mean to represent them in a binary fashion. For example, the type of all forests is represented as follows: 3 Backward Type Inference

let x any = element * {x any , x any } | () in

Main Principles

Formally, our type-checker takes as input:

• a given program e written in the XQuery fragment described in Figure 3;

• a type S in for documents actually given as input to e;

• a type S out for documents expected as output of e.

S in and S out are first compiled into their core representations t in and t out written using the grammar given in Figure 5. The type-checker then applies the inference process to e and t out as described in Section 3.3. This process yields an inferred input type t inf . This type represents the set of all documents admissible as input to e, or in other terms, the set of all documents t such that e(t) is a valid document with respect to t out . We finally check whether:

t in ⊆ t inf (1)
Technically, (1) is checked using the satisfiability-solver introduced in [START_REF] Genevès | Efficient static analysis of XML paths and types[END_REF]. If (1) holds then no error is reported. If (1) does not hold then we generate a counter-example tree illustrating why the program is found incorrect. The counter-example is a sample input document for which e will output a document which is invalid with respect to t out .

Inria

Logical Representation of Inferred Types

The type which is inferred by our process is represented using logical formulas written with the logic of [START_REF] Genevès | Efficient static analysis of XML paths and types[END_REF]. One crucial advantage of this representation is that it allows expressing properties over both ancestors and descendants of a given node. This is necessary to support XPath steps other than child and descendant found in XQuery programs but traditionally ignored in the literature [START_REF] Colazzo | Precision and complexity of XQuery type inference[END_REF]. Other advantages of this representation include the fact that it is expressive enough to support all XQuery types, it is succinct (types are represented as formulas of linear size compared to their regular expression syntax), and the satisfiability problem for a logical formula of size n can be efficiently decided with an optimal 2 O(n) worst-case time complexity bound with the solver of [START_REF] Genevès | Efficient static analysis of XML paths and types[END_REF]. The syntax of the logic in which the inferred type is expressed is defined as follows:

ϕ, ψ ::= formula true | ⊥ false | p | ¬p atomic prop. (negated) | X variable | ϕ ∨ ψ disjunction | ϕ ∧ ψ conjunction | a ϕ | ¬ a existential (negated) | µX.ϕ (least) fixpoint
where a ∈ {1, 2, 1, 2} are programs. Atomic propositions p correspond to labels for tree nodes. Intuitively, the logic allows one to formulate regular properties on trees: the programs "1" and "2" are respectively used to access the first child node and the next sibling node in an unranked tree. For instance, the formula a ∧ 1 (b ∧ 2 c) is satisfied at the root of the tree denoted by the term a(b, c). The logic also features converse programs 1 and 2 that respectively navigate in the opposite direction compared to 1 and 2.

The logic allows expressing recursion through the fixpoint binder. The recursive formula 1 (µX.a ∨ 1 X ∨ 2 X) states the existence of some node labelled with "a" at an arbitrary depth in the subtree. The meaning of the recursive formula µX.b ∨ 2 X is that either the current node is labeled b or some previous sibling of the current node is labeled b.

The interpretation of a logical formula is the set of finite trees such that the formula is satisfied at some tree node. From this perspective, a logical formula can be seen as an alternative representation of a finite tree automaton, or, equivalently a type (XML Schema). The semantics of this logic is intuitively explained through examples in [START_REF] Genevès | Impact of XML schema evolution[END_REF] and formally defined in [START_REF] Genevès | Efficient static analysis of XML paths and types[END_REF].

The Inference Process

The inference process is formalized by inference rules that cover all possible cases of instructions and expected output types. Specifically, we write an inference rule of the form:

rule-name H 1 H 2 ... H i t ←-e, t out
This rule means that, for the XQuery instruction e and for the expected output type t out , the input type t is inferred, provided hypotheses H 1 , H 2 , ... H i are satisfied. t represents a constraint that the input of e must satisfy in order for e to produce an output which satisfies the constraints given by t out . The above rule is named "rule-name".

The inference process is triggered by the application of the rule that applies to the root of the parse tree of the program. The XQuery program is decomposed in terms of subexpressions. The rule that applies at top level recursively calls rules for its sub-expressions. This decomposition of the program expression guides the traversal of the output type. Rule applications produce portions of the inferred type that are assembled in order to compose the final inferred type. Technically, portions are assembled when popping the stack of recursive calls of sub-rules. At the end of the inference process, we obtain a formula ψ. This formula is surrounded by some additional logical operators, as follows:

¬ 1 ∧ ¬ 2 ∧ µZ.ψ ∨ 1 Z ∨ 2 Z
so that it refers to the root of the input tree.

Auxiliary Definitions

We now introduce some auxiliary definitions used in the inference rules. For two node tests n and n we define the predicate: match(n, n

) def = (n = * ∨ n = * ∨ n = n ).
For a given nodetest n the function toF(n) computes a corresponding logical formula as follows: toF(σ) def = σ and toF( * ) def = . We also define ntoF(n, n

) def = toF(n) ∧ toF(n ).
We need some notations in order to deal with types. First, we introduce x as referring to the empty type: let x = () in x . The function θ(x) denotes the type bound to the variable x. For a given variable x, the function f (x) return the logical translation of θ(x), as follows:

f (x) = f (θ(x)) f (element n {x, x}) = toF(n) ∧ next(1, x1) ∧ next(2, x2) f (()) = ⊥ f (t1 | t2) = f (t1) ∨ f (t2) f (let x = t1 in t2) = f rec (t2)
In the last definition, the function f rec (t 2 ) does the same as f (t 2 ) except that it replaces all occurrences of x at top level in t 2 with µX.f rec (t 1 ) where X is a fresh variable, and the other (deeper) occurrences of x in t 2 with X.

We define a function particularly useful for describing the frontier of a type:

next(k, x) = next(k, θ(x)) next(k, t) =    ¬ k if t = () ¬ k ∨ k f (t) if t = () ∧ nullable(t) k f (t) if ¬nullable(t)
We introduce notations for performing substitutions in instructions, and also in types. The notation e 1 $v / e2 denotes the instruction e 1 in which all occurrences of $v are replaced by e 2 .

The notation t -→

x / x denotes the type expression t in which all (sibling) occurrences of x are replaced by x , as follows:

(element n {x1, x2}) -→ x / x = element n {x1, x } if x2 = x element n {x1, x2} otherwise
() -→ x / x = () (t1 | t2) -→ x / x = t1 -→ x / x | t2 -→ x / x (let x1 = t1 in t2) -→ x / x = let x1 = t1 -→ x / x in t2 -→ x / x

Inria

We define the widely used predicate nullable(t) that indicates whether the empty tree may belong to the language associated with some type t:

nullable(element n {x, x}) = false nullable(()) = true nullable(t1 | t2) = nullable(t1) ∨ nullable(t2) nullable(let x = t1 in t2) = nullable(t2)
The function ctoF(cond ) returns the logical translation of the condition cond , computed as follows:

ctoF(cond 1 ∨ cond 2) = ctoF(cond 1) ∨ ctoF(cond 2) ctoF(cond 1 ∧ cond 2) = ctoF(cond 1) ∧ ctoF(cond 2) ctoF(¬cond ) = ¬ctoF(cond ) ctoF(empty($var )) = ¬($var ) ctoF($v = $var ) =
while hasEq(cond ) simply tests whether the condition cond contains an equality test:

hasEq(cond 1 ∨ cond 2) = hasEq(cond 1) ∨ hasEq(cond 2) hasEq(cond 1 ∧ cond 2) = hasEq(cond 1) ∨ hasEq(cond 2) hasEq(¬cond ) = hasEq(cond ) hasEq(empty($var )) = false hasEq($var = $var ) = true
Finally we define the predicate nilable(e) which is true whenever instruction e might not produce anything as output. This predicate is analogous in spirit to nullable(t) but for instructions.

nilable(<σ>{e}</σ>) = false nilable( ) = true nilable(e1, e2) = nilable(e1) ∧ nilable(e2) nilable(for $v in e1 return e2) = nilable(e1) ∨ nilable(e) nilable(let $v := e1 return e2) = nilable(e ) nilable(if cond then e1 else e2) = nilable(e1) ∨ nilable(e2) nilable($v axis::n) = true nilable($var ) = Γ($var ) nilable(root()) = false

Inference Rules

For each case of instruction e, and each case of expected output type t out , we define a rule that infers a logical formula ϕ in that represents the set of acceptable input to e so that e generates something valid with respect to t out . The purpose of the inferred ϕ in is to represent all admissible inputs to e yet being the most constrained as possible. The more constrained ϕ in is, the more precise the type-checking algorithm will be.

One rule (or group of rules) is associated with each possible construct of the output type which can be: choice, recursion, empty sequence or element type (as defined by the grammar shown in Figure 5).

Choice and Recursion

The easiest constructs to deal with are choice types and recursive types, respectively treated by the rules expr-union and expr-rec in Figure 6. expr-union can be interpreted as follows: for e to generate something valid w.r.t. (t 1 | t 2 ), e can either generate something valid w.r.t t 1 or something valid w.r.t t 2 . The constraint inferred for the input simply requires that at least one of those two situations is satisfied, which is naturally formalized as a logical disjunction. The rule expr-rec simply propagates the analysis to the returned part of the let construct, provided that the type bound to the variable can be accessed using θ(x).

Empty Sequence

The case of the empty sequence as output type is treated by rules shown in Figure 7. One rule is given for each instruction as the inferred constraint depends on the nature of the instruction. For example, elem-empty infers the formula ⊥ (or, in other terms, the empty type) because the generation of an element cannot produce an empty sequence. On the opposite, empty-empty infers the formula (the type of any tree, or in other terms, no particular type constraint), since the empty instruction never generates anything, which matches the empty sequence expected as output. The rule child-empty handles the case where the construct "$v child::n" is supposed to generate an empty sequence: it infers the constraint that $v must not have any child matching n. Other rules follow the same spiritand are not detailed here for space limitations reasons.

Element Type

For the general case where an element type is expected as output, each instruction is dealt with by a few specifically designed inference rules. The inferred constraint varies a lot depending on the nature of the instruction and on the situation determined by the rule premises. Figures 8 and9 presents rules for all the main control statements, including the for loop, the if statement, and instructions in charge of output production. We comment on these rules below.

Generation of nodes. One of the simplest yet essential rule is elem-elem. This rule checks whether the node generated by the instruction is compatible with the expected node label of the output type. In addition, since the XQuery instruction produces a tree (and not a forest) the output type for siblings of the produced node must be nullable. Otherwise, elem-elem' infers the formula ⊥ in order to indicate the problem. empty-elem always infers ⊥ since the empty instruction (modeling no instruction at all) is simply not capable of generating the expected output type that requires the existence of at least one element.

Inria elem-empty ⊥ ←-<σ>{e}</σ>, ()

empty-empty ←-, () seq-empty t1 ←-e1, () t2 ←-e2, () t1 ∧ t2 ←-e1, e2, ()
for-empty t1 ←-e1, θ(xany) t2 ←-e2, () Conditional statements. The case of the "if" statement is especially interesting as it clearly illustrates to which extent the precision of the type-checker can be increased depending on the expressive power of the underlying logic. The rule if-elem applies whenever the condition does not contain any equality test. In this case, the logic is expressive enough to fully model the conditional statement: the rule infers two possible cases: either the input logically follows the restrictions expressed by the condition in which case the additional restrictions computed by the analysis of the "then" branch apply; or the input does not logically follow the restrictions computed from the analysis of the condition in which case the further restrictions computed by the analysis of the "else" branch apply. This complete logical modeling of the "if" statement cannot be achieved if the condition contains an equality test, because we do not know the result of the test statically (as it depends on values obtained at runtime). Rule if-elem' is in charge of this case: an equality test is modeled with the logical formula which abstracts over this part of the condition by not requiring any restriction on the input. Because of this unavoidable approximation, the global inferred formula is the conjunction of the approximation of the condition with one of the two possibilities obtained by the further analyses of the "then" and "else" branches.

¬t1 ∨ t2 $v /t 1 ←-for $v in e1 return e2, () let-empty t1 ←-e1, θ(xany) t2 ←-e2, () t2 $v /t 1 ←-let $v := e1 return e2, () if-empty t1 ←-e1, () t2 ←-e2, () t1 ∨ t2 ←-if cond then e1 else e2, () child-empty ϕ = 1 µX.toF(n) ∨ 2 X $v ∧ ¬ϕ ←-$v child::n, ( )
desc-empty ϕ = 1 µX.toF(n) ∨ 1 X ∨ 2 X $v ∧ ¬ϕ ←-$v desc::n, () parent-empty ϕ = µX. 1 toF(n) ∨ 2 X $v ∧ ¬ϕ ←-$v parent::n, () anc-empty ϕ = µX. 1 toF(n) ∨ 1 X ∨ 2 X $v ∧ ¬ϕ ←-$v anc::n, () psibl-empty ϕ = 2 µX.toF(n) ∨ 2 X $v ∧ ¬ϕ ←-$v psibl::n, () nsibl-empty ϕ = 2 µX.toF(n) ∨ 2 X $v ∧ ¬ϕ ←-$v nsibl::n, () root-empty ⊥ ←-root(), () var-empty ⊥ ←-$v , () var-empty' $v ←-$v, ()
Sequence of instructions. The case of a sequence of instructions e 1 , e 2 is especially hard to deal with as we have to determine which part of the output type is generated by e 1 and which part is generated by e 2 . This means that we have to perform a joint analysis of (e 1 , e 2 ) and elem-elem

(n = * ∨ n = σ) t ←-e, θ(x1) nullable(θ(x2)) t ←-<σ>{e}</σ>, element n {x1, x2} elem-elem' (n = * ∧ n = σ) ∨ ¬nullable(θ(x2)) ⊥ ←-<σ>{e}</σ>, element n {x1, x2} empty-elem ⊥ ←-, element n {x1, x2} seq-elem succ (e1, element n {x1, x2}) = ∅ ⊥ ←-(e1, e2), element n {x1, x2} seq-elem' S = succ (e1, element n {x1, x2}) S = ∅ ∀s ∈ S, x ∈ succ (e2, θ(s)) ⊥ ←-(e1, e2), element n {x1, x2} seq-elem" S = succ (e1, element n {x1, x2}) S = ∅ F = {s ∈ S | x ∈ succ (e2, θ(s))} ϕ = s∈F t s 1 ∧ t s 2 t s 1 ←-e1, (element n {x1, x2}) -→ s /x t s 2 ←-e2, θ(s) ϕ ←-(e1, e2), element n {x1, x2} for-elem ϕ = $v ∧ 1 f (element n {x1, x2}) ϕ ←-for $v in $v child:: * return $v , element n {x1, x2} for-elem' ϕ = $v ∧ 2 f (element n {x1, x2}) ϕ ←-for $v in $v nsibl:: * return $v , element n {x1, x2} for-elem" x ∈ succ (for $v in e1 return e2, element n {x1, x2}) S = succ (e2, element n {x1, x2}) t1 ←-e1, θ(xany) t first 2 ←-e2, element n {x1, x2} t2 = t first 2 ∧ s∈S buildc(s, e2, ∅) ¬t1 ∨ t2 $v /t 1 ←-for $v in e1 return e2, element n {x1, x2} for-elem" ' x ∈ succ (for $v in e1 return e2, element n {x1, x2}) ⊥ ←-for $v in e1 return e2, element n {x1, x2} let-elem t1 ←-e1, θ(xany) t2 ←-e2, element n {x1, x2} t2 $v /t 1 ←-let $v := e1 return e2, element n {x1, x2}
Figure 8: Rules for the main control instructions in the presence of the element type as output. the output type in order to determine at which location the output type can be split in two parts respectively generated by e 1 and e 2 . For this purpose, we introduce an auxiliary function succ (e, t) defined in Figure 10 . For a given instruction e and output type t, the function succ (e, t) computes all the possible remaining parts of the output type after removing all the possible parts that can be generated by e. This is represented using a set of type variables.

Inria if-elem ¬hasEq(cond ) c = ctoF(cond ) t1 ←-e1, element n {x1, x2} t2 ←-e2, element n {x1, x2} (c ∧ t1) ∨ (¬c ∧ t2) ←-if cond then e1 else e2, element n {x1, x2} if-elem' hasEq(cond ) c = ctoF(cond ) t1 ←-e1, element n {x1, x2} t2 ←-e2, element n {x1, x2} c ∧ (t1 ∨ t2) ←-if cond then e1 else e2, element n {x1, x2} root-elem ϕ = toF(n) ∧ ¬ 1 ∧ ¬ 2 ∧ next(1, x1) nullable(θ(x2)) ϕ ←-root(), element n {x1, x2} root-elem' ¬nullable(θ(x2)) ⊥ ←-root(), element n {x1, x2} var-elem nullable(θ(x2)) ϕ = toF(n) ∧ next(1, x1) ϕ ←-$v , element n {x1, x2} var-elem' ¬nullable(θ(x2)) ⊥ ←-$v , element n {x1, x2} var-elem" ϕ = toF(n) ∧ next(1, x1) ∧ next(2, x2) $v ∧ ϕ ←-$v, element n {x1, x2}
Intuitively, if we consider the case of a sequence e 1 , e 2 , succ (e 1 , t) returns the set of variables to be considered as possible entrypoints for e 2 . In other terms, succ (e 1 , t) represents the set of all possible places where t can be split in two parts: the first being generated by e 1 and the second by e 2 . The definition of succ (e, t) is presented in Figure 10 where t is used as a shorthand for element n {x 1 , x 2 } and where axis ∈ {child, desc, parent, anc, psibl, nsibl}. By default, succ (e, t) = ∅ for any pair (e, t) that has already been visited (so that the recursion stops).

By definition, if x ∈ succ (e, t) then e can produce an output that matches the entire output type t. If x ∈ succ (e, t) then the output type is expecting something else (a mandatory remaining part) that cannot be generated by e. Finally, succ (e, t) = ∅ means that e generates a pattern which is not acceptable for t.

Using this auxiliary function, we design the backward type inference rules seq-elem, seqelem' and seq-elem" for the sequence of instructions. seq-elem eliminates the cases where e 1 generates a pattern which is not compatible with the output type. seq-elem' eliminates the cases where e 1 does generate a pattern compatible with the output type, but e 2 does not. Finally, seq-elem" computes the set S of all admissible entrypoints for e 2 . The set F filters out entrypoints for which e 2 cannot fully generate the expected remaining part of the type. F contains the admissible entrypoints for e 2 so that e 1 , e 2 successfully generates an output which fully satisfies the entire expected output type. The inferred formula ϕ simply describes all acceptable splits of the output type so that e 1 , e 2 generates an output valid with respect to the output type.

Iteration and variable-binding. To better understand the case of the for loop and backward type inference performed by for-elem, recall that the semantics of the "for $v in e 1 return e 2 " statement consists in first evaluating instruction e 1 , and then in iterating over each member of the sequence obtained by the result of the evaluation of e 1 . Iteration is done by successively setting variable $v to each member of this sequence and executing e 2 each time accordingly. Obviously, e 2 may contain one (or possibly several) occurrences of $v . For this reason, backward inference for the for loop is intrinsically tied to backward inference for variables in navigation steps, and the behavior of for-elem must be understood together with the behavior of rules that deal with step-related variables, and in particular rules of Figure 11. Whenever a variable occurrence is encountered inside e 2 , a rule (e.g. child-elem) associates the expected output type to this variable by inferring a logical formula that represents the expected output type and that contains the name $v of the variable which is meant as a placeholder. This placeholder will be replaced at a later stage whenever the inference process will come back to the for loop that binds this variable (recall that the inference process is a depth-first tree traversal of the XQuery instruction parse tree). Rule for-elem" replaces all occurrences of $v in t 2 with the result t 1 of the analysis of the instruction e 1 bound to $v by the for loop. In this manner, constraints on $v coming from the output type, propagated by the rules in charge of steps, will properly apply later when the binding of $v is met.

Three rules handle the case of the for loop: for-elem, for-elem', for-elem". The rules for-elem and for-elem' handle peculiar cases where the inference simply consists in copying a portion of the output type into the inferred input type. The rule for-elem" is in charge of the more general remaining cases. Here, the principle is very similar to the one followed for the sequence (rule seq-elem"). This is because a statement for $v in e 1 return e 2 can be theoretically seen as an unbounded sequence of the form e 2 , e 2 , ..., e 2 . This is exactly what is done by the rule for-elem". For this purpose, we define an auxiliary predicate buildc(x , e, E) as follows: buildc(x , e, E)

def = buildc(s, e, E) def = t ∧ x∈S,x ∈E buildc(s, e, E ∪ {s}) if S = ∅ ⊥ if S = ∅ for s = x
where t ←-e, θ(s) and S = succ (e, θ(s)).

The general idea is that a successful path between an entry point for e 2 and x must exist. Basically the expected output type must be "consumed" entirely after a certain number of application of e 2 .

Finally, notice that the rule var-elem' raises an error whenever some next siblings are required in the output type, because they cannot be generated by $v which is bound to a single tree, by definition of for variables. var-elem" is in charge of let variables that can be bound to forests and which are simply substituted by rule let-elem.

Navigation in the input tree. Figure 11 presents rules that deal with all the instructions that perform navigation in the input tree. Most of the rules use the hypothesis H sibl that checks the compatibility of the expected output type with the nodes returned by the step:

H sibl def = sat(next(2, x 2 ) ∧ ϕ restrictSiblings (toF(n)))
Inria where the predicate sat(ψ) checks whether a given formula ψ is satisfiable, using a direct call to the solver of [START_REF] Genevès | Efficient static analysis of XML paths and types[END_REF]. In the above definition, ϕ restrictSiblings (ψ) ensures that all next siblings satisfy ψ, and is defined as follows:

ϕ restrictSiblings (ψ) def = ¬ 2 ∨ 2 µX.ψ ∧ (¬ 2 ∨ 2 X)
Notice that checking the hypothesis H sibl is facultative but increases precision.

Termination of the Algorithm

Proposition 3.1 The inference process terminates for any instruction e and output type t.

Proof (sketch): The inference process terminates because each inference rule recursively calls other rules on instructions whose sizes are strictly smaller compared to the size of the initial instruction. Therefore, the bounded size of the XQuery program parse tree guarantees termination of the inference process. The only exception are rules expr-union and expr-rec, which recursively call other rules on same-size instructions, but with output types whose sizes are strictly decreased. This guarantees termination even in the presence of recursion in the output type (due to the guarded recursion restriction). Specifically, in the presence of recursion in the output type, a rule xxx-elem will eventually apply in order to reach the recursive occurrence of a type variable. By examining all the xxx-elem rules (shown in Figures 8,9 and 11) we can see that each rule either performs a recursive call on an instruction whose size is decreased, or terminates directly (without any recursive call).

The next section notably details step by step how the implementation processes an example involving recursion in the output type.

Practical Experiments

Implementation Architecture

The whole system is implemented in Java and is obtained by the implementation and then the assembly of several components. First, we rely on a parser for XQuery expressions (we use JJTree to generate a basic parser from the XQuery normative grammar specification), and, more importantly an API for representing and manipulating Core XQuery expression parse trees. A set of parsers for DTDs, XML Schemas and Relax NG schemas read schema files and produce a unifying unranked regular tree grammar representation from a description in any of those languages. We use the already available "MSV" parser, and we convert its internal representation in terms of our CFT. At this stage, a converter translates the unranked regular tree grammar into the corresponding binary tree grammar. Using an API for manipulating binary tree grammars, we have implemented a compiler that translates the binary tree grammar in terms of a logical formula. We also use an API to generate and manipulate logical formulas. Using these two APIs we have implemented all the auxiliary predicates needed for the inference rules. Inference rules are implemented using the visitor pattern. The input XQuery expression is traversed, and corresponding rules are called on each subexpression, depending on the nature of the construct of the output type. Rules are directly implemented (as a separate Java class) as described in the present paper: each rule generates a portion of a logical formula, that possibly contains a variable that will be substituted by another piece of formula at a later step when the variable binder is met (when the rules for-xxx or let-xxx apply). The global logical formula is thus obtained by the assembly of its sub-formulas when the stack of recursive calls is emptied. Finally, we rely on the satisfiability solver of [START_REF] Genevès | Efficient static analysis of XML paths and types[END_REF] for checking the unsatisfiability of the negation of the implication between formulas representing the input type and the inferred input type2 .

The implementation of our tool is available from the following URL: http://tyrex.inria.fr/xqtc

Experimental Results and Discussion

We detail how a simple example is processed by the implementation in order to illustrate how the technical machinery works. Consider the program e defined below:

e def = let $v := root() return <r>{$v child:: * }</r>
This program generates a document with a r-labeled root whose children are the children of the root of the input tree. Consider also an output tree type t out defined as follows:

t out def = let x = () in let x = element b {x , x} | () in element r {x, x }
This type represents the set of documents with an r-labeled root which can have an arbitrary number of b children leaves (or, intuitively, r[b * ] for unranked trees). Concretely, the grammar "sample.dtd" describing this type is parsed and converted to a Context Free Type (CFT) matching the syntax given in Figure 4, as shown by the following trace:

Resulting CFT is: $b ->b(()) $1 ->($b | ($b, $1)) $r ->r(($1 | ())) $a ->a($b) Start symbol is $r
This grammar is then automatically converted into the binary tree type representation (matching the syntax shown in Figure 5):

Resulting BTT is: $Epsilon ->EPSILON $2 ->b($Epsilon, $Epsilon) | b($Epsilon, $2) $1 ->EPSILON | b($Epsilon, $Epsilon) | b($Epsilon, $2) $r ->r($1, $Epsilon) Start Symbol is $r
The XQuery program e is parsed, and the analysis is triggered at the root of the above output type:

Analyzing 'sample.xq' vs 'sample.dtd' starting at 'r'... Considered Input XQuery expression: let $v := root() return element r {child::* }

The system prints the tree of all rules that apply for the present example, as shown in the trace presented in Figure 12. The trace notably shows parameters for each intermediate rule called. The name of the applied rule is printed together with its input parameters (instruction and type) whenever the rule is triggered. Whenever the rule returns its result (potentially after calling other rules), the resulting formula corresponding to the inferred input type portion is printed. Indentation in the trace corresponds to the depth in the tree of rule calls. Specifically, the first rule triggered is let-elem of Figure 11, which is instantiated as follows:

The application of this rule recursively calls one rule for building t 1 and one rule for building t 2 . It therefore generates two branches.

For the first branch, since θ(xany) = (element * {xany, xany}) | () is a disjunction at top level, the formula t 1 is obtained by the application of expr-union, which in turn calls root-elem and root-empty. The application of root-empty directly yields the formula ⊥ and therefore only the result root-elem is relevant for the disjunction. This result is obtained as follows:

root-elem ϕ = ¬ 1 ∧ ¬ 2 ∧ next(1, xany) nullable(θ(xany)) ϕ ←-root(), element * {xany, xany}
This rule performs the auxiliary computations:

toF( * ) = , next(1, x any ) = ¬ 1 ∨ 1 f (x any ) which is equivalent to because f (x any ) = µX.(¬ 1 ∨ 1 X) ∧ (¬ 2 ∨ 2 X
) is equivalent to , and nullable(θ(x any )) = true. It then returns the inferred type t 1 = ¬ 1 ∧ ¬ 2 that simply requires the existence of a root in the input tree. For the second branch, the rule expr-rec is applied twice to go through the let statements in t out until the rule elem-elem applies for element r {x, x }. This rule application recursively triggers expr-union for splitting the choice θ(x). Again, two branches are created from the split: one that applies child-empty, which terminates immediately with $v ∧ ¬ 1 , and another one which triggers expr-union and so forth, as illustrated in 12.

If we pop the stack of recursive calls, at (2) we end up with t 1 as computed above and a value for t 2 returned by rule elem-elem, as shown in 12. The final inferred type is then obtained by the substitution t 2 $v / t1 which denotes t 2 where every occurrence of $v (X1 in the implementation trace) is replaced with t 1 . This yields the final formula t inf shown in Figure 13: This inferred formula is surrounded by a formula that ensures its satisfaction at the root of the input tree, before being used in the formula to check containment.

The first part of the formula in Figure 13 states that the root does not have any child (line 1), or the root has a first child labeled "b" (does not have any children) and an immediate sibling which is labeled "b" and do not have any children, as well as all its potential successors (recursion on X2, line 2), or the root has only one first child child labeled "b" without children and no sibling (line 3).

One can easily check that this is exactly the type that represents the set of all admissible input documents for e to generate a valid t out document.

Notice that the final inferred type contains duplicate formulas (it refers to the root three times). This is because rules do not communicate (different branches do not share their results) in the current state of the implementation. However, this duplication of subformulas is not a real issue, because duplicate subformulas are automatically factorized by the satisfiability solver.

Once t inf is computed, type-checking is performed by checking whether t inf ⊆ t in . This is formulated as follows:

phi => ~<-1>T & ~<-2>T & mu X. tinf | <1>X | <2>X
where tinf is the formula shown in Figure 13 and phi is the logical formula corresponding to t in .

For instance, if we instantiate t in as a type allowing one children labeled "a" under the root, then the system produces a counter-example of the form *[a]. Obviously, in realistic scenarios, more rules are triggered, the rule application tree is bigger, and generated formulas are much harder to read. Counter-examples, which are also more complex, become of greater value for the XQuery programmer. In hard cases, this counter-example can be given to a XQuery runtime debugger, for a step-by-step analysis to find the precise locations of the erroneous statement(s) in the program. Notice, that the soundness of our type-checker implies that the XQuery program generates an output which is necessarily not valid (with respect to the expected output type) when fed with the counter-example as input. Contrary to other approaches investigated in the literature that produce false negatives, here the effort spent in debugging is always relevant. Notice also that our type-checker is capable of detecting a wide range of errors, from basic ones to much more involved ones. The class of basic errors detected ranges from very basic ones such as inexistent elements, errors in element names, to wrong ordering in expected content models and generation of an element in inappropriate locations. The type-checker also detects much more subtle errors depending on the expressive power used to describe expected output type constraints. In particular, features such as context-sensitive content models allowed in XML schemas or in Relax NGs are fully captured by our BTT and logical modelings. Therefore the type-checker is equipped to detect errors caused by the generation of an output that matches a possible content model but not in the proper context.

The secret for capturing extremely precise context information is that we are capable of tracking precisely all the context manipulation performed by forward, backward and recursive path expressions. We believe that this removes a major obstacle that prevented the development of precise type-checkers and their widespread use. This is precisely the limitation of existing typecheckers, such as the pioneering Galax [START_REF] Fernández | Building an extensible xquery engine: Experiences with Galax (extended abstract)[END_REF] which is still among the few available implementations today. Galax is typically unable to detect the error induced by the use of the backward axis in the example given in Section 2, because it directly implements the type-system proposed in the XQuery recommendation [START_REF] Draper | XQuery 1.0 and XPath 2.0 formal semantics[END_REF].

Related Work

The closest works in terms of objectives are the ones of W3C [START_REF] Draper | XQuery 1.0 and XPath 2.0 formal semantics[END_REF] and [START_REF] Colazzo | Precision and complexity of XQuery type inference[END_REF]. [START_REF] Draper | XQuery 1.0 and XPath 2.0 formal semantics[END_REF] describes a type system based on forward type inference which is polynomial (except for nested let clauses). Colazzo goes one step further by a thorough analysis of precision and complexity of this typesystem and by introducing his own, more precise (but exponential) type system. Both works suffer from the same limitations inherent to forward type inference, as described in Section 1. The work in [START_REF] Colazzo | Precision and complexity of XQuery type inference[END_REF] fails to capture backward axes: the proposed type system only supports child and desc-or-self axes. Furthermore, it involves a complex decomposition of the "in" clause of the for loop, which can be avoided using backward type inference, without loss of precision. The type-system proposed by the W3C has been inspired by the seminal work found in [START_REF] Hosoya | XDuce: A statically typed XML processing language[END_REF], which is itself based on finite tree automata containment [START_REF] Hosoya | Regular expression types for XML[END_REF]. In the programming languages community, the XML type-checking problem has also been studied for other particular domainspecific languages such as CDuce [START_REF] Benzaken | CDuce: an XML-centric general-purpose language[END_REF], XSLT [START_REF] Kirkegaard | Static analysis of XML transformations in Java[END_REF] or with specific transformers like transducers [START_REF] Maneth | XML type checking with macro tree transducers[END_REF][START_REF] Maneth | Exact XML type checking in polynomial time[END_REF]. For a recent survey of related works on type-checking for XML, see [START_REF] Benzaken | XML typechecking[END_REF] and references thereof.

The closest work in terms of technical machinery and spirit is [START_REF] Tozawa | Towards static type checking for XSLT[END_REF] which develops backward type inference for a fragment of XSLT called XSLT0. This fragment only supports the parentto-child relationship, and its expressive power is incomparable to the much more expressive XQuery fragment we consider here. Furthermore, at the time, the logic proposed in [START_REF] Genevès | Efficient static analysis of XML paths and types[END_REF] on which we develop the present work was not known. This logic is key for an efficient implementation Inria because it avoids the drawbacks of the automata-based approach described in [START_REF] Tozawa | Towards static type checking for XSLT[END_REF]. Specifically, it overcomes the blow-ups due to tree automata complementation.

The concept of backward type inference was first theoretically introduced in [START_REF] Milo | Typechecking for XML transformers[END_REF]. They propose a theoretical framework based on k-pebble tree transducers, which is a output-tree producing version of finite tree automata. They show that the type inferred as input is definable in MSO (monadic-second order logic). In other terms, there exists a monadic-second order logic formula that describes the input type. Unfortunately, their method relies on a conversion from MSO to finite tree automata which requires non-elementary time complexity, that is, the time complexity is not bound by any fixed number of composition of exponentials. As a result, while this is an interesting theoretical result, this makes any direct implementation out of reach. Similar approaches have been proposed in [START_REF] Inaba | Multi-return macro tree transducers[END_REF][START_REF] Maneth | Exact XML type checking in polynomial time[END_REF].

Conclusion

We proposed a backward type inference algorithm and a type-checking method for XQuery programs. The XQuery fragment we consider is equipped with the main control statements (for loops, conditionals, let binders) as well as backward, forward and recursive navigation performed by XPath expressions. We also propose a prototype implementation of these techniques. This is a step in the design and development of a new generation of type-checkers for XQuery that: (i) are more precise, (ii) are feasible in practice (implementation is tractable and efficient) and (iii) natively support a larger set of features found in XQuery programs, and in particular backward XPath axes. We believe that we identified the main obstacle in type-checking XQuery, namely the combination of precision and practical feasibility, when the main traits of the XQuery language are considered.

One perspective for further work consists in converting the inferred formula to a XML representation (XML Schema). Another perspective for further work consists in implementing the support of attributes and basic types such as string and integer, which can be modeled in the logic using atomic propositions.

Figure 1 :

 1 Figure 1: Input Type for "catalog.xml".

Figure 2 :

 2 Figure 2: Expected Output Type.

Inria

Figure 3 :

 3 Figure 3: Core XQuery Fragment.

Figure 5 :

 5 Figure 5: Types (desugarized and binarized).

  expr-union t l ←-e, t1 tr ←-e, t2 t l ∨ tr ←-e, (t1 | t2) expr-rec t ←-e, t2 t ←-e, let x = t1 in t2

Figure 6 :

 6 Figure 6: Rules for choice and recursive types.

Figure 7 :

 7 Figure 7: Rules for the empty sequence as output.

Figure 9 :

 9 Figure 9: Rules for conditionals, variables and the root instruction in the presence of the element type as output.

  let-elemt1 ←root(), θ(xany) t2 ←-<r>{$v child:: * }</r>, tout t2 $v /t 1 ←let $v := root() return <r>{$v child:: * }</r>, tout

  succ (e, t1 | t2) = succ (e, t1) ∪ succ (e, t2) succ (e, let x = t1 in t2) = succ (e, t2)succ (<σ>{e}</σ>, ()) = ∅ succ ( , ()) = {x } succ (e1, e2, ()) = {x } if nilable(e1) ∧ nilable(e2) ∅ otherwise succ (for $v in e1 return e2, ()) = succ (e2, ()) succ (let $v := e1 return e2, ()) = succ (e2, ()) succ (if cond then e1 else e2, ()) = succ (e1, ()) ∪ succ (e2, ()) succ ($v axis::n, ()) = {x } succ ($var , ()) = {x } succ (root(), ()) = ∅ succ (<σ>{e}</σ>, t) = {x2} if match(σ, n) ∅ otherwise succ ( , t) = ∅ succ ((e1, e2), t) = x∈succ(e 1 ,t) succ (e2, θ(x)) if ¬nilable(e1)x∈succ(e 1 ,t) succ (e2, θ(x)) ∪ succ (e2, t) otherwise succ (let $v := e1 return e2, t) = succ (e2, t)succ (if cond then e1 else e2, t) = succ (e1, t1) ∪ succ (e2, t2) succ (for $v in e1 return e2, t) = k i=1 succ e i ,t such that k+1 i=1 succ e i , t = k i=1 succ e i , t where e def = e2 succ (root(), t) = {x2} succ $v axis::n , t = ∅ if ¬match(n , n) {x2} ∪ succ ($v axis::n , θ(x2)) if match(n , n) succ ($var , t) = Γ($var )

Figure 10 :

 10 Figure 10: Computation of the set of variables reached in type t after output production by e.

  x any

	u ::=		unit type
		element n {t}	element
	n ::=		name test
		σ	label
	|	*	wildcard
	t ::=		type
		u	unit type
	|	()	empty sequence
	|	t, t	sequence
	|	t | t	choice
	|	t?	optional
	|	t+	one or more
	|	t *	zero or more
	|	x	type reference

Figure 4: XQuery Types (with syntactic sugar).

n ::= name test σ label | * wildcard t ::= type element n {x, x} element with type references | () empty sequence | t | t choice | let x = t in t recursive type

RR n°8149

Checking containment A ⊆ B corresponds to checking the logical implication A ⇒ B. Since we use a satisfiability checker (and not a validity checker), this property is checked by testing the unsatisfiability of A ⇒ B = ¬A ∨ B, that is, the satisfiability of ¬(A ⇒ B) = A ∧ ¬B.Inria

Inferred input type represented as a formula:


Antoine Bautin

Olivier Simonin

François Charpillet

Franc ¸ois Charpillet

A Novel Frontier Allocation Algorithm for Multi-robot Exploration

Keywords: frontier-based exploration, multi-robot exploration, coordinated multirobot exploration, potential field, gradient methods, multi-robot task allocation, distributed robot systems

published or not. The documents may come   L'archive ouverte pluridisciplinaire

Introduction

Exploration of unknown environments by autonomous mobile robots can be necessary in many real world situations, typically for areas where human access is difficult or hazardous. In exploration tasks, multiple robots systems are advantageous because, using an efficient coordination strategy, they are more accurate and/or faster to explore the environment than single robot systems [START_REF] Stachniss | Exploration and Mapping with Mobile Robots[END_REF]. Furthermore, multi-robot systems using a distributed algorithm are robust to failures, flexible and scalable [START_REF] Bennet | Distributed control of multi-robot systems using bifurcating potential fields[END_REF]. Nevertheless collectively building a map with a team of robots also raises up some difficulties. Finding a good navigation strategy for each robot is not straightforward as the exploration policy of one robot strongly depends on the exploration policy of others. Another issue is the computational capabilities of the robots that are often limited when using multiple robots. Finally, in some cases, robots can negatively interact with each other, inducing blockage or avoidance maneuvers.

This work aims at providing an efficient method for assigning to each robot areas to visit within the environment in order to minimize the amount of time required to fully explore it. Frontiers are the boundaries between unexplored and explored empty/accessible areas. A robot "exploring a frontier" (moving towards a frontier) discovers new areas to add to the map and new frontiers. When complete exploration is the objective, every frontiers should be explored. In this paper, we show that a good heuristic is for each robot to go toward the frontier having fewer robots in its direction.

The main contribution of this paper is a novel algorithm for the robot-frontier assignment problem. Each robot is assigned to the frontier for which it is in the best position i.e. the frontier where there is the fewest robots between the frontier and the robot to be assigned (in travel distance). Experimental results in simulation show that this algorithm gives significantly better results than a nearest frontier assignment and similar or better results to a greedy assignment while having a lower computation complexity. Cooperation is achieved by the robots sharing their location coordinates and the information gathered about the environment.

This paper is structered as follows. Section 2, next, defines the problem before introducing the notations used throughout the paper. Section 3 reviews the existing literature on the multi-robot exploration problem. Section 4 describes our exploration strategy. Finally, in section 5, we compare the performance of our algorithm with previously proposed algorithms by simulation in various environments, then we present first experimental results with real robots.

Problem statement

The following presents the notations used and states formally the problem addressed. The fleet of robots is assumed to be homogeneous (identical robots) and equipped with exteroceptive sensors allowing them to build a map. To limit the scope of the problem, robot localization and mapping are not presented in this paper. It can either be done using an external localization system or by having the robots work with a common reference frame and using one of the Simultaneous Localization and Mapping (SLAM) algorithms in the literature (e.g. [START_REF] Thrun | Multi-robot slam with sparse extended information filers[END_REF], [START_REF] Howard | Multi-robot Simultaneous Localization and Mapping using Particle Filters[END_REF]). Communication is critical for cooperation, therefore we use a wireless communication network (WiFi) which covers the full area to be explored by the robots. Exactly one frontier is assigned per robot for 2 reasons. First, a robot exploring a frontier generally pushes it back and fits the best for exploring that frontier, therefore it is unavailable to explore another frontier. Second, robots should not be left standing still if no frontier is available to them because other robots exploring frontiers are likely to discover new ones and require support to explore them.

Notations

-R the set of robots, R : {R 1 ...R n } with n = |R| the total number of robots -F the set of frontiers, F : {F 1 ...F m } with m = |F| the number of frontiers -C a cost matrix with C ij the cost associated with assigning robot R i to frontier F j -A an assignment matrix with α ij ∈ [0, 1] computed as follows :

α ij = 1 if robot R i is assigned to F j 0 otherwise
The main objective is to minimize the overall exploration time. As the problem is dynamic -robots discovering an unknown environment -it is difficult to evaluate the final exploration duration during the system execution. Indeed, when selecting among different allocations, the impact of a given assignment on the global system performance is not known because no information about what is behind the frontiers is available. Consequently, optimization has to reevaluated at each time step or at least every time the robot observes the targeted frontier. The time for all assigned frontiers to be explored is determined by the maximum exploration time among all frontiers. The optimization criteria is therefore the minimization of the maximum cost :

C max (A) = max ∀i m j=1 α ij C ij (1)
The challenge of the frontier allocation lies in the number of possible assignments being equal to the number of permutations i.e. sequences without repetition. Therefore, in the best and most common case when n ≤ m, it is equal to m! (m-n)! . When n > m it becomes even greater. These figures make the search for the optimal assignment intractable for large teams of robots and an approximation is therefore necessary.

State of the art

In this section, we review previously proposed methods on multi-robot exploration strategies. These methods can be classified by their coordination method. First, implicit coordination that do not use communication for coordination. Then, the approaches which use communication to a central agent allocating an area to each robot or a decentralized decision making system.

Implicit coordination : nearest frontier

In 1997, Yamauchi introduced the very popular frontier-based exploration algorithm for single robot [START_REF] Yamauchi | A frontier-based approach for autonomous exploration[END_REF]. He first referred to frontiers as the border between known free space and an unexplored area. A robot moving towards a frontier will therefore sense new areas of the map. Repeating this operation increases the size of explored environment until the entire environment is explored: when no frontiers are left. In its multi-robot extension [START_REF] Yamauchi | Frontier-based exploration using multiple robots[END_REF] (see algorithm 1), robots share the gathered information so that they build a similar map resulting in a similar list of frontiers. Each robot moves towards its nearest frontier, makes an observation and broadcasts its results. This cooperatively built map is enough to achieve some coordination: when a frontier is explored by one robot, the information acquired is shared with the other active robots and the frontier will not be explored again by another robot. Coordination is said to be implicit because it is achieved only by sharing information gathered on the environment. No communication is necessary to coordinate the robots. This method is asynchronous, distributed and robust to robot failures.

This pioneering work put in evidence the central issue of assigning frontiers to each robot because, using this approach, several robots can be assigned to the same frontier not taking advantage of their number to explore different areas. Figure 1(a) illustrates a situation where two robots are assigned to the same frontier, leaving unexplored areas without robots (lines show the assigned robot-frontier pairs).

Input: R i , C i Cost Vector of R i Output: α ij assignment of robot R i to frontier F j begin α ij = 1 with j = argmin ∀F j∈F C ij end 3.

Coordination through communication : greedy assignment

Greedy algorithms are commonly used for task allocation and the frontier assignment problem is a task allocation problem. At each iteration of the allocation loop, the robotfrontier pair with lowest cost is selected, the robot is assigned to the frontier, and both are removed from their respective list. This is repeated until all robots have an assigned frontier. The standard way of applying this greedy algorithm is centralized and synchronous. A centralizer assigns a frontier to each robot, robots travel to their frontier, share the information collected on the environment and wait for a new assignment. The centralizer can wait for all robots to arrive at their frontier to assign the new set of frontiers (synchronous) or whenever a robot reaches its frontier (asynchronous). For a fair comparison between algorithms a decentralized and asynchronous version of the greedy allocation algorithm is given in Algorithm 2. Each robot computes the allocation of the other robots until it finds its assignment. Because robots have the same information about the environment including other robots locations, a robot can assume that the allocation computed for another robot will be the same as the one computed by that robot. An example of a greedy assignment is illustrated on figure 1(b). Due to the robots considering the assignment of other robots, robots are evenly assigned to frontier. However, note that frontier F 0 is not assigned while robots R 2 and R 5 go towards the same zone. Most frontier allocation approaches are greedy based [START_REF] Burgard | Collaborative Exploration of Unknown Environments with Teams of Mobile Robots[END_REF], [START_REF] Simmons | Coordination for multi-robot exploration and mapping[END_REF] [14].

Utility-based vs frontier-based

Utility, proposed by Simmons et al. [START_REF] Simmons | Coordination for multi-robot exploration and mapping[END_REF], refers to the difference or ratio between an estimated information gain and a cost. Evaluating it requires to estimate the expected area discovered from a target location reduced by the overlap in between robot sensed

k, j = argmin C kj ∀R k ∈ R, ∀Fj ∈ F α kj = 1 R = R \ R k , F = F \ Fj IF F = ∅ THEN F = Finit end
areas and the cost of reaching that target. Targets are greedily assigned on utility to robots thus maximizing information gain and minimizing the total cost. Utility-based approaches improves the frontier based approaches (see Burgard et al. [START_REF] Burgard | Coordinated multi-robot exploration[END_REF]) but induces an extra computation load. However, regarding frontier-based approaches, contiguous frontiers cells can be grouped or identified into a unique frontier (Franchi et al. [START_REF] Franchi | The sensor-based random graph method for cooperative robot exploration[END_REF]) thus making their performances close to utility-based approaches. In this case, utility and frontier based approaches avoid sending several robots toward nearby frontier cells.

Centralized vs decentralized systems

In a centralized coordination scheme, one central agent decides which frontier each robot should explore [START_REF] Simmons | Coordination for multi-robot exploration and mapping[END_REF]. Centralized coordination scheme represents a single point of failure and requires an additional computation and communication cost. In order to be decentralized, the utility based method was extended by Zlot et al. [START_REF] Zlot | Multi-robot exploration controlled by a market economy[END_REF] by using a market based approach where robots bid on targets, thus negotiating their assignments. Existing bidding algorithms for frontier allocation usually work with the same principle as a greedy algorithm. Auctions systems can be centralized [START_REF] Simmons | Coordination for multi-robot exploration and mapping[END_REF], one central agent receives bids from all robots and assigns frontiers to each robot, or decentralized as in [START_REF] Zlot | Multi-robot exploration controlled by a market economy[END_REF] and [START_REF] Chaimowicz | Dynamic role assignment for cooperative robots[END_REF], a robot discovering a frontier is auctioneer for this frontier. These approaches reduce the computation cost by making parallel computations of paths to frontiers and assignments but induce a communication overhead of O(nm) because each robot sends a bid for each frontier.

Proposed approach

Our approach to the frontier allocation problem is based on the distribution of robots among the frontiers. For this purpose, we do not only take into account the distance to frontiers. We consider the notion of position or rank of a robot towards a frontier, by counting how many robots are closer to the frontier. Before detailing the frontier allocation algorithm, we present the scheme of robots' behavior and the assumptions on the environnement representation.

Each robot performs repeatedly the four following steps :

1. Frontiers identification and clustering 2. Computation of the distances to frontiers 3. Assignment to a frontier 4. Navigation towards the assigned frontiers for a fixed time period

The map representation used is an Occupancy Grid (OG) [START_REF] Elfes | Using occupancy grids for mobile robot perception and navigation[END_REF] which is a square tessellation of the environment into cells of the desired size, maintaining a probabilistic estimate of their occupancy state. This map is built from the robot perceptions and broadcasted maps of other robot. To reduce the computation cost, robots are assumed to have a circular shape and to be holonomic. The configuration space grid is then computed by enlarging obstacles (including other robots) by the size of the robot. This configuration space grid is then used for frontier identification and path planning.

Steps 1, 2 and 3 are detailed in the next sections.

Frontier identification and clustering

Each robot maintains a list of frontier cells updated with each information received or acquired. To reduce the distance computation step and avoid assigning robots to frontiers cells that will be observed with the same perception, contiguous frontiers cells are grouped. The size of groups of frontiers cells is thresholded with respect to the size of sensing areas.

Distances and path computation

To evaluate robots positions we use, as the other methods, a cost matrix. In order to compute the cost matrix we build a local minimum free artificial potential field from each group of frontier using the wavefront propagation algorithm (WPA) [START_REF] Barraquand | Numerical potential field techniques for robot path planning[END_REF]. From each frontier cells in a group of frontiers, a monotonically increasing potential is built by iteratively propagating a wavefront through unoccupied cells in the Configuration grid. The result of the WPA gives for each cell in the environment the distance to the frontier using the shortest path. Building the cost matrix is then straightforward using the location information of each robot. In comparison, most approaches compute a path from each robot to each frontier (with a A* algorithm). Thus if a robot requires the cost for another robot, it needs to ask it to the other robot or to compute its path. The potential field grids is re-computed periodically, at least every time the robot is close to reaching the frontier, but ideally each time new information is significant enough to modify the configuration grid and could therefore affect the robot assignment.

Frontier Allocation

Frontier assignment is done in a decentralized way i.e. each robot autonomously decides which frontier it will explore next.

Our approach consists in assigning to a robot a frontier for which it is in best position, i.e. the frontier having the less robots closer than itself. Formally, we set P ij the position of a robot R i towards a frontier F j as:

∀R k ∈R, k =i, C kj <Cij
which computes the cardinal of the set of robots closer to the considered frontier than the robot being assigned.

By reasoning on positions instead of distances, two close robots will be assigned on frontiers where they will be in first position whatever the distances, thus favoring a better spatial distribution of robots on frontiers. Figure 2 illustrates such an assignment. Robot R 5 is assigned to frontier F 0 instead of a closer frontier. Indeed robot R 5 is in second position for frontiers F 1 , F 2 and F 3 . This provides a well balanced direction assignment, which was not the case with the greedy approach (see fig 1(b)). The algorithm for assignment, called Minimum Position, is given in Algorithm 3.

α ij assignment of robot R i foreach F j ∈ F do P ij = ∀R k ∈R, k =i, C kj <Cij 1 end α ij = 1 with j = argmin ∀F j∈F P ij

In case of equality choose the minimum cost among min P ij

Wavefront propagation stopping To limit the computation load, the propagation of a wavefront is stopped when it encounters the location of the robot computing its allocation. At this point all robots closer to frontiers have been reached by the wavefront. The robots not encountered are further to the frontier.

Parallel computation of wavefronts Further reduction of the computation load can be obtained by computing wavefront propagation in parallel. Wavefronts are started simultaneously and propagate at the same speed. When a wavefront encounters a robot it is paused. Then two cases are considered :

-If the encountered robot is the robot computing its assignment then the process is finished. The robot is assigned to the frontier corresponding to this wavefront. -If all wavefronts are paused on other robots, they are restarted sequentially from the lowest to the highest potential value in order to re-synchronize them. The whole process is repeated.

This process allows to synchronize the wavefronts propagation first on the number of encountered robots and second on the distance.

Figure 3 illustrates the result of a parallel wavefront computation.

Fig. 3. Resulting potential values from the wavefront propagation algorithm when stopped on the robot computing its assignated frontier (left) and using the parallel wavefront computation (right). Robot computing its allocation is in yellow. Cell color is white when no potential value has been computed in this cell, otherwise it has the color of the frontier associated with minimum potential values computed in that cell.

Path or trajectory planning

The wavefront propagation algorithm allows to navigate to the frontier by descending the negative gradient. A different planner can be used to account for non-holonomic or dynamic constraints but a feasible trajectory may not exist. Coordination in between robots is achieved only by cooperatively building the map and by sharing robots locations. This feature also applies to the decentralized versions of the greedy algorithms but in comparison the MinPos algorithm using the cost matrix is less complex. Furthermore, using the parallel wavefront computation, the cost matrix is not computed, only one complete path is computed: the one from the robot to its assigned frontier. In the next section, we show that this computation cost reduction does not compromise performances and can even improve them compared to state-of-the-art multi-robot exploration algorithms.

Experiments and analysis

Simulation : Frontier assignment evaluation

Evaluation of the proposed method was carried out in a simulator specifically developed. Environment and time are discrete, the robot's size is set to the dimension of a cell. Robots know with certainty their location and can sense their neighborhood perfectly at 360 • around them with a parameterized range. The simulated environments are buildings, randomly generated mazes and a regular grid (illustrated in figure 4). Exploration times are measured when robots have discovered every part of the environment.

Analysis

As a tentative explanation of the results obtained we analyze, in this section, different assignments on static crossroad situations.

During system execution, an adequate dynamical behavior emerges that tends to separate grouped robots. For example, as shown in Figure 6(a), two robots following each other to reach the same frontier will separate as soon as the first one moves away from an unassigned frontier, when re-computing its assignment frequently and as soon as it reached the frontier otherwise. Indeed, the second robot is then in first position towards this frontier and therefore assigned to it. With the nearest frontier algorithm both robots would have continued exploring the area behind frontier F 1 , with a greedy algorithm robots would have initially been assigned to the different frontiers.

Compared to the greedy assignment of frontiers the MinPos algorithm does not only consider distances to frontiers but also directions to frontiers. This feature has the advantage of separating grouped robots in different directions. For example, in figure 6(b), the MinPos assignment will send robot R 1 to frontier F 1 which is further away than F 2 and F 3 but in a different direction whereas the greedy assignment will send R 3 to F 2 and R 1 to F 3 . The MinPos assignment will lead to a shorter exploration time of all frontiers because once R 3 has explored F 2 it will then explore F 3 to complete the exploration (F 2 -F 3 are closer to each other than F 2 -F 1 ).

A limit of the MinPos frontier assignment appears when, from a robot point of view, there is a direction with multiple frontiers and multiple robots in front. The robot will consider the robots in front even though the number of frontiers is larger than the number of robots, leaving unassigned frontiers. Figure 6(c) illustrates such a situation where R 3 "sees" frontier F 1 with 2 robots in front and will go towards F 4 where it is in 2nd position. In these situations, a greedy assignment performs better. Nevertheless results show that the impact on performance are low.

Experiments with robots

The MinPos algorithm was also tested with up to four robots. The robots used are MiniRex robot built in the LISA lab at the university of Angers France. For exploration, they are equipped with a Hokuyo utm-30lx laser range sensor and three ultrasound range sensors. The environment to explore, shown in Figure 7, is approximately 35m 2 and features glass walls. Figure 7 shows the results of the exploration with 3 robots. The trajectories of each robot demonstrate the validity and efficiency of the proposed approach, indeed each robot explored a different part of the environment. The comparison of MinPos with nearest frontier with the MiniRex robots showed that the exploration is faster with MinPos and generates less conflict in between robots.

Videos of an exploration of the arena can be seen at www.loria.fr/ ˜bautin/ outputfile.avi and www.loria.fr/ ˜bautin/outputfile2.avi.

Conclusion

We addressed the problem of exploring an unknown environment with multiple autonomous robots. A novel algorithm is proposed to assign frontiers that should be explored by each robots. This algorithm addresses the limitation of previous approaches in that it achieves a good coordination with a low complexity algorithm not requiring coordination with explicit communication.

The proposed algorithm is based on the concept of position of a robot toward a frontier, defined by the number of robots closer to the frontier than the robot evaluating its position. To cooperate, the robots share their location and local maps. Each robot then decides autonomously which frontier it will explore next.

Performance measures in simulation demonstrated that our approach is significantly more efficient in total exploration time than the nearest frontier assignment. Our algorithm performs better than a utility greedy assignment of frontier when the number of robots is small and has similar performances when the number of robots grows. Furthermore, the MinPos algorithm has a lower complexity than greedy algorithms and does not require to compute a path from each robot to every frontier beforehand. Indeed, distances to frontiers are computed using a wavefront propagation started from frontiers independently of the number of robots.

We have successfully used this approach during the french robotics challenge Carotte1 that has been won by deploying five robots in a 120m 2 unkown 'appartement-like' environment. As future work, we are considering the use of a hybrid metric/topological map representation. We aim to further reduce bandwidth requirements by sharing only topological information in between robots exploring different parts of the environment. This should allow a more distributed and therefore scalable approach.

  (a) No consideration for other robots location. (b) Robot 5 and 2 go towards the same region.

Fig. 1 .

 1 Fig. 1. Resulting frontier assignment using the nearest frontier (a) and greedy (b) algorithms

Algorithm 2 :

 2 Greedy (decentralized) Complexity O(n 2 m) Input: Ri, C Cost Matrix Output: αij assignment of robot Ri to frontier Fj while Ri has no frontier assigned do Find

Fig. 2 .

 2 Fig. 2. Resulting frontier assignment using the MinPos algo. : directions taken are well balanced.

Algorithm 3 :

 3 MinPos Complexity O(nm)Input: R i , C cost matrix Output:

Fig. 4 .

 4 Fig. 4. Example of the environments used for the experiments: an hospital section, a regular grid, and a stable.

Figure 5 (

 5 Figure5(a) compares the exploration times given in simulation steps, while varying the number of robots of different methods. The methods compared are nearest frontier, the Burgard et al.[START_REF] Burgard | Coordinated multi-robot exploration[END_REF] greedy-based algorithm and MinPos on the hospital section environment. Results shown are an average of 60 runs of each algorithm with a given robot count. We observe that the Burgard et al. and Min Position algorithms are more efficient improving by 13% on average the number exploration steps required to fully explore the environment. On all the environments except the stable, when the number of robots is small (from 1 to 5 or 6 depending on the environment), the MinPos algorithm performs better. On the other hand, our implementation of the Burgard et al. algorithm has close but slightly better performance when the number of robots is large. Figure5(b) compares a greedy allocation of frontiers with MinPos allocation on a more realistic simulator, exploration times are in seconds. On the environment named stable the MinPos algorithm is 18% more efficient on average, and this improvement remains true regardless the number of robots. Results on the mean number of steps and standard deviation on all the test environments show that the MinPos algorithm has less variability. This has been confirmed by an analysis of variance test run on the obtained data.

Figure 5 (

 5 Figure5(a) compares the exploration times given in simulation steps, while varying the number of robots of different methods. The methods compared are nearest frontier, the Burgard et al.[START_REF] Burgard | Coordinated multi-robot exploration[END_REF] greedy-based algorithm and MinPos on the hospital section environment. Results shown are an average of 60 runs of each algorithm with a given robot count. We observe that the Burgard et al. and Min Position algorithms are more efficient improving by 13% on average the number exploration steps required to fully explore the environment. On all the environments except the stable, when the number of robots is small (from 1 to 5 or 6 depending on the environment), the MinPos algorithm performs better. On the other hand, our implementation of the Burgard et al. algorithm has close but slightly better performance when the number of robots is large. Figure5(b) compares a greedy allocation of frontiers with MinPos allocation on a more realistic simulator, exploration times are in seconds. On the environment named stable the MinPos algorithm is 18% more efficient on average, and this improvement remains true regardless the number of robots. Results on the mean number of steps and standard deviation on all the test environments show that the MinPos algorithm has less variability. This has been confirmed by an analysis of variance test run on the obtained data.

Fig. 5 .

 5 Fig. 5. Exploration results for simulations in the hospital (a) and stable (b) environment.

Fig. 6 .

 6 Fig. 6. (a) : two robots separating on a T intersection using MinPos; (b)(c) : comparisons with greedy assignment, frontier assignment using MinPos (top) and greedy (bottom)

Fig. 7 .

 7 Fig. 7. Photo of the environment (left), map and trajectories resulting from an exploration (right)

Acknowledgement: This work has been supported by the French National Research Agency (ANR) and Defence Procurement Agency (DGA) in the Cartomatic project of ANR Carotte