Wudage Melisachew
email: melisachew.chekol@inria.fr

Jérôme Chekol

Pierre Euzenat

Nabil Genevès

Layaïda

Chekol

Jérôme Euzenat
email: jerome.euzenat@inria.fr

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

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

SPARQL Query Containment Under SHI Axioms

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

Introduction

Access to semantic web data expressed in RDF (Resource Description Framework) may be achieved through querying. Currently, querying RDF graphs is done mainly with the SPARQL query language. It has been a source of research from various perspectives, in particular for extending the language and optimizing queries. Querying RDF graphs with SPARQL proceeds by matching graph patterns, i.e., triple patterns connected to form graphs by means of joins expressed using several occurrences of the same variable. Since queries in the semantic web are evaluated over huge RDF graphs, optimizations are necessary in order to find minimal queries to reduce the computational cost of query evaluation.

Query optimization aims at improving the runtime performance of query evaluation. Studies have contributed to query optimization using rewriting rules in particular in the relational algebra for databases [START_REF] Ioannidis | Query Optimization[END_REF][START_REF] Chandra | Optimal Implementation of Conjunctive Queries in Relational Data Bases[END_REF]. Similar approaches have also been applied to SPARQL [START_REF] Schmidt | Foundations of SPARQL Query Optimization[END_REF]. These works, however, need at some point to prove the correctness of query optimization, i.e., the semantics of the optimized query is the same as the original one. In other words, the results of a given query are exactly the same as the optimized one regardless of the considered database. This can be reduced to query containment. Thus, query containment plays a vital role in optimization. It can be defined as determining if the result of one query is included in the result of another one for any RDF graph. In addition, query containment can be of independent interest for performing other optimizations. For example, if a query q is contained in q , then q can be evaluated on the materialized view of q rather than on the whole data graph. To the best of our knowledge, the problem of SPARQL query containment (under a schema) has not been covered in the literature.

The aim of this paper is to address SPARQL query containment under a DL schema (the schema is formulated within the fragments of SHIQ). We apply an approach which has already been successfully applied for XPath [START_REF] Genevès | Efficient Static Analysis of XML Paths and Types[END_REF]. SPARQL is interpreted over graphs, hence we encode it in a graph logic, specifically the alternation-free fragment of the µ-calculus [START_REF] Kozen | Results on the propositional µ-calculus[END_REF] with converse and nominals [START_REF] Tanabe | A Decision Procedure for Alternation-Free Modal µ-calculi[END_REF] interpreted over labeled transition systems. We show that this logic is powerful enough to deal with query containment for the fragment of SPARQL considered here in the presence of RDFS and SHI (schema) axioms. Furthermore, this logic admits exponential time decision procedures that is implemented in practice [START_REF] Tanabe | A Decision Procedure for Alternation-Free Modal µ-calculi[END_REF]. Hence, our approach opens a way to use this implementation.

We introduce a translation of RDF graphs into transition systems and SPARQL queries and schema axioms into µcalculus formulae. Then, we show how query containment in SPARQL can be reduced to unsatisfiability in the µ-calculus. We prove a double exponential upper bound for the problem. An additional benefit of using a µ-calculus encoding is to take advantage of fixpoints and modalities for encoding recursion. They allow to deal with natural extensions of SPARQL such as path queries [START_REF] Alkhateeb | Extending SPARQL with regular expression patterns (for querying RDF)[END_REF] or queries modulo RDF Schema.

Preliminaries

RDF is a language used to express structured information on the Web as graphs. We present a compact formalization of RDF [START_REF] Hayes | RDF Semantics[END_REF]. Let U, B, and L be three disjoint infinite sets denoting the set of URIs (identifying a resource), blank nodes (denoting an unidentified resource) and literals (a character string or some other type of data) respectively. We abbreviate any union of these sets as for instance, UBL = U ∪ B ∪ L. A triple of the form (s, p, o) ∈ UB × U × UBL is called an RDF triple. s is the subject, p is the predicate, and o is the object of the triple. Each triple can be thought of as an edge between the subject and the object labelled by the predicate, hence a set of RDF triples is often referred to as an RDF graph. RDF has a model theoretic semantics [START_REF] Hayes | RDF Semantics[END_REF].

Example 1 (RDF Graph). Consider 8 triples of an RDF graph about writers and their works (all identifiers correspond to URIs, :b is a blank node):

{(Poe,wrote,thegoldbug), (Baudelaire,translated,thegoldbug), (Poe, wrote, theraven), (Mallarmé, translated, theraven), (theraven, type, Poem), (Mallarmé, wrote, :b), ( :b, type, Poem), (thegoldbug, type, Novel) } RDFS (RDF Schema) may be considered as a simple ontology language expressing subsumption relations between classes or properties [START_REF] Hayes | RDF Semantics[END_REF]). Technically, this is an RDF vocabulary used for expressing axioms constraining the interpretation of graphs. The RDFS vocabulary and its semantics are given in [START_REF] Hayes | RDF Semantics[END_REF]).

For our purpose, we consider four RDFS axioms: subclass, subproperty, domain and range. The DL fragment of RDFS is a subset of SHI. Hence RDFS axioms can be translated into SHI axioms. SHI Description logics are fragments of first-order logic that model a domain of interest in terms of concepts and roles (Baader et al. 2007). For this study, we consider the description logic SHI which is a fragment of SHIQ (Horrocks, [START_REF] Horrocks | Practical reasoning for expressive description logics[END_REF]. The satisfiability of SHIQ logic is proved to be EXPTIME. We assume standard notation for the syntax and semantics of SHI knowledge bases. We refer the reader to [START_REF] Horrocks | Practical reasoning for expressive description logics[END_REF] for the semantics of SHI.

Syntax In SHI, concepts and roles are formed according to the following syntax:

C ::= ⊥ | | A | ¬C | C 1 C 2 | C 1 C 2 | ∃r.C | ∀r.C r ::= p | p -
p denotes an atomic role, ⊥ represents an empty concept, A denotes an atomic concept, C denotes a complex concept, and r denotes a complex role which is an atomic role or its inverse.

SHI Axioms:

The TBox is a finite set of axioms consisting of concept inclusions (C 1 C 2 ), role inclusion (r 1 r 2 ), and transitivity trans(r) axioms.

SPARQL is a W3C recommended query language for RDF [START_REF] Prud'hommeaux | SPARQL Query Language for RDF[END_REF]. It is based on the notion of query patterns defined inductively from triple patterns: a tuple t ∈ UBV × UV × UBLV, with V a set of variables disjoint from UBL, is called a triple pattern. Triple patterns grouped together using SPARQL operators AND and UNION form query patterns (or graph patterns)1 . We use an abstract syntax that can be easily translated into the µ-calculus. Definition 1 (Query Pattern). A query pattern q is inductively defined as follows :

q ::= t ∈ UBV × UV × UBLV | q 1 AND q 2 | q 1 UNION q 2
We focus on SELECT queries which are the core of SPARQL queries. Definition 2. A SPARQL SELECT query is a query of the form q( -→ w ) where -→ w is a tuple of variables in V which are called distinguished variables, and q is a query pattern.

Example 2 (SPARQL queries). Consider the following queries q 1 (?x) and q 2 (?x) on the graph of Example 1: SPARQL has multiset (or bag) semantics, however, when dealing with containment, we consider set semantics. This is due to the undecidability of union of conjunctive queries under bag semantics (?).

The semantics of SPARQL queries is given by a partial mapping function ρ from V to UBL. The domain of ρ, dom(ρ), is the subset of V on which ρ is defined. Two mappings ρ 1 and ρ 2 are said to be compatible if ∀x ∈ dom(ρ 1 ) ∩ dom(ρ 2 ), ρ 1 (x) = ρ 2 (x). Further, if ρ 1 and ρ 2 are compatible, then ρ 1 ∪ ρ 2 is also a mapping. The evaluation of query patterns over an RDF graph G is inductively defined as follows:

t G = {ρ | dom(ρ) = var(t) and ρ(t) ∈ G}
where var(t) is the set of variables occurring in t.

q 1 AND q

2 G = q 1 G 1 q 2 G q 1 UNION q 2 G = q 1 G ∪ q 2 G q{ - → w } G = π-→ w ( q G )
Where the projection operator π-→ w selects only those part of the mappings relevant to variables in -→ w .

Example 3. The answers to queries q 1 and q 2 , of Example 2, on graph G of Example 1 are respectively {P oe, M allarme} and {Baudelaire, P oe, M allarme}. Thus, q 1 G ⊆ q 2 G .

Beyond this particular example, the goal of query containment is to determine whether this holds for any graph. Definition 3 (Containment). Given a set of axioms C and two queries q and q with the same arity, q 1 is contained in q 2 with respect to C, denoted q C q , iff q G ⊆ q G for every graph G satisfying C. Definition 4 (Equivalence). Two queries q and q under a set of axioms C are equivalent, i.e., q ≡ C q iff q C q and q C q.

The evaluation of SPARQL queries is proved to be PSPACE-complete. However, the evaluation problem is NPcomplete for the fragment containing only AND and UNION query patterns [START_REF] Pérez | Semantics and complexity of SPARQL[END_REF].

RDF Graphs as Transition Systems

Before presenting the encoding of RDF graphs as transition systems over which the µ-calculus is interpreted, we introduce the syntax and semantics of the µ-calculus.

µ-calculus

The modal µ-calculus [START_REF] Kozen | Results on the propositional µ-calculus[END_REF]) is an expressive logic which adds recursive features to modal logic using fixpoint operators. The syntax of the µ-calculus is composed of countable sets of atomic propositions AP , a set of nominals N om, a set of variables Var, and a set of programs Prog for navigating in graphs. A µ-calculus formula, ϕ, can be defined inductively as follows:

ϕ ::= | ⊥ | p | X | ¬ϕ | ϕ ∨ ψ | ϕ ∧ ψ | a ϕ | [a]ϕ | µXϕ | νXϕ
where p ∈ AP, X ∈ V ar and a ∈ P rog is either an atomic program or its converse ā. The greatest and least fixpoint operators (ν and µ) respectively introduce general and finite recursion in graphs [START_REF] Kozen | Results on the propositional µ-calculus[END_REF]. The semantics of the µcalculus is given over a transition system, K = (S, R, L) where S is a non-empty set of nodes, R : P rog → 2 S×S is the transition function, and L : AP → 2 S assigns a set of nodes to each atomic proposition or nominal where it holds, such that L(p) is a singleton for each nominal p. For converse programs, R can be extended as R(ā) = {(s , s) | (s, s ) ∈ R(a)}. In addition, a valuation function V : Var → 2 S is used to assign a set of nodes to each variable. For a valuation V , variable X, and a set of nodes S ⊆ S, V [X/S ] is the valuation that is obtained from V by assigning S to X. The semantics of a formula, in terms of a transition system K (a.k.a. Kripke structure) and a valuation function, is represented by ϕ K V . The semantics of basic µ-calculus formulae is defined as follows:

