Peter Schrammel
email: peter.schrammel@inria.fr

Bertrand Jeannet
email: bertrand.jeannet@inria.fr

Logico-Numerical Abstract Acceleration and Application to the Verification of Data-Flow Programs

Keywords: Verification, Static Analysis, Abstract Interpretation, Abstract Acceleration, Control Flow Graph Partitioning

published or not. The documents may come

L'archive ouverte

Introduction

This paper deals with the verification of safety properties about logico-numerical data-flow programs, i.e., programs manipulating Boolean and numerical variables. Verification of such properties amounts to checking whether the reachable state space stays within the invariant specified by the property.

Classical applications are safety-critical controllers as found in modern transport systems, as well as static checking of high-level simulation models, e.g. a model of a production line as depicted in Fig. 1. In such systems the properties to be proved, like throughput and workload, depend essentially on the relationships between the numerical variables of the system. Yet, there is an important observation that we are going to exploit: In many of these control systems large parts of the program simply count time or events, or, more generally, they perform rather regular linear arithmetic operations. Hence, it is appropriate to take advantage of a specialized analysis method that exploits this regularity in order Fig. 1: Example of a production line with buffers, machines, and splitting and combining material flows.

to improve verification performance and precision. In this paper, we will consider abstract acceleration [START_REF] Gonnord | Combining widening and acceleration in linear relation analysis[END_REF] for this purpose, which aims at computing in one step the effect of an unbounded number of loop iterations. However, at the same time, we are confronted with a huge Boolean state space in the applications we want to verify. Our contribution is therefore to extend abstract acceleration from purely numerical programs to logico-numerical programs in an efficient way.

Verifying logico-numerical data-flow programs by abstract interpretation. The reachability problem is not decidable for this class of programs, so analysis methods are incomplete. Abstract interpretation [START_REF] Cousot | Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints[END_REF] is a classical method with guaranteed termination for the price of an approximate analysis result. The key idea is to approximate sets of states S by elements S ♯ of an abstract domain. A classical abstract domain for numerical invariants in ℘(R n ) is the domain of convex polyhedra P ol(R n ) [START_REF] Cousot | Automatic discovery of linear restraints among variables of a program[END_REF]. An approximation S ♯ of the reachable set S is then computed by iteratively solving the fixed point equation characterizing S in the abstract domain. To ensure termination when the abstract domain contains infinitely increasing chains, one applies an extrapolation operator called widening, which induces additional approximations.

Since the analysis with a single abstract value gives only coarse results, it is usually conducted over a control flow graph (CFG) of the program. In the case of imperative programs, such a control graph can be obtained easily by associating control points with programming constructs as if-then-else or while. Data-flow programs do not have such constructs; yet, one can use finite-type variables such as Booleans to generate a control structure. Thus, the classical approach is to explicitly unfold the Boolean control structure by enumerating the Boolean state space and to analyze the numerical variables on the obtained CFG using a numerical abstract domain. The problem is that the analysis becomes intractable with larger programs because the number of control locations grows exponentially with the number of Boolean states.

Jeannet [START_REF] Jeannet | Dynamic partitioning in linear relation analysis. application to the verification of reactive systems[END_REF] proposed a method for iteratively refining the control structure and analyzing the system using a logico-numerical abstract domain, making it possible to deal with Boolean variables symbolically. We want to complement this approach with new partitioning techniques and analysis methods.

Organisation of the article. §2 gives an introduction to the abstract interpretation of logico-numerical programs, partitioning, and abstract acceleration. §3 and §4 describe our contributions on logico-numerical abtract acceleration methods, §5 presents our experimental results, and finally §6 discusses related work and concludes.

Analysis of Logico-Numerical Programs

Program model. We consider programs modeled as a symbolic transition system

I(s) A(s, i) → s ′ = f (s, i)
where (1) s and i are vectors of state and input variables, that are either Boolean or numerical; (2) I(s) is an initial condition on state variables; (3) A(s, i) is an assertion constraining input variables depending on state variables, and typically modeling the environment of the program; (4) f is the vector of transition functions. An example of such a program is

       I(b, x) = ¬b ∧ (x = 0) 1 ≤ ξ ≤ 3 →   b ′ x ′   =   (b ∧ x ≤ 5) ∨ β x + ξ if b ∧ x ≤ 5 0 otherwise  
An execution of such a system is a sequence

s 0 i 0 -→ s 1 i 1 -→ . . . s k i k -→ . . . such that I(s 0 ) and for any k ≥ 0, A(s k , i k ) ∧ s k+1 = f (s k , i k )).
The front-end compilation of synchronous data-flow programs, like Lustre, produces such a program model, that also includes various models of counter automata (by emulating locations using Boolean variables) [START_REF] Bardin | Fast: acceleration from theory to practice[END_REF].

We will use the following notations: s = (b, x) : state variable vector, with b Boolean and x numerical subvectors i = (β, ξ) : input variable vector, with β Boolean and ξ numerical subvectors C(x, ξ) : constraints over numerical variables, seen as a vector of Boolean decisions (for short C)

Transitions are written in the form A(b, β, C) → b ′ x ′ = f b (b, β, C) f x (b, β, C, x, ξ)
.

Numerical transition functions are written as a disjunction of guarded actions:

f x (b, β, C, x, ξ) = i g i (b, β, C) → a x i (x, ξ)
with ¬(g i ∧ g j ) for i = j. The program example above conforms to these notations.

Abstract interpretation

The state space induced by logico-numerical programs has the structure E = B m ×R n . As mentioned in the introduction, we adopt the abstract interpretation framework so as to abstract the equation S = S 0 ∪ post (S), S ∈ ℘(E) in an abstract domain and to solve it iteratively, using widening to ensure convergence.

We consider the domain A = ℘(B m ) × P ol(R n ) of convex states [START_REF] Jeannet | Partitionnement Dynamique dans l'Analyse de Relations Linéaires et Application à la Vérification de Programmes Synchrones[END_REF], which approximates a set of states coarsely by a conjunction of a Boolean formula and a single convex polyhedron. For instance the formula (b

∧ x ≤ 2) ∨ (¬b ∧ x ≤ 4) is abstracted by true ∧ x ≤ 4.
Partitioning the state space. We use state space partitioning to obtain a CFG in which each equivalence class of the partition corresponds to a location. Definition 1. A symbolic control flow graph (CFG) of a symbolic transition system is a directed graph Π, Π 0 , where -Π is the set of locations; each location ℓ ∈ Π is characterized by its location invariant ϕ ℓ (s), such that {ϕ ℓ (s) | ℓ ∈ Π} forms a partition of E. -Π 0 is the set of initial locations with I(s) = ℓ∈Π0 ϕ ℓ (s) -defines arcs between locations according to the transition relation:

∃s, i : ϕ ℓ (s) ∧ A(s, i) ∧ s ′ = f (s, i) ∧ ϕ ℓ ′ (s ′ ) ⇒ ℓ ℓ ′
There are several ways to define a partition inducing such a CFG. In predicate abstraction for instance, the partition is generated by considering the truth value of a finite set of predicates [START_REF] Graf | Construction of abstract state graphs with PVS[END_REF]. Here, we consider partitions defined by equivalence relations on Boolean state variables. For example, the fully partitioned CFG obtained by enumerating all Boolean states is characterized by the relation

b 1 ∼ b 2 ⇔ b 1 = b 2 .
Simplifying a CFG. In practice, partitioning is done by incrementally dividing the locations. Furthermore arcs between locations that are proved to be infeasible are removed. This can be done, e.g. by checking the satisfiability of the transition relation, e.g. using an SMT solver.

c τ =⇒ c ′ c ′′ τ ⊗
At last, transition functions are simplified by partial evaluation (using a generalized cofactor operator, see [START_REF] Coudert | Verification of synchronous sequential machines based on symbolic execution[END_REF]).

Analyzing a CFG. In the context of analysis by abstract interpretation, considering a CFG allows to apply widening in a more restrictive way, e.g. on loop heads only [START_REF] Bourdoncle | Efficient chaotic iteration strategies with widenings[END_REF]. Also the information loss due to the convex union is limited, because we assign an abstract value to each location: We consider the compound abstract domain (Π → A) where the concrete states S are connected to their abstract counterparts S ♯ by the Galois connection:

S ♯ = α(S) = λℓ . α(S ⊓ ϕ ℓ ) S = γ(S ♯ ) = ℓ∈Π γ(S ♯ ℓ )
Analyzing the partitioned system amounts to computing the least fixed point

S ♯ = S ♯,0 ⊔ λℓ . ℓ ′ ∈Π post (S ♯ ℓ ′ ) ⊓ ϕ ℓ where S ♯ , S ♯,0 ∈ (Π → A).

Abstract acceleration

