Keywords: Description logic, Refreshing semantics, Reasoning, Matching, Pattern containment. * (l q , t j , q t j ,0 ), * (q t j ,0 , t j , q t j ,1 1 , a, q t j ,2

Mes premiers remerciements vont tout naturellement vers mes directeurs de thèses, Marinette Bouet et Farouk Toumani. Merci pour votre temps, votre expertise, votre bienveillance et pour tout ce que que vous m'avez apporté aussi bien scientifiquement qu'humainement. Quelques mots ne suffiront jamais à exprimer la gratitude que j'éprouve à votre égard.

Je remercie également François Goasdoué, Nabil Layaïda et Mirian Halfeld Ferrari Alves d'avoir accepté d'évaluer ce travail de thèse ainsi que pour tous leur retours.

Je souhaite aussi remercier l'ensemble des membres du LIMOS avec une pensée toute particulière pour Béatrice qui trouve toujours une solution à mes problèmes.

Merci aux membres du département Génie Mathématique et Modélisation de Polytech de m'avoir fait confiance et permis de m'essayer à l'exercice d'enseignant. La variété des cours que vous m'avez confiée m'a permis de profiter pleinement de cette expérience.

Mes pensées se tournent maintenant vers mes collègues et amis qui ont égayé ces moments Merci Marina et Alexis C. pour vos précieux conseils et l'embellissement du bureau à Noël. Merci Matthieu pour ta gentillesse et ton aide avec les cours. Merci Alexis P. d'avoir partagé avec moi ce qui auraient pu être tes soliloques. Merci Ivan et Weixuan de m'avoir supporté au quotidien et d'avoir partagé avec moi votre culture.

Je termine ces remerciements par un immense Merci à mes proches pour leur

List of Figures

Introduction

Description Logics (DLs) are a family of knowledge representation and reasoning formalisms that have been proven useful in many application domains [START_REF] Baader | The description logic handbook: Theory, implementation and applications[END_REF]. DLs provide means for well-structured and formal representation of the conceptual knowledge of an application domain and various inference procedures to reason about the represented knowledge.

A DL Knowledge Base (KB) is composed of two components, called TBox and ABox, containing respectively general assertions describing relevant concepts and specific assertions about individuals and relationships among them.

For example, Table 1 depicts a KB made of two concept definitions, P rof essor and P hDStudent, where the concept P rof essor is described as a person who works in a university and has as a doctoral student : a PhD student. This knowledge base includes in addition assertions about individuals, stating that the individual Alan is an instance of P rof essor and Alice is an instance of P hDStudent, as well as assertion about a relationships between them (Alice is a doctoral student of Alan).

Query answering over DL KBs has recently emerged as an advanced mechanism for accessing data sources through an ontology [START_REF] Baget | Answering conjunctive regular path queries over guarded existential rules[END_REF][START_REF] Glimm | Conjunctive query answering for the description logic SHIQ[END_REF][START_REF] Calvanese | Data complexity of query answering in description logics[END_REF][START_REF] Xiao | Ontology-based data access: A survey[END_REF]. Indeed, in many application contexts, an ontology is used to formalize the conceptual information about the contents of multiple data sources. This knowledge is then exploited during query evaluation to deduce additional information to enrich query answers beyond the data that is explicitly stored in a source. General forms of queries investigated in the literature are first-order formula with possibly free variables [START_REF] Xiao | Ontology-based data access: A survey[END_REF]. As an example, consider the following conjunctive query which asks for a person that has a doctoral student: q ex (x) ← P ers(x), doctStudent(x, y)

The answers to such a query are a set of valid substitutions for the variables such that the KB entails the query. For example, an answer to the query q ex over KB 1 is Alan because the query σ(q ex ) obtained from q ex by substituting the variable x by σ(x) = Alan and y by σ(y) = Alice is entailed by the KB of Table 1.

Beyond such conventional queries in the pure database style, the description logic community has been interested very early by query languages that include explicit structural queries, i.e., queries asking about properties of individual and concepts [START_REF] Borgida | Asking queries about frames[END_REF]. In particular, the notion of concept patterns, i.e., concept descriptions containing variables, has been introduced in the mid-nineties as a declarative approach to specify queries over knowledge bases where the answers to such queries can be concepts : "Instead of just returning sets of individuals, our queries match concepts and filtered fragments of descriptions" [START_REF] Borgida | Asking queries about frames[END_REF]. As an example, consider the following pattern Q defined as an unknown part X with a certain relationship y with a university. Q ≡ X ⊓ ∃y.U niv P rof essor ≡ P ers ⊓ ∃worksIn.U niv ⊓ ∃doctStud.P hDStudent P hDStudent ≡ P ers ⊓ ∃studyIn.U niv ⊓ ∃advisor.P rof essor P rof essor(Alan), doctStud(Alan, Alice), P hDStudent(Alice)

Table 1: A DL knowledge base KB 1 .

Here, the variable X (called a concept variable) takes its values from a set of possible descriptions while the variable y (called a role variable) takes its values from a set of possible atomic role names. Such a query Q can be evaluated against an individual i or against a concept C. The query semantics is given by the notion of matching. For example, the individual Alan of the knowledge base KB 1 of Table 1 matches the pattern Q because if we consider the substitution σ such that σ(X) = P ers ⊓ ∃doctStudent.P hDStudent and σ(y) = worksIn then KB 1 entails the assertion σ(Q)(Alan) (i.e., Alan is an instance of σ(Q)). Similarly, the concept P rof essor matches the pattern Q because by considering the same substitution σ the knowledge base KB 1 entails P rof essor ⊑ σ(Q) (i.e., P rof essor is subsumed by the concept σ(Q)). A natural way to give a formal meaning to matching is through the notion of subsumption: given a description C and a pattern Q, the matching problem modulo subsumption asks whether there is a variable substitution such that C is subsumed by σ(Q) [START_REF] Borgida | Asking queries about frames[END_REF].

This thesis focuses on the extension of the notion of patterns to capture recursive queries, a class of queries which is intensively used in many modern application domains such as graph databases and semantic web. However, such an extension is far from being trivial and it requires to revisit the semantics of variables as illustrated below.

Example 1. Consider the following recursive query specified as a cyclic pattern and evaluated over the knowledge base KB 1 of Table 1: Academic ≡ P ers ⊓ ∃x.U niv ⊓ ∃y.Academic

Using standard semantics of variable substitution, whatever the considered substitution of the role variables x and y, neither of the concept P rof essor nor P hDStudent of KB 1 match the pattern Academic. However, the situation becomes different if we exploit a different semantics that enables to refresh the values of the variable x and y when unfolding the pattern Academic. We show below a partial unfolding of Academic where the variable x and y are refreshed (i.e., replaced by new variables) at each iteration over the concept Academic.

Academic ≡ P ers ⊓ ∃x 1 .U niv ⊓ ∃y 1 . (P ers ⊓ ∃x 2 .U niv ⊓ ∃y 2 .(. . .))

Academic

With such a semantics at hand, it becomes possible to compute a matcher that makes the concept P rof essor matching the pattern Academic (e.g., take a substitution that maps the first occurrences of x and y to worksIn and doctStud while their second occurrences are respectively mapped to studyIn and advisor). The obtained instantiation of the pattern Academic is the following: σ(Academic) ≡ P ers ⊓ ∃worksIn.U niv⊓ ∃doctStud.(P ers ⊓ ∃studyIn.U niv ⊓∃advisor.σ(Academic))

This thesis studies the extension of description logics with variables equipped with refreshing semantics in order to capture the expression of recursive structural queries as cyclic concept patterns. More specifically, we focus on a new description logic, called EL RV , that extends the description logic EL with refreshing role variables. Our definition of EL RV -patterns deviates from the one used in the literature with respect to the following features: (i) our definition of patterns is restricted to role variables while the literature mainly focuses on concept variables, and (ii) we support cyclic pattern definition and allow two different types of semantics for variables (i.e., refreshing and not refreshing semantics).

Viewing patterns as queries, we study three fundamental reasoning problems in the context of the logic EL RV , namely, matching , weak-subsumption and pattern containment.

Matching is used as core mechanisms to evaluate patterns over knowledge bases (i.e., computing answers to a query pattern) while pattern containment enables to determine when the answers of a pattern are contained in the answers of another pattern whatever the considered knowledge base. On an other side, weak-subsumption and matching can be viewed as extensions of respectively matching and unification to variables with refreshing semantics. More precisely, we make the following technical contributions:

• We introduce the description logic EL RV which extends the logic EL with refreshing variables. This extension impacts the semantics of pattern which can now produce infinite instances. We differentiate two kinds of instances : regular and irregular instances. A regular instances can be represented with a finite number of descriptions which corresponds to a finite EL-TBox. An instance is irregular if it can not be represented by such a TBox. Subsumption between regular instances in EL RV is equivalent to subsumption with regard to the greatest fix-point semantics in EL.

• We define three different reasoning tasks over EL RV ontologies. Matching and weak-subsumption are extension of respectively matching and unification, two nonstandard reasoning tasks of description logic with non-refreshing variables. Moreover, we introduce a brand new reasoning task: pattern containment. Pattern containment emphasizes on comparing patterns independently of the knowledge base. We demonstrate that if a solution exists then there exists a regular solution.

• We establish a correspondence between EL RV and a specific form of variable automata. This form, called description automata, entails all the instances of a pattern (i.e. regular and irregular) in a finite form. Reasoning in EL RV is then proven to be equivalent to study variants of simulation between description automata.

• We devise an algorithm to solve the different reasoning tasks resulting in proving that they are exptime-complete. We demonstrate their correctness leading to an exptime upper bound. The lower bound is obtained by reducing matching ( which is a special case of both pattern containment and weak-subsumption) to halting problem of alternating turing machine working on polynomially bounded input which is known to be exptime-complete [START_REF] Chandra | Alternation[END_REF].

This document presents research conducted in the context of this thesis separated in five chapters. Chapter 1 deals with preliminary notions of trees and description logics. It offers insights of both syntax and semantics of description logics. This chapter ends by presenting terminologies and how to reason over in order to make implicit knowledge explicit with the inference task known as subsumption.

Chapter 2 presents how variables and description logics can be combined. It first discusses the inferences tasks matching and unification that deals with non-refreshing variables. Introducing EL RV , a logic extending EL with refreshing variables, allows to defined pattern queries. Patterns queries are a set of EL RV -patterns allowing to query the knowledge base through different reasoning mechanisms : matching, weak-subsumption and pattern-containment. Finally, this chapter discusses the existence of regular solutions which can be expressed with finite EL-TBox.

Chapter 3 presents description automata, a class of automata that handles refreshing semantics. We strengthen the link between reasoning in description logics and automata theory by reducing reasoning in EL RV to reasoning with description automata. This reduction are based on variants of simulation which allow to solve matching, weaksubsumption and pattern containment.

Chapter 4 solves matching problem in EL RV . We design an algorithm, Check Match, that proves matching decidability in EL RV . This algorithm is inspired of product automata and consists in running simultaneously the two automata to construct a solution to the issued problem.

Chapter 5 emphasizes on discussing decidability for pattern containment and weaksubsumption. In these problems, variables may appear on both sides. Moreover, in case of pattern containment, the domain of variable valuation is infinite. The correct algorithm Check Simu ,inspired of Check Match, demonstrates that pattern containment and weaksubsumption are decidable. We prove that reasoning in EL RV is exptime-complete Chapter 1

Preliminaries

In this chapter, we introduce the technical background required for this thesis. We define trees and basics of description logics. The different notations introduced in this chapter are summarized in the Table 1.1.

Symbol Description

Labeled tree with τ the set of nodes, (τ, λ, δ) λ the node labeling function and δ the edge labeling function.

⊤

Trees

We use the following definition of a tree [START_REF] Henzinger | An assume-guarantee rule for checking simulation[END_REF]: A tree is a set τ ⊆ N * such that if xn ∈ τ , for x ∈ N * and n ∈ N, then x ∈ τ and xm ∈ τ for all 0 ≤ m < n. The elements of τ represent nodes: the empty word ε is the root of τ , and for each node x, the nodes of the form xn, for n ∈ N, are children of x. Given a pair of sets S and M , an ⟨S, M ⟩-labeled tree is a triple (τ, λ, δ), where τ is a tree, λ : τ → S is a node labeling function that maps each node of τ to an element in S, and δ : τ × τ → M is an edge labeling function that maps each edge (x, xn) of τ to an element in M .

We recall now the notion of tree homomorphism. Let t 1 = (τ 1 , λ 1 , δ 1 ) and t 2 = (τ 2 , λ 2 , δ 2 ) be two trees. A homomorphism from t 1 into t 2 is a mapping Z : τ 1 → τ 2 such that:

(i) Z(ε) = ε, and (ii) δ 2 (Z(c 1 ), Z(c ′ 1 )) = r, for all δ 1 (c 1 , c ′ 1 ) = r. A partial tree (tau ′ , λ ′ , δ ′ ) of a tree (τ, λ, δ) is such that there exists an homomorphism Z from (τ ′ , λ ′ , δ ′ ) to (τ, λ, δ) and in addition, λ ′ (i) = λ(Z(i)).

Description Logic 1.2.1 Introduction

"Description Logics" (DL) denotes a family of knowledge representation formalism that aims to transcript information about a specific domain. The representation offers a formal logic-based semantics used to describe an application domain. The domain is formalized by defining its relevant concepts (its terminology). They are of latter use to characterize the instances of this domain. Representing a domain requires to not only defines entities and their features but also to capture their relationships. The following vocabulary will be used :

• A concept is an unary predicate that represents a set of individual having specific features in commons. • A role is a binary relationship between individuals.

• An individual is an instance of a concept. Description logics do not limit themselves to description. Indeed, they offer a wide variety of reasoning mechanisms allowing to infer implicit knowledge from the explicit knowledge represented.

A Description logic L is a tuple made of (N A ,N R , C). N A and N R represents respectively primitive concepts and primitive roles corresponding to elementary knowledge. Elementary knowledge are by essence knowledge that can not be described and carry meaning by themselves. The constructors C allow to combine elementary knowledge in order to create complex descriptions denoted as L-descriptions. Since constructors formalize how knowledge can be associated, they dictate a logic L expressiveness.

In the remaining, we use the letters A, B to range over N A ; R, S to range over N R ; and C, D to range over L-concept descriptions (or simply, L-concepts).

The syntax and semantics of the description logic EL will now be explained.

The Description Logic EL

Syntax.

The Description logic EL which stands for Existential Language has been provided with three constructors :

• top concept (⊤),

• conjunction (⊓) and • existential restriction (∃R.C).

Chapter 1 Preliminaries

Description Logic

Given a set of atomic concepts N A and a set of roles N R , EL-descriptions are built according to the following syntax rules :

C := ⊤|A|C ⊓ D|∃R.C where A ∈ N A , R ∈ N R and C,D are EL-concept descriptions.
Even though EL offers few constructors it has been of interest for some application domains while displaying reasonable complexity for reasoning tasks. For instance, it can be used to define biomedical ontologies like Snomed CT [START_REF] Côté | Systematized nomenclature of human and veterinary medicine : Snomed international[END_REF] or the Gene Ontology. These ontologies can be seen as EL-TBoxes. Moreover, an extension of EL became also a standard for a subset of OWL 2. OWL stands for the Web Ontology Language which can be used to exploit reasoning procedures [START_REF] Horrocks | Owl: a description logic based ontology language for the semantic web[END_REF].

Example 2. To give examples of what can be expressed in EL, we suppose that U niversity and P erson are atomic concepts (i.e. {U niversity, P erson} ⊆ N A ) and study and teach are atomic roles (i.e. {study, teach} ⊆ N R ). Intuitively, P erson⊓∃study.U niversity and P erson⊓∃teach.U niversity are concepts describing respectively students and professors of a university. Existential restriction can be weakened by using the concept ⊤ to describe P erson ⊓ ∃teach.⊤ which defines a teacher as a person who is teaching at any educational level. Now that the syntax for each constructors has been provided, their semantics will be discussed.

Semantics.

The semantics of EL is formalized in terms of interpretation. An interpretation I is a pair (∆ I , . I ) where ∆ I is a non-empty set called the domain and . I is an interpretation function that assigns binary relations on ∆ I to role names and subsets of ∆ I to EL-concepts as shown in the semantics column of the following Table in In EL, it is possible to construct EL-description trees based on EL-description. The root of the tree corresponds to the EL-description. Each node of the tree corresponds to a concept, label of a node is made of primitive concepts appearing without existential restriction. For each existential restriction there is an edge labeled by the corresponding role to a new node representing the reached concept. A subsumption relationship, C ⊑ D is characterized by a homomorphism from the tree of D into the tree of C [START_REF] Baader | Computing least common subsumers in description logics with existential restrictions[END_REF].

1.2. Name Syntax Semantics Top concept ⊤ ∆ I Concept name A A I ⊆ ∆ I Role name R R I ⊆ ∆ I × ∆ I Conjunction C ⊓ D C I ∩ D I Existential restriction ∃R.C { a ∈ ∆ I |∃b ∈ C I .(a, b) ∈ R I } Table 1
A DL Knowledge Base (KB) is composed of two components, called TBox T and ABox A, containing respectively general assertions describing relevant concepts and specific assertions about individuals and relationships among them.

Terminologies.

Concept descriptions enable to describe class of objects. In order to specify how concepts relate to each other, description logics make use of terminological axioms. A terminological axiom can take the form of :

• An equality C ≡ D or • An inclusion C ⊑ D.
Semantics of axioms is also determined through an interpretation I. As expected, a terminological axiom C ⊑ D (resp. C ≡ D ) is satisfied by an interpretation I, if C I ⊆ D I (resp. C I = D I ). Let T be a set of terminological axioms, I satisfies T if and only if I satisfies each axiom of T . Two axioms ( or two sets of axioms ) are equivalent if they have the same models.

Different kinds of TBoxes are considered regarding properties of their axioms' set. From the less expressive to the most expressive, we have :

• Empty TBoxes : This class refers to TBoxes with no axiom.

• Simple TBoxes : TBoxes of this class are made of a set of equality axioms denoted as concept definitions. A concept definition is an equality axiom where the left-hand side is a concept name. The remaining will emphasize over simple TBox T which will be of later interest. This class corresponds to a set of concept definitions of the form P ≡ C, with P ∈ N def and C an EL-concept such that no P appears more than once on the left-hand side of a definition in T . Concept names appearing on the left-hand side of a definition are called defined concepts, and denoted by the set N def . All the other concepts occurring in T are called atomic concepts and are denoted by the set N A .

Example 5. Back to Example 3, we have : The semantics introduced previously is denoted as the descriptive semantics. However, terminologies may require to represent cyclic dependencies between defined concepts, i.e., a definition of an EL-concept P directly or indirectly refers to P itself. When cycles are involved, this semantics may be limiting [START_REF] Nebel | Terminological cycles[END_REF] and other semantics could be used, in particular greatest fix-point and least fix-point semantics [START_REF] Baader | Terminological cycles in a description logic with existential restrictions[END_REF]. The general idea is to extend a primitive interpretation J (i.e. an interpretation of primitive concepts and primitive roles) to the defined concepts of the TBox. An interpretation I is based on J if it has the same domain as J (i.e. ∆ I = ∆ J and its interpretation function coincides with the one of J on N A and N R (i.e. A I = A J and R I = R J ∀A ∈ N A and ∀R ∈ N R ). Given two interpretations I 1 and I 2 based on the same interpretation J , we have I 1 ⪯ J I 2 if and only if C I 1 ⊆ C I 2 , ∀C ∈ N def . It has been demonstrated in [START_REF] Baader | Terminological cycles in a description logic with existential restrictions[END_REF] that there exists a unique model of I of T such that :

• N A = {P erson, U
1. I is based on the primitive interpretation J , and 1.2 Description Logic Chapter 1 Preliminaries 2. I ′ ⪯ J I, ∀I ′ of T based on J Such a model is defined as a gfp-model of T . Lfp-model can be defined similarly by exchanging I ′ and I roles in [START_REF] Baader | Using automata theory for characterizing the semantics of terminological cycles[END_REF]. In order to illustrate and to develop benefits of considering different semantics, we will use the following Example 7 from [START_REF] Baader | Terminological cycles in a description logic with existential restrictions[END_REF].

Example 7. Let T = {IN ode ≡ N ode ⊓ ∃edge.IN ode} . This TBox contains a primitive concept, N ode and a primitive role, edge. The only definition IN ode is cyclic and represents node involved in an infinite path. Let consider the primitive interpretation J defined as follows :

• ∆ J = {m 0 , m 1 , m 2 , . . .} ∪ {n 0 } • N ode J = ∆ J • edge J = {(m i , m i+1 )|i ≥ 0} ∪ {(n 0 , n 0 )}
Nodes can be involved in an infinite path if it belongs to a cycle (n 0 ) or if it is involved in an infinite path (m i ). As a consequence, there are four ways to extend J .

1. {m 0 , m 1 , m 2 , . . .} ∪ {n 0 } 2. {m 0 , m 1 , m 2 , . . .} 3. {n 0 } 4. ∅
All of this models are models for the descriptive semantics. The last possibility, which represents the least-fix point model, is not relevant w.r.t the aimed definition. The first possibility, which is the greatest fix-point model, captures exactly the semantics of IN ode we are aiming for. Indeed the remaining models ignores either cycles [START_REF] Baader | Using automata theory for characterizing the semantics of terminological cycles[END_REF] or infinite paths (3). Greatest-fix point semantics is not always the best choice regarding concepts involved. Let consider the following concepts : T iger = Animal ⊓ ∃P arent.T iger and Lion = Animal ⊓ ∃P arent.Lion From a gfp point of view, T iger and Lion will always be interpreted the same way. The descriptive semantics on the other hand may interpret them differently which seems more appropriate.

Those definitions can easily be transferred to CGI by using semantics of equality and inclusion axioms. Moreover in case of an acyclic TBoxes, descriptive, greatest fix-point and least fix-point semantics are equivalent.

Normal Form

Alongside TBoxes, normal form of concept descriptions have been introduced. Normal form of an EL-description is a conjunction of EL-atoms. An EL-atom is either a primitive concept (i.e. an element of N A ) or an existential restriction of the form ∃R.C with C ∈ N def . Concretely, we say that a description C ≡ D is normalized if D is of the form :

A 0 ⊓ ... ⊓ A n ⊓ ∃r 0 .B 0 ⊓ ... ⊓ ∃r m .B m Chapter 1 Preliminaries 1.2 Description Logic where A 0 , ..., A n ∈ N A , r 0 , ...r m ∈ N R and B 0 , ..., B m ∈ N def .
Any EL-description can be transformed into a normalized form. In order to achieve the normalization process, definitions may be added to the terminology. This process has proven to be polynomial in [START_REF] Baader | Terminological cycles in a description logic with existential restrictions[END_REF]. As stated in this report, the resulting TBox may change w.r.t to the considered semantics. Normal forms are often used to solve reasoning tasks. Indeed, they define a standard form for description which simplifies the algorithm without damaging the complexity since this transformation is polynomial for EL.

Example 8. Back to Example 3, F rance and F renchU niversity are concepts in normal form. However, concepts F rance, Student and T eacher are not normalized since a primitive concept appears after an existential restriction. As a consequence, two new defined concept C 1 and C 2 are created. Their definition will respectively correspond to the primitive concept P aris and U niversity. However, C 1 and C 2 do fulfill the requirements of normal form. The normalized form of this TBox is :

F rance ≡ Country ⊓ ∃hasCapital.C 1 F renchU niversity ≡ ∃locate.F rance ⊓ U niversity Student ≡ ∃study.C 2 ⊓ P erson T eacher ≡ ∃teach.C 2 ⊓ P erson C 1 ≡ P aris C 2 ≡ U niversity Reasoning in EL w.

r.t a Terminology

Reasoning mechanisms unleash the potential of a terminology. Indeed, reasoning mechanisms allow to infer knowledge that is not explicitly expressed. There exists many reasoning procedure which can be qualified as standard like satisfiability or even nonstandard procedures like computing the least common subsumers, concept difference [START_REF] Baader | Computing the least common subsumer in the description logic EL w.r.t. terminological cycles with descriptive semantics[END_REF][START_REF] Baader | Least common subsumers and most specific concepts in a description logic with existential restrictions and terminological cycles[END_REF][START_REF] Baader | Standard and non-standard inferences in the description logic FL 0 using tree automata[END_REF][START_REF] Baader | Computing least common subsumers in description logics with existential restrictions[END_REF][START_REF] Zarrieß | Most specific generalizations wrt general EL-tboxes[END_REF]. However, we focus in this thesis on the subsumption inference problems and its non-standard extensions which will be discussed later. This problem is named after the relationship subsumption. It aims to statute whether a concept C is more general than a concept D or not. Subsumption in EL is proven to be polynomial and that, with or without TBox. In many cases, extensions of EL with more constructors leads to exptime-complete [START_REF] Baader | Pushing the EL envelope[END_REF][START_REF] Brandt | Polynomial time reasoning in a description logic with existential restrictions, gci axioms[END_REF]. However, compared to other logics with few constructors like FL 0 , it is an interesting feature. Indeed, FL 0 and its derived logics suffered from a blow-up of complexity while considering TBoxes. Subsumption in FL 0 is co-np-complete [START_REF] Nebel | Terminological reasoning is inherently intractable[END_REF], pspace-complete [START_REF] Kazakov | Subsumption of concepts in dl FL 0 for (cyclic) terminologies with respect to descriptive semantics is pspace-complete[END_REF] and exptime-complete [START_REF] Baader | Standard and non-standard inferences in the description logic FL 0 using tree automata[END_REF] for respectively acyclic, cyclic and general TBoxes.

It is worth to note that EL-concept descriptions of simple TBoxes can be viewed as directed labeled graphs. This representation unravel another characterization of subsumption in EL. Subsumption between EL-concept descriptions can be reduced to the existence of simulation between the graphs of the concept descriptions. In case of cyclic terminologies, there exists additional properties in order to support the different descriptive and fix-point semantics [START_REF] Baader | Terminological cycles in a description logic with existential restrictions[END_REF].

Conclusion of Chapter 1

This chapter covers the notion of trees which are seen as a tuple (τ, λ, δ) as well as the definition of homomorphism between trees. This relationship plays a key-role since it is linked with subsumption in description logics.

This chapter also emphasizes on the formal preliminaries of description logics using EL, which will be of later interest, as supporting example. It has introduced the syntax of a description logic as well as the semantics associated with. Considering a terminology impacts the semantics since cycle may requires different care. There are three main semantics known as descriptive semantics, greatest fix-point semantics and least fix-point semantics. It ends with the definition of the subsumption inference tasks named after the relationship between two concepts. Next chapters shows how logics can be enhanced with variables and the consequence over the subsumption inference mechanism.

Chapter 2 Refreshing Semantics in EL

This chapter presents how variables and description logics can be combined. Under the non-refreshing semantics, this combination notably led to the inference tasks : matching [START_REF] Baader | Matching in description logics[END_REF][START_REF] Baader | Matching in the description logic FL 0 with respect to general tboxes[END_REF][START_REF] Baader | Matching in description logics with existential restrictions[END_REF][START_REF] Baader | Matching with respect to general concept inclusions in the description logic EL[END_REF] and unification [START_REF] Baader | Extending unification in el towards general tboxes[END_REF][START_REF] Baader | Unification in the description logic EL[END_REF][START_REF] Baader | Unification of concept terms in description logics[END_REF]. After briefly exposing the benefits of considering variables with a refreshing semantics, EL RV is defined. EL RV extends EL by allowing refreshing variables as well as pattern queries. Patterns queries are a set of EL RV -patterns allowing to query the knowledge base through different reasoning mechanisms : matching, weak-subsumption and pattern-containment. Finally, this chapter discusses the existence of regular solution which can be expressed with finite EL-TBox. Notation introduced in this chapter are summarized in Table 2 Recently, expressiveness of description logics have been pushed forward with the introduction of variables. The set N X complements the sets of concept names, N A and N def , as well as roles N R . This set is made of both concept and role variables leading to two subsets N R X which denotes the set of variable replacing roles names and, N C X corresponding to variables standing for concept descriptions. Like any role or concept, variables can be used by constructors to build description that may contain variables. In this context, those descriptions are denoted as patterns. A ground description opposes this definition in the sense that it is a description without any variable.

Example 9.

Doctor ≡ P erson ⊓ ∃getP hDIn.U niv ⊓ ∃f ormerly.P hDStudent P hDStudent ≡ P erson ⊓ ∃studyIn.U niv ⊓ ∃supervisedBy.Doctor P attern ≡ X ⊓ ∃y.U niv In this example, Doctor and P hDStudent are ground description since they do not contain any variables. However, Academic possesses two variables X a concept variable and y a role variable.

An EL-Pattern is in normal form if:

P ≡ V 1 ⊓ ... ⊓ V n ⊓ ∃r 1 .B 1 ⊓ ... ⊓ r m .B m where V 0 , ..., V n ∈ N A ∪ N C X , r 0 , ..., r m ∈ N R ∪ N R X and B 0 , ..., B m ∈ N def ∪ N C X .
Even if the syntax for variables is clear, their semantics remains to be defined. A natural way to define semantics is through variable substitutions. Formally, a substitution function σ is a mapping from N X into the set of EL-concept description and primitive roles. It allows to map role (resp. concept) variables into roles (resp. concept descriptions). Obviously σ is extended to element of N A and N R by considering identity. Substitution functions are applied directly on EL-patterns using the following rules :

• σ(A) = A if A ∈ N A ∪ {⊤} • σ(C ⊓ D) = σ(C) ⊓ σ(D) with C,D two EL-patterns. • σ(∃R.C) = ∃σ(R).σ(C) with σ(R) = R if R ∈ N R Example 10. Let consider σ 1 , σ 2 such that :
• σ 1 (X) = P erson ⊓ ∃doctStudent.P hDStudent and σ 1 (y) = worksIn.

• σ 2 (X) = P erson and σ 2 (y) = studyIn .

Applying σ 1 and σ 2 to the previously introduced concepts results in : σ 1 (Doctor) ≡ σ 2 (Doctor) ≡ Doctor σ 1 (P hDStudent) ≡ σ 2 (P hDStudent) ≡ P hdStudent σ 1 (P attern) ≡ P erson ⊓ ∃doctStudent.P hDStudent

σ 1 (X) ⊓∃ worksIn σ 1 (y)
.U niv σ 2 (P attern) ≡ P erson

σ 2 (X) ⊓∃ studyIn σ 2 (y)
.U niv Subsumption changed in order to handle patterns and their variables. It evolved in two, interesting and non-standard, reasoning tasks known as matching and unification.

The matching problem aims to compare a pattern P and a ground description C w.r.t to the subsumption relationship. It consists in looking for a substitution σ such that the resulting concept σ(P ) fulfills a subsumption relationship with C. If such a substitution exists, it is considered as a solution and called a matcher. State of the art defines variations of the matching problem which are known as matching problem modulo equivalence and matching problem modulo subsumption.

Definition 2 (Matching Problem). Let T be a TBox, P an EL-pattern and C an ELground-description. Since matching aims to compare a ground-description and a pattern, matching problems modulo subsumption differs depending on the side of the pattern [START_REF] Baader | Matching in description logics[END_REF]. When the pattern is on the left, we talk about right-ground matching problem. On the other hand, if the pattern is on the right, it is a left-ground matching problem. Note that since {C ⊑ ? P } ≡ {C ⊓ P ≡ ? C}, any left-ground matching problem modulo subsumption can be resumed to a matching problem modulo equivalence.

However, in the case of a right-ground matching problem then we have {P ⊑ ? C} ≡ {P ⊓ C ≡ ? P }. The resulting equation modulo equivalence involve a pattern in both sides which is exactly the definition of unification. Definition 3 (Unification Problem). Let T be a TBox and P, Q two EL-patterns.

• A unification problem modulo equivalence w.r.t. a TBox T is an equation of the form P ≡ ? T Q. It has a solution if there exists a substitution σ such that σ(P ) ≡ T σ(Q) • A unification problem modulo subsumption w.r.t. a TBox T is an equation of the form P ⊑ ? T Q. It has a solution if there exists a substitution σ such that σ(P ) ⊑ T σ(Q)

For a unification problem [START_REF] Baader | Extending unification in el towards general tboxes[END_REF][START_REF] Baader | Unification in the description logic EL[END_REF][START_REF] Baader | Unification of concept terms in description logics[END_REF], the solutions are called unifiers. Since we have {P ⊑ ? Q} ≡ {P ⊓ Q ≡ ? P }, any unification problem modulo equivalence has a corresponding unification problem modulo subsumption. Although being recent, these problems have been attracting attention of many research for different settings. The next section focuses on known results for this reasoning tasks with regard to the state of the art.

Reasoning with Variables

Matching and unification problems aroused in description logics in late 90s. Those problem have shown proficiency to filter out the unimportant aspects of large concept descriptions appearing in knowledge base [START_REF] Borgida | Classic: A structural data model for objects[END_REF]. They can also be used as a tool in databases to detect redundancies [START_REF] Baader | Unification of concept terms in description logics[END_REF] or support integration [START_REF] Borgida | what's not in a name?" initial explorations of a structural approach to integrating large concept knowledge-bases[END_REF]. All of those applications exploit the capacity of a pattern to express a not completely specified form.

The literature around matching and unification problems mainly focuses on concept variables. Indeed, role variables are little considered because in logics without role constructors, solving the problem can be done by enumerating possibilities [START_REF] Baader | Unification of concept terms in description logics[END_REF].

So far, two families of logics have been widely investigated known as FL 0 based logics and EL based logics. Note that both of this family offer conjunction and either existential restriction (∃R.C) or value restriction (∀R.C). As a direct consequence, concept variables can be substitute by an infinity of possibilities. Thus preventing from enumerating potential solutions. FL 0 is a logic that allows for concept conjunction ⊓, value restriction ∀R.C and universal concept ⊤. Among the extensions of FL 0 that have been of interest, there are FL ⊥ , FL ¬ and ALN . FL 0 is extended by successively enriching its constructors to form these logics. Starting with FL ⊥ that unlocks the unsatisfiable concept (⊥). Then FL ¬ allows ⊥ and atomic negation (¬) and finally ALN extends FL 0 with ⊥, atomic negation (¬), unqualified number restriction ( ≤ n.R -≥ n.R). On the other hand ALE offers limited existential restriction (∃R.C) instead of unqualified number restriction.

Matching

Research on matching problems in FL 0 led to prove that this problem is polynomial without TBox [START_REF] Baader | Matching in description logics[END_REF] as well as in its extensions except ALE which will be discussed below. Those results have been achieved by exploiting the reduction, presented in [START_REF] Baader | Using automata theory for characterizing the semantics of terminological cycles[END_REF], of subsumption to language inclusion. Combining role variables and concept variables for FL 0 without TBox increases the complexity and is np-complete [START_REF] Baader | Unification of concept terms in description logics[END_REF].

Considering a general TBox blows up the complexity to exptime-complete [START_REF] Baader | Matching in the description logic FL 0 with respect to general tboxes[END_REF]. This results have been proved by extending the previous method based on automata theory and language inclusion. In their work, the authors introduced restricted TBoxes which offers a reduced complexity for this reasoning task. Those TBoxes are called forward Tboxes, i.e. TBoxes where the role depth on the left-hand side of a GCI is not larger than the role depth on the right-hand side. Forward TBoxes bears the advantage to lower the complexity to pspace-complete in this case. Similarly, considering backward Tboxes, i.e. TBoxes where the role depth on the right-hand side of a GCI is not larger than the role depth on the left-hand side, bears the same property.

EL-matching problem has a higher complexity by achieving np-complete even without TBoxes. Baader et al. [START_REF] Baader | Matching in description logics with existential restrictions[END_REF] demonstrated it by reducing matching into finding a homomorphism between description trees. The same method has been applied to ALE leading to the same complexity. EL does not suffer any blow up of complexity when considering a general TBox. The approach proposed in [START_REF] Baader | Matching with respect to general concept inclusions in the description logic EL[END_REF] exploits structural subsumption through a goal-oriented algorithm. Complexity results regarding matching problem are summarized in Table 2.2.

Description Logic

TBox Complexity

FL 0 ∅ ptime [1]
General Forward Tbox pspace-complete [START_REF] Baader | Matching in the description logic FL 0 with respect to general tboxes[END_REF] General Backward Tbox pspace-complete [START_REF] Baader | Matching in the description logic FL 0 with respect to general tboxes[END_REF] General Tbox exptime-complete [START_REF] Baader | Matching in the description logic FL 0 with respect to general tboxes[END_REF] FL ⊥ , FL ¬ , ALN ∅ ptime [START_REF] Baader | Matching in description logics[END_REF] General Tbox open

EL ∅ np-complete [12]
Acyclic Tbox np-complete [START_REF] Baader | Matching in description logics with existential restrictions[END_REF] General Tbox np-complete [START_REF] Baader | Matching with respect to general concept inclusions in the description logic EL[END_REF] ALE ∅ np-complete [START_REF] Baader | Matching in description logics with existential restrictions[END_REF] Table 2.2: Complexity results for matching

Unification

Unification considers equations of the form P ⊑ ? Q where both, P and Q are patterns. The major result for FL 0 is that unification of FL 0 -concept terms (i.e. w.r.t to empty Tbox) is exptime-complete [START_REF] Baader | Unification of concept terms in description logics[END_REF]. The authors used a similar approach to the one used to solve matching (i.e. reducing the problem to language inclusion problems). The extension of unification in FL 0 to general TBoxes is still an open-problem. FL ⊥ has also been investigated leading to unification w.r.t to an empty TBox to be in exptime [START_REF] Morawska | Unification in the description logic FL ⊥[END_REF].

The method employed consists in eliminating ⊥ from a given problem leading to a FL 0 problem that can be solved by known methods.

Likewise EL-matching, EL-unification is np-complete for empty TBox [START_REF] Baader | Unification in the description logic EL[END_REF]. Authors demonstrated that a local unifier could be defined and necessarily exists if a unifier exists. Then a goal-oriented algorithm has been designed to decide if such a local unifier can be computed. Research towards unification with general TBoxes are more advanced than those for FL 0 . Indeed, even if EL-unification w.r.t general TBoxes is still an open problem, in [START_REF] Baader | Extending unification in el towards general tboxes[END_REF] the authors achieved np-complete for cyclic restricted TBoxes. The restriction prohibits cycle of the form A ⊑ ∃R 1 .∃R 2 . . . . ∃R n .A. Such a cycle contradicts the definition of local unifier thus making their algorithm incomplete.

In an attempt to lower unification complexity variants of unification have been investigated. These variants are known as restricted unification [START_REF] Baader | Restricted unification in the dl FL 0[END_REF][START_REF] Baader | Restricted unification in the dl EL[END_REF]. It can be either syntactically restricted (i.e. limiting the role depth of concepts) or semantically restricted (i.e. limiting the length of interpretation). Such restrictions are derived from observations when it comes to choose a unifier among the proposed solutions. They allow to obtain a resulting concept close to the shape of those in the knowledge base. Regarding complexity of these reasoning tasks in FL 0 , let k be the limit depth allowed. Then, it is shown in [START_REF] Baader | Restricted unification in the dl FL 0[END_REF] that it remains in exptime if k is encoded in binary but drops to pspace if k is encoded in unitary. Unfortunately, none of the result followed for EL, it remains np-complete [START_REF] Baader | Restricted unification in the dl EL[END_REF] . The different results for concept variables are summarized in Table 2.3.

Description Logic

TBox Complexity

FL 0 ∅ exptime-complete [16]
General Tbox open

FL ⊥ ∅ in exptime[33] FL ¬ , ALN ∅ open EL ∅ np-complete [14] Acyclic Tbox np-complete [14] Cyclic Restricted np-complete [6] General Tbox open ALE ∅ open Table 2.

3: Complexity results for unification

In the context of description logic with variables, we will introduce variables with refreshing semantics in EL leading to the definition of the logic EL RV . Matching and unification problems will be extended in this scope and a new reasoning task known as pattern containment will be defined.

Definition of EL RV

Differences Between Variable Semantics

This section aims to illustrate the potential of introducing refreshing semantics in description logics using EL as example. Consequently, we will save technical aspects for later sections and emphasize here on presenting how valuable it can be. The example is based on the terminology containing these two definitions :

Doctor ≡ P erson ⊓ ∃getP hDIn.U niv ⊓ ∃f ormerly.P hDStudent P hDStudent ≡ P erson ⊓ ∃studyIn.U niv ⊓ ∃supervisedBy.Doctor
To this simple TBox, the pattern Academic is added and defined as : .U niv ⊓ ∃ f ormerly θ(y)

Academic ≡ P erson ⊓ ∃x.U
( P erson ⊓ ∃ studyIn θ(x) .U niv ⊓ ∃ supervisedBy θ(y) ((. . .))
To achieve this solution, the variable x (resp. y) is bound to getP hdIn (resp. f ormerly). Once Academic is unfold, the variables x and y are released from their respective bound. Variables x and y are now ready to be bound to a new value. In θ(Academic), the released x (resp. y) is bound to studyIn (resp. supervisedBy). Reaching Academic once again implies to unfold Academic which releases variables x and y and so on. The substitution θ is then defined as the substitution that alternates between {x = getP hDIn, y = f ormerly} and {x = studyIn, y = supervisedBy}.

A refreshing variable is a variable that has the ability to be released under some conditions in order to receive a new assignment. Refreshing semantics is the semantics that allows to use refreshing variables. Comparatively to non-refreshing semantics, refreshing semantics offers many more substitutions. Indeed, in the running problem, the set of primitive roles contains 4 roles (N R = {getP hDIn, f ormerly, studyIn, supervisedBy}). It means that there are 4 possibilities for x and 4 possibilities for y leading to a total of 16 possible substitutions under the non-refreshing semantics. On the other hand, refreshing semantics will release variables with each release associated to its own bound. In other words, we deal with an infinite number of variables which makes the set of possible substitutions infinite. This new possibilities may be solutions to reasoning problems as shown in the example.

Research conducted in this thesis differ from previous works in particular regarding variable semantics. Indeed, semantics for variables in description logics can be qualified as non-refreshing semantics. In our framework -role variables with refreshing and nonrefreshing semantics -, we have not only considered known problems such as matching and unification but also a new reasoning task denoted as pattern containment. Pattern containment aims to compare patterns w.r.t to their substitutions whatever the considered TBox.

The next section formally introduces refreshing semantics and its associated reasoning tasks in the scope of EL RV .

The EL RV Description Logic

We consider pattern queries expressed using the description logic EL extended with refreshing role variables. The obtained logic, called EL RV , is introduced below. An EL RVsignature is a pair Σ = (N C , N T ), where N C is the set of concept names (i.e. N A ∪ N def and N T = N R ∪ V the set of role terms. A role term t ∈ N T is either a role name (when t ∈ N R ) or a variable (when t ∈ V). We consider the set of variables V = N V R ∪ N V N as made of two disjoint sets of variables: N V R the set of refreshing variables and N V N the set of non refreshing variables. The sets

N C , N R , N V R and N V N are pairwise disjoint.
The description logic EL RV extends the logic EL with role variables. Given a signature Σ = (N C , N T ), EL RV -concept descriptions are built similarly to EL concepts while using roles terms instead of only role names. The concept Academic given in Example 1 is an example of an EL RV -definition with x and y refreshing variables. The particular case of EL RV -concepts without variables (called ground concepts) are EL-concepts.

An EL RV -TBox is a set of EL RV -concept definitions. We present now the notion of normalized EL RV -TBoxes. Let Σ = (N C , N T ), with

N T = N R ∪ V and V = N V R ∪ N V N ,
be an EL RV -signature and let T be an EL RV -TBox over the signature Σ. We say that T is normalized iff C ≡ D ∈ T implies that D is of the form:

A 0 ⊓ ... ⊓ A n ⊓ ∃r 0 .B 0 ⊓ ... ⊓ ∃r m .B m where A 0 , ..., A n ∈ N A , r 0 , ...r m ∈ N T and B 0 , ..., B m ∈ N def .
In the sequel, we assume that the EL RV -TBoxes are normalized. An EL RV pattern P is given by an EL RV -TBox, noted T P , which contains a definition of P .

Example 11. Assume a signature Σ = (N C , N T ) and let x ∈ N V R and y ∈ N V N be respectively a refreshing and a non-refreshing variable. Consider a query Q 1 expressed as an EL RV -pattern defined by the following TBox T Q 1 over the signature Σ.

T Q 1 = Q 1 ≡ A 1 ⊓ ∃x.C 1 C 1 ≡ A 2 ⊓ ∃y.Q 1
We explain now the difference between the set N V R of refreshing variables and the set N V N of non-refreshing variables. Given an EL RV -TBox T , a substitution σ maps a variable in N V N to a fixed value while the value assigned to a variable in N V R can be refreshed at each iteration over a cyclic definition. This semantics is captured through the notion of unfolding which turns (cyclic) EL RV -definitions with refreshing variables to equivalent (infinite) EL RV -definitions with non-refreshing variables. This is achieved by an unfolding process which replaces refreshing variables appearing in cyclic definitions of a given terminology by an infinite set of non-refreshing variables.

The notion of unfolding is formally defined below and then illustrated on an example.

Definition 4. (Pattern Unfolding.) Let T be an EL RV -TBox over an EL RV -signature Σ = (N C , N T ), with N T = N R ∪ V and V = N V R ∪ N V N . The unfolding of the Tbox T is a new Tbox, noted u(T ), over the EL RV -signature (N C , N R ∪ N V N ) such that each EL RV -pattern P = A 0 ⊓ ... ⊓ A n ⊓ ∃r 0 .B 0 ⊓ ... ⊓ ∃r m .B m of T is mapped into an EL RV -pattern u(P ) in u(T ).
The unfolding u is defined as follows:

• u(P ) = u(A 0 ) ⊓ ... ⊓ u(A n ) ⊓ ∃u(r 0 ).u(B 0 ) ⊓ ... ⊓ ∃u(r m ).u(B m ). • u(t) = t, ∀t ∈ N A ∪ N R ∪ N V N , i.e.
, u is the identity function over atomic concept names, role names and non-refreshing variables.

• if r i ∈ N V R then each new call to u(r i ) in the scope of u(P ) returns a new "fresh" variable from N V N . Note that, for r i = r j in the description P , the calls to u(r i ) and to u(r j ) return the same fresh variable while recursive calls to u(r i ) return different fresh variables.

Hence, an unfolding of an EL RV -pattern P enables to replace recursively each refreshing variable x by a new non-refreshing variable. Note that, in the case of refreshing variables that appear inside a cyclic definition of an EL RV -pattern P , the unfolding of P leads to an infinite EL RV -pattern u(P ) which uses an infinite set of variables.

We give below partial unfolding of the EL RV -pattern Q 1 of Example 11.

u(Q 1 ) ≡ A 1 ⊓ ∃x 0 .(A 2 ⊓ ∃y.(A 1 ⊓ ∃x 1 .(A 2 ⊓ ∃x 2 .(. . .)))
Note that during the unfolding process, each iteration through the concept Q 1 generates a new variable x i (a refreshing variable) while a unique variable y (non-refreshing variable) is used.

It is worth noting that an unfolding of an EL RV -pattern

P ≡ A 0 ⊓ ... ⊓ A n ⊓ ∃r 0 .B 0 ⊓ ... ⊓ ∃r m .B m can be viewed as a ⟨N def ∪ {q f }, N R ∪ N A ∪ N V N ⟩-labeled tree (τ P , λ, δ
) which is recursively defined as follows:

• λ(ε) = P • ∀i ∈ [0, n],
we have: i ∈ τ P , δ(ϵ, i) = A i and λ(i) = q f . The label q f is a specific keyword used to label the leaves of the tree.

• ∀i ∈ [n + 1, n + m + 1], we have: i ∈ τ P , δ(ε, i) = u(r i-n-1
) and i is the root of the tree τ B i-n-1

Example 12.

A 1 x 0 A 2 y A 1 x 1 A 2 y A 1 x 2 A 2 Q 1 q f C 1 q f Q 1 q f C 1 q f Q 1 q f C 1 q f Figure 2.1: Infinite Tree of the Unfolded Pattern Q 1 of Example 11.
Instantiations of EL RV -concept definitions (respectively, EL RV -TBoxes) are given by variable substitutions. Given a TBox T with a signature Σ = (N C , N T ), where N T = N R ∪V, a substitution σ is a mapping from V into the set of role names N R . A substitution σ is extended to EL RV -concepts in the obvious way, i.e.:

• σ(T ) = T if T ∈ N C ∪ {⊤} ∪ N R ; • σ(C ⊓ D) = σ(C) ⊓ σ(D) with C,D two EL RV -concepts; • σ(∃R.C) = ∃σ(R).σ(C). Definition 5. (Pattern Instances.) Let T be an EL RV -TBox over an EL RV -signature Σ = (N C , N T ), with N T = N R ∪ V and V = N V R ∪ N V N and let P ≡ A 0 ⊓ ... ⊓ A n ⊓ ∃r 0 .B 0 ⊓ ... ⊓ ∃r m .B m be an EL RV -pattern in T . Let σ : N V N → N R
be a variable substitution. Then σ(u(P )) is an instance of P w.r.t. the variable substitution σ.

In the sequel, we abuse of notation and we write σ(P ) instead of σ(u(P )) for a pattern instance of P w.r.t. σ. Figure 2.2 shows an instance σ(Q 1 ) of the pattern Q 1 of Example 11 given by a substitution σ that maps the variable y to σ(y) = S and each variable

x i to σ(x i ) = R 1 if i is even and σ(x i ) = R 2 if i is odd.
A 1 σ(x 0 ) R 1 A 2 σ(y) S A 1 σ(x 1 ) R 2 A 2 σ(y) S A 1 σ(x 2 ) R 1 A 2 Q 1 q f C 1 q f Q 1 q f C 1 q f Q 1 q f C 1 q f Figure 2.2: An Instantiation of the Pattern Q 1 of Example 11.
In addition, a substitution σ maps each EL RV -TBox T into an EL-TBox σ(T ) which is obtained by converting each EL RV -concept definition P ≡ C in T into an EL-concept definition σ(P ) ≡ σ(C). In the example, we have σ(

T Q 1 ) = {σ(Q 1 )}.
Pattern instances can be split into two categories : regular and irregular instances. A regular instances will make substitute its variables using a regular choice. As a consequence, regular instances can be represented by a finite T . For example, Figure 2.2 depicts a regular solution where the substitution of x alternates between R 1 and R 2 . This alternation is regular and can be represented in a finite way. The associated finite TBox would be σ(T

Q 1 ) = {σ(Q 1 ) ≡ A 1 ⊓ ∃R 1 .σ(C 1 ); σ(C 1 ) ≡ A 2 ⊓ ∃S.σ(Q ′ 1 ); σ(Q ′ 1 ) ≡ A 1 ⊓ ∃R 2 .σ(C ′ 1 ); σ(C ′ 1 ) ≡ A 2 ⊓ ∃S.σ(Q 1 )
}. Irregular instances are by opposition instances that can not be represented in a finite way. To illustrate this notion, we will use the TBox {P ≡ ∃x.P ′ ; P ′ ≡ ∃y.P } where both x and y are refreshing. The idea is to construct a substitution such that the resulting automata is the language R n 1 .R n 2 which is known to be irregular. Figure 2.3 depicts the corresponding tree. ε 0 00 000 0000 000000 0000000 Lemma 1. Let σ(P ) and θ(Q) be two instances of respectively two patterns P and Q. Then σ(P ) is subsumed by θ(Q) (i.e., σ(P ) ⊑ θ(Q)) iff there exists a homomorphism from θ(Q) to σ(P ).

σ(x0) R 1 σ(y0) R 2 σ(x0) R 1 σ(y1) R 1 σ(x2) R 2 σ(y2)
Proof. It is a direct extension of the characterization of subsumption in EL using the so-called EL-description trees [START_REF] Baader | Computing least common subsumers in description logics with existential restrictions[END_REF]. In fact, unfolding transforms potential cyclic definition with TBox into non-cyclic infinite description without TBox. As a consequence, the different subsumption semantics are all equivalent and subsumption is equivalent to tree homomorphism.

Subsumption between regular instances of two patterns is linked to subsumption w.r.t to the greatest fix-point semantics in EL as stated by the next lemma.

Lemma 2. Let σ(P ) and θ(Q) be two regular instances of respectively two patterns P and Q. Let σ reg (P ) and θ reg (Q) the corresponding EL finite descriptions. If

σ(P ) ⊑ θ(Q) then σ reg (P ) ⊑ gf p,T θ reg (Q) in EL.
Proof. By definition σ(P ) ⊑ θ(Q) implies that there exists a homomorphism from θ(Q) to σ(P ) in EL RV (Lemma 1). Since σ(P ) and θ(Q) being regular means that they can be represented with a finite EL-TBox. These T Box will corresponds to σ reg (P ) and θ reg (Q). Subsumption w.r.t to the greatest fix-point semantics in EL is characterized by simulation between the respective description graph [START_REF] Baader | Terminological cycles in a description logic with existential restrictions[END_REF]. Homomorphism between unfolded description graph preserves simulation. As a consequence we have σ reg (P ) ⊑ gf p,T θ(Q) reg (Q) in EL.

Reasoning with Refreshing Variables

In this thesis, patterns are viewed as queries defined in an EL RV -TBox and evaluated over an EL knowledge base. We focus in the sequel on three reasoning mechanisms: (i) matching, which is used as a mechanism to evaluate patterns over EL knowledge bases, (ii) weak-subsumption that extends unification and (iii) pattern containment, i.e., determining whether the result of a pattern is included in the result of another pattern whatever the considered knowledge base.

Definition 6 (Matching). Let T P be an EL RV TBox, let T g be an EL TBox and let T = T P ∪ T g . An EL RV matching problem is of the form C ⊑ ? T P where C is a concept in T g and P is a pattern of T P . A solution (or matcher) of this problem is a substitution σ such that C ⊑ σ(T ) σ(P ).

Matching is used as a base mechanism to evaluate a pattern against concepts and individuals of a knowledge base. Let T P be an EL RV -TBox including a defined pattern P and let KB = (T , A) be an EL knowledge base. A defined concept C of T is an answer of P over KB iff the matching problem C ⊑ ?

T P ∪T P has a solution. To match a pattern P against an individual i of an ABox A of KB we make use of the notion of most specific concept (msc). The msc of an individual i, noted msc(i), is a non-standard reasoning in description logics that enable to generalizes an individual to a concept by computing the least concept description in the available description language that has this individual as an instance [START_REF] Baader | Least common subsumers and most specific concepts in a description logic with existential restrictions and terminological cycles[END_REF]. Hence, it is natural to consider that an individual i of KB is in the answer of a pattern P over KB iff the matching problem msc(i) ⊑ ?

T P ∪T P is solvable. In [START_REF] Baader | Least common subsumers and most specific concepts in a description logic with existential restrictions and terminological cycles[END_REF] it is shown that for the description logic EL, if one considers cyclic terminologies under greatest fix-point semantics, the msc always exists and can be computed in polynomial time.

Consequently, as explained above, evaluating a pattern P over a knowledge base K = (T , A) turns to matching P against concepts and individuals (more precisely, their msc) of K. The computed matchers provides an explanation to why a concept C matches a pattern P . Example 13. For example, with the matcher σ of Example 1, the pattern instance σ(Academic) provides an explanation to why we can say that the concept P rof essor matches the pattern Academic w.r.t. the knowledge base of Table 1.

As for non-refreshing semantics, this problem can be extended with variables on both sides. It leads to the following definition for weak-subsumption that extends unification problem.

Definition 7 (Weak-subsumption). A pattern P of a TBox T P is weakly-subsumed by a pattern

Q of a TBox T Q , noted P ⊏ ∼T Q, iff ∃σ, ∃θ s.t. σ(P ) ⊑ θ(σ(T )) θ(Q), with T = T P ∪ T Q . A weak-subsumption problem, noted P ⊏ ∼ ? T Q is the problem of testing whether P ⊏ ∼T Q.
Pattern containment is a new reasoning task that aims to compare two patterns with a different semantics than unification. Definition 8 (Pattern containment). A pattern P of a TBox T P is contained in a pattern Q of a TBox T Q , noted P ⊑ Q, iff ∀σ, ∃θ s.t. σ(P ) ⊑ θ(σ(T )) θ(Q), with T = T P ∪ T Q . A pattern containment problem, noted P ⊑ ? Q is the problem of testing whether P ⊑ Q.

Pattern containment enables to compare patterns w.r.t. their respective answers as stated by the following lemma which is a direct consequence of Definition 8.

Lemma 3. Let P and Q be two patterns respectively defined in the EL RV TBoxes T P and T Q . Let T be an arbitrary EL TBox and let C be a concept of T . If P ⊑ Q then we have:

C ⊑ ? T P ∪T P is solvable ⇒ C ⊑ ? T Q ∪T Q is solvable Note that
matching is also a particular case of weak-subsumption where the pattern on the left is ground. The next section gives an insight in the shape of matchers considered later on.

Regular Matchers

This section discusses two main issues regarding the matching problem in the context of the logic EL RV :

(i) a matching problem may have infinitely many matchers that lead to instances of P that are incomparable w.r.t. subsumption and, (ii) some matchers can be represented by a finite EL RV -terminology (hereafter called regular matchers), there exists matchers that are not regular (i.e., a matcher σ such that the derived instance σ(T Q 2 ) cannot be represented by a finite EL RVterminology).

T 2 = C ≡ ∃R.A 1 ⊓ ∃S.C ⊓ ∃R.D, D ≡ ∃S.A 1 ⊓ ∃R.D ⊓ ∃S.C, T Q 2 = {Q 2 ≡ ∃x.A 1 ⊓ ∃y.Q 2 } with x, y ∈ N V R Table 2.4: The terminologies T Q 2 and T 2 .
µ(Q 2 ) N A 1 q f µ(Q 2 ) N A 1 q f µ(Q 2 ) N A 1 q f x 0 A 1 y 0 x 1 A 1 y 1 x 2 A 1 . . . Figure 2.4: Unfolding of Q 2 Consider the matching problem C ⊑ ? T Q 2 ∪T 2 Q 2 ,
where the terminologies T Q 2 and T 2 are shown at Table 2.4. The variables x and y are refreshing variables of Q 2 . Unfolding of Q 2 is depicted in Figure 2.4. Table 2.5 exhibits several possible matchers that solve this problem.

σ 1 (x i ) = R and σ 1 (y i ) = S, ∀i ∈ N (2.1) σ 2 (x i ) = R and σ 2 (y i ) = R if i is even σ 2 (x i ) = S and σ 2 (y i ) = S if i is odd (2.2)      ϕ k (x i ) = R and ϕ k (y i ) = S ∀i ∈ [1, k[ ϕ k (x k ) = R and ϕ k (y k ) = R ϕ k (x i ) = S and ϕ k (y i ) = R ∀i > k (2.3)
Table 2.5: Regular matchers.

We make the following observations.

• σ 1 and σ 2 are regular matchers in the sense that σ 1 (T Q 2 ) (respectively, σ 1 (T Q 2 )) can be described by a finite EL RV -Tbox. Table 2.6 shows the corresponding TBoxes.

• ϕ k , for k ∈ N defines an (infinite) family of matchers that solve our matching problem. Note that, for a fixed integer k, ϕ k is a regular matcher (Table 2.6 shows a corresponding TBox ϕ k (T Q 2 )).

• The matchers σ 1 , σ 2 and ϕ k , for k ∈ N, are pairwise incomparable w.r.t. subsumption in the sense that for any i, j ∈ N, with i ̸ = j, the concepts

σ 1 (T Q 2 ) = {σ 1 (Q 2 ) ≡ ∃R.A 1 ⊓ ∃S.σ 1 (Q 2 )} σ 2 (T Q 2 ) = σ 2 (Q 2 ) ≡ ∃R.A 1 ⊓ ∃R.σ 2 (Q ′ 2 ), σ 2 (Q ′ 2 ) ≡ ∃S.A 1 ⊓ ∃S.σ 2 (Q 2 ) ϕ k (T Q 2 ) =            ϕ k (Q 2 ) ≡ ∃R.A 1 ⊓ ∃S.ϕ k (Q ′ 2 ), ϕ k (Q ′ 2 ) ≡ ∃R.A 1 ⊓ ∃S.ϕ k (Q ′ 3 ), . . . ϕ k (Q ′ k ) ≡ ∃R.A 1 ⊓ ∃R.ϕ k (Q ′ k+1 ), ϕ k (Q ′ k+1 ) ≡ ∃S.A 1 ⊓ ∃R.ϕ k (Q ′ k+1 )           
Table 2.6: Representation of regular matchers as finite TBoxes.

ϕ i (Q 2 ), ϕ j (Q 2 ), σ 1 (Q 2 ), σ 2 (Q 2 )
are pairwise incomparable w.r.t. the subsumption relation.

We exhibit now a non regular matchers for our matching problem. Let u be an infinite geometric sequence u 0 , u 1 , . . . with u 0 > 1 and ∀i ∈ N, we have u i+1 -u i > 3. Let v and w be respectively two infinite sequences v 0 , v 1 , . . . and w 0 , w 1 , . . . such that v i = u i + 1 and w i = u i + 2, ∀i ∈ N. We define the substitution ρ u as follows:

• ρ u (x l ) = R and ρ u (y l ) = S if l is not a member of the sequences v or w • ρ u (x v i ) = R and ρ u (y v i ) = R for each member v i of the sequence v • ρ u (x w i ) = S and ρ u (y w i ) = S for each member w i of the sequence w
The substitution ρ u is a matcher of the considered matching problem. However, ρ u is not regular (i.e., it cannot be described by a finite TBox) as stated by the following lemma.

Lemma 4. Consider the matching problem

C ⊑ ? T Q 2 ∪T 2 Q 2 ,
where the terminologies T Q 2 and T 2 are given at Table 2.4. Let ρ u (Q 2 ) be the matcher defined as previously. For any substitution σ such that σ(T

Q 2 ) is a finite TBox, we have σ(Q 2 ) ̸ ≡ ρ u (Q 2 ).
Proof. W.l.o.g. assume u 0 > 1. The sequence y 0 , y 1 , . . . forms an infinite word τ = S u 0 RS u 1 -u 0 R . . . RS un-u n-1 . . . Note that the sequence u 1 -u 0 , . . . u n -u n-1 forms a geometric progression. Consequently, the occurrences of the sequences of S follows a geometric progression pattern and hence cannot be represented by a finite state automaton.

Fortunately, it is sufficient to look for regular matchers because if a matching problem is solvable then it necessarily has a regular matcher (Section 4.3 Corollary 2). The proof derives from the completeness of our matching algorithm.

Conclusion of Chapter 2

Even though being recent add-ons to description logics, variables have been a source of interesting research. At a terminological level, it mainly focuses over two non-standard reasoning tasks known as matching and unification. These reasoning tasks have been investigated for two families of logics based on EL and FL 0 . It has been demonstrated that complexity in EL is NP-Complete for both cases except for unification w.r.t general TBox which remains an open problem. It is an advantage comparatively to FL 0 which suffers a blow-up of complexity while considering the different kind of TBoxes.

The main contribution of this chapter is the definition of EL RV . EL RV extends EL by allowing refreshing semantics for role variables as well as considering cyclic pattern which can be seen as pattern queries. Pattern instance, which represents a pattern whose variables have been substitutes can be either regular or irregular. Regular solutions can be express with finite EL-TBox and preserve the subsumption relationship with regard to the greatest fix-point semantics.

Moreover, this new semantics for variables questioned known reasoning task such as matching and unification. We showed that unsolvable matching problems (Doctor ⊑ ? T Academic) in non-refreshing semantics would be solvable in refreshing semantics. Three reasoning tasks have then be introduced. Matching and unification have respectively been extended to matching and weak-subsumption to support refreshing variables. On the other hand, we define a brand new reasoning task : pattern containment. It allows to compare pattern queries results whatever the considered knwoledge base.

The next chapter introduces a framework based on the notion of description automata which will be of later used to solve reasoning mechanisms in EL RV .

Chapter 3

From EL RV Description Logic to Automata Adding refreshing semantics to description logic unlocked new ways to reason through EL RV -TBox and pattern queries. Due to the differences stated in the previous chapter, known algorithms can not handle refreshing semantics. This chapter will focus on introducing description automata. By extending, fresh variable automata, this class of automata will handle refreshing variables. Moreover, reasoning in EL RV will be reduced to simulation problems in the scope of description automata. Table 3

EL RV -Description Automata

Our reasoning procedures over EL RV -terminologies are built on the notions of EL RVdescription automata. Such automata recognize configuration trees which are nothing other than a syntactic variant of pattern instances. We associate with each EL RV -pattern P an EL RV -description automata A P such that there is a one-to-one correspondence between the configuration trees recognized by A P and the instances of P . Consequently, an EL RV -description automaton A P characterizes all the possible instances of its associated EL RV -pattern P .

Definition 9. (EL RV -description automaton.) Let P ≡ A 0 ⊓ ... ⊓ A n ⊓ ∃r 0 .B 0 ⊓ ... ⊓ ∃r m .B m be an EL RV -pattern defined in a T P over the signature Σ = (N C , N T ), with

N C = N def ∪ N A , N T = N R ∪ V and V = N V R ∪ N V N .
The EL RV -description automaton associated with P , denoted A P , is a tuple A P = (Q, L, Var, p 0 , q f , δ, κ) built as follows:

(i) L ⊆ N A ∪ N R is a finite alphabet, (ii) Var ⊆ V is a finite set of variables, (iii) Q = N def ∪ {q f } is a finite set of states,
(iv) q 0 = P is the initial state and q f is the final state,

(v) δ ⊆ Q × (L ∪ Var) × Q is a transition relation defined as follows: For each Q ≡ A 0 ⊓ ... ⊓ A n ⊓ ∃r 0 .B 0 ⊓ ... ⊓ ∃r m .B m ∈ T {(Q, A i , q f ) : f or i ∈ [0, n]} ∪ {(Q, r j , B j ) : f or j ∈ [0, m]} ∈ δ (vi) κ : Var → 2 Q is the refreshing function defined as follows: For each Q ≡ A 0 ⊓ ... ⊓ A n ⊓ ∃r 0 .B 0 ⊓ ... ⊓ ∃r m .B m ∈ T , ∀r j ∈ Var we have: κ(r j ) = {Q} if r j ∈ N V R , or κ(r j ) = ∅ if r j ∈ N V N .
Definition 9 associates with each defined concept P ≡ A 0 ⊓...⊓A n ⊓∃r 0 .B 0 ⊓...⊓∃r m .B m in a TBox T P an EL RV -description automaton A P whose states are made of the set of defined concept names of T in addition to a special final state q f . Transitions of A P are labelled either with letters, taken from an alphabet made of the atomic concept names and role names, or variables taken from the set of role variables. More precisely, each atomic concept name A i that appears in the definition of P leads to a transition from the node P to q f labeled with the letter A i . Each description ∃r i .B i that appears in the definition of P leads to a transition from the node P to the node B i (the initial state of the automaton A B i ) labeled with the term r i . When the term r i is a refreshing variable, its refreshing state is given by the function κ (i.e., in this case κ(r i ) = {P }). Note that Definition 9 extends naturally to ground concepts (i.e., when P do not contain variables). The obtained automaton A P is then a ground automaton without variables.

Figure 3.1 depicts the description automaton of the TBoxes T Q 2 and T 2 given at Example 2.6. The variables x and y are refreshed at state Q 2 , hence we have κ(x) = κ(y) = {Q 2 }.

EL RV -description automata can be viewed as a variant of variable automata with refreshing variables introduced in [START_REF] Belkhir | Fresh-variable automata: Application to service composition[END_REF][START_REF] Belkhir | Parametrized automata simulation and application to service composition[END_REF], where the notion of a run is however substantially modified in order to capture instantiation trees of EL RV patterns. Indeed, a description automaton of a given pattern P is in fact a compacted representation of all the possible instantiations of P . To make this statement more precise, we introduce the notions of

Q 2 N A 1 q f y x A 1 C N A 1 D q f S R R S A 1 R S Figure 3.1: Description Automata of T Q 2 and T 2 .
configurations and configuration trees and we show that these latter ones are equivalent to the instances of the pattern P .

A run of a description automaton A P is defined over configurations. Informally, a configuration gives the values assigned to variables at a given state of the execution of the automaton A P . Since, on one side a given state may be visited (infinitely) many times and on another side refreshing variables may see their assigned value changing at their refreshing states, a configuration includes a vector of integer used to distinguish between multiple value assignations to a given refreshing variable. More precisely, we define a configuration as a pair (q, → I ) where q is a state of A P and → I is a vector of integers, where the i th component of → I records the current index of the i th variable, assuming that the variables are sorted according to their lexicographic order. By this way, we are able to generate several copies of a refreshing variable by incrementing its corresponding component in the vector Example 14. Figure 3.2 shows a configuration tree of A Q 2 . Since the automaton A Q 2 contains two variables, x and y, the counter associated to its configurations is 2 dimensional. As an example, (Q 2 , (0, 0)) is a configuration in this tree which indicates that the current state of the execution of A Q 2 is Q 2 and the current copies of the variables are (x, 0) and (y, 0). This is because this configuration uses a counter → I = (0, 0) with leads to I x = 0 and I y = 0 (the copies of the variables x and y). The configuration (q f , (2, 2)) records a run which is at state q f while using the copies (x, 2) and (y, 2) of the variables x and y.

(Q 2 , (0, 0)) (N A 1 , (0, 0)) (q f , (0, 0)) (Q 2 , (1, 1)) (N A 1 , (1, 1)) (q f , (1, 1)) (Q 2 , (2, 2)) (N A 1 , (2, 2)) (q f , (2, 2)) σ(x, 0) A 1 σ(y, 0) σ(x, 1) A 1 σ(y, 1) σ(x, 2) A 1 . . .
The formal definition of a run is given below. Definition 10. (Run of an EL RV -description automaton.)

Let A P = (Q, L, Var, q 0 , δ, q f , κ) be a description automaton and let σ: Var × N → N R be a variable substitution. Let → G ∈ N |Var| be a counter and let S ⊆ Q × N |Var| . A run of A P using a substitution σ, denoted T (A P , δ) and called a configuration tree, is a ⟨S, L⟩-labeled tree (τ P , λ P , δ P ) constructed as follows:

• λ(ϵ) = (q 0 , → 0 ), a root of the tree, and let → G = → 0 , a global counter initialized to a vector of zero.

• Let n ∈ τ P be a node such that λ P (n) = (q, → I ). For every transition (q, t, q ′ ) ∈ δ a new child ni of n is generated according to the following sequence:

(1)

δ P (n, ni) = σ(t, I t ) if t ∈ Var t if t ∈ L (2) ∀y ∈ Var, if q ′ ∈ κ(y) then G y := G y + 1, and (3)
Let → I ′ = I ′ y = G y , ∀y ∈ Var, s.t. q ′ ∈ κ(y) I ′ y = I y otherwise (4) λ P (ni) = (q ′ , → I ′ )
Intuitively, when a run of a description automaton A P is at configuration (q, → I ) and there is a transition (q, t, q ′ ) in A P then the automaton A P moves to a configuration (q ′ , → I ′ ) upon the input t, if t is a letter in the alphabet L, or upon σ(t, I t ), if t is a variable. Note that, in this case σ(t, I t ) corresponds to the value assigned to the copy t It of the variable t by the substitution σ. For each variable y that is refreshed at the state q ′ a new copy of y is created at the configuration (q ′ , → I ′ ) which is materialized by a new value I ′ y in the vector → I ′ . To ensure that I ′ y is a new value (not already used before) a global counter → G is associated with each run of the automaton A P . For each variable x, G x stores the index of the newest copy of the variable x considered.

Definition 10 defines a run of a description automaton A P as a tree rooted at the configuration (q 0 , → 0 ). Note that, a ground automaton A C (i.e., an automaton without variable) has a unique configuration tree, which is noted hereafter T (A C , id). All the configurations of T (A C , id) have a zero dimension vector as a counter and hence the counter is omitted from the notation (i.e., we write (q) for such configurations).

Chapter 3 From EL RV to Automata 3.2 Reducing Reasoning in EL RV to Simulation Note that a partial configuration tree P T (A P , σ) is a partial tree of the configuration tree T (A P , σ);

Now that the definitions of the automata and their configuration tree has been given, the remaining will be devoted to unravel their link to pattern instances in order to reduce reasoning in EL RV into simulation with EL RV -description automata.

Reducing Reasoning in EL RV to Simulation

This section emphasizes on the link between substitutions and configuration trees. More particularly, we introduce a notion of equivalence between substitutions which is used in the subsequent lemma (Lemma 5) to establish a tight relationship between valuation in description logics (i.e., pattern instances) and configuration trees.

Definition 11 (Equivalence between substitutions). Let V, V ′ be two sets of variables and let V al be a set of constants. Let σ : V ∪ V al → V al and ϕ : V ′ ∪ V al → V al be two substitutions. Then we say that σ is equivalent to ϕ, and we write σ ≡ ϕ, iff there exists an isomorphism f between σ and ϕ which is the identity for element of V al.

Lemma 5 given below establishes a strong connection between patterns instances and configuration trees.

Lemma 5. Let P be an EL RV -pattern of a terminology T P and let A P be its corresponding description automaton. Then, we have: (i) ∀ϕ: ϕ(P ) is an instance of P , then there exists σ such that σ ≡ ϕ and T (A P , σ) is a configuration tree of A P (ii) ∀σ: T (A P , σ) is a configuration tree of A P , then there exists ϕ such that ϕ ≡ σ and ϕ(P ) is instance of P Proof. (i): we show that, given an instance ϕ(P ) = (τ, λ, δ), we construct a configuration tree T (A P , σ) = (τ ′ , λ ′ , δ ′ ) and an isomorphism f between ϕ and σ. Let → G be a global counter associated with the execution of A P . T (A P , σ) and f are inductively defined as follows:

• Initialization: ε ∈ τ ′ and λ ′ (ε) = (λ(ε), → 0 ). • Let n ∈ τ ′ with λ ′ (n) = (λ(n), → I ). For every ni ∈ τ : -ni ∈ τ ′ . -For every δ(n, ni) = ϕ(u(t)): * Let t x = (t, I t ) if t is a variable and t x = t if t is a constant. * δ ′ (n, ni) = σ(t x ) with σ(t x ) = ϕ(u(t)). This is because δ(n, ni) = ϕ(u(t))
implies that the description λ(n) includes an atom ∃x.λ(ni). Hence, by construction (Definition 9,(v), the automaton

A P includes a transition (λ(n), t, λ(ni)). * f (u(t)) = t x . * λ ′ (ni) = (λ(ni), → I ′ ) with I ′ x = G x if λ(ni) ∈ κ(x) and I ′ x = I x otherwise.
By construction, we have T (A P , σ) is a configuration tree of A P and f is the identity on constants and forms a one-to-one mapping between each variable u(x) of u(P ) and a pair (x, i),

with i ∈ N, of T (A P , σ) such that σ(t) = v iff δ(f (t)) = f (v) (i.e.,
f is an isomorphism between σ and ϕ).

(ii): : Similar reasoning can be applied by exchanging T (A P , σ) and ϕ(P ) roles.

P u(P )

A P σ(P ) σ(P ) σ(P ) T (A P , ϕ) T (A P , ϕ) T (A P , ϕ)
Description Logic Description Automata P isomorphism isomorphism Our translation of EL RV patterns to description automata is used to design decision procedures for the reasoning problems of our interest (i.e., matching, weak-subsumption and pattern containment). We introduce below the notion of universal simulation which is used to compare description automata w.r.t. to their configuration trees.

Definition 12 (Universal simulation). Let A P and A

Q two description automata. A Q is universally simulated by A P , noted A Q ≪ ∀ A P , if ∀σ, ∃θ such that there exists a homomorphism Z from T (A Q , θ) to T (A P , σ) with Z(ε) = ε. The universal simulation problem is the problem of testing whether A Q ≪ ∀ A P .
Let Z be an homomorphism from T (A Q , θ) = (τ, λ, δ) to T (A P , σ) = (τ, λ ′ , δ). We extend universal simulation to configurations as follows if Z(i) = j then we write λ(i) ≪ ∀ λ ′ (j) to denote the homomorphism from Z(i) to j Note that A Q ≪ ∀ A P is equivalent to (q 0 , → 0 ) ≪ ∀ (p 0 , → 0 ). We give now our main technical result consisting in the characterization of pattern containment between EL RVpatterns in terms of universal simulation between EL RV -description automata.

Theorem 1. Let P and Q be two EL RV -patterns and let A P and A Q be respectively the description automata of P and Q. A pattern containment problem P ⊑ ? Q has a solution if and only if

A Q ≪ ∀ A P .
This theorem is a direct consequence of Definition 12, Lemma 1 and Lemma 5. In the case P is a ground EL-concept, Theorem 1 also provides a characterization of matching using description automata as stated below.

Corollary 1. Let Q be an EL RV -pattern and C a ground EL RV -description. Let A Q and A C be respectively the description automata of Q and C. A matching problem C ⊑ ? Q has a solution if and only if

A Q ≪ ∀ A C .
In order to characterize weak-subsumption with simulation, we will use a slight variation of simulation called existential simulation noted ≪ ∃ .

Definition 13 (Existential Simulation). Let A P and A Q two description automata. A Q is existentially simulated by A P , noted A Q ≪ ∃ A P , if ∃σ, ∃θ such that there exists a homomorphism Z from T (A Q , θ) to T (A P , σ) with Z(ε) = ε. The existential simulation problem is the problem of testing whether A Q ≪ ∃ A P .

Let Z be an homomorphism from T (A Q , θ) = (τ, λ, δ) to T (A P , σ) = (τ, λ ′ , δ). We extend existential simulation to configurations as follows if Z(i) = j then we write λ(i) ≪ ∃ λ(j) to denote the homomorphism from Z(i) to j Theorem 2. Let P and Q be two EL RV -patterns and T Q and let A P and A Q be respectively the description automata of P and Q. A weak-subsumption problem P ⊏ ∼ ? T Q has a solution if and only if A Q ≪ ∃ A P .

As Theorem 1 is a direct consequence of Definition 12, Lemma 1 and Lemma 5. It also provides a characterization for matching since matching is a special case of weak-subsumption. Theorem 1 and Theorem 2 reduce matching, weak-subsumption and containment in the context of the logic EL RV into a simulation tests between description automata. Next chapters exploit this link to design algorithms that solve those reasoning tasks.

Comparison with Variables Automata

Description automata are inspired of fresh variable automata [START_REF] Belkhir | Fresh-variable automata: Application to service composition[END_REF][START_REF] Belkhir | Parametrized automata simulation and application to service composition[END_REF]. This class of automata introduced by Belkhir et al. extends variable automata to handle refreshing variables with infinite valuation domain. Research around this class of automata mainly deal with closure properties (i.e. closed under union, concatenation, Kleene operator and intersection). Simulation has been studied as a decision procedure and proved to be exptime-complete. It has notably been applied to service composition which can be reduced to simulation.

Compared to description automata, the formal definition is similar to fresh variable automata. However, our definition of runs differs. Thus preventing from directly using those results. The difference lies in the semantics of variables themselves. Indeed, there are two states for a variable in fresh variable automata, it is either free or bound. If it is not bound then any bound can be associated and this bound will be kept for the remaining until refreshment. Consequently, a variable refreshed by the same state may be bound to different value while running different branches. Description automata can not be so lenient regarding variables bound. Indeed, a strong property ensures that an instance may be synchronized within run.

Figure 3.4 presents an automaton that will be used to illustrate the main difference. This automaton can be either seen as a fresh variable automaton or a description automaton.

P A 1 A 2 x x Figure 3.4: Variable Automata A P
A language of a fresh variable automaton is given by its configuration automaton. Configurations of a fresh variable are pairs of the form (q, S) where q is a state and S the current value assignment. For example, the configuration (A 1 , {x = R 1 }) means that the current state is A 1 and x is assigned to R 1 . When a variable is bound, its assignment is added. When a variable is refreshed, its assignment is removed. As expected, the initial configuration is made of the initial state with an empty variable assignment. Figure 3.5(a) corresponds to the complete configuration automaton of the running example. We assume here that the alphabet is made of the (infinite) set {R 1 , R 2 , ..., R N }. In comparison, Figure 3.5(b) depicts the run associated to σ(x, 0) = R 1 .

(P, ∅) (A 1 , {x = R 3 } (A 2 , {x = R 3 } (A 1 , {x = R 1 }) (A 1 , {x = R 2 }) (A 1 , {x = R N }) (A 2 , {x = R 1 }) (A 2 , {x = R 2 }) (A 2 , {x = R N }) x x x x x x x x . . . . . . (a) Configuration Automata of A P ϵ 1 2 (P, (0)) (A 1 , (0)) (A 2 , (0)) σ(x, 0) = R 1 σ(x, 0) = R 1 (b) Configuration Tree T (A P , σ)

Figure 3.5: Runs of Fresh Variable Automata

As illustrated in the figures, the main difference it that a free variable transition of a fresh variable automata represents many transitions at the same time. On the other hand, in our definition of configuration tree a variable transition represent one transition among the many possible. The difference is not limited to choosing one possibility. Indeed, we ensure that any outgoing transition labeled by a same instance of a variable is assigned to the same value until refreshment. Thus making the definitions of runs intrinsically different. As demonstrated previously, this properties are important to capture the semantics of description logics.

Conclusion of Chapter 3

Reasoning in Description Logics with refreshing variables bring up new challenges to handle for matching, weak-subsumption and pattern containment. This chapter entails the definition of EL RV -description automata which allow to reduce reasoning tasks to simulation tests. EL RV -description automata are a class of automata inspired from fresh variable automata with however different notions of runs. This class naturally handles the refreshing variables while allowing to distinguish variable instances. This feature imply a one-to-one comparison between instances of a pattern and runs of its corresponding description automata.

We consider two kinds of simulation, universal and existential simulations. The main difference lies in the quantifier associated. Pattern-containment is then reduced to universal simulation and weak-subsumption to existential simulation. Matching is a special case of both pattern containment and weak-subsumption. As a consequence it can be reduced to the two simulations.

In the remaining, we exploit this reduction to design algorithms in order to solve the different reasoning tasks.

Chapter 4 Solving Matching in EL RV

Even though matching is a sub-problem of pattern containment and weak-subsumption, we will present an algorithm to solve it. The main motivation is pedagogical since it bears the advantage to only consider variable on one side. In order to ensure correctness of the algorithm, the required formal definitions of pconf and pcover are introduced. As a result, the algorithm Check Match is proven to be correct making matching in EL RV decidable. We postpone discussion about complexity of the problem to the next chapter since maching, weak-subsumption and pattern containment are in the same class of complexity. Table 4.1 summarizes notations introduced in this chapter.

Symbol Description

((q, → I ), c, M q ) Product configuration (pconf) M q Variable assignment ◁ Product cover (pcover)

M q →c Mappings of outgoing transitions from q into c Exec A P ,A C Product execution tree P T (A P , σ) Partial configuration tree Table 4.1: Notations introduced in Chapter 4

Presentation of Check Match

This section emphasizes on solving matching in EL RV using its reduction to universal simulation. Given an EL RV -description C and an EL RV -pattern Q, to solve C ⊑ ? T Q, the algorithm Check Match will test universal simulation between A Q and A C . This algorithm is inspired from product automata. The main idea of Check Match is to run synchronously A Q and A C , trying at each step to guess appropriate value assignments to variables of A Q in order to construct σ, called hereafter a witness substitution, such that there is a homomorphism from T (A Q , σ) into T (A C , id). Recall that T (A C , id) is the unique configuration tree of A C (since A C is ground). A given state in such a synchronized product is called a pconf (for product configuration).

In the rest of this section, we define formally the notions of pconf and pcover before presenting the algorithm Check Match. Definition 14 (pconf ). Let A Q be an EL RV -description automata and A C be a ground Presence of counters implies an infinity of configurations from A Q . Consequently, an infinity of pconf s can be produced accordingly. Thus leading any naive exploration algorithm to an infinite run. In order to prevent from such situations, we present the notion of pcover to cut exploration of infinite branches.

EL RV -description automata. A pconf is a triple ((q, → I ), c, S Q ) where (q, → I ) is a configura- tion of A Q , c is a state of A C and S Q is a mapping from Var Q × N into N R . The domain of S Q denoted dom(S Q ) ⊆ Var Q × N corresponds to the variable instances that appear in S Q . An assignment S Q is inconsistent if there exists (x, i) ∈ dom(S Q ) such that S Q (x, i) = a, S Q (x, i) =
Definition 15 (pcover). Let A Q be an EL RV -description automata and A C be a ground EL RV -description automata. Let pc = ((q, → I ), c, S Q ) and pc ′ = ((q ′ , → I ′ ), c ′ , S ′ Q ) be two pconf s. We say that pc ′ is covered by pc, and we note pc ′ ◁ pc, if and only if the following conditions hold:

(i) c = c ′ , (ii) q = q ′ and, (iii) For all (x, I x ) ∈ dom(S Q ), there exists (x, I ′ x ) ∈ dom(S ′ Q ) such that S Q (x, I x ) = S ′ Q (x, I ′ x )
Example 15. Let consider the three following pconf s :

pc 1 = (Q 2 , (3, 3), C, {(x, 3.) = R}) pc 2 = (Q 2 , (5, 5), C, {(x, 5) = S, (y, 5) = R}) pc 3 = (Q 2 , (6, 6), C, ∅)
The two first criteria of pcover are clearly respected for all the combination of these pconf . There are no pcover relationship between pc 1 and pc 2 . Indeed, if we focus on (x, 3) = R of pc 1 there does not exists (x, 5) = R in pc 2 which contradicts the third condition and reversely for (x, 5) = S. On the other hand, pc 3 having only free variables naturally leads to pc 1 ◁ pc 3 and pc 2 ◁ pc 3 .

Check Match (Algorithm 1) is based on a synchronized product of executions of description automata. Given two EL RV -description automata A C and A Q , the algorithm tests whether A Q ≪ ∀ A C . To achieve this task, Check Match explores a search space made of pconf s describing a specific state of a synchronous execution of A Q and A C . The algorithm Check Match starts at an initial pconf 0 = ((Q, → 0 ), C, S 0 = ∅), corresponding to the two initial configurations of T (A Q , σ) and T (A C , id) with initially an empty set of variable assignments. Then the idea is to explore the synchronous product of T (A Q , σ) and T (A C , id) to incrementally construct a witness σ by guessing at each pconf = ((q, → I ), c, S Q ) the appropriate values for the variables that are free at state q in order to preserve the homomorphism from T (A Q , σ) to T (A C , id).

More precisely, this amounts to constructing mappings from the outgoing transitions of the configuration (q, → I ) into the outgoing transitions of c (Algorithm 1 Line 4). Let M q →c be the set of such mappings. Each mapping M ∈ M q →c is made of a set of pairs (((q, → I ), x, (q ′ , → J )), (c, a, c ′ )) indicating that the transition ((q, → I ), x, (q ′ , → J )) of T (A Q , σ) is mapped to the transition (c, a, c ′ ) of T (A C , id). The algorithm makes a non-deterministic guess among the possible mappings. For the chosen mapping, S Q is extended into S ′ Q containing the new assignments. Indeed, for each element m i = (((q, → I ), x, (q ′ , → J )), (c, a, c ′ )) of M , the assignment (x, I x ) = a is generated. In other words,

S ′ Q = S Q ∪ m i ((x, I x ) = a)
. Any free remaining variable will receive a non-deterministic assignment to a value of the domain of valuation L C and stored in S Q . If the chosen mapping of M q →c generates an inconsistent extension of variable assignments S ′ Q then the Check Match algorithm returns false (Algorithm 1 Line 7).

If the extended assignment Line 12). The algorithm then recursively calls Check Match for each generated pc ′ i . Thus the processing of the mapping M succeeds if all such calls succeed (Algorithm 1 Line 14).

S ′ Q is consistent then it creates a new product configuration pc ′ i = ((q ′ , → J ), c ′ , S ′ Q ) for each element m i = (((q, → I ), x, (q ′ , → J )), (c, a, c ′ )) of M (Algorithm 1

Algorithm 1 Check Match

Input : A Q , A C ; pconf : pc = ((q, → I ), c, S Q ); Pconf's historic : Hist Output : True if A Q ≪ ∀ A C , False otherwise 1: if q is leaf
or there exists a cover of pc in Hist then Compute the mappings M q →c w.r.t. S Q 5:

Guess M ∈ M q →c ; let |M | = n 6: S ′ Q ← S Q extended according to pairs of M 7: if S ′ Q is inconsistent then 8:
return False for

m i = ((q, → I ), x, (q ′ , → J )), (c, y, c ′ )) ∈ M do 12: Compute pc ′ i = ((q ′ , → J ), c ′ , S ′ Q ) 13:
end for 14:

return i∈[1,n] Check Match(A Q , A C , pc ′ i , Hist) 15:
end if 16: end if Let focus on the first mapping M ε 1 which is represented in the box M ε 1 of the figure. The reached children 0 and 1 are respectively labeled by ((Q 2 , (1, 1)), C, ∅) and ((N A 1 , (0, 0)), C, {(x, 0) = S, (y, 0) = S}). The node 0 is dashed because it fulfills a pcover relationship. Indeed, 0 is such that the label of the previous node ε is covered by λ(0) therefore the algorithm stops. Regarding the node 1, the algorithm has to check the homomorphism from (N A 1 , (0, 0)) into C. There is no outgoing transition from C labeled by A 1 , consequently ((N A 1 , (0, 0)), A 1 , (q f , (0, 0))) can not be mapped into any outgoing transition from C. The set of mappings is then empty therefore the algorithm returns false (symbolized by the cross in the figure). All execution trees corresponding to M ε 1 are then completed and correspond to a failing run since there are no valid mapping. We will now look toward M ε 2 which is represented in the box labeled M ε 2 . This mapping produces children 0 and 1 such that λ(0) = ((Q 2 , (1, 1)), D, ∅) and λ(1) = ((N A 1 , (0, 0)), N A 1 , ∅). None of them are covered and their corresponding sets of mappings M 0 and M 1 are not empty.

A branch of a product execution tree is completed once it reached a covering node, a leaf or fails to find a simulation. If it continues, the algorithm guesses for each child a new mapping. Each non-deterministic choice of mapping and thus their combination leads to a different product execution tree. Chosen mappings may have children that will recursively call the algorithm. To differentiate these choices, we say that a product execution tree is associated to a combination of mappings M . The only mapping possible for the node 1, M 1 1 maps ((N A 1 , (0, 0)), A 1 , (q f , (0, 0))) into (N A 1 , A 1 , q f ). Note that the reached pconf contains the leaf q f so the algorithm naturally stops. There are two outgoing transitions from the configuration (Q 2 , (1, 1)):

t 1 = ((Q 2 , (1, 1)), (x, 1), (N A 1 , (2, 2))) t 2 = ((Q 2 , (1, 1)), (y, 1), (Q 2 , (2, 2)))
There are three outgoing transitions from (D):

t ′ 1 = (D, S, N A 1 ) t ′ 2 = (D, S, C) t ′ 3 = (D, R, D) The figure illustrates two mappings M 0 1 = {(t 1 , t ′ 3 ), (t 2 , t ′ 3 )} and M 2 2 = {(t 1 , t ′ 1 ), (t 2 , t ′ 2 )}.
The mapping M 0 1 fails for the same reasons as M ε 1 . Regarding M 0 2 , the reached children are 00 with λ(ε) ◁ λ(00) = ((Q 2 , (2, 2)), C, ∅) and 01 which is similar to 1 so the execution will naturally reach a leaf by choosing the only mapping possible M 01 1 . A successful product execution tree corresponds to the mapping The notion of product execution tree of Check Match will then be formally defined with regard to a mapping M . This mapping is a union of mappings corresponding to the recursive choices the algorithm made.

M with M = M ε 2 ∪ M 0 2 ∪ M 1 1 ∪ M 01 1 . ϵ ∨ ϵ 0 1 × ϵ 0 1 ∨ ϵ 0 01 00 01 1 10 ϵ 0 01 00 × 1 10 σ(y, 0) = S σ(x, 0) = S σ(y, 0) = R σ(x, 0) = R σ(y, 1) = S σ(x, 1) = S A1 σ(x, 1) = R σ(y, 1) = R A1 σ(y, 0) = R σ(x, 0) = R σ(y, 0) = R σ(x, 0) = R A1 ((Q2, (0, 0)), C, ∅) ((Q2, (0, 0)), C, ∅) ((Q2, (1, 1)), C, ∅) ((NA 1 , (0, 0)), C, {(x, 0) = S, (y, 0) = S}) ((Q2, (0, 0)), C, ∅) ((Q2, (1, 1)), D, ∅) ((NA 1 , (0, 0)), NA 1 , {(x, 0) = R, (y, 0) = R}) ((Q2, (1, 1)), D, ∅) ((Q2, (2, 2)), C, ∅) ((NA 1 , (1, 1)), NA 1 , {(x, 1) = S, (y, 1) = S}) ((NA 1 , (0, 0)), NA 1 , {(x, 0) = R, (y, 0) = R}) ((qf , (0, 0)), qf , {(x, 0) = R, (y, 0) = R}) ((qf , (1, 1)), qf , {(x, 1) = S, (y, 1) = S}) ((Q2, (1, 1)), D, ∅) ((NA 1 , (1, 1)), D, {(x, 1) = R, (y, 1) = R}) ((Q2, (2, 2)), D, ∅) ((NA 1 , (0, 0)), NA 1 , {(x, 0) = R, (y, 0) = R}) ((qf , (0, 0)), qf , {(x, 0) = R, (y, 0) = R}) ((Q2, (0, 0)), C, ∅) ((Q2, (0, 0)), C, ∅) M ε 1 M ε 2 M ε 2 ∪ M 0 2 ∪ M 1 1 ∪ M 01 1 M ε 2 ∪ M 0 1 ∪ M 1 1

Definition 16 (Product execution tree of Check Match w.r.t to M). Let

A Q = (Q Q , L Q , Var Q , q 0 , δ Q , q f , κ Q ) and A C = (Q C , L C , Var C , c 0 , δ C , c f , κ C ) be two description automata. Let → G ∈ N |Var Q | be
a counter and let S be the set of all possible pconf . A run of Check Match, denoted Exec A Q ,A C and called a product execution tree, is a ⟨S, L C ⟩-labeled tree (τ, λ, δ) constructed as follows:

• λ(ε) = ((q 0 , → 0 ), c 0 , ∅), a root of the tree, and let → G = → 0 , a global counter initialized to a vector of zero.

• Let n ∈ τ be a node such that λ(n) = ((q, → I ), c, S q ) For each m i in ((q, → I ), t, (q ′ , → J )), (c, a, c ′ )) ∈ M ,a new child ni of n is generated according to the following sequence:

(i) δ(n, ni) = S q (t, I t ) = a, t ∈ Var Q a t ∈ L C (ii) ∀y ∈ Var, if q ′ ∈ κ(y) then G y := G y + 1, and (iii) Let → J = J y = G y , ∀y ∈ Var, s.t. q ′ ∈ κ(y) J y = I y otherwise (iv) λ(ni) = ((q ′ , → J ), c ′ , S ′ q ) with S ′ q = S q ∪ {(x, I x ) → a|(((q, → I ), x, (q ′ , → J )), (c, a, c ′ )) ∈ M }.
Everything required to prove correctness of the algorithm is now defined. The next section will then detail termination, soundness and completeness of Check Match.

Correctness of Check Match 4.3.1 Termination of Check Match

A run of the algorithm with the initial pconf leads to an exploration of its associated execution tree. An execution tree may be infinite, however we aim here to prove that only a finite part is explored leading to the algorithm's halt. The algorithm stops exploring a branch if one of the following occurs: (i) A leaf has been reached.

(ii) The chosen mapping M q →c of a visited pconf failed.

(iii) A pconf fulfills cover criteria.

The two first cases will not be discussed since by definition they terminate. It remains to discuss potential infinite branches. In our context, it means that there exists an infinite sequence of pconf s without pcover. The following property ensures that using pcover prevents from an infinite branch.

Property 1. Let A Q = (Q Q , L Q , Var Q , q 0 , q f , δ Q , κ Q ) be a description automaton and A C = (Q C , L C , Var C , c 0 , c f , δ C , κ C ).
For any infinite sequence of pconf pc 1 .pc 2 .pc 3 ...pc n , there exists i < j such that pc i ◁ pc j .

Proof. Let assume the infinite sequence of pconf pc 1 .pc 2 .pc 3 ...pc n . Q P and Q C are finite sets. As a direct consequence, there exists q q ∈ Q Q such that there are an infinite number of pc k of the form (q k = (q q , I k ), c, S q k ) withing the infinite sequence.

Let focus on this infinite set of pc k . For any pconf there are up |D| |Var Q | different possible variable assignments with the finite domain D = L C . Therefore, in the considered infinite set, there are at least two pconf with the same assignment.

Consequently, if we take pc k = (q k = (q q , I k ), c k = c, S q k ) as defined above then there exists k < k ′ such that pc k ′ = (q k ′ = (q q , I ′ k ′ ), c k ′ = c, S q k ′ ) and the following can be observed :

1. c k = c k ′ ,
2. q q = q q and 3. For all (x, I x ) ∈ dom(S q k ), there exists (x, I ′ x ) ∈ dom(S q k ) such that S q ′ k (x, I x ) = S q k ′ (x, I ′ x ) Consequently, pc k and pc ′ k are such that pc k ◁ pc ′ k and k < k ′ which concludes the proof.

As a direct consequence Check Match has the following property.

Property 2. The algorithm Check Match terminates.

Soundness of Check Match

A run of the algorithm with the initial pconf leads to an exploration of its associated execution tree. We will consider here, Exec A Q ,A C = (τ, λ, δ) corresponding to a successful run of Check Match.

From Exec A Q ,A C , we are able to extract a partial configuration tree P T (A Q , σ) of A Q and a partial configuration tree P T (A C , id). The algorithm ensures the following properties :

(i) There is a homomorphism from P T (A Q , σ) into the partial-tree of P T (A C , id).

(ii) P T (A Q , σ) and P T (A C , id) can be extended to configuration trees T (A Q , σ) and T (A C , id) such that there is a homomorphism between

T (A Q , σ) into T (A C , id) (Lemma 6). Based on Exec A Q ,A C = (τ, λ, δ), we define the partial trees P T (A Q , σ) = (τ Q , λ Q , δ Q ) and P T (A C , id) = (τ C , λ C , δ C ) as follows : • ∀n ∈ τ , λ(n) = ((q, → I ), c, S q ) then λ Q (n) = (q, → I ) and λ C (n) = (c). • δ Q (n, ni) = δ C (n, ni) = δ(n, ni).
Configuration trees are associated to a function σ, the corresponding σ of this tree is the union of all variable assignments of the run, i.e. σ = S q . By construction, it is clear that there is a homomorphism between those trees (i.e. Z(i) = i).

These trees are partial configuration trees for two reasons :

(i) A branch has been cut by pcover preventing from the infinite branch of T (A Q , σ) or T (A C , id).

(ii) Only outgoing transitions of A C required to mimic A Q are explored. Some outgoing transitions of A C may not be explored by the algorithm.

Example 19. Figure 4.2 depicts how to extract trees from Exec A Q 2 ,A C on the running example. Based on the successful product execution tree presented before, we extract a configuration tree of A Q 2 by keeping only configurations of A Q 2 in the labels. For example, the node ε (labeled by

((Q 2 , (0, 0)), c, ∅) in Exec A Q ,A C
) is labeled by (Q 2 , (0, 0)) in the extracted tree (which is exactly the label of the root of a configuration tree of A Q 2 ). The corresponding witness σ is made of all the mapping choices : σ = {(y, 0) = S, (x, 0) = R, (y, 1) =, (x, 1) = S}

We apply the same process to extract a partial tree of T (A C , id). For instance, it leads to C for the label of the node ε. Since C is ground, the substitution function which is the identity does not appear explicitly. This figure also illustrates why the resulting tree is only a partial-tree. The transition (C, S, C) of A C should have led to the edge (ε, S, 2) with λ C (2) = C. However, it was not used during the simulation process which makes the obtained tree incomplete.

ε 0 01 00 010 1 10 σ(y, 0) = R σ(x, 0) = R A 1 σ(y, 1) = S σ(x, 1) = S A 1 ((Q 2 , (0, 0)),///// C, ∅) (Q 2 , (1, 1)) (Q 2 , (2, 2)) (N A1 , (1, 1)) (N A1 , (0, 0)) (q f , (1, 1)) (q f , (0, 0)) ε 0 01 00 010 1 10 R R A 1 S S A 1
(////////////// (Q 2 , (0, 0)),C, / ∅) It remains to show that pcover does not damage the existence of a homomorphism. The intuition is to exploit the characteristics of the pcover. The space explored by a covering pconf is wider than the space explored by a covered one (Definition 15 Item (iii)). Therefore if the covered one succeeded, the covering one, which encloses even more possibilities, will succeed.

(N A1 ) (D) (C) (N A1 ) (q f ) (q f ) Z(ε) Z(0) Z(1)
Lemma 6. Let A Q = (Q Q , L Q , Var Q , q 0 , q f , δ Q , κ Q ) be a description automaton and A C = (Q C , L C , Var C , c 0 , c f , δ C , κ C
) be a ground description automaton. For any pconf pc i = ((q i , → I ), c i , S i ) and pc j = ((q j , → J ), c j , S j ) with i < j and such that pc i ◁ pc j . Then

(q j , → J ) ≪ ∀ (q i , → I ) and c i ≪ ∀ c j
Proof. Since c i = c j by definition of pcover this part is trivial.

Let focus on (qj, → J ) ≪ ∀ (q i , → I ) by definition of pcover we have :

• q i = q j and
• For all (x, J x ) ∈ dom(S j ), there exists (x, I x ) ∈ dom(S i ) such that S i (x, I x ) = S j (x, J x )

Then for any outgoing edge of (q, → J ) which is of the form ((q, → J ), x, (q ′ , → J ′ )) there is an outgoing edge ((q, → I ), x, (q ′ , → I ′ )).

The different cases are :

• x is a constant which is trivial.

• (x, I x ) is free (i.e. (x, I x ) / ∈ dom(S i )) then (x, J x ) is free. For all σ such that σ(x, I x ) = a, we can construct σ ′ such that σ ′ (x, J x ) = a = σ(x, I x ).

• (x, I x ) is not free (i.e. S i (x, I x ) = a) and (x, J x ) is free then we can take S j (x, J x ) = a.

• (x, I x ) is not free and (x, J x ) is not free either. We have S i (x, I x ) = S j (x, J x ) = a by definition of pcover.

The reached configuration (q ′ , → I ′ ) and (q ′ , → J ′ ) are such that (q ′ , → J ′ ) ◁ (q ′ , → I ′ ). The same reasoning can then be recursively applied. Thus leading to (q j ,

→ J ) ≪ ∀ (q i , → I ).
While looking for a witness, the algorithm checks the pconf pc i = ((q i , → I ), c i , S i ) in order to have (q i , → I ) ≪ ∀ c i . It stops when a leaf is reached which is a trivial or when it finds a cover pc j = ((q j , → J ), c j , S j ) for this configuration (i.e. pc i ◁ pc j ). In this case, (q i , → I ) ≪ ∀ c i has been verified during the run. Therefore, thanks to Lemma 6 and transitivity of universal simulation, we have (q j , → J ) ≪ ∀ c j .

Property 3. The algorithm Check Match is sound.

The finite automaton corresponding to the witness can be constructed by fusing covered nodes. Thus leading to consider σ repeating itself with a regular pattern. The witness will then takes the shape of a finite set of definitions giving a regular matcher. Nodes labeled with ground-description are also merged independently of their counters.

Example 20. The Figure 4.3 depicts the construction of the ground automaton corresponding to the generated witness. To be more precise the nodes ε and 00 are fused and the resulting nodes is named σ(Q 2 ). The node 0 is renamed σ(Q ′ 2 ) because it represents a different valuation of variables. Regarding the couples (01, 1) and (010, 10), each member of a same couple are fused since they represent the same ground concept. The resulting nodes are respectively named after the ground concept: N A 1 and q f . This automaton is then translated into a fnite TBox σ(T Q 2 ). Proof. Assume that there exists a witness σ 0 such that there is a homomorphism Z from

σ(T Q 2 ) = σ(Q 2 ) ≡ ∃R.A 1 ⊓ ∃R.σ(Q ′ 2 ), σ(Q ′ 2 ) ≡ ∃S.A 1 ⊓ ∃S.σ(Q 2 ) σ(Q 2 ) N A1 σ(Q ′ 2 ) q f σ(x, 0) = R A 1 σ(y, 0) = R σ(x, 1) = S σ(y, 1) = S
T (A Q , σ 0 ) into T (A C , id).
Since the set of mappings M q →c are exhaustive, we can use Z to lead the algorithm to choose the mappings corresponding to σ 0 . Thanks to the fact that the algorithm terminates (Property 2), the algorithm necessarily stops. If the algorithm answers false, it means that the variable assignment is not consistent which contradicts the fact that σ 0 is a witness. If the algorithm answers true, the algorithm may have stopped while constructing a witness σ. Due to pcover, we may have σ ̸ = σ 0 . However, soundness (Property 3) ensures that σ is also a solution. Consequently, if a solution exists the algorithm answers yes.

The proof of the Lemma 7 shows that given a solution to lead the algorithm, there necessarily exists a regular solution σ resulting in the following corollary.

Corollary 2. An EL RV matching problem C ⊑ ?

T Q has a solution iff it has a regular solution.

Check Match has been proven to terminate as well as being sound and complete making matching in EL RV decidable.

Conclusion of Chapter 4

This chapter presents the algorithm Check Match which demonstrates that matching in EL RV is decidable. Its main idea is to run synchronously the two automata A Q and A C leading to consider product configurations that combine a configuration of A Q , a configuration of A C to keep track of the synchronous run and a mapping S Q to preserve variable assignments.

This result is used as a baseline for the next chapter which will extends the proposed algorithm to both pattern containment and weak-subsumption.

Chapter 5 Solving Pattern Containment in EL RV

This chapter represents the main contribution of this thesis. It consists in solving pattern containment by designing an algorithm named Check Simu. The algorithm follows the idea of the synchronous product of Check Match while introducing the notion of constraints to handle variables on both sides. It leads to the definition of extended product configuration and extended cover with regard to a set of constraints. The algorithm is proven to be correct making pattern containment decidable. Moreover, we study the complexity of pattern containment and more generally of the reasoning tasks in EL RV . We prove that it is exptime-complete. The lower-bound is achieved by a reduction of matching problem to halting problem of alternating turing machine which is polynomially bounded by the size of the input. Table 5.1 summarizes notations introduced in this chapter.

Symbol

Description

pc = ((q q , → I ), (q p , → J )) Extended product configuration (epconf) C Set of constraints R V (q) Relevant constraints w.r.t q = (q q , → I ) C |q Relevant set of constraints w.r.t q QF (C) Quantified constraint associated to C ◁ C
Extended cover w.r.t a set of constraints C Table 5.1: Notations introduced in Chapter 5

From Matching to Pattern Containment

We previously demonstrated how to solve matching, a special case of pattern containment. The approach presented is the root of our method to solve pattern containment. However, some differences must be enlighten in order to extend the algorithm. The main difference lies in variable's domain of valuation. Matching focuses on mapping variables into a finite domain made of constants appearing in the ground definition C. Considering variables on both sides requires mapping function to consider mapping : It enlarges the size of the valuation domain to an infinite size. It is explained by the fact that there are an infinite number of variables induced by refreshment and cycles. Moreover, the domain of valuation of variables can not be limited to constant of P and Q as we did for matching. Indeed, the pattern containment problem asks for such a relationship w.r.t to any TBox. The following example will illustrate the impact of such a constraint. Let consider the following patterns :

• T Q = {Q ≡ ∃z.Q ⊓ ∃y.A 2 ⊓ ∃x.A 1 } • T P 1 =    P 1 ≡ ∃R.P 2 ⊓ ∃R.P 3 P 2 ≡ ∃S.P 1 ⊓ ∃R.P 3 ⊓ w.P 3 P 3 ≡ A 1 ⊓ A 2    • T P ′ 1 =    P ′ 1 ≡ ∃R.P ′ 2 ⊓ ∃R.P ′ 3 P ′ 2 ≡ ∃S.P ′ 1 ⊓ ⊓w.P ′ 3 P ′ 3 ≡ A 1 ⊓ A 2   
The variable x is a non-refreshing variable while all the others variables are refreshing variables. Let us first focus on the the pattern containment problem P ′ 1 ⊑ Q. It is worth to note the answer changes if one considers a specific TBox instead of "for all TBoxes" of pattern containment's definition. Indeed, P ′ 1 ⊑ Q is not solvable for all the ground TBox but only for the ones dealing with N R = {R}. For instance, considers a T Box that involves N R = {R, S}, then for the substitution σ such that σ(w, i) = S there exists no substitution θ such that the subsumption relationships holds. On the other hand, the pattern containment problem P 1 ⊑ Q is solvable and will be used as a running example in the remaining discussion about pattern containment. Figure 5.1 depicts the automata related to those definitions.

Q N A1 N A2 q f z x y A 1 A 2 P 1 P 3 P 2 q f R R A 1 A 2 R S w P ′ 1 P ′ 3 P ′ 2 q f R A 1 A 2 R S w

Presentation of Check Simu

This section presents the algorithm Check Simu, which is used to test universal simulation between EL RV -description automata. Let

A Q = (Q Q , L Q , Var Q , q 0 , δ Q , q f ,
κ Q ) and A P = (Q P , L P , Var P , p 0 , δ P , p f , κ P ) be two description automata. To test whether A Q ≪ ∀ A P , the main idea behind Check Simu is to run synchronously A Q and A P , trying to construct iteratively two generic instantiations θ G and σ G of, respectively, A Q and A P , which ensure that ∀σ, ∃θ such that there exists a homomorphism from T (A Q , θ) to T (A P , σ). The two substitutions are called generic because θ G maps variables of A Q to constants or variables that appear in an execution of A P (i.e.: θ G : Var Q × N → L P ∪ (Var P × N)) while σ G is the identity function. More precisely, the algorithm Check Simu runs A Q and A P trying to generate two generic configurations trees

T (A Q , θ G ) = (τ, λ 1 , δ 1 ) and T (A P , σ G ) = (τ, λ 2 , δ 2 )
over the same tree structure τ . The trees T (A Q , θ G ) and T (A P , σ G ) are synchronized in the sense that when processing a node i ∈ τ , with λ 1 (i) = (q, → I ) and λ 2 (i) = (p, → J ), the algorithm maps each transition (q, t, q ′ ) of A Q to a transition (p, t ′ , p ′ ) in A P such that t = t ′ . To achieve this task, the algorithm creates a new child ij with λ 1 (ij) = (q ′ , → I ′ ) and

λ 2 (ij) = (p ′ , → J ′ ) and generates a new equality constraint δ 1 (i, ij) = δ 2 (i, ij) to ensure that the two transitions are synchronized. Note that δ 1 (i, ij) = θ G (t, I t ) if t is a variable of A Q and δ 1 (i, ij) = t is t is a constant in A Q . Similarly, δ 2 (i, ij) is either a constant t ′ or σ G (t ′ , I t ′ ) if t ′ is a variable of A P .
Consequently, a generated constraint has the form of an equality between either a constant or θ G (t, I t ) from one side and a constant or σ G (t, I t ) from the other side (c.f., definition 17). The generated set of constraints is quantified to obtain a quantified constraint formula where variables in T (A Q , θ G ) are existentially quantified while variables of T (A P , σ G ) are universally quantified (c.f., definition [START_REF] Belkhir | Fresh-variable automata: Application to service composition[END_REF]. By construction, the algorithm ensures that the identity mapping Z id : τ → τ such that Z id (i) = i is a homomorphism from T (A Q , θ G ) to T (A P , σ G ). In addition, a second important property ensured by the algorithm is that if the generated formula is satisfiable then one can prove that for any substitution σ, there exists θ = σ • θ G such that there is a homomorphism from

T (A Q , θ) into T (A P , σ) i.e. A Q ≪ ∀ A P .
In the remaining, we define the notion of constraints, epconf (extended product configuration) and epcover (extended product cover) to formally present the algorithm Check Simu. Variables of A P are referred as universal variables since A P is associated to the universal quantifier in pattern containment definition. Similarly, variables of A Q are referred to as existential variables.

Definition 17 (Constraint). Let A Q ≪ ∀ A P be a universal simulation problem. An associated constraint is a statement of one of the following forms:

• (x, i) = (y, j), • (x, i) = a, or • a = b
where x, y are variables from Var Q ∪ Var P , i, j ∈ N and a,b are constants from L Q ∪ L P .

In the following C denotes a set of constraints and C T the transitive closure of C w.r.t. to the equality relationship. The following definition formalizes the notion of epconf . Definition 18 (epconf). Let A Q , A P be two description automata. An epconf is a tuple (q, p) where q is a configuration of A Q , p is a configuration of A P . Example 21. For example, we can consider the following epconf s :

• ((Q, (0, 0, 0)), (P 1 , (0))) and;

• ((Q, (0, 1, 1)), (P 3 , (3))).

When testing A Q ≪ ∀ A P , we want to check out for all valuations of variables in A P there exists a valuation of variables in A Q . Therefore, universal simulation requires to quantify variables involved in constraints in order to preserve this information.

To preserve this semantics, we will exploit the notion of quantified constraints formula. It allows to consider universal quantifier in addition to the classic existential quantifier.

Definition 19 (Quantified constraint formula). Let A Q ≪ ∀ A P be a universal simulation problem and let C = {ψ 1 , . . . , ψ n } be a set of associated constraints using variables x 1 , . . . , x m from Var P and variables y 1 , . . . , y l from Var Q . The quantified constraint formula associated to C, denoted QF (C), is of the form ∀x 1 , . . . ∀x m , ∃y 1 , . . . , ∃y l (ψ 1 ∧ ... ∧ ψ j ).

All constraints ψ i can only be equality constraint as stated in Definition 17. In this context, quantified constraint formula corresponds to quantified constraint for positive equality constraint languages. Our objective is to ensure that considered quantified constraint formula are satisfiable for infinite domain since we aims to solve it for any TBox. Satisfiability for quantified constraint formula w.r.t positive equality constraint languages and infinite domain is proven to be np-complete [START_REF] Bodirsky | Quantified equality constraints[END_REF].

We say that a set of constraints is satisfiable if the corresponding quantified constraint formula is satisfiable. It is clear that any instance of a variable of Var P can be mapped to only one instance of Var Q (or a constant). Otherwise, the quantified formula generated would inevitably be unsatisfiable.

Example 22. Let x, y, z be variables and a be a constant.

• ∀(w, 0), ∀(w, 1), ∃(z, 0), (((w, 0) = (z, 0)) ∧ ((w, 1) = (z, 0))) is not satisfiable. Indeed, we can infer ∀(w, 0), ∀(w, 1), (w, 1) = (w, 0) which is unsatisfiable since w is a universal variable.

• ∀(w, 0), ∃(y, 0), (((w, 0) = (y, 0)) ∧ ((y, 0) = R)) is not satisfiable. Indeed, we can infer ∀(w, 0), (w, 0) = R which is not satisfiable when dealing with infinite valuation domains.

• ∀(w, 0), ∃(y, 0), ∃(z, 0), (((w, 0) = (y, 0)) ∧ ((z, 0) = R)) is satisfiable.

Definition 20 (Constraint set equivalence). Let C 1 and C 2 be two sets of constraints.

The set

C 1 is equivalent to C 2 , noted C 1 ≡ C 2 if : 1. (x, i) = (y, j) ∈ C 1 iff (x, i ′ ) = (y, j ′ ) ∈ C 2 2. (x, i) = a ∈ C 1 iff (x, i ′ ) = a ∈ C 2
Example 23. Let the following sets of constraints :

• C 1 = {((w, 1) = (z, 0))} • C 2 = {((w, 0) = R), ((w, 1) = (z, 0))} • C 3 = {((w, 3) = R), ((w, 4) = (z, 1))}
Following the definition of set equivalence (Definition 20), we have :

C 3 ≡ C 2 .
More precisely, for (w, 0) = R we have (w, 3) = R and for (w, 1) = (z, 0) we have (w, 4) = (z, 1). C 1 does not have any constraint of the form (w, j) = R which makes it not equivalent to the other two.

Relevance of a constraint depends on the epconf it is associated with. For example, let us consider C = {(x, 2) = (w, 2), (x, 1) = S, (w, 4) = (x, 3)} and the epconf pc = ((N A 1 , (3, 3, 3)), (P, (4))). The configuration (P, ( 4)) has only one counter, whose current value is 4 and we assume that this counter is associated with the variable w. Therefore, we know that the only constraint that constrains (P, (4)) is (w, 4) = (x, 3). Indeed, starting from (P, (4)), only the instance (w, 4) must be considered therefore (x, 2) = (w, 2) does not carry any information for this configuration. We introduce the notion of relevant variables which limits constraint sets to relevant set of constraints w.r.t to a epconf . Definition 21 (Relevant constraints w.r.t. a configuration c). Let C be a set of constraint and let c = (q c , I c ) be a configuration.

• We define the set of relevant variables of c as R

V (c) = {(x, I cx )|x ∈ V \ κ -1 (q c )}.
• The relevant constraints of C w.r.t. a configuration c is defined as:

C |c = {(t 1 = t 2 ) ∈ C T |(t 1 ∈ R V (c) ∨ t 2 ∈ R V (q c )}.
Example 24. Let consider the configuration (Q, (0, 1, 1)) of A Q , the relevant variables are then (x, 0), (y, 1) and (z, 1). Let the following sets of constraints :

• C 1 = {((w, 1) = (z, 0))} • C 2 = {((w, 0) = R), ((w, 1) = (z, 0))} • C 3 = {((w, 3) = R), ((w, 4) = (z, 1))}
The relevant constraints are respectively :

• ∅ • ∅ • {((w, 4) = (z, 1))}
We dispose now of all the tools required to define pcover in the scope of pattern containment problems.

Definition 22 (epcover w.r.t a set of constraints). Let A Q and A P be two EL RV -description automata and let pc = (q, p) and pc ′ = (q ′ , p ′ ) be two epconf s. Let C be a set of constraints.

We say that pc ′ is covered by pc w.r.t. C, and we note pc ′ ◁ C pc, if and only if the following conditions hold: 1. q p = q p ′ and C |p ≡ C |p ′ 2. q q = q q ′ and C |q ≡ C |q ′

We are now ready to present our algorithm Check Simu (Algorithm 2). Given two EL RV -description automata A Q and A P , the algorithm tests whether A Q ≪ ∀ A P . To achieve this task, Check Simu explores a search space made of epconf s where each epconf describes a specific state of a synchronous execution of A Q and A P . When exploring an epconf (q, p), the algorithm makes non deterministic choices to map outgoing transitions of q to outgoing transitions of p while generating new constraints which are recorded in a global set of constraints. The algorithm starts with the initial epconf pc 0 = ((q 0 , → 0 ), (p 0 , → 0 )) made of the initial configuration (q 0 , → 0 ) of A Q and the initial configuration (p 0 , → 0 ) of A P . The initial global set of constraints C is empty. The idea is to explore the synchronous product and to try constructing two generic substitutions θ G and σ G by guessing at each epconf pc = ((q q , → I ), (q p , → J )) the appropriate mappings in order to preserve a homomorphism from T (A Q , θ G ) into T (A P , σ G ). More precisely, it aims to construct all mappings from the outgoing transitions of (q q , → I ) into outgoing transitions of (q p , → J ) (Algorithm 2 Line 3). Let M qq →qp be such a set of mappings.

Each mappings is a set of pairs of the form (((q q , → I ), t q , (q ′ q , → I ′ )), ((q p , → J ), t p , (q ′ p , → J ′ ))). The algorithm then guesses a mapping M ∈ M qq →qp (Algorithm 2 Line 7) and constructs a set of constraints C M made of constraints derived from the mapping M : for each pair (((q q , → I ), t q , (q ′ q , → I ′ )), ((q p , → J ), t p , (q ′ p , → J ′ ))) in M , a new constraint (t q = t p ) is added to C M . The global set of constraints C is then augmented with the new set C M (Algorithm 2 Line 8). If the global set of constraints is not satisfiable (i.e., the associated quantified constraint formula QF(C) is not satisfiable), the algorithm returns f alse (Algorithm 2 Line 9).

If the global set of constraints C is satisfiable the algorithm creates a new epconf pc ′ i = ((q ′ q , → I ′ ), (q ′ p , → J ′ )) for each element m i = (((q q , → I ), t q , (q ′ q , → I ′ )), ((q p , → J ), t p , (q ′ p , → J ′ ))) of M (Algorithm 2 Line 14). The algorithm then recursively calls Check Simu for each generated pc ′ i . Thus the processing of the mapping M succeeds if all such calls succeed (Algorithm 2 Line 16).

The algorithm stops and returns true if a leaf of A Q is reached or if a cover condition is fulfilled (Algorithm 2 Line 1).

In order to show correctness of the algorithm we need to define the execution tree of Check Simu. The next section will explain step by step how it is obtained before giving its formal definition.

Algorithm 2 Check Simu

Input : A Q , A P ; Epconf : pc ; Epconf's historic : Hist Output : True if A Q ≪ ∀ A P , False otherwise 1: if q is not a leaf and Check Cover(A Q , A P , pc, Hist) == f alse then 2:

Hist ← Hist ∪ {pc} 3:

Compute the mappings M q →p 4:

if M q →p = ∅ then Guess a mapping M from M q →p 8:

C ← C ∪ C M 9:
if C is not satisfiable then

for m i = (((q, → I ), t q , (q ′ , → I ′ )), ((p, → J ), t p , (p ′ , → J ′ ))) ∈ M do 14: Compute pc ′ i = ((q ′ , → I ′ ), (p ′ , → J ′ )) 15:
end for

Termination of Check Simu

A run of the algorithm with the initial epconf leads to an exploration of its associated execution tree. An execution tree may be infinite, however we aim here to prove that only a finite part is explored leading to the algorithm's halt. The algorithm stops exploring a branch if one of the following occurs:

(i) A leaf has been reached.

(ii) The chosen mapping M q →p of a visited epconf failed.

(iii) An epconf is covered by a previous one.

The two first cases will not be discussed since by definition they terminate. It remains to discuss potential infinite branches. In our context, it means that there exists an infinite sequence of epconf s. The following property ensures that using epcover prevents from an infinite branch. Property 4. Let Exec A Q ,A P be a product execution tree of two description automata A Q and A P and let C be its associated set of global constraints. For any infinite sequence pc 1 .pc 2 .pc 3 ...pc n of epconf s of Exec A Q ,A P , there exists i < j such that pc i ◁ C pc j .

Proof. Let A Q = (Q Q , L Q , Var Q , q 0 , q f , δ Q , κ Q ) and A P = (Q P , L P , Var P , p 0 , p f , δ P , κ P ). Let consider an infinite sequence pc 1 .pc 2 .pc 3 ...pc n of epconf s of Exec A Q ,A P . Q P and Q Q are finite sets. A a direct consequence, there exists q q ∈ Q Q and q p ∈ Q P such that there are an infinite number of pc k of the form (q k = (q q , I k ), p k = (q p , J k )) within this sequence.

If we take pc k as defined above then there exists k < k ′ such that pc k ′ = (q k ′ = (q q , I ′ k ′ ), q p ′ = (q p , J ′ k ′ )) and the following can be observed :

1. C |q k ≡ C |q k ′ 2. C |p k ≡ C |p k ′
Indeed, an instance of a variable of A Q has a total of (L P + Var P + 1) possible assignments which is a finite number. It is explained by the fact that if an existential variable is mapped to two different universal variables, the corresponding quantified formula is not satisfiable which limits Var P × N to Var P . Since epcover compares each relevant variable bounds, there are only a finite number of different possible mappings. Consequently, pc k and pc ′ k are such that pc k ◁ C pc ′ k and k < k ′ which concludes the proof.

As a direct consequence Check Simu has the following property.

Property 5. The algorithm Check Simu terminates.

Soundness of Check Simu

A run of the algorithm with the initial epconf leads to an exploration of its associated execution tree. We will consider here, Exec A Q ,A P = (τ, λ, δ) corresponding to a successful run of Check Simu.

From Exec A Q ,A P , we are able to extract a partial configuration tree P T (A Q , θ G ) of A Q and a partial configuration tree P T (A P , σ G ). The algorithm ensures the following properties :

(i) There is a homomorphism from P T (A Q , θ G ) into the partial-tree of P T (A P , σ G ) of A P .

(ii) P T (A Q , θ G ) and P T (A P , σ G ) can be extended to configuration trees T (A Q , θ G ) and T (A P , σ G ) such that there is a homomorphism between

T (A Q , θ G ) into T (A P , σ G ) (Lemma 8).
Based on Exec A Q ,A P = (τ, λ, δ), we define the partial trees P T (A Q , σ G ) = (τ Q , λ Q , δ Q ) and P T (A P , θ G ) = (τ P , λ P , δ P ) as follows :

• ∀n ∈ τ , λ(n) = ((q q , → I ), (q p , → J )) then λ Q (n) = (q q , → I ) and λ P (n) = (q p , → J ) • δ Q (n, ni) = δ P (n, ni) = θ G (t q ) = σ G (t p ) = t p
Configuration trees are associated to a function, here θ G is done according to the set of constraints of the execution tree C M while σ G is identity. By construction, it is clear that there is a homomorphism Z id between those trees such that Z id (i) = i. The tree labeled with configuration of A Q is a partial tree of a configuration tree and the one labeled with configuration of A P is a partial tree T (A P , σ G ).

Then ∀σ, θ = σ • θ G is a possible substitution for A Q such that the homomorphism is preserved.

These trees are partial configuration trees for two reasons :

(i) A branch has been cut by epcover preventing from the infinite branch of T (A Q , σ G ) or T (A P , θ G ).

(ii) Only outgoing transitions of A P required to mimic A Q are explored. Some outgoing transitions of A P may not be explored by the algorithm.

Figure 5.3 illustrates the resulting partial configuration trees of the running example. The following lemma states that epcover perserve the homomorphism for complete trees.

Lemma 8. Let A Q = (Q Q , L Q , Var Q , q 0 , q f , δ Q , κ Q )
and A P = (Q P , L P , Var P , p 0 , p f , δ P , κ P ) be two description automata. Let C be a set of constraints. For any epconf pc 1 = ((q 1 , → I ), (p 1 , → J )) and pc 2 = ((q 2 ,

→ I ′ ), (p 2 , → J ′ )) such that pc 1 ◁ C pc 2 w.r.t C. Then (q 2 , → I ′ ) ≪ ∀ (q 1 , → I ) and (p 1 , → J ) ≪ ∀ (p 2 , → J ′ )
Proof. By definition of epcover we have :

• p 1 = p 2 and C |p 1 ≡ C |p 2

• q 1 = q 2 and C |q 1 ≡ C |q 2

Correctness of Check Simu

Then for any outgoing edge of (q 2 , → I ′ ) which is of the form ((q 2 , → I ′ ), x, (q ′ , → K ′ )) there is an outgoing edge ((q 1 , → I ), x, (q ′ , → K)). The different cases are : • x is a constant which is trivial.

• For all unconstrained (x, I ′ x ) then (x, I x ) is unconstrained then for any σ ′ (x, I ′ x ) = t, we can construct σ such that σ(x, I x ) = t = σ(x, I x ).

• ∀((x,

I ′ x ) = t) ∈ C |q 2 , then (x, I x ) = t ∈ C |q 1 The reached configuration (q ′ , → K) and (q ′ , → K ′ ) are such that (q ′ , → K) ◁ C (q ′ , → K ′
). The same reasoning can then be recursively applied. Similarly, (p 1 ,

→ J ) ≪ ∀ (p 2 , → J ′
) is obtained by exchanging roles of p 1 and p 2 compared to q 1 and q 2 . While looking for the generic substitutions θ G and σ G , the algorithm checks the pconf

Completeness of Check Simu

The algorithm makes an exhaustive exploration thanks to computation of all the mappings (Algorithm 2 Line 3). Proof of completeness is then similar to the proof of Check Match using a given solution one can guide the algorithm. If the algorithm returns false, it demonstrated that the solution was not correct since the computation of mappings is exhaustive. Otherwise soundness ensures the algorithm's answer is good.

Property 7. The algorithm Check Simu is complete.

Extension to Weak-Subsumption

Pattern containment and weak-subsumption are two problems involving variable on both sides. Fortunately, decidability of weak-subsumption can be achieved similarly with a minor change to handle the specific features of the problem. Indeed, the simulation problem we aim to solve is A Q ≪ ∃ A P which only requires the existence of a substitution for both automata.

The main difference lies in the definition of the quantified constraint formula required for satisfiability. Intuitively, the quantified constraint formula applied the quantifier "∀" for any variable from A P and the quantifier "∃" for variables from A Q accordingly to the simulation definition. However, existential simulation does not carry any difference between variables since both sides are associated to the quantifier "∃". Consequently, the formula generated is a classic constraint formula defined as follows : ψ∈C ψ with C a set of constraints.

Example 27. Consider the following EL RV -terminology where all the variables that occur in EL RV -descriptions are refreshing variables. An execution of the algorithm is presented in Figure 5.5. The algorithm will return true.

A 1 ≡ A B 1 ≡ B C ≡ ∃R.B 1 P ≡ ∃x.P ⊓ ∃z.C ⊓ ∃z.B 1 ⊓ ∃S.A 1 Q ≡ ∃R.Q 2 ⊓ ∃R.C ⊓ ∃y.B 1 Q 2 ≡ ∃R.Q ⊓ ∃S.B 1 ⊓ ∃S.A 1
The proof of termination does not change since the number of configurations remains the same. However, in case of weak-subsumption, the substitution domain can be reduced to constants of A P and A Q since we only look for the existence of a solution.

Q Q 2 A 1 B 1 C q f R R y R R S A B S (a) A Q P A 1 C B 1 q f x z R z S A B (
σ(x, 0) = R σ(z, 0) = R σ(z, 0) = σ(y, 0) = R σ(x, 1) = R σ(z, 1) = S B 1 S = S A 1 R B 1 B 1 (Q, (0), P, (0, 0)) (Q 2 , (0), P, (1, 1))
(Q, (1), P, (2, 2))

(B 1 , (0), B 1 , (1, 1)) (q f , (0), q f , (1, 1)) (A 1 , (0), A 1 , (1, 1)) (q f , (0), q f , (1, 1)) (C, (0), C, (0, 0)) (B 1 , (0), B 1 , (0, 0)) (q f , (0), q f , (0, 0)) (B 1 , (0), B 1 , (0, 0)) (q f , (0), q f , (0, 0)) (z, 0) = R (y, 0) = (z, 0) (x, 0) = R (z, 1) = S (x, 1) = R

Complexity of Reasoning Tasks in EL RV

The algorithm Check Simu is proven to be correct as is Check Match. We will now demonstrate that these algorithms are optimal. The lower bound is achieved by a reduction from an alternating turing machine's problem to matching problem. The upper bound will be obtained by estimating the size of the space of search in the worst case. The next section give the details to compute those bounds resulting in a tight upper and lower bounds.

Lower Bound : ATM Halting and Matching

The exptime-hardness of checking universal simulation between EL RV -description automata is obtained by a reduction from the existence of infinite execution of an Alternating Turing Machine M working on a space polynomially bounded by the size of the input. This later problem is known to be exptime-complete [START_REF] Chandra | Alternation[END_REF].

Definition 24. Alternating Turing machine [START_REF] Chandra | Alternation[END_REF] An alternating Turing machine M is a tuple (Q, q 0 , Γ, δ, mode) where :

• Q is the set of states

• q 0 is the initial state

• Γ is the set of tape symbols

• mode : Q → {∀, ∃, accept, reject}. is the labelling function of control state

• δ : Q × Γ → P(Q × Γ × {L, R}) Figure 5.
6 represents an example of an alternating turing machine composed of three states. Among them, there are one universal state (q 0 ) and two existential states (q 1 and q 2 ). This machine will be later used to illustrate the reduction of universal simulation.

A configuration C of M is of the form y 1 , ..., qy j , ..., y n where q ∈ Q a state of M , and the head points actually on the j th letter of the tape (i.e., y i are the letters of the word w on the tape). A transition qa → bRq ′ is applicable from a configuration C if the letter pointed by the head is equal to a (y j = a), then the successor C' of C is equal to y ′ 1 , ...y ′ j , q ′ y ′ j+1 , ..., y ′ n s.t y k = y ′ k for k ∈ [1, n] and k ̸ = j and y ′ j = b. It can be rewritten over configuration as C qa/bRq ′ -→ C ′ or even (y 1 , ..., qy j , ..., y n ) qa/bRq ′ -→ (y ′ 1 , ...y ′ j , q ′ y ′ j+1 , ..., y ′ n ). The machine M then starts on C 0 = q 0 y 1 , ..., y n , where y i = w i , the i th letter of the input word w. The definition of acceptance of an alternating Turing machine is recursive :

• If the configuration C is in an accepting control state q, then C is accepting.

• If the configuration C is in a rejecting control state q, then C is rejecting.

• If the configuration C is in a universal control state q, then C is accepting if all the configurations reachable from C in one step are accepting and rejecting if some configurations reachable from C in one step are rejecting.

• If the configuration C is in an existential control state q, then C is accepting if some configurations reachable in one step are accepting and rejecting when all configurations reachable in one step are rejecting (the case of classical nondeterministic Turing machine correspond to an alternating machine where all states are existential).

M is said to accept an input word w if the initial configuration of M is accepting, and to reject w if the initial configuration is rejecting. A configuration reachable in one step from configuration C is called a successor of C and the set of successors of C is denoted successors(C). We consider the problem of the existence of an infinite execution of an Alternating Turing machine M on an input word w = w 1 , ..., w n . That is given a word w as input then whatever the transitions of universal states of M the machine must continue the execution. For existential states of M , the,machine must have at least a transition such that the machine continues its execution. Thus, rejecting states are states without outgoing transitions.

The machine works on a space bounded by the size n of the input word w. Hence, if the head points on x 1 the machine is not allowed to move to the left (i.e. execute a transition labelled with L), and if the head points on x n the machine is not allowed to move to the right (i.e. execute a transition labelled with R).

Given an Alternating Turing Machine M working on a space polynomially bounded by the size of the input word w. We construct two description automata denoted as A control and A test such that M has an infinite execution on the input w if and only if A test ≪ ∀ A control . Note that in the reduction A control will be a ground automata hence considering a matching problem which is a special case of pattern containment. Therefore, we will only aim to prove the existence of a substitution for A test .

We consider a function nt: Q → N such that it gives for each state q of M the number of outgoing transitions. For practical purpose, each state q of M will consider a specific order over transitions t j with j ∈ [1,nt(q)]. This order will be used later on to build A control and A test .

Construction of A control decomposes transitions of the original machine M . To do so, we will encode each state q of M as a state l q in A control . Moreover, we denote a set of states {q t j ,i } such that the j th transition t j of q can be decomposed. A transition of M first reads the letter in x pointed by the head then the transition replaces value stored in the cell x and moves the head accordingly. Each steps will then corresponds to a specific transition in A control . A control focuses on capturing the structure and the behaviour defined in M . In other words it emphasizes on the input word w and transitions of M . Each transition in M is encoded into a sequence of transitions in A control . Note that the structure induced differs regarding the mode of the state (i.e. universal or existential).

Definition of A control :

Let A control = (L control , Var control , Q control , q 0,control , q f,control , δ control , κ control ) defined as follows :

• The set of letters L control is composed of : -{l q |q ∈ Q} with Q the set of states of M -{q t j ,i } a set of additional states such that i ∈ [0, 3] and j ∈ [1, m] with m as defined above -{q init,i } a set of additional states used to mimic the input w with i ∈ [0, n[ univ, a state that can loop on itself with any letter of L control

• q 0,control = q init,0

• q f,control = ∅

• The set of transitions δ control is composed of :

-For each letter of w = w 1 ...w n : {q init,i , w i , q init,i+1 } for i ∈ [0, n[ and (q init,n-1 , w n , l q 0 ) -For each transition t j of q such that q a/bd -→ q ′ where q is an existential state of M , j ∈ [1,nt(q)] :

A control alone only encodes the behaviour of the alternating turing machine. On the opposite, A test emphasizes on the tape and the head position. It considers a set of variables where each element x i corresponds to the i th cell of the tape. For each state of q in M , we then denote q x i the state encoding q in M with the head on the i th cell.

In A test , the set {q x,t j ,i } is used to decompose transitions of M with q the state considered, x representing the variable pointed by the head and t j the transition. By making a wise use of L and R, we can link the transition toward the state simulating the head position in a deterministic way. As we did for A control , we will use a set of additional transitions to capture the behaviour of universal states and existential states.

Definition of A test :

Let A test = (L test , Var test , Q test , q 0,test , q f,test , δ test , κ test ) defined as follows :

• The set of letters L test is composed of :

-{t j } with j ∈ [1, m], the symbols representing the transitions of M and m = max({nt(q)|q ∈ Q}) the maximal number of transitions for one state in M .

-{w i } the symbols. corresponding to the letters of the input

w with i ∈ [1, |w| = n].
-Γ ∪ {L, R}, the symbols used in M reject a letter to model failing states of M .

• The set of variable Var test is composed of :

-{x i } with i ∈ [1, |w| = n],
refreshing variables corresponding to the n letters of the input word w.

choice a refreshing variable required for existential state of M

• The set of states Q test is composed of :

-{q x i |q ∈ Q} with Q the set of states of M and x i representing the position of the head on the i th cell in M -{q x,t j ,i } a set of additional states such that x target the outgoing variable used by the state, i ∈ [0, 3] and j ∈ [1, m] with m as defined above.

-{q init,i } a set of additional states to initialize w with i ∈ [0, n[

• q 0,test = q init,0

• q f,test = ∅

• The set of transitions δ test is composed of :

-For each letter of w = w 1 ...w n : {q init,i , x i , q init,i+1 } for i ∈ [0, n[ and (q init,n , x n , q x 1 )

-For each transition t j of q such that q a/bd -→ q ′ where q is an existential state of M , j ∈ [1,nt(q)] and for i ∈ [1, n]: * (q x i , t j , q x i ,t j ,0 ) , If the simulation fails because A control can not simulate A test , it means that the move of M can not be done according to the current values of the tape. We will now present how behaviours of initialization, universal states and existential states are captured by universal simulation.

• Initialization : A sequence of states/transitions is added such that concatenating labels of the transitions forms w. This sequence ends reaching the state representing in A control the initial state of M . The same is done in A test with the corresponding variables instead of letters of w. Note that this sequence leads to the state representing the initial state of M with the head on the first letter. The only possibility for an homomorphism is to associate to each variable x i the letter w i . Figure 5.7 illustrates of both A control and A test initialization on the running example for the word w = ab.

q init,0 q init,1 q 0 • Universal states : The constructions in both automata are identical up to variables. For example, let consider the same transition (q 0 , b/aL, q 1 ) knowing it is the second transition and that the head is on the first letter. This transition is respectively encoded in A test and A control as :

x 1 x 1 x 2 . . . (a) A test q init,0 q init,1 l q 0 a b . . . (b) A control
{(q 0 x 1 , t 2 , q 0 x 1 ,t 2 ,1 ), (q 0 x 1 ,t 2 ,1 , x 1 , q 0 x 1 ,t 2 ,2 ), (q 0 x 1 ,t 2 ,2 , x 1 , q 0 x 1 ,t 2 ,3 ), (q 0 x 1 ,t 2 ,1 , L, q 1

x 2 )} {(l q 0 , t 2 , q 0 t 2 ,1 ), (q 0 t 2 ,1 , b, q 0 t 2 ,2 ), (q 0 t 2 ,2 , a, q 0 t 2 ,3 ), (q 0 t 2 ,3 , L, l q 1 )} It is quite intuitive to see that the homomorphism will map (q 0 x 3 ,t 2 ,1 , x 3 , q 0 x 3 ,t 2 ,2 ) into (q 0 t 2 ,1 , b, q 0 t 2 ,2 ). This is possible only if the value of the instance of x 3 is equal to b. Then, by definition, x 3 is freed in q x 3 ,t 2 ,2 . This lead to a brand new instance of x 3 which is immediately associated to a (otherwise simulation fails). Figure 5.8 illustrates universal structure on the running example for the state q 0 . q 0 x 1 q 0

x 1 ,t 1 ,1 q 0

x 1 ,t 1 ,2 q 0 x 1 ,t 1 ,3 q 0 x 1 ,t 2 ,1 q 0 x 1 ,t 2 ,2 q 0 x 1 ,t 2 ,3 • Existential states The construction focuses on choosing which transitions must be checked out. Since the decomposition of the transition is similar than for universal states once the choice is done, we will focus on the two first transitions. For example, let consider the transitions of q 1 with the head on the second letter. We have t 1 for (q 1 , b/aL, q 0 ) and t 2 for (q 1 , b/bL, q 0 ) then they will be respectively in A test and A control encoded as :

q 1 x 2 q 2 x 2 t 1 x 1 x 1 R t 2 x 1 x 1 R . . . . . . (a) A test l q 0 q 0 t 1 ,1 q 0 t 1 ,2 q 0 t 1 ,3 q 0 t 2 ,1 q 0 t 2 ,2 q 0 t 2 ,3 l q 1 l q 2
{(l 1 q , t 2 , q 1 t 2 ,0 ), (q 1 t 2 ,0 , t 2 , q 1 t 2 ,1 ), (q 1 t 2 ,0 , t 1 , univ)...} {(q 1 x 2 , t 2 , q 1 x 2 ,t 2 ,0 ), (q 1 x 2 ,t 2 ,0 , choice, q 1 x 2 ,t 2 ,1 )...} and {(l 1 q , t 2 , q 1 t 1 ,0 ), (q 1 t 1 ,0 , t 1 , q 1 t 1 ,1 ), (q 1 t 1 ,0 , t 2 , univ)...} {(q 1

x 2 , t 2 , q 1 x 2 ,t 1 ,0 ), (q 1 x 2 ,t 1 ,0 , choice, q 1 x 2 ,t 1 ,1 )...} Since choice is refreshed by (q 1

x 2 ), any configuration involving this state will always deal with a brand new (free) instance. Any outgoing transitions will then synchronize choice value. It means that a choice can be made but it will be synchronized in both paths. Let assume choice = t 1 , then if there is an homomorphism, it will map q 1

x 2 ,t 1 ,1 into q 1 t 1 ,1 and map q 1 x 2 ,t 2 ,1 into univ. Figure 5.9 illustrates universal structure on the running example for the state q 1 q 1 x2 q 1 x2,t1,0 q 1 x2,t1,1 q 1 x2,t1,2 q 1 x2,t1,3 q 1 t1,0 q 1 t1,1 q 1 t1,2 q 1 t1,3 q 1 t2,0 q 1 t2,1 q 1 t2,2 q 1 t2,3 l q 0 univ t 1 Given an alternating turing machine M an input word w, we construct A control and A test as explained previously denoted as the description automata associated to M and w. The next lemma shows the connection between the existence of infinite execution of the machine M over the word w and the test of simulation between A test and A control . Theorem 3. Let M be an alternating Turing machine working in space bounded by the size of an input word w, and let A control and A test the description automata associated to M and w. Then, M has an infinite computation on w if and only if A test ≪ ∀ A control .

q 1 x2,t2,0 q 1 x2,t2,1 q 1 x2,t2,2 q 1 x2,t2
Proof. The initializing phase will enforce each letter w i on the corresponding variable x i leading to the matching pconf ((q 0

x 1 , → 0 ), l q 0 , {(x, i) = w i ∀i ∈ [1, n]}).

Complexity Analysis

If l q 0 is a universal state then there is only one possibility that maps the edge labeled t j of A test into the edge labeled t j of A control . If it returns false it means that there is no homomorphism for at least one edge which corresponds to M halting.

If l q 0 is an existential state then choice is free. Resulting in choice mapped into t j with j ∈ [1, nt(l q 0 )]. Then any transitions that does not correspond to choice will fulfils simulation requirements thanks to the universal state. The remaining transition will then be checked by processing the same transition in A control . If none of choice possibilities works, then all transitions failed which corresponds to M halting.

Finally, states without outgoing edges in M automatically produces a fail since it has an outgoing edge in A test but not in A control which also corresponds to M halting.

Consequently, if A test ≪ ∀ A control it means that M as an infinite run on the input word w.

Constructing A control requires only polynomial transformation M . The number of states induced is :

|Q| + 3 * {q∈Q|mode(q)=∀} nt(q) + 4 * {q∈Q|mode(q)=∃} nt(q) + 1 + n

The same can be done for transitions which gives : (4 * {q∈Q|mode(q)=∀} nt(q) + {q∈Q|mode(q)=∃} nt(q)(4 + nt(q))) + n + |L| It is immediate to see that the construction of A control is polynomial in the size of M and w.

The same can be done for A test which bears the same difference for universal and existential since the structure are similar. The number of states induced is : n * (|Q| + 3 * {q∈Q|mode(q)=∀} nt(q) + 4 * {q∈Q|mode(q)=∃} nt(q)) + n Regarding the number of transition, we have : n * ( {q∈Q|nt(q)=0} 1 + 4 * {q∈Q|mode(q)=∀} nt(q) + 5 * {q∈Q|mode(q)=∃} nt(q)) + n It is clear to see that the construction of A test is also polynomial in the size of M and w.

Corollary 3. Deciding if a matching problem in EL RV has a solution is exptime-hard.

Upper Bound : Size of the Search Space

The exptime upper bound lies in the number of different pconf explored. In other words, by the size of the space of search considered by the Algorithm Check Simu. In order to demonstrate its exponentially, we define three factors :

• n : the number of states (i.e. the maximum in both automata)

• v : the number of variables • D : the domain of valuation of variables.

The algorithm explores a space made of pconf s which concerns two states forming a basis of n * n pconf s. Two pconf s sharing the same states are seen different by the algorithm up to the current value assignments. Luckily, we only need to consider a finite number of possibilities thanks to relevant variables. It amounts to D v possibilities for variables of A Q . there is no additional requirements for variables of A P since valuation for these variables are a consequence of edge mappings from A Q to A P . We then have a total of n 2 * D V different pconf s. It can be rewritten in e 2 ln(n)+v ln(D) giving exponentially. As matching is a special case of pattern containment, it also gives a tight upper bound for this problem.

Conclusion of Chapter 5

This chapter presents the algorithm Check Simu which demonstrates that pattern containment in EL RV is decidable. Its main idea is to extend Check Match by running synchronously the two automata A Q and A P . It leads to consider extended product configuration where both sides may contain variables transitions. As a consequence, we introduce the notion of constraints and set of constraints. The run of the algorithm is done regarding a global set of constraints to ensure synchronism.

For an epconf only specific variables and thus constraints are relevant regarding the counters. The extended cover, epcover, exploits this information to define a relationship which is independent of the counter. This extended notion led to demonstrate that the algorithm is correct. Changes required to adapt the algorithm to handle weak-subsumption are presented.

This chapter also emphasizes on the complexity analysis of the different reasoning tasks of EL RV . The upper bound is given by the space of search which is exponential w.r.t the entries. Moreover, halting problem working on a space polynomially bounded by the size of the input of alternating turing machine can be reduced to matching problem. Alternating turing machines have three key points, initialization, exponential states and universal states where each of them corresponds to a specific structure with description automata. Since this problem is known to be exptime-complete, we can infer, with the upper bound, that matching is exptime-complete. Moreover, matching is a subproblem of both, weak-subsumption and pattern containment leading to both of them being exptime-complete.

Conclusion

Our work explores reasoning with variables in description logics by introducing refreshing semantics. This semantics is characterized by the possibility to give a new assignment after releasing a variable's bound where the classic semantics does not offer any way to release a bound. The first contribution consists in introducing this semantics for EL which resulted in the definition of EL RV , a logic coping with refreshing role variables using EL-constructors. Pattern instances augment reasoning possibilities of EL RV . These instances have been demonstrated to be either regular or irregular. In the case, two regular instances have a subsumption relationship in EL RV , it implies a subsumption relation w.r.t to the greatest fix-points semantics in EL. Thanks to this newly possible substitutions, reasoning in EL RV can go further than reasoning in EL. Indeed, problems without solution may find a meaningful solution thanks to the refreshing semantics. We respectively extend matching and unification into matching and weak-subsumption in EL RV . In addition, we introduce a third reasoning task, namely pattern containment, which allow to compare two queries whatever the considered terminology.

In order to address these problems in EL RV and to handle the potentially infinite instances, description automata have been defined. This class of automata can handle refreshing semantics for variables and allow to represent a pattern. Reasoning in EL RV can be reduced to variants of simulation between description automata. Pattern containment used the notion of universal simulation while weak-subsumption exploits existential simulation. Matching can be characterized by both of them since it is a sub-problem of both, weak-subsumption and pattern containment. Matching then acts as a lower bound for the three problems allowing to prove that they are optimal. The main results following: matching, weak-subsumption and pattern containment are exptime-complete.

Works conducted in this thesis offer multiple research perspectives. Firstly, we considered only role variables however it would be interesting to consider concept variables. The main challenge comes from the fact that even for matching, the domain of valuation is infinite. Indeed, a concept variable may stand for any concept description. Current solutions do not handle such possibilities. In order to cope with concept variables, one interesting research direction would be to investigate a model that use refreshing role variables to simulate concept variables.

A result of this thesis puts in evidence the link between subsumption in EL RV and subsumption in EL with regard to the greatest fix-point semantics. It would be interesting to investigate if a link with descriptive semantics could be unraveled.

We presented the wide variety of potential matcher induced by the multiple pattern instances. A very interesting research axis would be to question the quality of a matcher. How to answer the question "What is the best matcher ?". Usually, one chooses the closest concept to the targeted concept. However, in Section 2.2.4, we presented many matchers that are incomparable w.r.t to the subsumption relationship. Closeness of the concept might be the first property but might not suffice in such cases. Additional properties are required to qualify the best solution. For instance, a solution that requires the less number of definitions to be defined would be an interesting track. Note that such a criteria immediately makes regular solution of better quality than irregular ones. To go further, extending these results to more expressive logics based on EL such as ALE would be interesting.

Finally, a more consequent research axis would be to study another logic that offers both low complexity and interesting possibilities : FL 0 . This logic has been widely studied in presence of non-refreshing variables. Like EL, FL 0 subsumption can be characterized with automata theory. However, it is reduced to language inclusion instead of simulation. Description automata can be extended to FL 0 but it remains to question language inclusion in order to exploit this link. Once again, it would be valuable to question regular and irregular matchers as well as decidability of reasoning in this framework.

2. 1

 1 Infinite Tree of the Unfolded Pattern Q 1 of Example 11. . . . . . . . . . .

. 2 :

 2 Syntax and semantics of EL constructors We say that two concepts C, D are equivalent, and write C ≡ D, if C I = D I for all interpretations I. A concept C is less general than a concept D, noted, C ⊑ D if C I ⊆ D I . This relation is called the subsumption relationship. As expected, if C ⊑ D and D ⊑ C then we have C ≡ D.

  niversity, Country, P aris} • N R = {teach, locate, study, hasCapital} • N def = {F renchU niversity, Student, T eacher, F rance} An interpretation I is a model of T if and only if for all definitions A ≡ C ∈ T we have P I = C I . We say that C is subsumed by D w.r.t. T , written C ⊑ T D, iff C I ⊆ D I holds for every model I of T .

Example 6 .

 6 Example 3 displays a TBox that can be qualified as acyclic. However, if we add the following definitions : Doctor ≡ P erson ⊓ ∃getP hDIn.U niversity ⊓ ∃f ormerly.P hDStudent P hDStudent ≡ Student ⊓ ∃supervisedBy.Doctor Doctor appears in the definition of P hDStudent and P hDStudent appears in the definition of Doctor. Therefore, these definitions creates an indirect cycle. Thus illustrating cyclic TBoxes.

Figure 2 .

 2 1 depicts the tree representation of the unfolded pattern Q 1 of Example 11. Each node is labeled by the corresponding concept in the TBox. Leaves are labeled by q f and have an incoming edge labeled by an atomic concept name.

Figure 2 . 3 :

 23 Figure 2.3: Irregular Instance of the Pattern P .

→I.

  In the sequel, we use the following notations. Let → G ∈ N |Var| be a tuple of integer. → G is called a counter and is used to associate an integer value with each variable in Var. More precisely, we assume that each variable x ∈ Var is associated with a fixed position in → G, noted G x , which gives the value of the counter of x in →

Figure 3 . 2 :

 32 Figure 3.2: A Configuration Tree of the Automaton A Q 2 .

Figure 3 . 3 :

 33 Figure 3.3: Schematical relationships between representations

  b and a ̸ = b with a and b two constants.

Example 18 .

 18

Figure 4 .

 4 1 explores two possibilities accessible from the mapping M ε 2 based on the mappings produced by the nodes 0 and 1.

Figure 4 . 1 :

 41 Figure 4.1: Fragment Execution Trees of Check Match

Figure 4 . 2 :

 42 Figure 4.2: Partial Configuration Trees Extracted from Exec A Q ,A C

Figure 4 . 3 :

 43 Figure 4.3: Witness of C ⊑ ? Q 2

5. 2 From

 2 Matching to Pattern Containment Chapter 5 Solving Pattern Containment (i) A variable into a constant, (ii) A constant into a constant and, (iii) A variable into a variable.

Figure 5 . 1 :

 51 Figure 5.1: Description Automata of Respectively Q, P 1 and P ′ 1 .

pc 1 =Property 6 . 1 ,Figure 5 . 3 :

 16153 Figure 5.3: Partial Configuration trees extracted from Exec A Q ,A P 1

Figures 5 .

 5 Figures 5.4 depict respectively the EL RV -description automata of the EL RV -patterns P and Q. The refreshing state of both x and z is the state P (i.e., κ(x) = κ(z) = {P }) while the refreshing state of y is the state Q (i.e., κ(y) = {Q}).

Figure 5 . 4 :

 54 Figure 5.4: Automata of Example 27

Figure 5 . 5 :

 55 Figure 5.5: Potential Execution Tree to solve A Q ≪ ∃ A P

Figure 5 . 6 :

 56 Figure 5.6: Example of Alternating Turing Machine

-

  {t j } with j ∈ [1, m], the symbols representing the transitions of M and m = max({nt(q)|q ∈ Q}) the maximal number of transitions among states of M -{w i } the letters of the input w with i ∈ [1, |w| = n] -Γ ∪ {L, R}, the symbols used in M reject a specific symbol only used by the state univ • Var control = ∅ • The set of states Q control is composed of :

Figure 5 . 7 :

 57 Figure 5.7: Example of Initialization for the Input Word ab

Figure 5 . 8 :

 58 Figure 5.8: Example of Universal Construction Corresponding to q 0

(a) A test l q 1

 1

Figure 5 . 9 :

 59 Figure 5.9: Example of Existential Construction Corresponding to q 1

Lemma 9 .

 9 Deciding if a pattern containment problem in EL RV has a solution is in exptime. This result coupled with Corollary 3 immediately implies the following theorem : Theorem 4. Deciding if a pattern containment problem in EL RV has a solution is exptime-complete.

Corollary 4 .

 4 Deciding if a matching problem in EL RV has a solution is exptime-complete.

  Note that any equality axiom can be transformed into two inclusion axioms. For example F renchU niversity ≡ ∃locate.F rance ⊓ U niversity would become {F renchU niversity ⊑ ∃locate.F rance ⊓ U niversity, ∃locate.F rance ⊓ U niversity ⊑ F renchU niversity}. In order to deal with a unique kind of axiom, this transformation is handful.

Example 3. The following definitions form a simple TBox T . F rance ≡ Country ⊓ ∃hasCapital.P aris F renchU niversity ≡ ∃locate.F rance ⊓ U niversity Student ≡ ∃study.U niversity ⊓ P erson T eacher ≡ ∃teach.U niversity ⊓ P erson • General concept inclusion (GCI) TBoxes : TBoxes of this class are made of a set of axioms without any restriction. Example 4. Let us consider the CGI made of the following definition : F renchU niversity ≡ ∃locate.F rance ⊓ U niversity T eacher ⊑ ∃teach.U niversity ⊓ P erson F emale ⊓ ∃study.U niversity ⊑ ∃study.U niversity ⊓ P erson

  .1

	2.1 TBoxes with Variables
	2.1.1 Introduction
	Symbol Description
	V	Set of variables
	N R X	Set of role variables
	N T	Set of role variables and primitive roles
	N C X	Set of concept variables
	N V R	Set of refreshing variables
	N V N	Set of non-refreshing variables
	P	Pattern
	u(P )	Unfolded pattern
	σ(P )	Unfolded pattern instance
	P ⊑ ? T D Matching problem w.r.t T P ⊏ ∼ ? T Q Weak-subsumption problem w.r.t T P ⊑ ? Q Pattern containment problem
	Table 2.1: Notations introduced in Chapter 2

  • A matching problem modulo equivalence w.r.t. a TBox T is an equation of the form C ≡ ? T P . It has a solution if there exists a substitution σ such that C ≡ T σ(P ) • A matching problem modulo subsumption w.r.t. a TBox T is an equation of the form C ⊑ ? T P . It has a solution if there exists a substitution σ such that C ⊑ T σ(P )

  Refreshing semantics increases substitution possibilities with, in particular, θ such that the resulting concept θ(Academic) is a matcher : Doctor ≡ P erson ⊓ ∃getP hDIn.U niv ⊓ ∃f ormerly.( P erson ⊓ ∃studyIn.U niv ⊓ ∃supervisedBy.(. . .)) ⊑ gf p,T θ(Academic) ≡ P erson ⊓ ∃ getP hdIn

niversity ⊓ ∃y.Academic with x, y two role variables.

The matching problem Doctor ⊑ ? gf p,T Academic does not have any solution from a state of the art point of view. θ(x)

  .1 summarizes notations introduced in this chapter.

	Symbol Description
	A P	Description automata corresponding to the pattern P
	Q	Set of states of A P
	L		Set of edges labels of A P
	Var	Set of variables of A P
	q 0		Initial state of A P
	q f		Final state of A P
	δ		Transition function of A P
	κ		Refreshing function of A P
	→
	(q p ,	I )	Configuration of a description automata
	T (A P , σ) Configuration tree of A P w.r.t σ
	≪ ∀	Universal simulation
	≪ ∃	Existential simulation
			Table 3.1: Notations introduced in Chapter 3

Acknowledgements

Chapter 4 Solving Matching

The algorithm stops the exploration of a branch and return true when it reaches a product configuration pc ′ = ((q ′ , → J ), c ′ , S ′ Q ) where q ′ is a leaf of T (A Q , σ) or when pc covers another product configuration already explored in the historic Hist of the actual branch (Algorithm 1 Line 1).

In order to show correctness of the algorithm we need to define the execution tree of Check Match. The next section will explain step by step how it is obtained before giving its formal definition.

Product Execution Tree of Check Match

The algorithm Check Match starts with the initial pconf 0 = ((Q, → 0 ), C, S 0 = ∅). In order to construct a witness σ, the algorithm can non-deterministically choose a mapping of the set M q →c to explore ( Algorithm 1 Line 5).

Example 16. In Figure 4.1, the algorithm starts at the initial product configuration pconf 0 = ((Q 2 , (0, 0)), C, ∅) and tries to construct a witness σ. There are two outgoing transitions from the configuration (Q 2 , (0, 0)):

There are three outgoing transitions from (C):

Consequently, the set of mappings M Q 2 →C includes all the possible mappings from Each choice leads to consider a different product execution tree. Nonetheless, the algorithm then constructs children pc ′ i issued of the chosen mapping ( Algorithm 1 Line 12). Check Match then makes a recursive call using the resulting children ( Algorithm 1 Line 14). This recursive call tries to complete the witness σ for the reached children. There are three possibilities for a child :

• A child fulfills cover criteria.

• A child fails to produce a consistent mapping.

• A child makes a non-deterministic choice.

Example 17. In Figure 4.1, the two mappings are represented for pconf 0 , each of them leading to specific execution trees.

Product Execution Tree of Check Simu

The algorithm Check Simu starts with the initial epconf 0 = ((Q, → 0 ), (P 1 , → 0 )). Possible mappings are generated and stored in the set M Q →P 1 ( Algorithm 2 Line 3). One mapping is selected non-determinstically and the satisfiability of the corresponding constraints is verified (Algorithm 2 Line 9).

Example 25. In Figure 5.2, the algorithm starts at the initial product configuration epconf 0 = ((Q, (0, 0, 0)), (P 1 , (0))) with an empty set of constraints. There are three outgoing transitions from the configuration (Q, (0, 0, 0)):

There are two outgoing transitions from (P 1 , (0)):

Consequently, the set of mappings M Q →P 1 includes all the possible mappings from

In the figure, choices made by the algorithm are symbolized by the ∨ nodes. The left side corresponds to M ε 1 and the right side to M ϵ 2 . In both cases, the set of constraints generated is the same, i.e. {(x, 0) = R, (y, 0) = R, (z, 0) = R}. The corresponding quantified constraint formula, ∃(x, 0), (y, 0), (z, 0), (((x, 0

Each choice leads to consider a different product execution tree. Nonetheless, the algorithm then constructs children pc ′ i issued of the chosen mapping. ( Algorithm 2 Line 14). Check Simu then makes a recursive call using the resulting children ( Algorithm 2 Line 16). There are three possibilities for a child :

• It concerns a leaf or satisfies cover criteria.

• It fails to produce a satisfiable mapping.

• It chooses non-deterministically a mapping.

Example 26. In Figure 5.2, each mapping leads to its specific execution trees. For the mapping M ε 1 , the reached children 0, 1 and 2 are respectively labeled by ((Q, (0, 1, 1)), (P 3 , (0))), ((N A 2 , (0, 0, 0)), (P 2 , (1))) and ((N A 1 , (0, 0, 0)), (P 2 , (1))). For those three nodes there are no mappings possible since variables can not be substituted by element of the set N A . The set of mappings is then empty therefore the algorithm returns false (symbolized by the cross in the figure). We will now look toward M ε 2 which produces a tree such that λ(0) = ((Q, (0, 1, 1)), (P 2 , (1)))

λ(1) = ((N A 2 , (0, 0, 0)), (P 3 , (0))) λ(2) = ((N A 1 , (0, 0, 0)), (P 3 , (0)))

The involved states are not leaves and cover criteria is not satisfied. The the set of mappings which is not empty is computed. Thus the algorithm continues its execution. Note that for the nodes 1 and 2, there is only one successful mapping so we will not discuss this part. Regarding, the node 0, Figure 5.2 depicts two possible mappings. There are three outgoing transitions from the configuration (Q, (0, 1, 1)):

t 1 = ((Q, (0, 1, 1)), (x, 0), (N A 1 , (0, 1, 1))) t 2 = ((Q, (0, 1, 1)), (y, 1), (N A 2 , (0, 1, 1))) t 3 = ((Q, (0, 1, 1)), (z, 1), (Q, (0, 2, 2)))

There are three outgoing transitions from (P 2 , (1)): On the left side, we depict the mapping

However, the quantified constraint formula, ∀(w, 1), ∃(x, 0), (y, 0), (y, 1), (z, 0), (z, 1)(((x, 0) = R) ∧ ((y, 0) = R) ∧ (z, 0 = R) ∧ ((y, 1) = (w, 1) ∧ ((x, 0) = (w, 1))) is not satisfiable. Indeed, it contains (((x, 0) = R) ∧ ((x, 0) = (w, 1))) which infers ∀(w, 1), ((w, 1) = R). On the other hand, the mapping

} is successful and leads to new children which will makes a recursive call until the cover criteria is verified, a leaf is reached or it fails. In the figure, this criteria is verified for 0 and 000 since we have λ(0) ◁ C λ(000) which is reached after one more step.

The notion of product execution tree of Check Simu will then be formally defined with regard to a mapping that generates a set of constraints : C M . This mapping is a union of mappings corresponding to the recursive choices the algorithm makes.

Definition 23 (Product execution tree of Check Simu w.r.t to M).

be counters. Let S be the set of all possible epconf and let L be L P ∪ Var P × N. A run of Check Simu, denoted Exec A Q ,A P and called a product execution tree, is a ⟨S, L⟩-labeled tree (τ, λ, δ) constructed as follows:

• λ(ϵ) = ((q 0 , → 0 ), (p 0 , → 0 ), a root of the tree, and let

, a global counter initialized to a vector of zero.

• Let n ∈ τ be a node such that λ(n) = ((q q , → I ), (q p , → J )). For each m i in (((q q , → I ), t q , (q ′ q , → I ′ )), ((q p , → J ), t p , (q ′ p , → J ′ ))) ∈ M ,a new child ni of n is generated according to the following sequence:

(iv) ∀y ∈ Var P , if q ′ p ∈ κ(y) then G P y := G P y + 1, and

The tree of the Figure 5.2 shows execution trees of A Q ≪ ∀ A P . Note that transitions labeled with (x, i) = t p , instead of t p as stated in the definition, are here to illustrate bounding of variable during the execution. Everything required to prove correctness of the algorithm is now defined. The next section will then detail correctness of Check Simu.

(NA 2 , (0, 0, 0), P2,

(Q, (0, 0, 0), P1, (0))

(NA 2 , (0, 0, 0), P3, (0))

(NA 2 , (0, 0, 0), P3, (0)) (qf , (0, 0, 0), qf