K V = S p K V = L(p), p ∈ AP ∪ N om, L(p) is singleton for p ∈ N om X K V = V (X), X ∈ Var ¬ϕ K V = S\ ϕ K V ϕ ∧ ψ K V = ϕ K V ∩ ψ K V , ϕ ∨ ψ K V = ϕ K V ∪ ψ K V a ϕ K V = {s ∈ S | ∃s ∈ S.(s, s ) ∈ R(a) ∧ s ∈ ϕ K V } [a]ϕ K V = {s ∈ S | ∀s ∈ S.(s, s ) ∈ R(a) ⇒ s ∈ ϕ K V } µXϕ K V = {S ⊆ S | ϕ K V [X/S ] ⊆ S } νXϕ K V = {S ⊆ S | S ⊆ ϕ K V [X/S ] }
The next sections introduce a representation of RDF graphs as transition systems and queries as µ-calculus formulas.

Encoding of RDF graphs

An RDF graph is encoded as a transition system in which nodes correspond to RDF entities and RDF triples. Edges relate entities to the triples they occur in. Different edges are used for distinguishing the functions (subject, object, predicate). Expressing predicates as nodes, instead of atomic programs, makes it possible to deal with full RDF expressiveness in which a predicate may also be the subject or object of a statement. Definition 5 (Transition system associated to an RDF graph). Given an RDF graph, G ⊆ U B × U × U BL, the transition system associated to G, σ(G) = (S, R, L) over AP = UBL ∪ {s , s }, is such that:

• S = S ∪ S with S and S the smallest sets such that

∀u ∈ U G , ∃n u ∈ S , ∀b ∈ B G , ∃n b ∈ S , and ∀l ∈ L G , ∃n l ∈ S , • ∀t = (s, p, o) ∈ G, n s , n t ∈ R(s), n t , n p ∈ R(p),
and

n t , n o ∈ R(o), • L : AP → 2 S ; ∀u ∈ U G , L(u) = {n u }, ∀b ∈ B G , L(b) = S , L(s ) = S , ∀l ∈ L G , L(l) = {n l } and L(s ) = S , • ∀n t , n t ∈ S , n t , n t ∈ R(d).
The program d is introduced to render each triple accessible to the others and thus facilitate the encoding of queries. The function σ associates what we call a restricted transition system to any RDF graph. Formally, we say that a transition system K is a restricted transition system iff there exists an RDF graph G such that K = σ(G).

A restricted transition system is thus a bipartite graph composed of two sets of nodes: S , those corresponding to RDF entities, and S , those corresponding to RDF triples. For example, Figure 1 When checking for query containment, we consider two constraints: (i) the set of programs is fixed:

P rog = {s, p, o, d, s, p, ō, d}, and (ii) a model must be a restricted transition system. The last constraint can be expressed in the µ-calculus as follows: Proposition 1 (RDF restriction on transition systems). A formula ϕ is satisfied by some restricted transition system if and only if ϕ ∧ ϕ r is satisfiable by some transition system, i.e. ∃K r ϕ Kr = ∅ ⇐⇒ ∃K ϕ ∧ ϕ r K = ∅, where:

ϕ r = νX.θ ∧ κ ∧ (¬ d ∨ d X) in which θ = s s ∧ p s ∧ o s ∧ ¬ s ∧ ¬ p ∧ ¬ ō and κ = [s]ξ ∧ [p]ξ ∧ [o]ξ with ξ = (¬ s ∧ ¬ o ∧ ¬ p ∧ ¬ d ∧ ¬ d ∧ ¬ s s ∧ ¬ ō s ∧ ¬ p s).
The formula ϕ r ensures that θ and κ hold in every node reachable by a d edge, i.e. in every triple node. The formula θ forces each s node to have one and only one subject, predicate and object. The formula κ navigates from a s node to every reachable s node, and forces the latter not to be directly connected to other subject, predicate or object nodes.

If a µ-calculus formula ψ appears under the scope of a least µ or greatest ν fixed point operator over all the programs {s, p, o, d, s, p, ō, d} as, µX.ψ ∨ s X ∨ p X ∨• • • or νX.ψ∧ s X ∧ p X ∧• • • , then, for the sake of legibility, we denote the recursion components of the respective formulae as mu(X) for the µ recursion part and nu(X) for the ν recursion part. Thus, the formulae become µX.ψ ∨ mu(X) and νX.ψ ∧ nu(X).

SPARQL Query Containment

In this section, we encode queries and schema axioms as µcalculus formulas. Then, we reduce query containment under schemas to µ-calculus unsatisfiability and prove the correctness of this reduction.

Encoding Queries as µ-calculus Formulae

Queries are translated into µ-calculus formulas. The principle of the translation is that each triple pattern is associated with a sub-formula stating the existence of the triple somewhere in the graph. Hence, they are quantified by µ so as to put them out of the context of a state. In this translation, variables are replaced by nominals or some formula that are satisfied when they are at the corresponding position in such triple relations. A function called A is used to encode queries inductively on the structure of query patterns. AND and UNION are translated into boolean connectives ∧ and ∨ respectively. When encoding q q , we call q left-hand side query and q right-hand side query.

Encoding left-hand side query: the encoding of a lefthand side query q is done such that every term (distinguished and non-distinguished variables and constants) in the query becomes a nominal in the µ-calculus. Hence, the encoding of q is A(q) such that:

A((x, y, z)) = µX. s x ∧ p y ∧ o z ∨ mu(X) A(q 1 AND q 2 ) = A(q 1 ) ∧ A(q 2 ) A(q 1 UNION q 2 ) = A(q 1 ) ∨ A(q 2 )
In order to encode the right-hand side query, we need the notion of cyclic queries. Definition 6 (Cyclic Query). A SPARQL query is referred to as cyclic if a transition graph induced from the query patterns is cyclic. The transition graph2 is constructed in the same way as done in Definition 5.

Example 4. q is cyclic, as shown graphically, q(x) = (x, a, y), (y, b, z), (z, c, r), (r, d, y) Encoding right-hand side query: the encoding of the right-hand side query q is different from that of the left due to the non-distinguished variables that appear in cycles in the query. The distinguished variables and constants are encoded as nominals whereas the non-distinguished variables ndvar(q ) are encoded as follows:

• First, for each triple t i ∈ q , introduce a fresh nominal n i , i.e., t(t i ) = n i . This nominal is satisfied in a triple node S in a restricted transition system.

• Second, we use a function that assigns a formula for each x ∈ ndvar(q ) as follows:

-If x occurs only once in q , x is encoded as .

-If x appears multiple times in q and x ∈ t i ∈ q , then

m i ={x → ϕ |    ϕ = s t(t i ) if subject(x) or ϕ = p t(t i ) if predicate(x) or ϕ = ō t(t i ) if object(x) }
Note that there is an exponential number of m i 's in terms of the number of non-distinguished variables. More precisely, there are at most O(n k ) mappings, where n is the number of triples where nondistinguished variables appear, and k is the number of non-distinguished variables. • Finally, the function A uses t and m to encode the query inductively:

A(q, m) = |m| i=1 A(q, m i ) A((x, y, z), m) = µX. t((x, y, z)) ∧ s d(m, x) ∧ p d(m, y) ∧ o d(m, z) ∨ mu(X) A(q 1 AND q 2 , m) = A(q 1 , m) ∧ A(q 2 , m) A(q 1 UNION q 2 , m) = A(q 1 , m) ∨ A(q 2 , m) d(m, x) =    ϕ if (x → ϕ) ∈ m if unique(x) x otherwise
Example 5. Consider the encoding of q 1 q 2 of Example 2. To encode q 1 , freeze the variables and constants and proceed with A such that A(q 1 ) = (µX.( s x ∧ p translated ∧ o l) ∨ mu(X))

∨ (µX.( s x ∧ p wrote ∧ o l) ∨ mu(X)) ∧ (µX.( s l ∧ p type ∧ o Poem) ∨ mu(X))
To encode q 2 , one first computes t and m. Hence, t((x, translated, l)) = n 1 , t((l, type, P oem)) = n 2 , t((x, wrote, l)) = n 3 and m = {m 1 , m 2 , m 3 } where

m 1 = {y → ō n 1 }, m 2 = {y → s n 2 }, and m 3 = {y → ō n 3 }. Finally, A(q 2 , m) = |m| i=1 A(q, m i ) = (µX.(n 1 ∧ s x ∧ p translated ∧ o ō n 1 ) ∨ mu(X) ∧ µX.(n 2 ∧ s ō n 1 ∧ p type ∧ o Poem) ∨ mu(X)) ∨ µX.(n 3 ∧ s x ∧ p wrote ∧ o ō n 1 ) ∨ mu(X) ∨ (µX.(n 1 ∧ s x ∧ p translated ∧ o s n 2 ) ∨ mu(X) ∧ µX.(n 2 ∧ s s n 2 ∧ p type ∧ o Poem) ∨ mu(X)) ∨ µX.(n 3 ∧ s x ∧ p wrote ∧ o s n 2 ) ∨ mu(X) ∨ (µX.(n 1 ∧ s x ∧ p translated ∧ o ō n 3 ) ∨ mu(X) ∧ µX.(n 2 ∧ s ō n 3 ∧ p type ∧ o Poem) ∨ mu(X)) ∨ µX.(n 3 ∧ s x ∧ p wrote ∧ o ō n 3 ) ∨ mu(X)

Encoding Axioms

Besides the encoding of the queries, we introduce the encoding of SHI schema axioms as below. Definition 7. Given a set of axioms c 1 , c 2 , ..., c n of a schema C, the µ-calculus encoding of C is:

η(C) = η(c 1 ) ∧ η(c 2 ) ∧ ... ∧ η(c n ).
Where η translates each axiom into an equivalent formula using ω which in turn recursively encodes concepts and roles:

η(r 1 r 2 ) = νX. r 1 ⇒ r 2 ∧ nu(X) η(C 1 C 2 ) = νX. ω(C 1 ) ⇒ ω(C 2 ) ∧ nu(X) ω(A) = A ω(¬C) = ¬ω(C) ω(⊥) = ⊥ ω(C 1 C 2 ) = ω(C 1 ) ∧ ω(C 2 ) ω(∃r.C) = s p r ∧ o ( s o ω(C)) ω(∀r.C) = [s] [p]r ⇒ [o]([s][o]ω(C)) ω(∃r -.C) = ō p r ∧ s ( s o ω(C)) ω(∀r -.C) = [ō] [p]r ⇒ [s]([s][o]ω(C)) η(trans(r)) = νX. s p r ∧ o (y ∧ s ( p r ∧ o z)) ⇒ ( p r ∧ o z) ∧ nu(X)
So far we proposed various functions to produce formulas corresponding to the encodings of queries and schema axioms. Hence, the problem of containment under a schema can be reduced to formula unsatisfiability in µ-calculus as:

q C q ⇔ η(C) ∧ A(q) ∧ ¬A(q , m) ∧ ϕ r is unsatisfiable.
For the sake of legibility in writing, we use Φ(C, q, q ) to denote η(C) ∧ A(q) ∧ ¬A(q , m) ∧ ϕ r .

Reducing Containment to Unsatisfiability

We prove the correctness of reducing query containment to unsatisfiability test.

Lemma 1. Given a set of schema axioms

C = {c 1 , • • • , c n }, C has a model iff η(C) is satisfiable.
Lemma 2. For any SPARQL query q, q is satisfiable iff A(q) and A(q, m) are satisfiable.

Proof. (sketch) We prove for A(q, m), the proof for A(q) is immediate. (⇒) a canonical instance of q can be converted into a transition system that satisfies A(q, m). (⇐) any formula corresponding to a query encoding is satisfiable. However, each satisfying model may not be a restricted transition system. Thus, we use A(q, m) ∧ ϕ r (Proposition 1), to guarantee that satisfying models are restricted transition systems. As such, it can be shown that a model of the formula A(q, m) ∧ ϕ r can be turned into a graph G that satisfies q.

Theorem 1 (Soundness). Given queries q and q , and a set of axioms C, if Φ(C, q, q ) is unsatisfiable, then q C q .

Proof. (sketch) We show the contrapositive. If q C q , then Φ(C, q, q ) is satisfiable. It can be verified that every model of C in which there is at least one tuple satisfying q but not q can be a satisfying model for Φ(C, q, q ). Theorem 2 (Completeness). Given queries q and q , and a set of axioms C, if Φ(C, q, q ) is satisfiable, then q C q .

Proof. Φ(C, q, q ) is satisfiable ⇒ ∃K. Φ(C, q, q ) K = ∅. Consequently, K is a restricted transition system due to ϕ r K = ∅ (cf. Proposition 1). Using K = (S ∪ S , R, L) we construct a model I = (∆ I , • I ) of C such that q q holds:

• ∆ I = S , A I = A K for each atomic concept A, • I = K , for a top concept, • r I = {(s, s ) | ∀t ∈ r K ∧ t ∈ S ∧ (s, t ) ∈ R(s) ∧ (t , t) ∈ R(p) ∧ (t , s ) ∈ R(o)}
for each atomic role r, • for each constant c in q and q , c I = c K , • for each distinguished and non-distinguished variable v in q, v I = v K , and

• for each distinguished variable v in q , v I = v K .
One can utilize Lemma 1, to verify that indeed I is a model of C. Thus, it remains to show that q I ⊆ q I . From our assumption, one anticipates the following:

A(q) ∧ ¬A(q ) K = ∅ ⇒ A(q) K = ∅ and ¬A(q , m) K = ∅ ⇒ A(q) K = ∅ and A(q , m) K = ∅
Note here that, if a formula ϕ is satisfiable in a restricted transition system K r , then ϕ Kr = S. We use a function f to construct an RDF graph G from the interpretation I. f uses assertions in I to form triples:

f (a ∈ A I ) = (a, type, A) ∈ G f ((a, b) ∈ r I ) = (a, r, b) ∈ G f ((a, b) ∈ (r -) I ) = (b, r, a) ∈ G f ((x, y, z)) = (x, y, z) ∈ G, ∀(x, y, z) ∈ q
As a consequence, q G = ∅ and q G = ∅ because G contains all those triples that satisfy q and not q . Therefore, we get q G ⊆ q G . Fundamentally, there are two issues to be addressed (i) when q contains a cycle and (ii) when q is not cyclic. (i) can be dealt with nominals, i.e., since cycles can be expressed by a formula in a µ-calculus extended with nominals and inverse, cyclic queries can be encoded by such a formula. Hence, the constraints expressed by ¬A(q , m) are satisfied in a transition system containing cycles. On the other hand, (ii) if there are no cycles in q , then replacing non-distinguished variables with suffices (cf. Lemma 2).

Complexity

In the following, we establish the complexity of the containment problem under schema axioms. The schema axioms can be formed using the fragments of SHIQ. More specifically, the fragments without number restrictions. The expressiveness of the schema language is limited as such due to the expressive power of the logic used for the encoding: µ-calculus with nominals and converse becomes undecidable when extended with graded modalities [START_REF] Bonatti | The Complexity of Enriched µ-calculi[END_REF].

Proposition 2. SPARQL query containment under SHI schema axioms can be determined in a time of

2 O(n 2 log n) where n = O(|η(C)| + |A(q)| + |A(q )|)
is the size of the formula, and η(C), A(q) and A(q ) denote the encodings of schema axioms C, and queries q and q .

Note that due to duplication in the encoding of q 2 , the size of |A(q 2 )| is exponential in terms of the non-distinguished variables that appear in cycles in the query. Hence, we obtain a 2EXPTIME upper bound for containment. As pointed out in [START_REF] Calvanese | Conjunctive Query Containment and Answering under Description Logics Constraints[END_REF], the problem is solvable in EXPTIME if there is no cycle on the right hand side query. This complexity is a lower bound due to the complexity of satisfiability in µ-calculus which is 2 O(n 2 log n) [START_REF] Sattler | The Hybrid µ-Calculus[END_REF][START_REF] Tanabe | A Decision Procedure for Alternation-Free Modal µ-calculi[END_REF].

Related Works

In the following we briefly review works that previously established closely related results for related query languages. We took a similar approach as [START_REF] Genevès | Efficient Static Analysis of XML Paths and Types[END_REF] that established the optimal complexity for XPath query containment and provided an effective implementation.

Studies on the translation of SPARQL into relational algebra and SQL [START_REF] Cyganiak | A relational algebra for sparql[END_REF][START_REF] Chebotko | Semantics preserving sparql-to-sql query translation for op-tional graph patterns[END_REF] indicate a close connection between SPARQL and relational algebra in terms of expressiveness. In [START_REF] Polleres | From SPARQL to rules (and back)[END_REF], a translation of SPARQL queries into a datalog fragment (non-recursive datalog with negation) that is known to be equally expressive as relational algebra (RA) was presented. This translation makes the close connection between SPARQL and rule-based languages explicit and shows that RA is at least as expressive as SPARQL. Tackling the opposite direction, it was recently shown in [START_REF] Angles | The expressive power of sparql[END_REF] that SPARQL is relationally complete, by providing a translation of the above-mentioned datalog fragment into SPARQL. As argued in [START_REF] Angles | The expressive power of sparql[END_REF], the results from [START_REF] Polleres | From SPARQL to rules (and back)[END_REF] and [START_REF] Angles | The expressive power of sparql[END_REF] taken together imply that SPARQL has the same expressive power as relational algebra. From early results on query containment in relational algebra and first-order logic, one can infer that containment in relational algebra is undecidable (contrary to the results in [START_REF] Chekol | PSPARQL query containment[END_REF]. Therefore, containment of SPARQL queries is also undecidable. Hence, in this paper, we considered a fragment of SPARQL containing only conjunction and disjunction for this study.

The most closely related work is [START_REF] Calvanese | Conjunctive Query Containment and Answering under Description Logics Constraints[END_REF] in which query containment under description logic constraints is studied based on an encoding in propositional dynamic logic with converse (CPDL). They establish 2EXPTIME upper bound complexity for containment of queries consisting of union of conjunctive queries under DLR schema axioms. Our work is similar in spirit, in the sense that the µ-calculus is a logic that subsumes CPDL, and may open the way for extensions of the query languages and ontologies (for instance OWL-DL). Besides, the two languages are different since SPARQL allows for predicates to be used as subject or object of other triple patterns and can be in the scope of a variable. This is not directly allowed in DLR (union) of conjunctive queries. Our encoding of RDF graphs and SPARQL queries preserves this capability.

Other related results come from the study of query entailment and query answering. Query entailment (and hence containment) in DLs ranging from ALCI to SHIQ is shown to be 2EXPTIME-hard in [START_REF] Lutz | The complexity of conjunctive query answering in expressive description logics[END_REF][START_REF] Glimm | Conjunctive query answering for the description logic shiq[END_REF][START_REF] Eiter | Query answering in description logics with transitive roles[END_REF]. In this paper we do not deal with the same query language than the one dealt with in [START_REF] Glimm | Conjunctive query answering for the description logic shiq[END_REF]). In fact, the supported SPARQL fragment is strictly larger than the one studied in [START_REF] Glimm | Conjunctive query answering for the description logic shiq[END_REF]. Specifically, UCQs in [START_REF] Glimm | Conjunctive query answering for the description logic shiq[END_REF]) are made of C(x), R(x, y) for an atom C, a role R, and variables x and y, whereas we do also support queries capable of querying concept and role names at the same time, such as q(x) = (x, y, z). Further, the purpose of reducing the problem to µ-calculus is exactly about extending query containment to even more features (such as SPARQL 1.1 paths with recursion, entailment regimes, and negation). For instance, it is known that recursive paths can be easily supported in mucalculus (using fixpoints) whereas it is known that extending previous approaches with this feature is notoriously difficult. Beyond this, the novelty of the study is the reduction of the SPARQL containment problem to µ-calculus satisfiability, and the advantages of using such a logic: great expressivity, good computational properties, extensibility. The main focus of the contribution is not the complexity bound by itself but rather a new approach with a broader logic, paving the way for future extensions as it was never done before.

Here, we would like to emphasize that, in addition to the complexity bound we provide, no implementation has been reported in previous works, whereas in our case our work opens the way to use an implementation like the one in [START_REF] Tanabe | A Decision Procedure for Alternation-Free Modal µ-calculi[END_REF] or [START_REF] Genevès | Efficient Static Analysis of XML Paths and Types[END_REF].