As mentioned in the introduction, acceleration [START_REF] Bardin | Fast: acceleration from theory to practice[END_REF] aims at computing exactly (or precisely in the case of abstract acceleration [START_REF] Gonnord | Combining widening and acceleration in linear relation analysis[END_REF][START_REF] Gonnord | Accélération abstraite pour l'amélioration de la précision en Analyse des Relations Linéaires[END_REF]) the effect of a self-loop. The basic idea is to replace a loop transition by its transitive closure (Fig. 2) by providing a formula τ ⊗ (X) computing τ * (X) = k≥0 τ k (X).

Basic concepts. A loop transition τ has the structure: g → a meaning "while guard g do action a". Our extension of abstract acceleration to numerical inputs [START_REF] Schrammel | Extending abstract acceleration to data-flow programs with numerical inputs[END_REF] deals with loop transitions of the form

A L 0 J x ξ ≤ v k Ax+Lξ≤v ∧ Jξ≤k → x ′ = C T x ξ + u Cx+Tξ+u (1)
Existing acceleration methods can deal with transitions where the matrix C is a diagonal matrix with zeros and ones only or when it is periodic (∃p > 0, l > 0 : C p+l = C p ). Throughout this paper, we will call such numerical transition functions accelerable, whereas we regard general affine transformations (with an arbitrary C) as non-accelerable.

Widening and acceleration. Acceleration gives us a formula for computing the transitive closure of accelerable loop transitions. Widening is still needed in the case of non-accelerable transitions, outer loops of nested loops and to

b 1 ¬b 1 b 0 ∧ x 1 = 0∧ x 2 = 0 x 1 ≤ 9 → x 1 + +; x 2 + + x 1 ≤ 9 → x 1 + +; x 2 + +; b 2 := ¬b 2 x 1 > 9 → x 1 := 0; b 1 := ¬b 1 x 1 > 9 → x 1 := 0; x 2 := 0; b 1 := ¬b 1
Fig. 3: Self-loop ready to be accelerated (left). Acceleration not applicable (right). guarantee convergence when there are multiple self-loops in the same control location (see the concept of flat systems in [START_REF] Bardin | Fast: acceleration from theory to practice[END_REF]). The main advantages of abstract acceleration in comparison with widening result from two properties:

-Idempotency (τ ⊗ (X) = τ ⊗ (τ ⊗ (X))), which simplifies the fixed point computation (widening usually requires more than one step to stabilize);

-Monotonicity X 1 ⊑ X 2 ⇒ τ ⊗ (X 1 ) ⊑ τ ⊗ (X 2 )
, that makes the analysis more robust and predictible (whereas widening operators are not monotonic).

Classical application of abstract acceleration

We describe now the classical way to apply abstract acceleration to the analysis of logico-numerical programs, for which this paper proposes major enhancements. Numerical acceleration can be applied to self-loops where the numerical state evolves while the Boolean state does not: see Fig. 3 for an example and a counterexample. The tool Aspic [START_REF] Gonnord | The ASPIC tool: Accelerated symbolic polyhedral invariant computation[END_REF] is based on the enumeration of the Boolean state space which trivially yields a CFG that fulfills this requirement.

Example 1. We will try to infer invariants on the following running example:

I(b, x) = ¬b0 ∧ ¬b1 ∧ x0 = 0 ∧ x1 = 0 ∧ x2 = 0 true →                            b ′ 0 = b0 ∨ (¬b0 ∧ x0 > 10 ∧ x1 > 10) b ′ 1 = b1 ∨ (¬b1 ∧ x0 > 20) x ′ 0 =    x0 + 1 if (¬b0 ∧ ¬b1 ∧ x0 ≤ 10 ∧ β) ∨ (b0 ∧ ¬b1 ∧ x0 ≤ 20) 0 if ¬b0 ∧ ¬b1 ∧ x0 > 10 ∧ x1 > 10 x0 otherwise x ′ 1 = x1 + 1 if ¬b0 ∧ ¬b1 ∧ x1 ≤ 10 ∧ ¬β x1 otherwise x ′ 2 = x2 + 1 if (¬b0 ∧ ¬b1 ∧ (x0 ≤ 10 ∧ β ∨ x1 ≤ 10 ∧ ¬β)) ∨ (b0 ∧ ¬b1) x2 otherwise
The counting patterns of this example (see Fig. 4b) is representative of the production line benchmarks presented in Section 5.

Generating a numerical CFG. At first, one performs a Boolean reachability analysis in order to reduce the state space of interest (b 0 ∨ ¬b 1 in the case of our running example). Starting from the most simple CFG of the program consisting of a single location with a self-loop (see Fig. 4a), standard techniques are used for (1) enumerating the Boolean state space and (2) simplifying the transitions by source and destination location using partial evaluation. Afterwards, (3) the Boolean input variables are replaced by explicit non-deterministic transitions (see Fig. 4b). This CFG is purely numerical, but the guards of the loop transitions might still be non-convex. Transforming the guard into a minimal DNF and splitting the transition into several transitions, one for each conjunct, yields a CFG with self-loops compatible with the transition scheme of A single self-loop like in location b 0 ∧ ¬b 1 in Fig. 4b can now be "flattened" into a transitive closure transition (cf. Fig. 2).

b 0 ∨ ¬b 1 τ (a) Initial CFG ¬b 0 ∧ ¬b 1 b 0 ∧ ¬b 1 b 0 ∧ b 1 x 0 ≤ 10 → x ′ 0 = x 0 + 1; x ′ 2 = x 2 + 1 x 1 ≤ 10 → x ′ 1 = x 1 + 1; x ′ 2 = x 2 + 1 x 0 > 10 ∧ x 1 > 10 → x ′ 0 = 0 x 0 ≤ 20 → x ′ 0 = x 0 + 1; x ′ 2 = x 2 + 1 x 0 > 20 → x ′ 2 = x 2 + 1 (
Multiple self-loops. However, the obtained CFG usually contains multiple self-loops like in location ¬b 0 ∧ ¬b 1 in Fig. 4b. In this case a simple "flattening" as in Fig. 2 is not possible: For the fixed point computation we must take into account all sequences of self-loop transitions in this location. Actually, the idempotency of accelerated transitions can be exploited in order reduce these sequences to those where the same transition is never taken twice successively: For the two accelerable loops we have to compute:

τ ⊗ 1 (X)⊔τ ⊗ 2 (X)⊔τ ⊗ 2 •τ ⊗ 1 (X)⊔τ ⊗ 1 •τ ⊗ 2 (X)⊔τ ⊗ 1 •τ ⊗ 2 •τ ⊗ 1 (X)⊔τ ⊗ 2 •τ ⊗ 1 •τ ⊗ 2 (X)⊔.
. . This infinite sequence may not converge, thus in general, widening is necessary to guarantee termination. However, in practice the sequence often converges after the first few elements (see [START_REF] Bardin | Fast: acceleration from theory to practice[END_REF]).

The technique implemented in Aspic consists in expanding multiple selfloops into a graph of which the paths represent these sequences, as shown in Fig. 5 in the case of three self-loops, and to solve iteratively the fixed point equations induced by the CFG as sketched in §2.1, using widening if necessary. Moreover, Aspic implements methods to accelerate circuits of length greater than one.

Logico-Numerical Abstract Acceleration

Our goal is to exploit abstract acceleration techniques without resorting to a Boolean state space enumeration in order to overcome the limitations of current tools (e.g. [START_REF] Gonnord | The ASPIC tool: Accelerated symbolic polyhedral invariant computation[END_REF]) w.r.t. the analysis of logico-numerical programs.

o τ i τ i τ i τ o τ o τ o τ ⊗ 1 τ ⊗ 2 τ ⊗ 1 τ ⊗ 3 τ ⊗ 2 τ ⊗ 3
Fig. 5: Computation of three accelerable self-loops τ 1 , τ 2 and τ 3 . τ i and τ o are the incoming resp. outgoing transitions of the location.

b 0 ∨ ¬b 1 τ 1 : ¬b 0 ∧ ¬b 1 ∧ x 0 ≤ 10 → x ′ 0 = x 0 + 1; x ′ 2 = x 2 + 1 τ 2 : ¬b 0 ∧ ¬b 1 ∧ x 1 ≤ 10 → x ′ 1 = x 1 + 1; x ′ 2 = x 2 + 1 τ 3 : b 0 ∧ ¬b 1 ∧ x 0 ≤ 20 → x ′ 0 = x 0 + 1; x ′ 2 = x 2 + 1 τ r
Fig. 6: Acceleration of Ex. 1 in a CFG with a single location: The upper three self-loops are accelerable. The rest of the system is summarized in the transition τ r where the Boolean equations are not the identity.

In this section we will first discuss some related issues in order to motivate our approach before presenting methods that make abstract acceleration applicable to a CFG, which now may contain loops with operations on both Boolean and numerical variables.

Motivations for our approach

A first observation is that identifying self-loops is more complex when Boolean state variables are not fully encoded in the CFG. Indeed, if a symbolic CFG contains a "syntactic" self-loop (ℓ, τ, ℓ) with τ : g(b, x, ξ) → (b, x) = f (b, x, ξ), there is an "effective" self-loop only for those Boolean states b ∈ ϕ l such that g(b, x, ξ) ∧ b = f b (b, x, ξ) is satisfiable1 . For instance, the self-loop around location ¬b 1 in Fig. 3 is not an "effective" self-loop.

This observation also applies to circuits, where numerical inputs have to be duplicated : If there is a circuit (ℓ, τ 1 , ℓ ′ ) and (ℓ ′ , τ 2 , ℓ) with τ i : g i (s, ξ) → s ′ = f i (s, ξ) for i = 1, 2, the composed transition has the form τ : g(s, ξ, ξ ′ ) → s ′′ = f (s, ξ, ξ ′ ). This strongly limits in practice the length of circuits that can be reduced to self-loops and accelerated. In this paper, we will not deal with such circuits, and we consider only self-loops.

We give a definition for a logico-numerical self-loop which can be accelerated by the known methods, because the Boolean part of the transition function is the identity:

Definition 2 (Accelerable logico-numerical transition). A transition τ is said to be accelerable if it has the form g b (b, β) ∧ g x (C) → b ′ x ′ = b a(x, ξ) , where g x (C) → x ′ = a(x, ξ) is accelerable according to §2.2.
A naive approach to our problem could be to partition the system into sufficiently many locations, until we get self-loops that correspond to Def. 2. This approach is simple-minded for two reasons: (i) There might be no such Boolean states in the program at all; (ii) in the case of Fig. 3, simply ignoring the Boolean variable b 2 would make the (syntactic) self-loop accelerable without impacting the precision. More generally, it may pay off to slightly abstract the behaviour of self-loops in order to benefit from precise acceleration techniques.

Another important remark is that we do not necessarily need to partition the system into locations to apply acceleration: it is sufficient to decompose the selfloops: Starting from the basic CFG with a single location and a single self-loop, we could split the loop into loops where the numerical transition function can be accelerated and the Boolean transition is the identity and a last loop where this is not the case. Fig. 6 shows the result of the application of this idea to our running example of Fig. 4.

This allows us to separate the issue of accelerating self-loops in a symbolic CFG, addressed in this section, from the issue of finding a suitable CFG, addressed in §4. We will use a dedicated partitioning technique to find an appropriate CFG in order to render effective our logico-numerical acceleration method.

Decoupling numerical and Boolean transition functions

We consider self-loops (ℓ, τ, ℓ) with τ : [START_REF] Gonnord | Combining widening and acceleration in linear relation analysis[END_REF], where π is the function that approximates a set S ∈ E by a Cartesian product, e.g. π((B

A(s, i) → b ′ x ′ = f b (s, i) f x (s, i) . We use the abstractions ℘(E) = ℘(B m × R n ) ---→ ← --- π id ℘(B m ) × ℘(R n ) ---→ ← --- α id A = ℘(B m ) × P ol(R n ) discussed in §2.
1 ×X 1 )∪(B 2 ×X 2 )) = (B 1 ∪B 2 )×(X 1 ∪X 2 ). If τ is accelerable in the sense of abstract acceleration, then π • τ * ⊆ τ ⊗ .
Our logico-numerical abstract acceleration method relies on decoupling the numerical and Boolean parts of the transition function τ with

τ b : A(s, i) → b ′ x ′ = f b (s, i) λ(s, i). x and τ x : A(s, i) → b ′ x ′ = λ(s, i). b f x (s, i) .
We can approximate τ * as follows:

Proposition 1. τ * ⊆ (π • τ b • τ * x ) *
. See [START_REF] Schrammel | Logico-numerical abstract acceleration and application to the verification of data-flow programs[END_REF] for details of the proof. Briefly, we prove first

τ ⊆ π • τ b • (id ∪ τ x ). Then, with (id ∪ τ x ) ⊆ τ * x we conclude τ * ⊆ (π • τ b • τ * x )
* . Now, we assume that τ x is accelerable in the sense of Def. 2, which means that A(s, i) = g b (b, β)∧g x (x, ξ) and f x (s, i) = a(x, ξ). By applying Prop. 1, we obtain that (π•τ b •τ ⊗

x ) * is a sound approximation of τ * . Although we could prove that the involved Kleene iteration is bounded and converges without applying widening, there exists a more efficient alternative in which numerical and Boolean parts are computed in sequence, so that numerical acceleration is applied only once.

Proposition 2. If τ x is accelerable, then (1) (π • τ b ) * • π • τ * x • π is idempotent, and (2) τ * ⊆ (π • τ b ) * • π • τ * x • π
See [START_REF] Schrammel | Logico-numerical abstract acceleration and application to the verification of data-flow programs[END_REF] for details of the proof. The intuition for (1) is the following: If the guard g x ∧ g b is satisfied, i.e. the transition can be taken, we saturate the numerical dimensions first; then we saturate the Boolean ones. The point is now, that the application of τ b does not enable "more" behavior of the numerical variables. Thus, re-applying the function has no effect. Then we can prove (2): from Prop. 1 follows

τ * ⊆ (π•τ b •τ * x ) * = ((π•τ b ) * •τ * x ) * ⊆ ((π • τ b ) * • π • τ * x • π) * = (π • τ b ) * • π • τ *
x • π (for the last step, we use (1) and the fact that the function includes the identity).

The following theorem implements Prop. 2 in the abstract domain A. We use the notation h = f ↓ X ("f partially evaluated on the convex polyhedron X"), to denote any (simpler) formula h such that X(x, ξ)

⇒ (h(b, β, C) = f (b, β, C)). Theorem 1. If a transition τ is such that τ x is accelerable, then τ * can be approximated in A with τ ⊗ : A → A (B, X) → τ b b [X ⊗ ] * (B) , X ⊗ where -X ⊗ = (τ x x ) ⊗ (X) -(τ x x ) ⊗ is the abstract acceleration of τ x x : g x (x, ξ) → x ′ = a(x, ξ) -τ b b [X](B) = f b ↓ (X ⊓ g x ) (b, β, C) | b ∈ B ∧ g b (b, β) -(τ b b [X]) * (B) = lfp(λB ′ . B ∪ τ b b [X](B ′ )). Moreover, (τ b b [X]
) * (and thus τ ⊗ ) can be computed in bounded time as the least fixed point of a monotonic function in the finite lattice ℘(B m ).

In other words, we compute the transitive closure X ⊗ of τ x using numerical abstract acceleration and saturate τ b partially evaluated over X ⊗ .

Discussion. At the first glance the approximations induced by this partial decoupling seem to be rather coarse. However, it is not really the case in our context for two reasons:

1. The correlations between Boolean and numerical variables that are lost by our method are mostly not representable in the abstract domain A anyway. For example, consider the loop x ≤ 4 → (b ′ = ¬b; x ′ = x+1), where b could be the least significant bit of a binary counter for instance: starting from (b, x) ∈ {(true, 0)} the exact reachable set is {true} × {0, 2, 4} ∪ {false} × {1, 3, 5}; its abstraction in A is {⊤} × {0 ≤ x ≤ 5}. Hence, this information will also be lost in a standard analysis merely relying on widening. Yet, due to numerical acceleration we can even expect a better precision with our method. 2. We will apply this method to CFGs (see §4) in which the Boolean states defining a location exhibit the same numerical behavior and thus, decoupling is supposed not to seriously affect the precision.

Until now we studied the case of a single self-loop. In the presence of multiple self-loops we expand the graph in the same way as with purely numerical transitions, e.g. as shown in Fig. 5, and we apply Thm. 1 to each loop. As in the purely numerical case, widening must be applied in order to guarantee convergence.

Example 2. We give the results obtained for our running example: Analyzing the enumerated CFG in Fig. 4b using abstract acceleration gives 0 ≤ x 0 ≤ 21∧ 0 ≤ x 1 ≤ 11∧ x 0 + x 1 ≤ x 2 ≤ 44 bounding all variables2 . Analyzing the system on a CFG with a single location using decoupling and abstract acceleration still bounds two variables (0 ≤ x 0 ≤ 21 ∧ 0 ≤ x 1 ≤ 11 ∧ x 0 + x 1 ≤ x 2 ), whereas, even on the enumerated CFG standard analysis does not find any upper bound at all:

0 ≤ x 0 ∧ 0 ≤ x 1 ∧ x 0 + x 1 ≤ x 2 .

Decoupling accelerable from non-accelerable and Boolean transition functions

Theorem 1 applies only if the numerical transition functions are accelerable. If this is not the case, we can reuse the idea of Prop. 1, but now by decoupling the accelerable numerical functions from Boolean and non-accelerable numerical functions:

τ a : A(s, i) →   b ′ x ′ n x ′ a   =   λ(s, i). b λ(s, i). x n a(x, ξ)   , τ n,b : A(s, i) →   b ′ x ′ n x ′ a   =   f b (s, i) f n (s, i) λ(s, i). x a   Proposition 3. τ * ⊆ (π • τ n,b • τ * a ) * ⊆ (π • τ n,b • τ ⊗ a )
* However, Prop. 2 does not apply any more, because the function τ a depends on non-accelerated numerical variables updated by τ n,b . Moreover, widening is required because τ * n,b is not guaranteed to converge in a bounded number of iterations.

Using inputization techniques

Inputization (see [START_REF] Bres | State abstraction techniques for the verification of reactive circuits[END_REF] for instance) is a technique that treats state variables as input variables. This method is useful to cut dependencies. For example, it can be employed to reduce (π

• τ b ) * • π to π • τ ′ b • π in Prop. 1,
τ b : b ′ 0 = ¬b0 b ′ 1 = b1 b ′ 2 = b2 ∧ x ≥ 0 τ ′ b : b ′ 0 = β0 b ′ 1 = b1 b ′ 2 = β2 ∧ x ≥ 0
Our experiments show that this technique is quite useful: the speed-up gained by removing loops often pays off in comparison to the approximations it brings about.

Partitioning Techniques for Logico-Numerical Acceleration

The logico-numerical acceleration method described in the previous section can be applied to any CFG. However, in order to make it effective we apply it to a CFG obtained by a partitioning technique that aims at alleviating the impact of decoupling on the precision. This section proposes such partitioning techniques that generate CFGs in which the Boolean states that exhibit the same numerical behavior are grouped in the same locations, so that it is likely that the numerical transition functions in loops do not depend on Boolean state variables.

Basic technique. In order to implement this idea we generate a CFG that is characterized by the following equivalence relation:

Definition 3.
(Boolean states with same set of guarded numerical actions)

b 1 ∼ b 2 ⇔    ∀β 1 , C : A(b 1 , β 1 , C) ⇒ ∃β 2 : A(b 2 , β 2 , C) ∧ f x (b 1 , β 1 , C) = f x (b 2 , β 2 , C) and

vice versa

The intuition of this heuristics is to make equivalent the Boolean states that can execute the same set of numerical actions, guarded by the same numerical constraints.

Example 4. We illustrate the application of this method to Example 1. We first factorize the numerical transition functions by actions:

(x ′ 0 , x ′ 1 , x ′ 2 ) =            (x0 +1 , x1 , x2 +1) if (¬b0 ∧ ¬b1 ∧ x0 ≤ 10) ∨ (b0 ∧ ¬b1 ∧ x0 ≤ 20) ( x0 , x1 +1 , x2 +1) if ¬b0 ∧ ¬b1 ∧ x1 ≤ 10 ( 0 , x1 , x2 ) if ¬b0 ∧ ¬b1 ∧ x0 > 10 ∧ x1 > 10 ( x0 , x1 , x2 +1) if b0 ∧ ¬b1 ∧ x0 > 20 ( x0 , x1 , x2 ) otherwise
Then by applying Def. 3 we get the equivalence classes {¬b 0 ∧¬b 1 , b 0 ∧¬b 1 , b 0 ∧b 1 }: the obtained CFG is the one of Fig. 4b.

In the worst case, as in Ex. 4 above, a different set of actions can be executed in each Boolean state, thus the Boolean states will be enumerated. In the other extreme case in all Boolean states the same set of actions can be executed, which induces a single equivalence class. Both cases are unlikely to occur in larger, real systems.

From an algorithmic point of view, we represent all our functions with bdds and mtbdds [START_REF] Bryant | Graph-based algorithms for boolean function manipulation[END_REF], and we proceed as follows: We factorize the numerical transition functions by the numerical actions (trivial with mtbdds):

f x (b, β, C, x, ξ) = 1≤i≤m g i (b, β, C) → a x i (x, ξ)
Then we eliminate the Boolean inputs β, and we decompose the results into (∃β :

g i (b, β, C)) = 1≤j≤ni g b ij (b) ∧ g x ij (C) where g x ij (C) may be non-convex. The equivalence relation ∼ of Def. 3 can be reformulated as b 1 ∼ b 2 ⇔ ∀i∀j : g b ij (b 1 ) ⇔ g b ij (b 2
). This last formulation reflects the fact that in the resulting CFG the numerical function f x specialized on a location ℓ does not depend any more on b. Hence, the information loss is supposed to be limited.

Reducing the size of the partition. An option for having a less discriminating equivalence relation is to make equivalent the Boolean states that can execute the same set of numerical actions regardless of the numerical constraints guarding them. Definition 4. (Boolean states with same set of numerical actions)

b 1 ≈ b 2 ⇔    ∀β 1 , C 1 : A(b 1 , β 1 , C 1 ) ⇒ ∃β 2 , C 2 : A(b 2 , β 2 , C 2 ) ∧ f x (b 1 , β 1 , C 1 ) = f x (b 2 , β 2 , C 2 )

and vice versa

We clearly have ∼⊆≈. For example, if we have two guarded actions b ∧ x ≤ 10 → x ′ = x + 1 and ¬b ∧ x ≤ 20 → x ′ = x + 1, ∼ will separate the Boolean states satisfying resp. b and ¬b, whereas ≈ will keep them together.

Another option is to consider only a subset of the numerical actions, that is, we ignore the transition functions of some numerical variables in Defs. 3 or 4. One can typically focus only on variables involved in the property. According to our experiments, this method is very efficient, but it relies on manual intervention.

Experimental Evaluation

Our experimentation tool nbACCel implements the proposed methods on the basis of the logico-numerical abstract domain library BddApron [START_REF] Jeannet | Bddapron: A logico-numerical abstract domain library[END_REF].

Benchmarks. Besides some small, but difficult benchmarks, we used primarily benchmarks that are simulations of production lines as modeled with the library Quest for the LCM language3 (see Fig. 1) for evaluating scalability. These models consist of building blocks like sources, buffers, machines, routers for splitting and combining flows of material and sinks, that synchronize via handshakes. The properties we want to prove depend on numerical variables, e.g. (1) maximal throughput time of the first element passing the production line, or (2) minimal throughput of the production line. Inputs could serve modeling nondeterministic processing and arrival times, but we did not choose benchmarks with numerical inputs in order to enable a comparison with Aspic [START_REF] Gonnord | The ASPIC tool: Accelerated symbolic polyhedral invariant computation[END_REF].

Results. We compared our tool nbACCel with NBac [START_REF] Jeannet | Dynamic partitioning in linear relation analysis. application to the verification of reactive systems[END_REF] and Aspic. The results are summarized in Table 1. The tools where launched with the default options; for nbACCel we use the partitioning heuristics of Def. 4 and the inputization technique of §3.4. We do not need the technique of §3.3 for our examples.

Discussion. The experimental comparison gives evidence about the advantages of abstract acceleration, but also some potential for future improvement: -nbACCel can prove a lot of examples where NBac fails: this is due to the fact that abstract acceleration improves precision, especially in nested loops where the innermost loop can be "flattened", which makes it possible to recover more information in descending iterations. -nbACCel seems to scale better than NBac: First, the idempotency of abstract acceleration reduces the number of iterations and fixed point checks. Second, our heuristics generates a partition that is well-suited for analysisthough, for some of the larger benchmarks, e.g. LCM quest 4-1, the dynamic partitioning of NBac starts to pay off, whereas our static partition is more fine-grained than necessary, which makes us waste time during analysis. -Once provided with an enumerated CFG, Aspic is very fast on the smaller benchmarks. However, the current version (3.1) cannot deal with CFGs larger than a few hundred locations. We were surprised that some of the small examples were not proven by Aspic. We suspect that this is due to some information loss in widening. -The analysis using logico-numerical acceleration proved twice as many benchmarks and turned out to be 20% faster than a standard analysis of the same CFG with widening with delay 2 and two descending iterations. -Applying the more refined partition of Def. 3 to our benchmarks had only a minor influence on performance and precision, and not applying inputization had no impact on the verification of properties, but it slowed down the analysis by 25% on average. -Generally, for the benchmarks LCM quest 1 to 4 property 2 was not proved by the tools. Here, the combination of our heuristics with dynamic partitioning for further refining the critical parts of the CFG could help.

We propose techniques for accelerating logico-numerical transitions, that allow us to benefit from the precision gain by numerical abstract acceleration as used in the tool Aspic, while tackling the Boolean state space explosion problem encountered when analysing logico-numerical programs. Experimentally, our tool nbACCel is often able to prove properties for the larger benchmarks, unlike the two other tools we tested -and this on CFGs that are ten times smaller than the CFGs obtained by enumeration of the reachable Boolean state space.

Although our method is based on the partial decoupling of the Boolean and numerical transitions, the experiments confirm our intuition that our method generally improves the precision. We attribute this to the following observations: first, numerical abstract acceleration reduces the need for widening; second, the information that we might lose by decoupling would often not be captured by the abstract domain anyway; and at last, the CFG obtained by our partitioning method particularly favors the application of our logico-numerical acceleration method.

This work raises interesting perspectives: Regarding abstract acceleration, the acceleration of multiple self-loops deserves additional investigation in relation with partitioning techniques. Concerning partition refinement, the combination of our approach with dynamic partitioning à la [START_REF] Jeannet | Dynamic partitioning in linear relation analysis. application to the verification of reactive systems[END_REF] seems to be worth pursuing. In particular partitioning according to numerical constraints is mandatory for proving properties relying on non-convex inductive invariants. Such improvements should allow to tackle a wider range of benchmarks.

Related Work. To our knowledge there is no work about the application of abstract acceleration to logical-numerical data-flow programs, but there is work on related methods that we tailored to fit our purpose. In §2 we already discussed in detail the concepts of abstract acceleration [START_REF] Gonnord | Combining widening and acceleration in linear relation analysis[END_REF][START_REF] Gonnord | Accélération abstraite pour l'amélioration de la précision en Analyse des Relations Linéaires[END_REF], on which our work is based, and that we extended in [START_REF] Schrammel | Extending abstract acceleration to data-flow programs with numerical inputs[END_REF].

Jeannet [START_REF] Jeannet | Dynamic partitioning in linear relation analysis. application to the verification of reactive systems[END_REF] uses in the tool Nbac partitioning heuristics that are based on the property being analyzed in order to cut paths between initial and bad states. The tool interleaves partitioning steps with analysis (dynamic partitioning), thus the "dangerous" state space is reduced in each step. Bouajjani et al. [START_REF] Bouajjani | Minimal model generation[END_REF] describe a partition refinement algorithm for the Lustre compiler using bisimulation. We think that we could exploit it to refine our CFG, when we fail to prove the property.

Alternative approaches for verifying properties about data-flow programs rely on bounded model-checking or k-induction techniques, which both exploit the efficiency of modern SMT solvers. Hagen and Tinelli [START_REF] Hagen | Scaling up the formal verification of Lustre programs with SMT-based techniques[END_REF] describe the application of these two approaches to the verification of Lustre programs. Another example is the HySat tool [START_REF] Fränzle | Hysat: An efficient proof engine for bounded model checking of hybrid systems[END_REF], a bounded model-checker for hybrid systems with piecewise linear behavior -our methods allow to analyze discretizations of such systems. HySat relies on the integration of linear constraint solving with SAT solving. The interesting point is that they deal implicitly with large Boolean control structures by encoding them into linear pseudo-Boolean constraints.

Fig. 2 :

 2 Fig. 2: Self-loop transition (left) and accelerated transition (right).

Fig. 4 :

 4 Fig. 4: Transformation of the program of Example 1. τ is the global transition. The guards are already convex in the obtained CFG.

Example 3 .

 3 where τ ′ b is computed by inputizing in τ b the Boolean state variables having a transition function which is neither the identity nor constant. The loop τ b can be approximated by the transition τ ′ b where β 0 and β 2 correspond to b 0 and b 2 manipulated as Boolean inputs:

Table 1 :

 1 Experimental comparison between Aspic, nbACCel and Nbac.

			Aspic	nbACCel	Nbac
			vars size	time	size time size time
		Gate 1	4/4/2 7	?	5 0.73	24	?
		Escalator 1	5/4/2 12 0.14 (0.04) 9 0.49	22	?
		Traffic 1	4/6/0 18 0.14 (0.01) 16 0.19	5	3.49
		Traffic 2	4/8/0 18	?	16 0.35	28	?
		LCM Quest 0a-1 7/2/0 7 0.04 (0.01) 5 0.04	5	0.05
		LCM Quest 0a-2 7/3/0 6 0.05 (0.01) 4 0.05	8	0.19
		LCM Quest 0b-1 10/3/0 19 0.08 (0.01) 12 0.08	9	?
		LCM Quest 0b-2 10/4/0 17 0.09 (0.01) 11 0.20	33	?
		LCM Quest 0c-1 15/4/0 28 0.17 (0.01) 16 0.16	8	0.86
		LCM Quest 0c-2 15/5/0 25 0.20 (0.05) 14 0.24	50 14.8
		LCM Quest 1-1 16/5/0 114 1.99 (0.48) 42 0.92	6	2.45
		LCM Quest 1-2 16/6/0 100	?	34	?	>156 >
		LCM Quest 1b-1 16/5/0 55 0.92 (0.04) 29 0.37	15	?
		LCM Quest 1b-2 16/5/0 45 0.76 (0.12) 23 0.47	61	?
		LCM Quest 2-1 17/6/0 247	c	82 7.84	9	12.8
		LCM Quest 2-2 17/7/0 198	>	62	?	>76 >
		LCM Quest 3-1 25/5/0 483 26.5 (14.4) 58 8.49	12 3.76
		LCM Quest 3-2 25/6/0 481	c	54	? >1173 >
		LCM Quest 3b-1 26/6/0 1724	>	170 43.8	14 19.1
		LCM Quest 3b-2 26/7/0 1710	>	162 >	>32 >
		LCM Quest 3c-1 26/6/0 1319	>	130 34.2	9	?
		LCM Quest 3c-2 26/7/0 1056	c	98	>	>70 >
		LCM Quest 3d-1 26/6/0 281	>	81 5.43	49	?
		LCM Quest 3d-2 26/7/0 266	c	73	?	446	?
		LCM Quest 3e-1 27/7/0 638	>	140 20.6	49	?
		LCM Quest 3e-2 27/8/0 514	>	110 6.46 >28 >
		LCM Quest 4-1 27/7/0 4482	>	386 186	9 50.1
		LCM Quest 4-2 27/8/0 3586	>	290 >	>6	>
	vars : Boolean state variables / numerical state variables / Boolean inputs
	size : number of locations of the CFG
	time : in seconds (Aspic: total time (time for analysis))
	?	: "don't know" (property not proved)
	>	: timed out after 600s
	c	: out of memory or crashed
	(Benchmarks on http://pop-art.inrialpes.fr/people/schramme/nbaccel/)

We assume here that Bool. inputs β have been encoded by non-determinism, see §2.3.

Over-approximated result: the actual polyhedron has more constraints.

http://www.3ds.com

⋆ This work was supported by the INRIA large-scale initiative Synchronics.


Wudage Melisachew

Chekol

Jérôme Euzenat

Pierre Genevès

Nabil Layaïda

A Benchmark for Semantic Web Query Containment, Equivalence and Satisfiability

Keywords: Reasoning, semantic web, SPARQL queries, RDFS, containment, equivalence, satisfiability, benchmark Raisonnement, web sémantique, requêtes SPARQL, RDFS, inclusion, équivalence, satisfaisabilité, référentiel de test

The problem of SPARQL query containment has recently attracted a lot of attention due to its fundamental purpose in query optimization and information integration. New approaches to this problem have been put forth, that can be implemented in practice. However, these approaches suffer from various limitations: coverage (size and type of queries), response time (how long it takes to determine containment), and the technique applied to encode the problem. In order to experimentally assess implementation limitations, we designed a benchmark suite offering different experimental settings depending on the type of queries, projection and reasoning (RDFS). We have applied this benchmark to three available systems using different techniques highlighting the strengths and weaknesses of such systems.

Introduction

Since its recommendation by W3C, SPARQL has come to widespread prominence in the semantic web world. Broad and diverse studies are being conducted in order to improve and extend this language. To this end, recently, static analysis of the language has attracted reasonable attention, due to its foundational advantages in query optimization, satisfiability and information integration. This problem has long been observed and extensively studied for relational database query languages. On the other side, in the semantic web, where data is stored sporadically, large datasets are being made available due to the rapid emergence of linked data, queries are executed at remote endpoints, it is obvious that static analysis of SPARQL queries is relevant. Beyond this, in SPARQL 1.1 federated queries are introduced, these are queries that are evaluated at several remote endpoints and the final result is merged at the sender's premises. Thus, checking the satisfiability of these queries before sending them to the remote endpoint saves communication time. Furthermore, often queries are embedded in programs (Java, C++, and other programming languages), static analysis is useful to avoid runtime errors in these settings.

Static analysis covers containment, equivalence and satisfiability. Several studies of these problems have been carried out for different query languages: from conjunctive queries in relational databases, conjunctive queries in description logic, to SPARQL queries most recently. These studies are often supported by sound mathematical theorems and complexity results. However, a shortcoming of these studies is that they have little or no experimental evaluation. To overcome this shortcoming, we test the containment and equivalence of tree-structured SPARQL queries using a prototype implementation.

In general, a query is referred to as cyclic if the graph structure induced from the query is cyclic. It has been long noted that cyclic queries contribute to a further jump in the complexity of containment and equivalence problems. Most notably, Chandra and Merlin 1977 [START_REF] Chandra | Optimal Implementation of Conjunctive Queries in Relational Data Bases[END_REF] proved that containment and equivalence of relational conjunctive queries is NP-complete. However, this complexity reduces to P if the queries are acyclic [START_REF] Bernstein | Using semi-joins to solve relational queries[END_REF][START_REF] Yannakakis | Algorithms for acyclic database schemes[END_REF]. Further, the study in [START_REF] Calvanese | Conjunctive Query Containment and Answering under Description Logics Constraints[END_REF] demonstrated that containment of DLR (description logics with n-ary relations) conjunctive queries is double exponential but this complexity bound reduces to exponential if the query on the right-hand side of the containment has a tree structure. In other words, cycles among the non-distinguished variables contribute to a further jump in containment and equivalence complexity. Meanwhile, we observed that most of the queries currently used are acyclic. Hence, considering acyclic query containment is relevant.

The overall purpose of this paper is designing a benchmark tailored for tree-structured queries and evaluating the performance of the current state-of-the-art using this benchmark. In previous work [START_REF] Chekol | SPARQL query containment under RDFS entailment regime[END_REF] and [START_REF]SPARQL query containment under SHI axioms[END_REF], we developed techniques for encoding queries and schema axioms into the µ-calculus [START_REF] Kozen | Results on the propositional µ-calculus[END_REF] in order to determine the containment of SPARQL queries in the presence of schema axioms. As such, we have proved a double exponential upper bound for containment and equivalence problems. Interestingly, this bound reduces to exponential if the right-hand side query has a tree-structure. Using this encoding scheme and exponential time satisfiability solvers from [START_REF] Tanabe | A Decision Procedure for the Alternation-Free Two-Way Modal µ-calculus[END_REF] and [START_REF] Genevès | Efficient Static Analysis of XML Paths and Types[END_REF], we conduct an experiment to test the containment and equivalence of tree-structured SPARQL queries. In doing so, we modify the encoding in [START_REF] Chekol | SPARQL query containment under RDFS entailment regime[END_REF][START_REF]SPARQL query containment under SHI axioms[END_REF] in order to use the solver from [START_REF] Genevès | Efficient Static Analysis of XML Paths and Types[END_REF]. We compare the performance of these two satisfiability solvers, [START_REF] Tanabe | A Decision Procedure for the Alternation-Free Two-Way Modal µ-calculus[END_REF] and [START_REF] Genevès | Efficient Static Analysis of XML Paths and Types[END_REF]. Moreover, we also evaluate the performance of the subsumption and equivalence solver from [START_REF] Letelier | Static analysis and optimization of semantic web queries[END_REF]. However, as it is not an exponential time solver like the other two ( [START_REF] Tanabe | A Decision Procedure for the Alternation-Free Two-Way Modal µ-calculus[END_REF] and [START_REF] Genevès | Efficient Static Analysis of XML Paths and Types[END_REF]), we judge its performance on its own. Outline: after presenting the foundations of RDF(S) and SPARQL ( §2), we provide an in depth analysis of the structure of benchmark ( §3), followed by a description of the current state-of-the-art of query containment systems ( §4), using these systems we conduct experiments and explain the results ( §5). We finalize this study with a summary concluding remarks ( §7).

Preliminaries

We present the foundations of RDF, schema language SHI, and Tree-structured SPARQL queries.

RDF

Resource Description Framework (RDF) is a W3C standard language to create machine-readable content in the semantic web. RDF describes resources using a directed graph with a subject node connected to an object node and is labelled by a predicate. The subject, predicate and object make up a triple and a set of triples form a graph.

Example 1 An RDF graph that models a university domain. givesCourse domain Person.

RDFS

RDF has a simple schema language called RDF Schema (RDFS) that enables to express concept and property hierarchies as well as typing restrictions. In this work, we consider a benchmark setting containing the containment problem under the presence of core RDFS axioms namely subclass (sc), subproperty (sp), domain (dom), and range (range). Nonetheless, RDFS lacks some useful constructs (negation, inverse properties, existential concept and so on) in order to be a complete schema language. Since a description logic fragment of RDFS is a subset of SHI, we consider it for this study.

SHI

RDF has a simple schema language called RDF Schema (RDFS) that allows to express concept and property hierarchies as well as typing restrictions. Nonetheless, RDFS lacks some useful constructs (negation, inverse properties, existential concept and so on) in order to be a complete schema language. Since a description logic fragment of RDFS is a subset of SHI, we consider it for this study. We use an abstract syntax that can be easily translated into the µ-calculus.

Definition 1 A query pattern q is inductively defined as follows :

q ::= UBV × UV × UBLV | q 1 . q 2 | {q 1 } UNION {q 2 } | q 1 OPTIONAL {q 2 }
Example 3 illustrates this. We refer the readers to [START_REF] Prud | SPARQL query language for RDF[END_REF] for a formal presentation and semantics of SPARQL.

Example 3 Consider the following queries, taken from the benchmark, that retrieve students' information from the university dataset in Example 1.

Select all students' information.

SELECT ?x ?y ?z ?t ?ssn ?a ?sex ?e ?d ?c WHERE { Q7a ?x a :Student . ?x :name ?y . ?x :nickName ?z . ?x :telephone ?t . ?x :ssn ?ssn . ?x :age ?a . ?x :sex ?sex . ?x :emailAddress ?e . ?x :memberOf ?d . ?x :takesCourse ?c . } Select master students' information.

SELECT ?x ?y ?z ?t ?ssn ?a ?sex ?e ?d ?c WHERE { Q7b ?x a :Student . ?x :name ?y . ?x :nickName ?z . ?x :telephone ?t . ?x :ssn ?ssn . ?x :age ?a . ?x :sex ?sex . ?x :emailAddress ?e . ?x :memberOf ?d . ?x :takesCourse ?c . ?x :masterDegreeFrom ?master . } Definition 2 (Containment) Given a set of RDFS axioms S and queries Q 1 and Q 2 with the same arity, Q 1 is contained in Q 2 with respect to S, denoted Q 1 C Q 2 , if and only if the answers of Q 1 are included in the answers of Q 2 for every graph G satisfying S.

Example 4 From the queries in Example 3, Q7b Q7a and Q7a Q7b.

In order to benchmark and assess the current state-of-the-are, for this study, we have identified a class of SPARQL queries called tree-structured queries. These are queries that have a tree structure when seen as a graph. The following section introduces this notion.

Tree-structured SPARQL Queries

In relational databases, Bernstein and Chiu [START_REF] Bernstein | Using semi-joins to solve relational queries[END_REF] classified queries into two types: tree (is an undirected graph in which any two vertices are connected by exactly one simple path) and cyclic queries. An algorithm to decide whether a query is cyclic or not was presented in their paper. This algorithm is based on the idea of representing queries as hypergraphs. Infact, queries have often been considered as hypergraphs (see [START_REF] Chekuri | Conjunctive query containment revisited[END_REF][START_REF] Bernstein | Using semi-joins to solve relational queries[END_REF] for instance). It is possible to represent queries as hypergraphs where the nodes of the hypergraph are the variables and constants in the query. There is one hyperedge corresponding to each query subgoal that includes the variables and constants occurring in that subgoal. These studies proved that (Boolean) conjunctive query evaluation, while NP-hard in general, is polynomial in case of acyclic queries, i.e., queries whose associated hypergraphs are acyclic [START_REF] Yannakakis | Algorithms for acyclic database schemes[END_REF]. This distinction of queries as tree and cyclic has its advantages: for example, the evaluation of acyclic (Boolean) conjunctive queries is highly parallelizable [START_REF] Gottlob | The complexity of acyclic conjunctive queries[END_REF].

Borrowing the same notion from databases, we propose to view SPARQL queries as graphs. More specifically, a SPARQL query is represented as a bipartite graph, with two kinds of nodes: triple nodes and terms nodes (are URIs, blank nodes, and literals). Using this graph, one is able to determine whether a query is cyclic or not, a formal definition is given below. Definition 3 (Cyclic Query) A SPARQL query is referred to as cyclic if and only if a graph constructed from the query patterns is cyclic and acyclic otherwise. To the best of our knowledge, no experimental work has been conducted to verify how many of real world queries are acyclic or cyclic. To answer this question, we analysed the DBpedia (http://dbpedia.org) query log and obtained 378530 real world queries, out of which 15.8% were syntactically incorrect. Using the remaining 74.2%, we tested the cyclicness and acyclicness of queries and found out that: more than 87% of semantic web queries, as visible through DBpedia logs, are acyclic, i.e., a graph constructed from query elements is acyclic, and the remaining 13% are cyclic. This lays the foundation that acyclic queries make up a major part of the real world queries, thus, their separate study is fundamental. Detailed results on the analysis of the structure of queries (tree, directed acyclic graph (DAG), and cyclic) are presented in Table 2

Benchmark

In this section, we present the query containment setup, structure of the benchmark suite and the benchmark description.

Query Containment Setup

Query containment is the problem of determining if the result of one query is included in the result of another for any RDF graph. Its advantages are broad: query optimizations, information integration, satisfiability for instance. A test case for containment comprises two queries Q 1 and Q 2 , and an optional schema S. The query containment solver (QC solver) produces yes or no answers, i.e., yes if Q 1 is contained in Q 2 and no otherwise. A general workflow diagram designed for this purpose is illustrated in Figure 2.

Q 1 Q 2 S QC Solver Q 1 S Q 2 ?
Figure 2: General workflow of query containment test

Structure of the Benchmark

The four key requirements of a benchmark laid out by the benchmark handbook [START_REF] Gray | Benchmark handbook: for database and transaction processing systems[END_REF] are: understandability i.e., the queries and hence axioms should be understandable, scalability, portability i.e., being able to run on different platforms, and finally relevance i.e., testing typical operations such as joins, disjunctions, and typing restrictions. Thus, we designed the benchmark following these principles.

Benchmark queries are chosen according to the following criteria: projection (or no projection), operator nesting, number of connectives (joins and disjunctions), and requiring RDFS reasoning. Our queries also vary in general characteristics like selectivity, query size, and different types of joins. One thing that should be noted is that, the benchmark criteria are selected in line with the capacity of the current state-of-the-art. The benchmark contains three test suites:

-Union of Conjunctive Queries with Projection (UCQProj) this setting comprises 28 queries which have variables in the SELECT clause (aka distinguished variables) hence the name projection. In addition to the projection, the queries are chosen according to selectivity, number of conjunction and unions, and size (in terms of the number of connectives). For instance, consider the queries in Example 3 which contain 9 (Q7a) and 10 (Q7b) conjunctions respectively. This test suite assesses containment solvers that support projection and union of conjunctive queries.

-Conjunctive Queries with No Projection (CQNoProj) this suite is designed to address the containment of basic graph patterns (conjunctive queries). It contains 20 queries differing in the number of conjunctions and variables they contain. This test suite is developed for containment solvers that do not support projection of variables in queries. Also, in this test suite, disjunctive (union) queries are not allowed.

-Union of Conjunctive Queries under RDFS reasoning (UCQrdfs) this test suite, as its name implies, is designed for containment of queries that require RDFS reasoning. Thus, a set of RDFS schemas are selected in order to be able to test containment in the presence of these constraining schemas. The four schemas cover concept and property hierarchies, and typing (domain and range) restriction axioms. Along with the schemas, the test suite contains 18 queries differing in the: number of operators, number of distinguished variables, and having projection (or no projection).

Benchmark Description

We have identified three test suites: UCQProj, CQNoProj, and UCQrdfs, for containment of treestructured union of conjunctive SPARQL queries under RDFS axioms. In this section, we detail each of these test suites. The benchmark is available on line at http://sparql-qc-bench. inrialpes.fr/.

UCQProj

In this test suit, there are 28 test cases (p1 -p28 shown in Table 2). Each test case comprises two tree-structured union of conjunctive queries. The test cases differ in the number of distinguished variables (Dvars) and connectives (conjunction or union). To this end, in the table, the size of the queries measured in terms of the number of connectives is depicted. Tests are carried out using this benchmark with the solvers AFMU and TreeSolver.

CQNoProj

as discussed in Section 3.2, this test suite contains conjunctive queries with no projection (denoted as nop followed by case number, shown in Table 3) is designed for containment of basic graph patterns. For this case, we have identified 20 different test cases (nop1 -nop20), each case represents containment between two queries. All the test cases in this setting are shown in Table 3, along with the number of connectives and variables in the queries. In query containment under RDFS reasoning, there are 28 test cases (rdfs1 -rdfs28 of Table 5). In comparison to the test cases in UCQProj and CQNoProj setting, the query sizes are small. Each test case is composed of two tree-structured UCQs and a schema.

C1 Q9a Q9c 0 0 0 1 1 rdfs2 C1 Q9c Q9a rdfs3 C1 Q9a Q9b 0 0 0 0 1 rdfs4 C1 Q9b Q9a rdfs5 C1 Q9b Q9c 0 0 0 1 1 rdfs6 C1 Q9c Q9b rdfs7 C1 Q9d Q9e 4 4 0 0 1 rdfs8 C1 Q9e Q9d rdfs9 C2 Q10b Q10d 0 0 0 0 1 rdfs10 C2 Q10d Q10b rdfs11 C2 Q10e Q10b 1 0 0 0 1 rdfs12 C2 Q10b Q10e rdfs13 C3 Q11b Q11c 0 0 0 0 1 rdfs14 C3 Q11c Q11b Axiom AND UNION Dvars rdfs15 C3 Q11b Q11d 0 0 0 0 1 rdfs16 C3 Q11d Q11b rdfs17 C3 Q11c Q11d 0 0 0 0 1 rdfs18 C3 Q11d Q11c rdfs19 C3 Q11b Q11a 0 0 0 0 1 rdfs20 C3 Q11a Q11b rdfs21 C3 Q11e Q11a 0 0 1 0 1 rdfs22 C3 Q11a Q11e rdfs23 C4 Q13a Q13b 3 1 3 1 2 rdfs24 C4 Q13b Q13a rdfs25 C4 Q13a Q13c 3 1 3 1 2 rdfs26 C4 Q13c Q13a rdfs27 C4 Q13b Q13c 3 1 3 1 2 rdfs28 C4 Q13c Q13b

Tested Query Containment Solvers

In this section, we present three state-of-the-art query containment solvers. These systems are tested using the benchmark suite.

AFMU

AFMU, stands for Alternation Free two-way MU-calculus [START_REF] Tanabe | A Decision Procedure for the Alternation-Free Two-Way Modal µ-calculus[END_REF], is a satisfiability (SAT) solver for the alternation fragment of µ-calculus. It is a prototype implementation which determines the satisfiability of a µ-calculus formula by producing a yes or no answer.

TreeSolver

TreeSolver: the XML tree logic solver1 performs static analysis of XPath queries which comprises containment, equivalence and satisfiability. To perform these tasks, the solver translates XPath queries into µ-calculus formulas and then it tests the unsatisfiability of the formula. 3, used for experimentation. This wrapper, together with the solvers, is used to determine query containment.

SPARQL-algebra

SPARQL-algebra is an implementation of SPARQL query subsumption and equivalence based on the theoretical results in [START_REF] Letelier | Static analysis and optimization of semantic web queries[END_REF]. This implementation supports AND and OPTIONAL queries with no projection. An on line version of the solver is available at http://db.ing.puc.cl/ sparql-algebra/.

A summary of the features supported by state-of-the-art of query containment solvers is presented in Table 6.

Out of the three systems used in the experiments, AFMU and TreeSolver are µ-calculus satisfiability solvers that need an intermediate system that translates queries into formulas (based on previous works) to determine containment whereas SPARQL-algebra is self contained.

Using the containment solvers we designed an experimental setup that comprises several software components. This setup is illustrated in Figure 4, it is mainly based on the theoretical results developed in our previous works [START_REF] Chekol | SPARQL query containment under RDFS entailment regime[END_REF][START_REF]SPARQL query containment under SHI axioms[END_REF][START_REF] Chekol | PSPARQL query containment[END_REF]. The components of the architecture are detailed as follows:

• Jena SPARQL parser2 -Jena is an open source semantic web framework for Java. It provides an API, ARQ, for parsing and evaluating SPARQL queries. We used this API to parse queries and create µ-calculus formulas.

• Mu-calculus Encoder -this component consists of a package for graph construction, cycle detection, and formula creation from queries and axioms (η(S)

∧ A(Q 1 ) ∧ ¬A(Q 2 )
). It has two parts, the first component produces the formulas for the solver AFMU and the second one computes the formulas for the TreeSolver.

• SAT solvers -once the formulas are created, satisfiability solvers are used to determine the unsatisfiability of the formula and hence containment. Presently, for tree-structured queries, two SAT solvers, AFMU and TreeSolver, are available.

Next, experimental results produced using the benchmark are explained.

Q 1 Q 2 S ARQ Parser ARQ Parser µ-calculus Encoder η(S)∧A(Q 1 )∧ ¬A(Q 2 )
Jena parser SAT solver

Yes No

Figure 3: Query containment wrapper around SAT solvers

Experimentation

All the experiments were conducted in a MacBook Pro V10.6.8, Intel Core i7, 2GHz processor speed, and 4GB memory. We carried out two sets of experiments. The first one involves cycle detection -this is done in order to assess the relevance and the percentage of tree-structured real world queries thereby underlining the purpose of the study. The second one involves three experiments on the containment of tree-structured UCQs. The details are explained in the following sections. It is beyond the scope of this paper to provide an in-depth comparison of existing solvers. Rather, we want to give first insights into the state-of-the art and highlight deficiencies of engines based on the benchmark outcome.

Q 1 Q 2 S ARQ Parser SPARQL- algebra µ-calculus Encoder 1 µ-calculus Encoder 2
Jena parser AFMU TreeSolver

Yes No

Figure 4: Experimental setup for query containment test

Inria

We conducted tests to compare the performances of the containment solvers AFMU, Tree-Solver and SPARQL-algebra.

1st Experimental setting: UCQProj

The test suite used for this experiment is UCQProj (see Section 3.3.1). We compared two systems: TreeSolver and AFMU. As can be seen in Figure 5, the TreeSolver outperforms AFMU in all of the benchmark test cases. Further, in one of the cases (p16), where the queries have more than 9 joins, AFMU was not responsive after running 1.5 hours. This behaviour is not unique to AFMU, as whenever there are more than 10 joins in the query, the same situation is observed in the TreeSolver. For instance, for the test case p16, the TreeSolver was non-responding in some runs and in some others it eventually runs out of space.

2nd Experimental setting: CQNoProj

In the benchmark, the test suite used for this experiment is CQNoProj (see Section 3.3.2). In light of the fact that, SPARQL-algebra supports only CQs with no projection, we deemed it as necessary to evaluate its performance against TreeSolver and AFMU. The results of this comparison are depicted in Figure 6. From the graph, it can be seen that the performance of SPARQL-algebra is much faster than that of AFMU or TreeSolver. In fact, this comes as no surprise, due to the reason that the latter are exponential time solvers whereas the first is polynomial time solver. Note also that, whenever containment is determined between queries that contain more than 10 joins, Tree Solver and AFMU become non-responsive (do not terminate).

3rd Experimental setting: UCQrdfs

The test suite used for this experiment is UCQrdfs (cf. Section 3.3.3). In this experiment, the containment of tree-structured UCQs under RDFS reasoning is tested. Three approaches that are used to encode the containment problem under RDFS axioms is presented in [START_REF] Chekol | SPARQL query containment under RDFS entailment regime[END_REF]. For this task, we have chosen the schema encoding approach -amounts to encoding the schema axioms as µ-calculus formulas [START_REF] Chekol | SPARQL query containment under RDFS entailment regime[END_REF].

The results presented in Figure 7 show that except for one case (rdfs13) the TreeSolver out performs AFMU. In fact, like the other two experimental settings, when the query size gets larger both solvers either take a substantial amount of time or run out of space or become non-responsive. In summary, all the solvers under all of the experimental settings responded positively i.e., they all determined containment correctly except for SPARQL-algebra. It responded negatively, in test cases nop7 and nop8 cf. Table 3, when blank nodes are used in the queries.

Discussion

As it can be observed in the experiments, a lot needs to be done in order to alleviate the shortcomings of the current systems. Here, we discuss the pros and cons of these systems.

AFMU

In terms of capacity AFMU, is able determine containment of acyclic UCQs under ontological axioms. Specially, for queries of reasonable size, the solver determined their containment correctly. The problem is that when queries have large size (for instance, more than 8 joins), the solver takes more than 1/2 hour or becomes non-responsive. This is shown in the result graph in Figure 5 for test cases p15 and p16, also in Figure 6 for test cases fnop15 and nop16. However, the implementation of this solver is very poor, even the authors had documented that it can be improved so as to have faster response times. In fact, this is reflected in the experiments that it has the worst performance out of the three. Therefore, reimplementing or improving the solver should be noted as a perspective.

Inria

In another note, to be able to determine containment of general UCQs (beyond the treestructured ones), an extension of the solver is compulsory.

TreeSolver

this solver works well with tree-structured queries and RDFS reasoning if the queries have reasonable size, it has an on line version, and it also supports static analysis of XPath queries among others. Its limitations are similar to that of AFMU: no support for cyclic queries, and queries of large size (for example, nop16 and p16).

SPARQL-algebra

the advantages of this solver compared to the others are that, it supports subsumption of OP-TIONAL query patterns and also cyclic CQs. Its limitations include: no support for distinguished variables, i.e., no projection, UNION, and reasoning. Moreover, basic graph patterns (AND queries) with blank nodes are not supported, in fact, this is reflected in the experiment cf. section 5.2 test cases nop7 and nop8 in Figure 6.

In this paper, we have first studied the profile of real-world queries with respect to theoretical characterisation and found that (1) a large part of these queries are acyclic, and (2) those parts that either contain projections (effective SELECT) or not, are significant. From this, we have designed a containment benchmark made of three first query containment test suites testing projection, no projection and RDFS reasoning.

We have applied these to existing containment solvers (AFMU, TreeSolver and SPARQLalgebra). Obviously, current µ-calculus solvers are not optimised for conjunctive queries without projection which are better dealt with by SPARQL-algebra. Hence, so far the best strategy is to use one solver when queries are conjunctive and do not have projection and another when they have projection, union and axioms.

These analyses confirm that our benchmarks are well-suited for pinpointing the theoretical shortcomings of containment solvers. These experimental results show that the current state-ofthe-art is at its early stage and requires improvement and new ways to determine containment and equivalence of queries, in order to become a useful tool for query optimizers. In the future, we plan to work towards this direction.

Additionally, we will improve and extend this benchmark, e.g., adding other test suites designed for containment of queries under expressive description logic axioms such as OWL2.

Related Works

Recently, static analysis and optimization of SPARQL queries has attracted widespread attention, notably [START_REF] Chekol | SPARQL query containment under RDFS entailment regime[END_REF][START_REF]SPARQL query containment under SHI axioms[END_REF][START_REF] Chekol | PSPARQL query containment[END_REF][START_REF] Letelier | Static analysis and optimization of semantic web queries[END_REF] for static analysis and [START_REF] Groppe | Optimization of SPARQL by using coreSPARQL[END_REF][START_REF] Stocker | SPARQL Basic Graph Pattern Optimization Using Selectivity Estimation[END_REF][START_REF] Schmidt | Foundations of SPARQL Query Optimization[END_REF][START_REF] Letelier | Static analysis and optimization of semantic web queries[END_REF] for optimization. These studies have grounded the theoretical aspects of these fundamental problems. However, to the best of our knowledge, there is only one implementation from [START_REF] Letelier | Static analysis and optimization of semantic web queries[END_REF] and it supports only conjunction and OPTIONAL queries with no projection.

On the other hand, in databases, containment of union conjunctive queries (UCQs) is well studied and has a well know NP-complete complexity. The importance of the study of this problem goes beyond the field of databases, it has its fair share from the description logic community. Many of the works, from description logics, concentrated on the problem of query answering as containment follows from it. These works, have sound theoretical proofs, algorithms, mathematical explanations, and so on. However, they lack an implementation (or experimentation) of their approaches.

In line with CQs in databases and description logic worlds, we have regular path querieslanguages that are used to query arbitrary length paths in graph databases -in semi structured data. Like CQs, they have been used and studied widely. They are different from CQs in that, they allow recursion by using regular expression patterns. The problem of containment has been addressed for extensions of this language. In this regard, a prominent language used in semi-structured data is XPath. This language has been studied extensively over the last decade. These studies are all round, from extending or limiting to static analysis. Static analysis of XPath queries has been studied in [START_REF] Genevès | Efficient Static Analysis of XML Paths and Types[END_REF], encompassing containment, equivalence, coverage, and satisfiability of XPath queries. This work is motivated by [START_REF] Genevès | Efficient Static Analysis of XML Paths and Types[END_REF] in that the approach to study these problems using a graph logic and providing an implementation which has been put to practice.

Finally, various SPARQL query evaluation performance benchmarks have been proposed [START_REF] Bizer | Benchmarking the performance of storage systems that expose SPARQL endpoints[END_REF][START_REF]The Berlin SPARQL benchmark[END_REF][START_REF] Schmidt | SPˆ2Bench: a SPARQL performance benchmark[END_REF], but no SPARQL query containment benchmark to our knowledge.

Conclusion

In this paper, we have first studied the profile of real-world queries with respect to theoretical characterisation and found that (1) a large part of these queries are acyclic, and (2) those parts that either contain projections (effective SELECT) or not, are significant. From this, we have designed a containment benchmark made of three first query containment test suites testing projection, no projection and RDFS reasoning.

We have applied these to existing containment solvers (AFMU, TreeSolver and SPARQLalgebra). Obviously, current µ-calculus solvers are not optimised for conjunctive queries without projection which are better dealt with by SPARQL-algebra. Hence, so far the best strategy is to use one solver when queries are conjunctive and do not have projection and another when they have projection, union and axioms.

These analyses confirm that our benchmarks are well-suited for pinpointing the theoretical shortcomings of containment solvers. These experimental results show that the current state-ofthe-art is at its early stage and requires improvement and new ways to determine containment and equivalence of queries, in order to become a useful tool for query optimizers. In the future, we plan to work towards this direction.

Additionally, we will improve and extend this benchmark, e.g., adding other test suites designed for containment of queries under expressive description logic axioms such as OWL2.

Example 5

 5 Figure 1: Cyclic query

Figure 5 :

 5 Figure 5: Results for UCQProj test suite (logarithmic scale)

Figure 6 :Figure 7 :

 67 Figure 6: Results for CQNoProj test suite (logarithmic scale)

  Example 2 An SHI schema modeling a university domain is shown in Example 1. UBV × UV × UBLV, with V a set of variables disjoint from UBL (URIs, Blank nodes and Literals), is called a triple pattern. Triple patterns grouped together using operators AND (.) and UNION form query patterns. We do not consider OPTIONAL and FILTER query patterns because containment over the full SPARQL is undecidable.

	PostgradStudent Student UndergradStudent Student
	Department Faculty Faculty University
	Staff Student	⊥
	Professor Person Student Person
		Chair ≡ Person ∃headOf.Department
		Student ≡ Person ∃takesCourse.Course
		Professor ≡ Person ∃givesCourse.Course
	∃headOf.	Professor takesCourse ≡ givesCourse -
		Staff AdministrativeStaff Professor
	2.3 SPARQL
	SPARQL is W3C recommended query language based on simple graph patterns. It allows vari-
	ables to be bound to components in the input RDF graph. In addition, operators akin to
	relational joins, unions, left outer joins, selections, and projections can be combined to build
	more expressive queries. Queries are formed from query patterns which in turn are defined in-
	ductively from triple patterns: a tuple t ∈
			Inria

Table 1 :

 1 .3.1.Beyond the cyclic and acyclic tests, we checked how many of the queries have projection, i.e., not all variables in the graph pattern are distinguished, or not. In this setting, we found out Cycle detection that 63.4% of the queries have projection and 36.6% of the queries have no projection. Further, all of the cyclic queries have projection and out of the tree-structured ones, 65% of the queries have projection and the rest have no projection. These results motivate the design principles for the benchmark.

	Inria

Table 3 :

 3 CQNoProj 3.3.3 UCQrdfs in this test suite, there are 4 different schemas, C1-C4 in Table4. The table also shows that the type and number of axioms used in each schema.

	Inria

Table 4 :

 4 Axiom types for each of the four schemas.

	Schema Axiom types
	C1	subclass (2)
	C2	domain (1) and range (1)
	C3	subproperty (2), subclass (1) and domain (1)
	C4	subclass (1)
	Axiom	AND	UNION	Dvars
	rdfs1

Table 5 :

 5 UCQrdfs

Table 6 :

 6 Unlike the A comparison of features supported by current systems AFMU solver, the unsatisfiability test is performed in a time of 2 O(n) whereas it is 2 O(n log n) for AFMU, where n is the size of the formula. The SAT solver component of this system is taken for our purpose.Around the SAT solvers, AFMU and TreeSolver, we have implemented a wrapper, depicted in Figure

		No projection	Projection	Reasoning
	CQ	AFMU, TreeSolver, AFMU, TreeSolver AFMU, TreeSolver
		SPARQL-algebra
	UCQ	AFMU, TreeSolver AFMU, TreeSolver AFMU, TreeSolver
	OPTIONAL	SPARQL-algebra	-	-
	Blank nodes AFMU, TreeSolver AFMU, TreeSolver AFMU, TreeSolver

RR n°8128

http://wam.inrialpes.fr/websolver/ Inria

http://jena.sourceforge.net/documentation.html RR n°8128