Finally, the evaluation of SPARQL query under schema constraints is considered by W3C under the entailment regime principle in which SPARQL queries are evaluated by taking into account the semantics of a schema language [START_REF] Kollia | SPARQL query answering over OWL ontologies[END_REF]. It is possible to define query containment under such entailment regimes (cf. (?) for instance). However, because the schema is not made explicit in entailment regimes, this would not allow to consider containment under a particular schema as we did here. And this could be very useful particularly because (1) schema are very often separated from the data and (2) this allows for compiling the schema.

Conclusion

We have introduced a mapping from RDF graphs into transition systems and the encodings of queries and schema axioms in the µ-calculus. We proved that this encoding is correct and can be used for checking query containment. We have provided implementable algorithms, as a consequence, this work opens a way to use available implementations of µcalculus satisfiability solvers from [START_REF] Tanabe | A Decision Procedure for Alternation-Free Modal µ-calculi[END_REF] and [START_REF] Genevès | Efficient Static Analysis of XML Paths and Types[END_REF]. Beyond this, we have established a double exponential upper bound for containment test under SHI axioms.

As a future work, we plan to extend the schema language with nominals (becomes SHOI) and analyse the optimality of the complexity. Because nominals are part of the logic, the complexity of containment under SHOI axioms has already a 2EXPTIME upper bound. Furthermore, what would be interesting is, to identify the fragments of SPARQL queries and DLs that can be encoded in the fragments of µ-calculus with nominals and converse, graded modalities and converse, and nominals and graded modalities [START_REF] Bonatti | The Complexity of Enriched µ-calculi[END_REF][START_REF] Tanabe | A Decision Procedure for Alternation-Free Modal µ-calculi[END_REF].

Figure 1 :

 1 Figure 1: Transition system encoding the RDF graph of Example 1. Nodes in S are black anonymous nodes; nodes in S are the other nodes (d-transitions are not displayed).

We do not consider OPTIONAL and FILTER query patterns because containment over the full SPARQL is undecidable.

The transition graph is similar to the tuple-graph used in[START_REF] Calvanese | Conjunctive Query Containment and Answering under Description Logics Constraints[END_REF] to detect the dependency among variables.


Melisachew Wudage Chekol

Jérôme Euzenat

Pierre Genevès

Nabil Layaïda

SPARQL Query Containment under RDFS Entailment Regime

The problem of SPARQL query containment is defined as determining if the result of one query is included in the result of another for any RDF graph. Query containment is important in many areas, including information integration, query optimization, and reasoning about Entity-Relationship diagrams. We encode this problem into an expressive logic called µ-calculus: where RDF graphs become transition systems, queries and schema axioms become formulas. Thus, the containment problem is reduced to formula satisfiability test. Beyond the logic's expressive power, satisfiability solvers are available for it. Hence, this study allows to exploit these advantages.

Introduction

SPARQL is a W3C recommended query language for RDF. The language is being extended with different entailment regimes and regular path expressions 3 . The semantics of SPARQL relies on the definition of basic graph pattern matching that is built on top of RDF simple entailment [START_REF] Tanabe | A Decision Procedure for Alternation-Free Modal µ-calculi[END_REF]. However, it may be desirable to use SPARQL to query triples entailed from subclass, subproperty, range, domain, and other relations which can be represented using RDF schema. The SPARQL specification defines the results of queries based on RDF simple entailment. The specification also presents a general parametrized definition of graph pattern matching that can be expanded to other entailments beyond simple entailment. Query answering under the RDFS entailment regime can be achieved via: [START_REF] Alkhateeb | Extending SPARQL with regular expression patterns (for querying RDF)[END_REF] materialization (computing the deductive closure of the queried graph) [?], (2) rewriting the queries using the schema, and (3) hybrid (combining materialization and query rewriting). We use a technique based on the approaches [START_REF] Alkhateeb | Extending SPARQL with regular expression patterns (for querying RDF)[END_REF] and [START_REF] Barceló | Expressive languages for path queries over graph-structured data[END_REF] to study the problem of SPARQL query containment under the RDFS entailment regime.

Query containment is defined as determining if the result of one query is included in the result of another one for any RDF graph. It has been a central point of research due to its vital role in query optimization, information integration and reasoning about Entity-Relationship diagrams [?]. In [START_REF] Barceló | Expressive languages for path queries over graph-structured data[END_REF], a double exponential upper bound is proved for containment of union of conjunctive queries (UCQs) under expressive description logic constraints. Beyond UCQs, containment of (two-way) regular path queries (2RPQs) have been studied extensively [5, ?]. These languages are used to query graph databases and containment has been shown to be PSPACE-complete and EXPTIME-hard under the presence of functionality constraints [START_REF] Calvanese | Answering Recursive Queries under Keys and Foreign Keys is Undecidable[END_REF]. On the other hand, the containment of conjunctive 2RPQs is EXPSPACE-complete, this bound jumps to 2EXPTIME when considered under expressive description logic (DL) constraints [START_REF] Calvanese | Containment of regular path queries under description logic constraints[END_REF]. In fact, this problem has already been implicitly addressed in [START_REF] Barceló | Expressive languages for path queries over graph-structured data[END_REF] when DLR (DLs with n-ary relations) constraints are used. More recently, Path SPARQL (PSPARQL [?]) query containment has been studied in [START_REF] Genevès | Efficient Static Analysis of XML Paths and Types[END_REF] where a double exponential upper bound is established. In this work, we consider the same approach as [START_REF] Genevès | Efficient Static Analysis of XML Paths and Types[END_REF] and prove that containment of PSPARQL queries under RDF schema axioms has a double exponential upper bound. However, it is exponential if the query on the right hand side has a tree structure (cf. for example, [START_REF] Barceló | Expressive languages for path queries over graph-structured data[END_REF]). Further, paths are being included in the new version of SPARQL (called SPARQL1.1), thus this work can be used to test containment of path SPARQL queries under the RDFS entailment regime.

To study containment, we apply an approach which has already been successfully applied for XPath [START_REF] Prud | SPARQL Query Language for RDF[END_REF]. SPARQL is interpreted over graphs, hence we encode it in a graph logic, specifically the alternation-free fragment of the µ-calculus [START_REF] Tanabe | A Decision Procedure for the Alternation-Free Two-Way Modal µ-calculus[END_REF] with converse and nominals [?] interpreted over labeled transition systems. We show that this logic is powerful enough to deal with query containment for union of conjunctive SPARQL queries under the RDFS entailment regime. Furthermore, this logic admits exponential time decision procedures that is implemented in practice [?,?,11]. Hence, our approach opens a way to take advantage of these implementations. We introduce a translation of RDF graphs into transition systems and SPARQL queries and RDF schema into µ-calculus formulae. Then, we show how query containment in SPARQL under RDFS entailment can be reduced to unsatisfiability in the µ-calculus.

In summary, the contribution of this work is fourfold: (1) we formulate the problem of query containment under the RDFS entailment regime in three different ways, (2) since paths are included in the new version of SPARQL, this work can be used to determine containment of path queries (under RDF schema as well), (3) we show how to extend the schema language to the description logic SH (short for, role transitivity S and role hierarchy H), and (4) we prove a double exponential upper bound for containment.

Preliminaries

This section introduces the foundations of RDF(S), SPARQL, and µ-calculus.

RDF(S)

RDF is a language used to express structured information on the Web as graphs. We present a compact formalization of RDF [START_REF] Tanabe | A Decision Procedure for Alternation-Free Modal µ-calculi[END_REF]. Let U, B, and L be three disjoint infinite sets denoting the set of URIs (identifying a resource), blank nodes (denoting an unidentified resource) and literals (a character string or some other type of data) respectively. We abbreviate any union of these sets as for instance, UBL = U ∪ B ∪ L. A triple of the form (s, p, o) ∈ UB × U × UBL is called an RDF triple. s is the subject, p is the predicate, and o is the object of the triple. Each triple can be thought of as an edge between the subject and the object labelled by the predicate, hence a set of RDF triples is often referred to as an RDF graph. RDF has a model theoretic semantics [START_REF] Tanabe | A Decision Procedure for Alternation-Free Modal µ-calculi[END_REF].

Example 1 (RDF Graph). Consider the following RDF graph (all identifiers correspond to URIs and :b is a blank node):

G ={(john, childOf, mary), (childOf, sp, ancestor), ( :b, hasF ather, john), (ancestor, dom, P erson), (ancestor, range, P erson)} RDF Schema (RDFS) may be considered as a simple ontology language expressing subsumption relations between classes or properties [START_REF] Tanabe | A Decision Procedure for Alternation-Free Modal µ-calculi[END_REF]. Technically, this is an RDF vocabulary used for expressing axioms constraining the interpretation of graphs. The RDFS vocabulary and its semantics are given in [START_REF] Tanabe | A Decision Procedure for Alternation-Free Modal µ-calculi[END_REF]. There, inference rules (shown in Table 1) are given which allow to deduce or infer new triples using the schema and RDF graph. Definition 1. A SPARQL query pattern q is inductively defined as follows:

q = t ∈ UBV × e × UBLV | q 1 AND q 2 | q 1 UNION q 2 e = uri | x | e e | e • e | e + | e * Definition 2.
A SPARQL SELECT query is defined as q( -→ w ) where -→ w is a tuple of variables in V that are called distinguished variables, and q is a query pattern.

Example 3 (SPARQL queries). Consider the following queries q(?x) and q (?x)refer to the domain of ρ is exactly the set of variable in P , i.e., dom(ρ) = V (P ), terms in the range of ρ occur in G, -If P , obtained from P by replacing blank nodes with either URIs, blank nodes, or RDF literals is such that: the RDF graph sk(ρ(P )) is RDFSentailed by sk(G). The function sk(.) replaces blank nodes with fresh URIs (URIs that are neither in the queried graph nor in the query).

Since SPARQL's entailment regimes only change the evaluation of basic graph patterns, the evaluation of query patterns can be defined in the standard way [15, ?]. The evaluation of query patterns over an RDF graph G is defined inductively:

q 1 AND q 2 G = q 1 G 1 q 2 G q 1 UNION q 2 G = q 1 G ∪ q 2 G q( - → w ) G = π-→ w ( q G )
The projection operator π-→ w selects only those part of the mappings relevant to variables in -→ w . For detailed discussions we refer the reader to [?,?].

Example 4. The answers to query q and q (under simple entailment semantics) of Example 3 on graphs G of Example 1 and cl(G) of Example 2 are: q G = ∅ but q cl(G) = {john, mary} and q G = {john, mary}. Thus, q cl(G) = q G . Clearly, q G ⊆ q G . Note also that, q when evaluated over G under the RDFS entailment is equivalent to q evaluated under simple entailment semantics.

Beyond these particular examples, the goal of query containment is to determine whether this holds for any graph.

Definition 4 (Containment). Given an RDFS schema S and queries q and q with the same arity, q is contained in q under the RDFS entailment regime, denoted q S rdfs q , iff for any graph G satisfying the schema S, q G ⊆ q G . The evaluation of SPARQL queries (also under the RDFS entailment regime) is proved to be PSPACE-complete. However, the evaluation problem is NP-complete for the fragment containing only AND and UNION query patterns [?,?,?].

To determine containment, SPARQL queries are encoded as µ-calculus formulas, next we present a brief introductory about this logic.

µ-calculus

The modal µ-calculus [START_REF] Tanabe | A Decision Procedure for the Alternation-Free Two-Way Modal µ-calculus[END_REF] is an expressive logic which adds recursive features to modal logic using fixpoint operators. The syntax of the µ-calculus is composed of countable sets of atomic propositions AP , a set of nominals N om, a set of variables Var, a set of programs Prog for navigating in graphs. A µ-calculus formula, ϕ, can be defined inductively as follows:

ϕ ::= | ⊥ | p | X | ¬ϕ | ϕ ∨ ψ | ϕ ∧ ψ | a ϕ | [a]ϕ | µXϕ | νXϕ
where p ∈ AP, X ∈ V ar and a ∈ P rog is either an atomic program or its converse ā. The greatest and least fixpoint operators (ν and µ), respectively introduce general and finite recursion in graphs [START_REF] Tanabe | A Decision Procedure for the Alternation-Free Two-Way Modal µ-calculus[END_REF].

The semantics of the µ-calculus is given over a transition system, K = (S, R, L) where S is a non-empty set of nodes, R : P rog → 2 S×S is the transition function, and L : AP → 2 S assigns a set of nodes to each atomic proposition or nominal where it holds, such that L(p) is a singleton for each nominal p. For converse programs, R can be extended as

R(ā) = {(s , s) | (s, s ) ∈ R(a)}.
Besides, a valuation function V : Var → 2 S is used to assign a set of nodes to each variable. For a valuation V , variable X, and a set of nodes S ⊆ S, V [X/S ] is the valuation that is obtained from V by assigning S to X. The semantics of a formula, in terms of a transition system K (a.k.a. Kripke structure) and a valuation function, is represented by ϕ K V . The semantics of basic µ-calculus formulae is defined as follows:

p K V = L(p), p ∈ AP ∪ N om, L(p) is singleton for p ∈ N om X K V = V (X), X ∈ V ar ¬ϕ K V = S\ ϕ K V K V = S ϕ ∧ ψ K V = ϕ K V ∩ ψ K V , ϕ ∨ ψ K V = ϕ K V ∪ ψ K V a ϕ K V = {s ∈ S|∃s ∈ S.(s, s ) ∈ R(a) ∧ s ∈ ϕ K V } [a]ϕ K V = {s ∈ S|∀s ∈ S.(s, s ) ∈ R(a) ⇒ s ∈ ϕ K V } µXϕ K V = {S ⊆ S| ϕ K V [X/S ] ⊆ S } νXϕ K V = {S ⊆ S|S ⊆ ϕ K V [X/S ] }
µ-calculus formulas are interpreted over labeled transition systems. Thus, we propose an encoding of an RDF graph as a transition system in which nodes correspond to RDF entities and RDF triples. Edges relate entities to the triples they occur in. Different edges are used for distinguishing the functions (subject, object, predicate). Expressing predicates as nodes, instead of atomic programs, makes it possible to deal with full RDF expressiveness in which a predicate may also be the subject or object of a statement.

Definition 5 (Transition system associated to an RDF graph [START_REF] Genevès | Efficient Static Analysis of XML Paths and Types[END_REF]). Given an RDF graph, G ⊆ U B × U × U BL, the transition system associated to G, σ(G) = (S, R, L) over AP = UBL ∪ {s , s }, is such that:

-S = S ∪ S with S and S the smallest sets such that ∀u ∈ U G ,

∃n u ∈ S , ∀b ∈ B G , ∃n b ∈ S , and ∀t ∈ G, ∃n t ∈ S , -∀t = (s, p, o) ∈ G, n s , n t ∈ R(s), n t , n p ∈ R(p), and n t , n o ∈ R(o), -L : AP → 2 S ; ∀u ∈ U G , L(u) = {n u }, ∀b ∈ B G , L(b) = S , L(s ) = S , ∀l ∈ L G , L(l) = {n l } and L(s ) = S , -∀n t , n t ∈ S , n t , n t ∈ R(d).
The program d is introduced to render each triple accessible to the others and thus facilitate the encoding of queries. The function σ associates what we call a restricted transition system to any RDF graph. Formally, we say that a transition system K is a restricted transition system iff there exists an RDF graph G such that K = σ(G).

A restricted transition system is thus a bipartite graph composed of two sets of nodes: S , those corresponding to RDF entities, and S , those corresponding to RDF triples. For example, Figure 1 shows the restricted transition system associated with the graph of Example 1. When checking for query containment, we consider the following restrictions: (i) the set of programs is fixed: P rog = {s, p, o, d, s, p, ō, d}, and (ii) a model must be a restricted transition system. The latter constraint can be expressed in the µ-calculus as follows:

Proposition 1 (RDF restriction on transition systems [START_REF] Genevès | Efficient Static Analysis of XML Paths and Types[END_REF]). A formula ϕ is satisfied by some restricted transition system if and only if ϕ ∧ ϕ r is satisfiable by some transition system, i.e. ∃K r ϕ Kr = ∅ ⇐⇒ ∃K ϕ ∧ ϕ r K = ∅, where:

ϕ r = νX.θ ∧ κ ∧ (¬ d ∨ d X) in which θ = s s ∧ p s ∧ o s ∧ ¬ s ∧ ¬ p ∧ ¬ ō and κ = [s]ξ ∧ [p]ξ ∧ [o]ξ with ξ = (¬ s ∧ ¬ o ∧ ¬ p ∧ ¬ d ∧ ¬ d ∧ ¬ s s ∧ ¬ ō s ∧ ¬ p s ).
The formula ϕ r ensures that θ and κ hold in every node reachable by a d edge, i.e. in every s node. The formula θ forces each s node to have a subject, predicate and object. The formula κ navigates from a s node to every reachable s node, and forces the latter not to be directly connected to other subject, predicate or object nodes. If a µ-calculus formula ψ appears under the scope of a least µ or greatest ν fixed point operator over all the programs {s, p, o, d, s, p, ō, d} as, µX.

ψ ∨ s X ∨ p X ∨• • • or νX.ψ∧[s]X ∧[p]X ∧• • • then,
for the sake of legibility, we denote the recursion components of the respective formulae as mu(X) for the µ recursion part and nu(X) for the ν recursion part.

Encoding SPARQL Queries

In this section, we show how to encode queries as µ-calculus formulas. Then, in the next section, we use this encoding to test query containment under the RDFS entailment regime. Before discussing the encoding procedure, we briefly assess the issue of blank nodes. Blank nodes are existential variables that denote the existence of unnamed resources. Their definition matches the definition of non-distinguished variables in a query. Thus, blank nodes in the queries can be considered as non-distinguished variables. As a result, every occurrence of a blank node in the query is replaced by a fresh variable.

Queries are translated into µ-calculus formulas. The principle of the translation is that each triple pattern is associated with a sub-formula stating the existence of the triple somewhere in the graph. Hence, they are quantified by µ (least fixed point) so as to put them out of the context of a state. In this translation, variables are replaced by nominals which will be satisfied when they are at the corresponding position in such triple relations. A function called A is used to encode queries inductively on the structure of query patterns. AND and UNION are translated into boolean connectives ∧ and ∨, respectively. When encoding q q , we call q left-hand side query and q right-hand side query. Cyclic dependencies among the non-distinguished variables in the query on the right-hand side create problems in the encoding process: because variables in cycles cannot be simply encoded using atomic propositions (APs) or . As APs can be true in several nodes in the transition system (resulting in the loss of connectedness). Thus, we provide separate encodings for q and q .

Encoding left-hand side query: to encode the left-hand side query, one proceeds by encoding the distinguished or non-distinguished variables and constants using nominals. Basically, the variables and constants are frozen (i.e., equivalent to obtaining a canonical instance of the query). Afterwards, a recursive function A is used to inductively construct a formula. Regular expression patterns that appear in the query are encoded using the function R. It takes two arguments (the predicate which is a regular expression pattern and the object of a triple).

A (x, e, z) = µX. s x ∧ R(e, z) ∨ mu(X) if a non-distinguished variable appears only once, then it is encoded as .

A(q 1 AND q 2 ) = A(q 1 ) ∧ A(q 2 ) A(q 1 UNION q 2 ) = A(q 1 ) ∨ A(q 2 ) R(uri, y) = p uri ∧ o y R(x, y) = p x ∧ o y R(
if a non-distinguished variable appears multiple times, then one performs the subsequent steps: 1. for each t i ∈ q, t(t i ) = n i , i.e., introduce a nominal for each triple, 2. for each z ∈ t i = (x i , e i , y i ) ∈ q, a set of mappings containing formula assignments are generated as:

m i ={z → ψ |                ψ = ϕ(s, e i ) if subject(z) ∧ e i ∈ var(q) ψ = s t(t i ) if subject(z) ∧ e i ∈ var(q) ψ = ϕ(o, e i ) if object(z) ∧ e i ∈ var(q) } ψ = ō t(t i ) if object(z) ∧ e i ∈ var(q) ψ = p t(t i ) if predicate(z) ∧ e i ∈ var(q)
s and o denote subject and object of a triple and ϕ is defined as: Note that there is an exponential number of m i 's in terms of the number of non-distinguished variables. More precisely, there are at most O(k n ) mappings, where n is the number of triples in which non-distinguished variables appear and k is the number of non-distinguished variables. finally function A works inductively on the query structure using m to generate the formula. As for the left-hand side query, R is used to produce the encodings of regular expressions.

A(q, m) = |m| i=1 A(q, m i ) d(m, x) =      ψ if (x → ψ) ∈ m if unique(x) x otherwise A (x, e, z), m = µX. s d(m, x) ∧ R(d(m, e), d(m, e)) ∨ mu(X) A(q 1 AND q 2 , m) = A(q 1 , m) ∧ A(q 2 , m) A(q 1 UNION q 2 , m) = A(q 1 , m) ∨ A(q 2 , m)
Example 6 (Encoding queries). Consider the encoding of q q , where q(x, z) = (x, (c d) • (a b), z) q (x, z) = (x, (c d), y) AND (y, a b, z)

-The encoding of q is obtained by freezing the query and recursively constructing the formula using A.

A(q) = µX. s x ∧ R (c d) • (a b), z ∨ mu(X) = µX. s x ∧ ( p c ∨ p d) ∧ o s (( p a ∨ p b) ∧ o z) ∨ mu(X)
-The encoding of q is as follows:

• the constants and distinguished variables are encoded as nominals,

• y ∈ var(q ) is encoded as ϕ(o, (c d)), since y is an object of the triple (x, (c d), y). Hence, m 1 = {y → ( ō p c ∨ ō p d)}. On the other hand, y can also be encoded as ϕ(s, (a b)), since y is a subject of the triple (y, a b, z). Thus, we get m 2 = {y → ( s p a ∨ s p b)}. • finally, we use A to encode q recursively, A(q , m) = A(q , m 1 )∨A(q , m 2 )

= µX. s x ∧ ( p c ∨ p d) ∧ o ( ō p c ∨ ō p d) ∨ mu(X) ∧ µY. s ( ō p c ∨ ō p d) ∧ ( p a ∨ p b) ∧ o z ∨ mu(Y ) ∨ µX. s x ∧ ( p c ∨ p d) ∧ o ( s p a ∨ s p b) ∨ mu(X) ∧ µY. s ( s p a ∨ s p b) ∧ ( p a ∨ p b) ∧ o z ∨ mu(Y )
Example 7 (Containment test). We show containment of the following queries: select all descendants and ancestors (q) whose names are "john" and (q ) who share the same name.

q(x, y) = (x, name, "john") AND (x, ancestor * , z) AND (z, name, "john") q (x, y) = (x, name, y) AND (x, ancestor * , z) AND (z, name, y)

We proceed by first obtaining their encodings. Consider the encoding of q q , we encode triple patterns using θ and m = {y → ō name}.

A(q) = µX.θ(x, name, "john") ∨ mu(X) ∧ µX.θ(x, ancestor * , z) ∨ mu(X) ∧ µX.θ(z, name, "john") ∨ mu(X)

¬A(q , m) = νX.¬θ(x, name, ō name) ∧ nu(X) ∨ νX.¬θ(x, ancestor * , z) ∧ nu(X) ∨ νX.¬θ(z, name, ō name) ∧ nu(X)
The formula A(q) ∧ ¬A(q , m) is unsatisfiable because A(q) demands its model to satisfy the encoding of each triple pattern somewhere in the transition system. On the contrary, the formula ¬A(q , m) requests this model to satisfy the negation of the encoding of the triples in the entire transition system. Hence, this leads to a contradiction and no such model exists for the formula. Therefore, q q . On the other hand, it can be verified similarly to arrive at q q.

5 Query Containment under RDFS Entailment

In the following, we propose three approaches to determine query containment under the RDFS entailment regime: encoding the RDFS semantics, query rewriting, and encoding the schema approaches.

Encoding the RDFS Semantics Approach

When queries are evaluated under the RDFS entailment regime, the queried graph is materialized or saturated using RDFS inference rules (or simply rules) and the schema. Henceforth, implicit or inferred triples are considered when computing the result of the query. Since no specific graphs are considered when dealing with containment, we encode schema and rules. In addition, blank nodes that appear in the schema graph are skolemized, i.e., replaced by fresh constants that do not appear neither in the queries nor schema.

Definition 7. The encoding of an RDF schema graph S = {t 1 , • • • , t n } is produced by encoding each schema triple t i = (x, y, z) ∈ S such that:

Φ S = n i=1∧ti∈S µX.( s x ∧ p y ∧ o z) ∨ mu(X)
x, y, and z are atomic propositions corresponding to triple elements.

Definition 8 (Encoding inference rules). The µ-calculus encoding of RDFS inference rules of Table 1 is the disjunction of formulas (1) to ( 6) such that:

(1) νX. θ(x, sc, θ(y, sc, z)) ⇒ θ(x, sc, z) ∧ nu(X)

(2) νX. θ(x, type, θ(a, sc, b)) ⇒ θ(x, type, b) ∧ nu(X) (3) νX. θ(x, sp, θ(y, sp, z)) ⇒ θ(x, sp, z) ∧ nu(X) (4) νX. θ(x, θ(a, sp, b), y) ⇒ θ(x, b, y) ∧ nu(X) (5) νX. θ(x, θ(a, dom, b), y) ⇒ θ(x, type, b) ∧ nu(X) (6) νX. θ (x, θ(a, range, b), y) ⇒ θ(y, type, b) ∧ nu(X) θ(x, y, z) = x ∧ s ( p y ∧ o z) θ (x, y, z) = z ∧ ō p (y ∧ s x)
We denote this formula by Φ R .

So far, we have produced the encoding of SPARQL queries A(q) and A(q, m), RDFS inference rules Φ R , and schema triples (axioms) Φ S . In the following, we reduce query containment to unsatisfiability in µ-calculus and prove the correctness of this reduction.

Lemma 1. Given an RDF schema S and a graph G, G |= S ⇔ Φ S is satisfiable.

Lemma 2. For any SPARQL query q, q is satisfiable iff A(q) and A(q, m) are satisfiable.

Proof. (sketch) We prove for A(q, m), the proof for A(q) is immediate.

(⇒) a model obtained from an instance of q can be converted into a transition system that satisfies A(q, m).

(⇐) any formula corresponding to a query encoding is satisfiable. However, each satisfying model may not be a restricted transition system. Thus, we use A(q, m) ∧ ϕ r (Proposition 1), to guarantee that satisfying models are restricted transition systems. As such, it can be shown that a model of the formula A(q, m)∧ ϕ r can be turned into a graph G that satisfies q.

For the sake of legibility, we denote Φ R ∧Φ S ∧A(q)∧¬A(q , m)∧ϕ r by Φ(S, q, q ). Theorem 1 (Soundness and Completeness). Given SPARQL queries q and q and a schema S, Φ(S, q, q ) is unsatisfiable if and only if q S rdfs q .

Proof. (⇒) we prove the contrapositive, q S rdfs q ⇒ Φ(S, q, q ) is satisfiable. Assume there exists a graph G that entails the schema graph S, also assume that there exists a tuple -→ a ∈ q G and -→ a ∈ q G . We construct a restricted transition system K from G. Using Lemma 1, it is obvious that Φ S is satisfiable in K. Besides, ϕ r K = ∅ (cf. Proposition 1). Now let us use -→ a to instantiate the distinguished variables in q and q . Using the encodings of the instantiated queries and from Lemma 2, one deduces that A(q) K = ∅ and A(q , m) K = ∅. The later is not satisfiable in K because the nominals corresponding to the constants are not satisfied. Consequently, ¬A(q , m) K = ∅ and A(q)∧¬A(q , m) is satisfiable. Therefore, we arrive at Φ(S, q, q ) is satisfiable.

(⇐) we show that if Φ(S, q, q ) is satisfiable, then q rdf s q . Consider a restricted transition system model K for Φ(S, q, q ). We construct an RDF graph G from K. From Lemma 1, it follows that G |= S. Thus, it remains to verify that q G ⊆ q G . To do so, we start from the assumption, A(q) ∧ ¬A(q , m) K = ∅. Subsequently, A(q) = ∅ and A(q , m) K = ∅ because G contains all those triples that satisfy q and not q . Besides, if q contains a cycle, the constraints expressed by ¬A(q , m) are satisfied due to the ability, in a µ-calculus extended with nominals and converse, to express a formula that is satisfied in cyclic models. Therefore, q S rdfs q .

Query Rewriting Approach

SPARQL query containment under RDFS entailment regime can be determined by rewriting queries using the RDFS inference rules (shown in Table 1) and then reducing the encoding of the rewriting to unsatisfiability test. The rewriting is done using PSPARQL as explained in the following definition.

Definition 9 (SPARQL to PSPARQL). Given a SPARQL query q, a rewriting function τ produces its PSPARQL equivalent as follows: UNION (y, x, s) AND (x, sp * .range.sc * , o) τ ((s, x, o)) = (s, x, o) when x is a variable τ (q 1 AND q 2 ) = τ (q 1 ) AND τ (q 2 ) τ (q 1 UNION q 2 ) = τ (q 1 ) UNION τ (q 2 ) Definition 10 (Containment under RDFS entailment). Given an RDF schema S, queries q and q , and a rewriting function τ . q is contained in q under RDFS entailment, denoted q S rdfs q , if and only if τ (q) S τ (q ).

Theorem 2 (Soundness and Completeness). Given an RDF schema S and SPARQL queries q and q , q S rdfs q ⇔ Φ S ∧A(τ (q))∧¬A(τ (q ), m)∧ϕ r is unsatisfiable.

Proof. The proof of this theorem follows from that of Theorem 1.

Encoding the Schema Approach

In this approach, in order to determine query containment under the RDFS entailment regime, we encode the schema triples (axioms) as formulae. As a consequence, the encoding of the axioms constrains a model satisfying the formula. We consider subclass, subproperty, domain, range, and transitivity (Tr(sc) or Tr(sp)) schema axioms.

Definition 11. Given a set of axioms s 1 , s 2 , ..., s n of a schema S, the µ-calculus encoding of S is: η(S) = η(s 1 ) ∧ η(s 2 ) ∧ ... ∧ η(s n ).

We use a function η to translate each s i into an equivalent µ-calculus formula:

η((C 1 , sc, C 2 )) = νX. (C 1 ⇒ C 2 ) ∧ nu(X) η((R 1 , sp, R 2 )) = νX. (R 1 ⇒ R 2 ) ∧ nu(X) η((R, dom, C)) = νX. s ( p R ⇒ p type ∧ o C) ∧ nu(X) η((R, range, C)) = νX. ō p R ⇒ s ( p type ∧ o C) ∧ nu(X) η(T r(sc)) = νX. θ(x, sc, θ(y, sc, z)) ⇒ θ(x, sc, z) ∧ nu(X) η(T r(sp)) = νX. θ(x, sp, θ(y, sp, z)) ⇒ θ(x, sp, z) ∧ nu(X)
In the following, for legibility, we denote Φ(S, q, q ) = η(S)∧A(q)∧¬A(q , m)∧ϕ r .

Theorem 3 (Soundness and Completeness). Given queries q, q , and a set of RDF schema axioms S, q S rdfs q if and only if Φ(S, q, q ) is unsatisfiable.

Proof. (sketch) Soundness: Φ(S, q, q ) unsatisifiable implies that q S rdfs q . We show the contrapositive, if q S rdfs q , then Φ(S, q, q ) is satisfiable, holds. One can verify that every model G of S in which there is at least one triple satisfying q but not q can be turned into a transition system model for Φ(S, q, q ). Completeness: Φ(S, q, q ) satisfiable implies q 1 S rdfs q 2 . Assume that there exists a restricted transition system K that satisfies Φ(S, q, q ). This entails that, ϕ r K = ∅ (cf. Proposition 1). Now, from K = (S, R, L) we need to construct an RDF graph G that is model of S such that q S rdfs q holds: for every RDFS concept C in the schema, {(s, type,

C) | ∀s , s ∈ S ∧ t ∈ S .(s , t) ∈ R(s) ∧ (t, s ) ∈ R(p) ∧ (t, s) ∈ R(o) ∧ s ∈ C K }. -for each RDFS property P in the schema, {(s, P, s ) ∈ G | ∀t ∈ P K ∧ t ∈ S.(s, t ) ∈ R(s) ∧ (t , t) ∈ R(p) ∧ (t , s ) ∈ R(o)}, - add
every schema axiom to G and for each triple t i ∈ q, add t i to G.

Since every RDF graph entails its schema graph, we obtain that G is a model of S. Thus, it remains to show that q G ⊆ q G . From our assumption, one anticipates A(q) ∧ ¬A(q ) K = ∅ which implies A(q) K = ∅ and A(q , m) K = ∅. Note here that, if a formula ϕ is satisfiable in a restricted transition system K, then ϕ K = S. Further, it is holds that q G = ∅ and q G = ∅ because G contains all those triples that satisfy q and not q . Therefore, we get q G ⊆ q G . Since cycles in queries can be expressed by a formula in a µ-calculus extended with nominals and inverse, the constraints expressed by ¬A(q , m) are satisfied in a transition system containing cycles.

Complexity

Due to duplication in the encoding of the right hand side query q , the size of |A(q , m)| is exponential in terms of the non-distinguished variables that appear in cycles in the query. Thus, we obtain a 2EXPTIME upper bound for containment independent of the approaches. That is, the complexity bound applies to all the approaches. As pointed out in [START_REF] Barceló | Expressive languages for path queries over graph-structured data[END_REF], the problem is solvable in EXPTIME if there is no cycle in the query on the right hand side. In this case, this complexity is a lower bound due to the complexity of satisfiability in µ-calculus. Proposition 2. SPARQL query containment under the RDFS entailment can be solved in a time of 2 O(n) , where n is the size of the encoding.

All the three approaches have the same complexity bound, the difference lies on their extensibility. While encoding the RDFS semantics ( §??) and query rewriting ( §??) approaches are tied to the schema language which makes it harder for easy extension, the schema encoding approach ( §??) can be extended to use a more expressive schema language than RDFS. For instance, we can extend the schema language to SH where a concept C can be a bottom concept ( ), an atomic concept A, or a complex concept ¬C or C ∩ D. A role r is an atomic role. An SH TBox consists of concept inclusion, role inclusion and role transitivity axioms We can expand the proof of Theorem 1, to prove the correctness of this reduction. And thus, retaining the double exponential upper bound. Beyond this, we can even extend SH to the fragments of SROIQ [?]. More specifically, the fragments without number restrictions. The expressiveness of the schema language is limited as such due to the expressive power of the logic used for the encoding: µ-calculus with nominals and converse becomes undecidable when extended with graded modalities [?].

Conclusion

In this work, we have presented a translation of RDF graphs into labeled transition systems over which µ-calculus formulas are interpreted. We also have provided functions to produce the encodings of queries, inference rules and schema as formulas. Henceforth, query containment under RDFS entailment is reduced to formula satisfiability test in the µ-calculus. We introduced three approaches to achieve this, namely (1) encoding the RDFS semantics, (2) query rewriting, and (3) encoding the schema. Unlike (1) and ( 2), the third approach can be extended for a more expressive schema language as shown in §??, while maintaining a double exponential upper bound complexity. The power of the logic and our encoding allows for taking advantage of more expressive schema language. For instance, a good candidate could be the description logic SROIQ [?] underlying OWL 2.

In the future, we plan to investigate the optimality of the upper bound considering a more expressive schema language than RDF schema. Additionally, we plan to study containment of path queries with counting quantifiers (SPARQL 1.1 property hierarchies) using a fragment of µ-calculus called graded µ-calculus [?].

Fig. 1 .

 1 Fig. 1. Transition system encoding the RDF graph of Example 1. Nodes in S are black anonymous nodes; nodes in S are the other nodes (d-transitions are not displayed).

Example 5 .

 5 e e , y) = (R(e, y) ∨ R(e , y)) R(e • e , y) = R(e, s R(e , y)) R(e + , y) = µX.R(e, y) ∨ R(e, s X) R(e * , y) = R(e + , y) ∨ s yIn order to encode the right-hand side query, we need the notion of cyclic queries.Definition 6 (Cyclic Query). A SPARQL query is referred to as cyclic if a transition graph induced from the query patterns is cyclic. The transition graph 5 is constructed in the same way as done in Definition 6. Consider q(x) = (x, a•e, y) AND (y, b, z) AND (z, c * , r) AND (r, d, y) which is cyclic, as shown graphically, Encoding right-hand side query: the distinguished variables and constants are encoded as nominals whereas the non-distinguished variables are encoded as:

ϕ

  (s, a) = s p a ϕ(o, a) = ō p a ϕ(s, a • b) = ϕ(s, a) ϕ(o, a.b) = ϕ(o, b) ϕ(s, a b) = ϕ(s, a) ∨ ϕ(s, b) ϕ(o, a b) = ϕ(o, a) ∨ ϕ(o, b) ϕ(s, a + ) = ϕ(s, a) ϕ(o, a + ) = ϕ(o, a) ϕ(s, a * ) = ϕ(s, a) ϕ(o, a * ) = ϕ(o, a)

τ

  ((s, sc, o)) = (s, sc + , o) τ ((s, sp, o)) = (s, sp + , o) τ ((s, p, o)) = (s, x,o) AND (x, sp * , p) such that p / ∈ {sc, sp, type} τ ((s, type, o)) = (s, type.sc * , o) UNION (s, x, y) AND (x, sp * .dom.sc * , o)

  [?]. Role inclusion and transitivity axioms can be encoded in the same way as it is done in Definition 13. The encoding of concept inclusion axioms is slightly different, thus, we extend η as follows:η((C, sc, D)) = νX. (ω(C) ⇒ ω(D)) ∧ nu(X) ω(⊥) = ⊥ ω(A) = A ω(¬C) = ¬ω(C) ω(C D) = ω(C) ∧ ω(D)

Table 1 .

 1 RDFS inference Rules

	Subclass (sc)			Subproperty (sp)		Typing (dom, range)
	(a, sc, b) (b, sc, c) (a, sc, c)	(1)	(a, sp, b) (b, sp, c) (a, sp, c)	(3)	(a, dom, b) (x, a, y) (x, type, b)	(5)
	(a, sc, b) (x, type, a) (x, type, b)	(2)	(a, sp, b) (x, a, y) (x, b, y)	(4)	(a, range, b) (x, a, y) (y, type, b)	(6)
	Example 2. Using the inference rules, we can be infer the triples {(john,type,Person),
	(mary,type,Person), (john, ancestor,mary)}. Hence, the deductive closure of
	graph G in Example 1 contains:
	cl(G) = {(john, childOf, mary), (childOf, sp, ancestor), ( :b, hasF ather, john),
	(john, type, P erson), (mary, type, P erson), (john, ancestor, mary),
	(ancestor, dom, P erson)}
	2.2 SPARQL
	SPARQL is a W3C recommended query language for RDF [15]. PSPARQL (Path
	SPARQL) extends SPARQL with regular expression patterns [?]. The only dif-
	ference between the syntax of SPARQL and PSPARQL is on triple patterns. In
	this study, we refer to both SPARQL and PSPARQL queries as SPARQL un-
	less explicitly stated. Triple patterns in PSPARQL contain regular expressions in
	property positions instead of only URIs or variables as it is the case in SPARQL.

Table 1

 1 Definition 3 (SPARQL under RDFS entailment semantics). Given an RDF graph G and a basic graph pattern P , a partial mapping function ρ is a solution for G and P under RDFS-entailment, ρ ∈ P G , if:

	for vocabulary terms-on the graph of Example 1 and 2:
	SELECT ?x WHERE { ?x type Person . }
	SELECT ?x WHERE {{ ?x ?p ?y . ?p sp*.dom.sc* Person . }
	UNION {?y ?p ?x . ?p sp*.range.sc* Person . } }

SPARQL1.1, working draft http://www.w3.org/TR/sparql11-query/

We do not consider OPTIONAL and FILTER query patterns as containment over full SPARQL (equally expressive as relational algebra[START_REF] Alkhateeb | Extending SPARQL with regular expression patterns (for querying RDF)[END_REF]) is undecidable.

The transition graph is similar to the tuple-graph used in[START_REF] Barceló | Expressive languages for path queries over graph-structured data[END_REF] to detect dependency among variables.


Yuan Liu

Jean-Pierre Nikolovski

Nazih Mechbal

Moustapha Hafez

Michel Vergé

Tactile objects based on an amplitude disturbed diffraction pattern method

Tactile sensing is becoming widely used in human-computer interfaces. Recent advances in acoustic approaches demonstrated the possibilities to transform ordinary solid objects into interactive interfaces. This letter proposes a static finger contact localization process using an amplitude disturbed diffraction pattern method. The localization method is based on the following physical phenomenon: a finger contact modifies the energy distribution of acoustic wave in a solid; these variations depend on the wave frequency and the contact position. The presented method first consists of exciting the object with an acoustic signal with plural frequency components. In a second step, a measured acoustic signal is compared with prerecorded values to deduce the contact position. This position is then used for human-machine interaction ͑e.g., finger tracking on computer screen͒. The selection of excitation signals is discussed and a frequency choice criterion based on contrast value is proposed. Tests on a sandwich plate ͑liquid crystal display screen͒ prove the simplicity and easiness to apply the process in various solids. © 2009 American Institute of Physics. ͓doi:10.1063/1.3276549͔

In their work, Ing et al. 1,2 presented an acoustic timereversal process for in solid localization of finger "impact." Comparing with other acoustic approaches such as Rayleigh wave approach 3,4 or time-of-flight techniques, 5,[START_REF] Dieulesaint | French Patent No[END_REF] the timereversal technique can be applied to most solids without any prior knowledge of acoustic properties. However, many human-machine interfaces prefer "touch" sensing than impact localization, because touch is perceived as a more userfriendly interaction. 7,[START_REF] Malik | Proceedings of the 6th International Conference on Multimodal Interfaces ͑State[END_REF] Indeed, some modern interaction modes such as "multitouch" 9 are difficult to achieve with "impacts," since it requires generating several impacts simultaneously on the tactile surface.

Recently, an alternative method based on the crosscorrelation of selective absorption of the vibration modes has been presented. 10 This process is suitable for static contact localization. However, this process based on an absorption technique cannot address some particular uses such as stylus tip localization. In that case, contact creates more diffraction effect of the propagating acoustic waves than absorption. In this letter, we propose a tactile process based on an amplitude disturbed diffraction pattern ͑ADDP͒ phenomenon of an impulse acoustic wave. It expresses the following physical phenomenon: a human finger ͑or stylus͒ in contact with the objects affects the acoustic wave propagation in the solid. These disturbances depend on the finger position and the frequency of excited signal. With analysis and a calibration procedure of this variation, we can locate precisely the contact position.

In the following examples, two emitters ͑piezoelectric transducers Pz27 type by Ferroperm, Denmark͒ transmit repetitive Lamb waves ͑period 1 ms͒ in the solid Analytically, the received acoustic signal r͑t͒ can be expressed as a function of emitted signal e͑t͒, the object property and geometry G, the contact position P, and contact surface S at a given pressure a͒ Author to whom correspondence should be addressed. Electronic mail: jean-pierre.nikolovski@cea.fr.

͑1͒

The first step is a training step. The tactile surface of the object is divided into an array of predefined "contact points." For a copper plate 100ϫ 75ϫ 0.45 mm 3 large, 36ϫ 32 predefined points are sequentially touched by an artificial silicone finger. The contact surface, roughly 25 mm 2 , is assured by same contact pressure. The Fourier transform of received signal at each contact point P i,j can be expressed by Eq. ͑2͒ R i,j ͑f͒ = F͑E͑f͒,G, P i,j ,S͒. ͑2͒

In the following example, the E͑f͒ and G are constants, as we maintain the same conditions during the training step. The variation of S is negligible, so we consider that the received signal r͑t͒ is only function of contact position P R i,j ͑f͒ = F͑P i,j , f͒. ͑3͒

In the second step, the user touches the copper plate, say at position PЈ. The measured acoustic signal r Ј ͑t͒ is then com- pared with all stored training signals and an array of distances is calculated

D i,j = ͚ f ͉RЈ͑f͒ -R i,j ͑f͉͒. ͑4͒
The contact position can be visualized on a figure representing the normalized distances with a gray amplitude scale, as in Fig. 2. By using a recognition process of one measured signal among all the reference signals, we are able to find the position of contact.

Compared to the acoustic time-reversal process in which the acoustic signal is produced from the finger impact, meaning the acoustic plate is passive, this method enhances an active acoustic plate featuring a process that continuously generates Lamb wave packets, 1000/s. This tactile technology is said "active" as regards Lamb wave generation, meaning excitation signals are fundamental to its reliability.

We define a disturbed diffracted pattern contrast value as criterion of frequency choice. For that matter which defines another step in the tactile process, the plate is excited with a sinusoidal signal and followed by 70ϫ 60 sequentially contacts on the surface with an interval of 1 mm. The recorded signals are compared with the original signal obtained without contact. Figure 3 shows disturbed diffraction patterns at two different frequencies, one at 60 kHz, nonresonant, the other at 79.620 kHz, resonant. Images reveal different contrast features which is quantified with the contrast value formula.

Beforehand we calculate with Eq. ͑5͒ the mean derivative values of ADDP in the neighborhood of each contact point, except at boundaries. The neighborhood consists of eight neighboring points surrounding the point of interest

d i,j ͑f͒ = ͚ m=i-1 i+1 ͚ n=j-1 j+1 ͉R m,n ͑f͒ -R i,j ͑f͉͒/͓8 ء R i,j ͑f͔͒. ͑5͒
Then a mean derivative contrast value C͑f͒ for the entire ADDP image is calculated for one frequency which yields

C͑f͒ = ͚ i=2 69 ͚ j=2 59 d i,j ͑f͒/͑58 ء 68͒. ͑6͒
Applied to Fig. 3, the contrast values are 0.0134 at 60 kHz and 0.0247 at 79.62 kHz. This indicates that the ADDP is more spatially contrasted at resonance frequency. Uneven ADDP is not suitable for several reasons. First, ADDP at resonance frequencies depends a lot on boundary conditions of the object and also changes with ambient temperature variations. This would make it difficult to ensure process reliability even if frequency shifts due to temperature variations can be calculated and compensated. 11 However, it is not the case with boundary condition variations which cannot be predicted and compensated.

Second, at resonance frequencies, as ADDP is highly inhomogeneous and spatially redundant, as shown in Fig. 3͑b͒, many areas have the same amplitude variation values. As a consequence, it becomes difficult to clearly identify the contact position among several other eligible contact points.

Intermediate C͑f͒ values are associated with more regular ADDP which allow establishing a relationship between an amplitude signal variation and a contact point.

Very small C͑f͒ values are not suitable either, because it means uniform ADDP and then an impossibility to discriminate one contact position from the other.

As a consequence, nonresonant intermediate C͑f͒ values is the best criterion to validate a particular frequency. We propose a maximum threshold value of 0.02 and a minimum threshold value of 0.01, which have been tested and validated in our experiments with a copper plate and a liquid crystal display ͑LCD͒ screen; however, these values may be adjusted according to the situation.

Once a particular frequency is selected, we propose a criterion based on correlating a prospective ADDP to previously selected ones, to find out if adding another frequency fЈ helps improving the localization resolution. Following previous criterion, that frequency should first have a medium C͑f͒ value, then, its associated ADDP spatial distribution should be significantly different from all previous ones, because otherwise it would give similar information as regards discrimination of the contact point. Consequently, if there are already N frequency components in the excitation signal, the FIG. 2. Contrast images based on the normalized distances from one reference signal to all others. The contact position appears in black. Neighboring points exhibit small distances which implies a limit to the spatial resolution of the learning process.

Ά GNC͑0͒ =1, GNC͑N +1͒ = GNC͑N͒ ء 2 Nء ͟ i=1 N ͓1-Corr͑f i , fЈ͔͒. · ͑7͒
Where GNC͑N +1͒ is the revised value of GNC after adding a frequency. An additional frequency is accepted if the revised GNC value stays above 0.5.

Amplitude variations of acoustic signals are analyzed to make fuzzy partitions of the tactile surface and to indicate which part of the object is touched by the finger. If different frequencies have different ADDP as shown in Fig. 4,wecan combine several fuzzy partitions to go back to the exact position of contact with a high spatial resolution.

This ADDP tactile method is completely different from the absorption method 1 in previous work. Indeed, the absorption method is based on amplitude variations at resonance frequencies. With this method, working at resonance frequency is almost necessary because amplitudes of signal variation are easier to measure with thick materials. In this work we use only nonresonant frequencies as they have lower contrast values C͑f͒.

Our tactile process has been tested with different objects, such as glass plates, curved copper shells, or the upper layer of LCD screen. Figure 5 ͑video͒ illustrates the process applied to a 4 in. LCD screen. We use two emitters and one PZT receiver, all arbitrary shaped. 13ϫ 10 predefined tactile points are calibrated in the training step, a matrix of reference signals is then obtained.

The acoustic wave emitters and the receiver are placed on different layers, thus the acoustic waves propagate through the whole solid before being measured. This touch screen has a response time lower than 10 ms. As a mean of comparison, a time reversal process requires as many boundary reflections as possible to increase reliability and then a longer time window in order to digitize and cross-correlate acoustic signals. It is therefore more time consuming. With the presented ADDP method,a4m sacquisition window is enough.

In this letter, a tactile acoustic process based on ADDP is proposed and tested to transform various solids such as metal plates or LCD screens to real-time, drag-and-drop capable interactive objects. A method to select the frequency of the excitation signals is suggested. It is based on the calculation of normalized distances and selects preferably nonresonant frequencies. It requires simple signal processing and its efficiency in various solids has been proved. As it is derived from a time reversal approach, both methods share almost the same advantages and the same physical limitations. However, this active method allows the use of simple finger touch, which constitutes a real advance compared to previous work in state of the art.

  ͑Received 17 September 2009; accepted 25 November 2009; published online 23 December 2009͒

  Fig. 1. The excitation signals come from a Tektronix 3012 function generator and are composed of 40 frequency components. These frequencies are uniformly distributed between 20 and 100 kHz with an interval of 2 kHz. When a human finger comes in contact with the object, after a short stabilization time, say less than 1 ms, the acoustic waves are measured with one or two piezoelectric receivers. Typically, acoustic signals are digitized with a Pico ADC 212/50 data acquisition card during a 4 ms time window at a sampling frequency of 195.31 kHz. A computer is used to drive the function generator and the data acquisition card. Signal processing and image rendering are carried out in the Matlab environment.

FIG. 1 .

 1 FIG. 1. ͑Color online͒ Training step of the disturbed acoustic diffraction tactile process on a copper plate. 32ϫ 36 predefined positions are sequentially touched by an index; received reference signals from two PZT transducers are stored according to the contact positions.

FIG. 3 .

 3 FIG. 3. ͑Color online͒ ADDP based on relative amplitude variations according to the contact positions. With ͑a͒ an emission signal at an arbitrary frequency 60 kHz; or ͑b͒ at a resonance frequency 79.620 kHz.

  G. Ribay, S. Catheline, D. Clorennec, R. K. Ing, N. Quieffin, and M. Fink, IEEE Trans. Ultrason. Ferroelectr. Freq. Control 54, 378 ͑2007͒.

FIG. 4 .

 4 FIG.4. ͑Color online͒ Fuzzy partitions at different frequencies. Large number of diversified partitions makes it possible to find out a precise position of contact.