=Paper=
{{Paper
|id=Vol-1350/paper-42
|storemode=property
|title=Reasoning
in description logics with variables: preliminary results
regarding the EL logic
|pdfUrl=https://ceur-ws.org/Vol-1350/paper-42.pdf
|volume=Vol-1350
|dblpUrl=https://dblp.org/rec/conf/dlog/AkrounNT15
}}
==Reasoning
in description logics with variables: preliminary results
regarding the EL logic==
https://ceur-ws.org/Vol-1350/paper-42.pdf
Reasoning in description logics with variables:
preliminary results regarding the EL logic
Lakhdar Akroun, Lhouari Nourine, and Farouk Toumani
1
INRIA, Grenoble, France
lakhdar.akroun@inria.fr
2
LIMOS, CNRS, Blaise Pascal University, Clermont-Ferrand, France
nourine, ftoumani@isima.fr
Abstract. This paper studies the extension of description logics with
variables ranging over infinite domains of concept names and role names.
As a preliminary work, we consider more specifically the extension of the
logic EL with variables and we investigate in this context two reason-
ing mechanisms, namely compliance (a kind of matching) and pattern
containment. The main technical results are derived by establishing a
correspondance between the EL logic and finite variable automata.
1 Introduction
We consider description logics augmented with variables ranged over concept
names and role names. As an example, consider the following description:
B ≡ P erson u ∃works-f or.X u ∃graduated-f rom.X (1)
where the variable X takes its values from an infinite set of possible atomic
concept names. B specifies the set of persons that work for the same type of
organization they were graduated from. Specifications of type (1) are called
hereafter a pattern definition and B is called a pattern name (or simply a pat-
tern). An instanciation of a pattern is given by variable valuations. For example,
if the variable X is assigned as value the atomic concept name University (re-
spectively, eSchool ), we obtain the following description B1 (respectively, B2 )
which is compliant with the pattern B:
B1 ≡ P erson u ∃works-f or.U niversity u ∃graduated-f rom.U niversity
B2 ≡ P erson u ∃works-f or.eSchool u ∃graduated-f rom.eSchool
Variables can also be used in role places as illustrated by the following pattern
definition:
B3 ≡ P erson u ∃Y.Z u ∃.graduated-f rom.Z
The concept B3 specifies the set of persons that have a relation (i.e., any kind of
role) with the same type of organization they are graduated from. Indeed, the
concept B1 is compliant with B3 and it is also the case of the concept B4 defined
as follows:
B4 ≡ P erson u ∃evaluates.eSchool u ∃graduated-f rom.eSchool
Our framework supports terminological cycles as illustrated below with the pat-
tern B5 which specifies the persons that work for the same type of organization
they are graduated from and have a relative who also work for the same type of
organization she is graduated from.
B5 ≡ P erson u ∃works-f or.X 0 u ∃graduated-f rom.X 0 u ∃has-relative.B5
For a description logic L, we denote by LV the obtained logic augmented with
concept variables and role variables. We study the following reasoning mecha-
nisms in this framework (formal definitions are given later in the paper):
– Compliance which asks whether a description E is compliant with a pattern
C.
– Pattern containment which, given two pattern definitions C1 and C2 , asks
whether every description E compliant with C1 is also compliant with C2 .
Indeed, the notion of a concept pattern (i.e., a concept description containing
variables) is not new and has already been used, in particular, in the context of
two non-standard reasonings, namely matching [1] and unification [2,4]. Given
a concept pattern D and a concept description C, the matching problem asks
whether there is a substitution σ of the variables by concept descriptions such
that C v σ(D). Unification is a generalization of matching. It takes as input
concept patterns and asks whether there exist a substitution of the variables by
concept descriptions that makes the concept patterns equivalent. Our definition
of concept patterns deviate from the one used in the literature with respect to
the following features: (i) our definition of concept patterns is more liberal in the
sense that we allow concept variables as well as role variables while usually only
concept variables are allowed in concept patterns, (ii) we support cyclic pattern
definitions and, inspired from the guarded variable automata theory, we consider
two different types of semantics of variables (i.e., refreshing and not refreshing
semantics), and (iii) our interpretation of variables is however more restrictive in
this paper since we consider only atomic variables (i.e., we assume that variables
take their values from an infinite set of atomic concept names and role names).
An extension of this framework to variables that stand for descriptions would be
an interesting research direction. From the reasoning perspective, our notion of
compliance coincides with matching however, up to our knowledge, the notion
of pattern containment has never been investigated in the literature.
We expect the proposed framework to be useful in various applications. For
example, concept patterns have already been proven to be beneficial in applica-
tions where a given user is interested ‘to search the knowledge base for concepts
having a certain not completely specified form’ [6]. Targeting a similar purpose,
we envision our framework to be useful as query language to: (i) formulate queries
over terminologies. For example, the concept B3 given above can be viewed as
a query over a given terminology while the concepts B1 and B2 are examples
of answers to such a query, or (ii) to formulate ontological queries (i.e., queries
over an ontology) in the context of an Ontology Based Data Access (OBDA)
approach [7]. The reasoning mechanisms studied in this paper can prove partic-
ularly relevant to handle query evaluation and optimisation in such contexts.
Organization of the paper. Section 2 presents some preliminary notions regarding
state machines and guarded variable automata. Section 3 recalls some basic
notions of the EL description logic and describes the extension of this logic with
variables, the obtained logic is called ELV . Section 4 studies the compliance and
the containment problems in the context of the ELV logic. We conclude and
draw future research directions in section 5. Proofs are omitted and are included
in the extended version of this paper [13].
2 Preliminaries
We first recall the notion of state machines [9] and simulation preorder between
state machines. A State Machine M is a tuple < ΣM , QM , FM , Q0M , δM >, where:
ΣM is a finite alphabet, QM is a set of states with Q0M ⊆ QM the set of initial
states and FM ⊆ QM the set of final states, δM ⊆ QM × ΣM × QM is a set
of labeled transitions. If QM is finite then M is called a finite state machine. If
q ∈ Q0M is an initial state of a machine M , we say that M is rooted at q.
Let M =< ΣM , QM , FM , Q0M , δM > and M 0 =< ΣM 0 , QM 0 , FM 0 , Q0M 0 , δM 0 >
be two (eventually, infinite) state machines. A state q1 ∈ QM is simulated by a
state q10 ∈ QM 0 , noted q1 q10 , iff the following two conditions hold : (i) ∀a ∈ ΣM
and ∀q2 ∈ QM such that (q1 , a, q2 ) ∈ δM , there exists (q10 , a, q20 ) ∈ δM 0 such that
q2 q20 , and (ii) if q1 ∈ FM , then q10 ∈ FM 0 . M is simulated by M 0 , noted
M M 0 , iff ∀qM ∈ Q0M , ∃qM 0 0
0 ∈ QM 0 s.t. qM qM 0 .
We briefly introduce now the notion of (Guarded) Variable Automata [5].
Let X be a finite set of variables and Σ an infinite alphabet of letters. The set
G of guards is inductively defined as follows: G := true | α = β | α 6= β | G ∧ G
where α, β ∈ Σ ∪ X . A GVA is a tuple A = (Σ, X , Q, Q0 , δ, F, µ), where Σ is
an infinite set of letters, X is a finite set of variables, Q is a finite set states,
Q0 ⊆ Q is a finite set of initial states, δ : Q × (ΣA ∪ X ) × G → 2Q is a transition
function where ΣA ⊂ Σ is a finite set of alphabet, F ⊆ Q is a finite set of final
states and µ : X → 2Q is called the refreshing function.
In the sequel, we write (q, t, g, q 0 ) to denote a transition from q to q 0 , when
0
q ∈ δ((q, t, g)). At every point in time, a run of a GVA A is determined by its
instantaneous description (or simply, configuration). A configuration of a GVA
A is given by a pair id = (q, σ) where q ∈ Q is a state in A and σ : X → Σ is a
variable valuation. A valuation σ is extended to be the identity over the elements
of Σ. The satisfaction of a guard g by a valuation σ, denoted σi |= g, is defined
as usual. A run of A starts at an initial configuration id0 = (q0 , σ0 ), with q0 ∈ Q0
an initial control state of A and σ0 an arbitrary valuation of the variables of X 3 .
Then A moves from a configuration idi = (qi , σi ) to a configuration idj = (qj , σj )
over the letter σi (t) if there is a transition (qi , t, g, qj ) ∈ δ s.t. σi |= g and
σi (x) = σj (x), ∀x ∈ X \ µ(qj ) (i.e., σi and σj coincide on the values of the
variables that are not refreshed at the state qj ). Hence, given a GVA A, the runs
of a A is captured by an infinite state machine called the extended machine of
A and denoted E(A). Roughly speaking, E(A) is made of all the configurations
of A and all the transitions between these configurations. Simulation between
two guarded automata A and B, noted A B, is defined as simulation between
their associated state machines, i.e., A B iff E(A) E(B).
3 Description logic with variables
Let NA and NR be respectively two disjoint and potentially infinite sets of atomic
concept names and role names and let L be a description logic. Let NC be an
infinite set of concept names including the atomic concept names (i.e., NA ⊆
NC ). Concept descriptions specified in the logic L (or L-descriptions) are built
from concept names NC and role names NR using the constructors of L. The
semantics of L-descriptions is defined as usual. Let NCT ⊂ NC and NRT ⊂ NR be
respectively two finite sets of concept names and role names. An L-terminology
T over the set of concept names NCT and the set of role names NRT is a set of
concept definitions of the form A ≡ D, where A ∈ NCT is a concept name and D
is an L-description. Atomic concept names (i.e., elements of NA ) are prohibited
from appearing in a left-hand side of a definition while the the concept names
occurring of NCT \ NA , called defined concepts, must appear at the left-hand
side of a definition. We assume that a terminology does not contain multiple
definitions and we allow cyclic definitions. In this paper, we study reasoning in
the context of a gfp-semantics [3].
Introducing variables. Let NA , NR and NC defined as previously. For a
description logic L, we note by LV the corresponding description logic augmented
with variables. To define the logic LV , we extend the sets of concept names and
roles names with variables. Let Ncv and Nrv be respectively the sets of concept
and role variables. The sets Ncv , Nrv and NR ∪ NC are pairwise disjoints. In
the sequel, we use the letters X, Y, . . . to denote variables. An LV -terminology
is defined over the set of concept terms NCT ⊂ NC ∪ Ncv and role terms NRT ⊂
NR ∪Nrv . Hence, LV -patterns (or simply patterns), are built from concept terms
NCT and role terms NRT using the L-constructors. Therefore, an LV -terminology
is a set of pattern definitions of the form C ≡ D, where C ∈ NCT \ (NA ∪ Ncv ) is
a concept name and D is an LV -description. We allow indeed cyclic definitions
in LV -terminologies.
3
Note that we adopt a slight different vision of configurations than [5] who considers,
for example, a unique initial configuration id0 = (q0 , ∅).
Pattern valuation. Concept (respectively, role) variables take their values from
the infinite set of atomic concept names (respectively, role names). This is
captured by the notion of valuation. A variable valuation is a mapping σ :
Ncv ∪ Nrv → NA ∪ NR which maps concept variables into atomic concepts and
role variables into role names. We denote by Val the infinite set of all such
possible valuations. Valuations are straightforwardly extended to LV -patterns
by considering that a valuation is the identity on elements of NC ∪ NR . Con-
tinuing with the example of section 1, and taking a valuation σ1 such that
σ1 (X) = U niversity, σ1 (Y ) = works-f or and σ1 (Z) = U niversity we obtain
σ1 (B) ≡ B1 and σ1 (B3 ) ≡ B1 . If we consider now a valuation σ2 such that
σ2 (X) = σ2 (Z) = eSchool and σ2 (Y ) = evaluates we obtain σ2 (B) ≡ B2 and
σ2 (B3 ) ≡ B4 . Hence, for an LV -pattern C, σ(C) is an L-description. As a conse-
quence, an LV -pattern C describes a (potentially infinite) set of L-descriptions
(corresponding to the potentially infinite number of possible valuations). We
extend the notion of valuation to LV -teminologies as follows: given an LV -
terminology T and a variable valuation σ, we denote by σ(T ) the terminology
made of the definitions of the form A ≡ σ(D) such that A ≡ D is a pattern
definition in T . Therefore, an LV -terminology T specifies an (infinite) set of
L-terminologies σ(T ), ∀σ ∈ Val.
Variants of variable semantics. Several possibilities exist to define the seman-
tics of variables depending on the restrictions imposed on variable valuations.
We borrow the notion of non-deterministic reassignment of variables from vari-
able automata semantics [10,8,5], to define in this paper two classes of variable
semantics: refreshing vs. non refreshing variable semantics. The demarcation be-
tween these two kinds of semantics lies in the valuation of variables that appear
in the scope of a terminological cycle. A non refreshing semantics requires to
have a unique valuation of such variables while a refreshing semantics enables to
assign different values to the same variable for each unfolding of a cycle. To make
the meaning of each semantics clear, let us consider again the pattern B5 given
at section 1. A one-step unfolding of B5 leads to the following pattern descrip-
tion: P erson u ∃works-f or.X 0 u graduated-f rom.X 0 u ∃has-relative.(P erson u
∃works-f or.X 00 u graduated-f rom.X 00 u ∃has-relative.B5 ). A non-refreshing se-
mantics allows only valuations σ that satisfy σ(X 0 ) = σ(X 00 ) while a refreshing
semantics permits to have different valuations for X 0 and X 00 (i.e., we may have
σ(X 0 ) 6= σ(X 00 )). Indeed, in a non-refreshing semantics, the same variable can be
used for both X 0 and X 00 and hence the number of variables used in a (unfolded)
definition is always finite. The case of refreshing semantics is different since in
this case a cyclic pattern refers (implicitly) to an infinite number of variables. To
keep the number of variables finite, we allow the possibility to refresh the values
of a given variable during the unfolding of a given definition. For example, a valu-
ation of the pattern B5 using the assignment σi leads to the definition: σi (B5 ) ≡
P ersonu∃works-f or.σi (X 0 )ugraduated-f rom.σi (X 0 )u∃has-relative.σi+1 (B5 ).
Hence, the valuation of a LV -pattern C is provided by a (potentially infinite)
sequence of valuations σ0 , . . . , σn , where σ0 is the initial valuation and where each
valuation σi+1 coincides with the valuation σi on the non refreshed variables (i.e.,
σi (X 0 ) = σi+1 (X)0 if X 0 is not refreshed) while σi+1 assigns new values to the
refreshed variables.
We use the following notation to distinguish between these two classes
of semantics: r-semantics denotes refreshing variables semantics (valuations
Valr ) while nr-semantics denotes non refreshing variables semantics (valua-
tions Valnr ). Let t ∈ {r, nr} and C be an LV -pattern. We denote by Dt (C)=
{σ(C) | ∀σ ∈ Valt } the infinite set of L-descriptions obtained from the pattern
C by the valuations of Valt .
Reasoning in description logics with variables. Let T and T 0 two LV -
terminologies. We say that T and T 0 are coherent if NCT ∩ NCT 0 = ∅.
Let t ∈ {r, nr}. Let C and D be two LV -patterns of an LV -terminology T 0
and let E be an L-description of an L-termonilogy T 00 coherent with T 0 . Let T =
T 0 ∪ T 00 . In this paper we are interested by the following reasonings.
– E is compliant with C w.r.t. a t-semantics, noted E 6tT C, iff there exists
a valuation σ ∈ Valt such that E vσ(T ) σ(C) (i.e., E is subsumed by σ(C)
w.r.t. the terminology σ(T )).
– C is contained in D w.r.t. a t-semantics, noted C tT 0 D, iff for every L-
description E of an L-termonilogy T 00 , we have E 6tT C implies E 6tT D
(i.e., every description E which is compliant with C w.r.t. a t-semantics is
also compiant with D w.r.t. a t-semantics),
4 The case of the logic ELV
In this paper, we study reasoning in the context of a gfp-semantics while we
believe that our framework can be extended to descriptive and lfp-semantics as
well. We are interested by classes of description logics in which reasoning w.r.t. a
gfp-semantics can be characterized using a finite state machine (e.g., automata
or graphs ([3,12]).
We provide below a characterization of compliance and pattern containment,
w.r.t. a gfp-semantics, in ELV . We explain briefly how to turn any ELV -pattern
definition C into a variable automata AtC . To achieve this task, we adapt the
EL-normal form proposed in [3] to ELV -patterns. Let T be an ELV -terminology.
An ELV -pattern definition C ≡ D ∈ T is in a normal form if D is of the form
D ≡ V1 u . . . u Vm u ∃W1 .D1 u . . . u ∃Wn .Dn
for m, n ≥ 0 and each Vi is either an atomic concept name or a concept variable
(i.e., Vi ∈ NA ∪ Ncv , for i ∈ [1, m]), and Dj is a defined concept name (i.e.,
Dj ∈ NCT \ (NA ∪ Ncv ), for j ∈ [1, n] and each Wi is a role term (i.e., Ri ∈ NRT
(Ri ). A pattern terminology T is said normalized if all the pattern definitions it
contains are in a normal form. W.o.l.g., we assume that two pattern definitions
in a normalized terminology use disjoint sets of variables. It is worth noting
that, since concept variables do not range over defined concept names, the
normalization process proposed in [3] can be straightforwardly extended to
our context to transform any ELV -terminology into a normalized one. As an
example, a normalized terminology containing the defined concepts of our
running example is given below:
B ≡ P erson u ∃works-f or.D1 u ∃graduated-f rom.D1
B1 ≡ P erson u ∃works-f or.D2 u ∃graduated-f rom.D2
B2 ≡ P erson u ∃works-f or.eSchool u ∃graduated-f rom.eSchool
B4 ≡ P erson u ∃evaluates.D3 u ∃graduated-f rom.D3
B5 ≡ P erson u ∃works-f or.D4 u ∃graduated-f rom.D4 u ∃has-relative.B5
D1 ≡ X
D2 ≡ U niversity
D3 ≡ eSchool
D4 ≡ X 0
Fig. 1. Mapping ELV -pattern definitions into variable automata.
Mapping ELV -patterns into variable automata. Let T be a normalized ELV -
terminology. We explain below how to map defined concepts and patterns of T
into variable automata. Let QT = NCT \ (NA ∪ Ncv ) be a set of states made
of the defined concepts of T . Each concept definition or ELV -pattern C ≡ V1 u
. . . u Vm u ∃W1 .D1 u . . . u ∃Wn .Dn of T is turned into a variable automaton
AtC = (ΣC , XC , QC , Q0 , δ, F, µ) defined as follows:
– the alphabet ΣC ⊆ NA ∪ NR ∪ {T op}, is made of a subset of atomic concept
names, role names and the T op concept,
– the set of variables XC ⊆ Ncv ∪ Nrv , is made of a subset of concept and role
variables,
– the set of states QC ⊆ QT ∪ {C, Sf }, is made of the states of QT reacheable
from the state C,
– Q0 = {C} is the set of initial states of the automaton and F = {Sf } is its
set of final states,
– the transitions are unguarded (i.e., G = ∅). The transition function δ is
defined as follows:
• (q, T op, true, Sf ) ∈ δ, ∀q ∈ QC , i.e., there is an edge labeled T op from
every node q in QC to the final state Sf ,
• (C, Vi , true, Sf ) ∈ δ, ∀i ∈ [1, m], i.e., each term Vi is turned into an edge,
labeled Vi , from the node C to the final state Sf .
• (C, Wi , true, Di ) ∈ δ, ∀i ∈ [1, n], i.e., each term ∃Wi .Di is turned into
an edge, labeled Wi , from the node C to the node Di .
– the refreshing function µ is defined as follows:
• if t = r then µ(x) = QC , ∀x ∈ X
• if t = nr then µ(x) = ∅, ∀x ∈ X
The proposed mapping of a pattern C ≡ V1 u . . . u Vm u ∃W1 .D1 u . . . u ∃Wn .Dn
into an automaton AtC = (ΣC , XC , QC , Q0 , δ, F, µ) is depicted at figure 1(a)
while the figure 1(b) shows the variable automaton AtB5 corresponding to the
pattern B5 of section 1. Figure 2(a) shows E(ArB5 ), the extended automaton
of ArB5 , for the case of a variable refreshing semantics (i.e. t = r). Note that,
Fig. 2. The extended automaton E(AtB5 ).
this machine includes an infinite set of initial states (i.e., the configurations
(B5 , σi ), ∀σi ∈ Valr ). In the case of a refreshing semantics, the cyclic role has-
relative relates a given state (B5 , σi ) to all the other possible states (B5 , σj ),
∀σj ∈ Valr , thereby making each machine rooted at an initial configuration
(B5 , σi ) an infinite state machine. In the case of a non-refreshing semantics (i.e.
t = nr), E(Anr B5 ) is made of an infinite set of, pairwise disconnected, finite state
machines rooted at (B5 , σi ), ∀σi ∈ Valnr (c.f., figure 2(b)). The following lemma
establishes a connection between subsumption in ELV and simulation between
instances of variable automata.
Lemma 1. Let t ∈ {r, nr} and let C and D be two ELV -patterns in a ELV -
terminology T . Let σ ⊆ Valt , then σ(C) vσ(T ) σ(D) iff σ(AtD ) σ(AtC ).
Let T be an EL-terminology T . This lemma is derived from the observation
that the set of all the automata E(AtC ), of the patterns C of T , corresponds
to a slight modification of the notion of EL-description graph [3] of the EL-
terminology σ(T ), where: (i) a set of final states (Sf , σ) with σ ∈ Valt , marked
as a final states, is added to the graph, and (ii) the atomic concepts are turned
into edges from the nodes representing defined concepts to the final states (Sf , σ).
It is clear that such a transformation of a description graph of a terminology T
preserves the simulation relation between the nodes of the initial graph. Hence,
the characterization of subsumption w.r.t. gfp-semantics using the simulation
relation is still valid in our context.
Therefore reasoning over C can be reduced to reasoning over the correspond-
ing variable automata AtC . However, despite the correspondance established
by lemma 1, reduction of compliance and containment to simulation between
variable automata is not straightforward and requires additional transforma-
tions. Consider for example the following pattern definitions in a terminology
T = {E ≡ ∃r1 .D3 , A ≡ ∃X.D1 u ∃Y.D2 , Di ≡ T op, for i ∈ {1, 2, 3}}. The corre-
sponding automata AtE and AtA are depicted at figure 3(a). It is easy to check
that E is compliant with A w.r.t. any t-semantics. Indeed, for any valuation σ
which satisfy σ(X) = σ(Y ) = r1 , we have σ(AtA ) AtE and hence E vσ(T ) σ(A)
(which implies that E is compliant with A). However, we have clearly AtA 6 AtE .
As a witness of non simulation take any valuation σ 0 which satisfy σ 0 (X) 6= r1
or σ 0 (Y ) 6= r1 , and in this case we have Atσ0 (A) 6 Atσ0 (E) (which implies that
AtA 6 AtE ). Despite this fact, it is still possible to reduce compliance to simula-
tion after a transformation of the automata AtA and AtE into two new automata,
denoted ĀtA and ĀtE (c.f., figure 3(b)). The main intuition underlying the pro-
posed transformation is to construct new automata that satisfy the following
property: ĀtA ĀtE iff ∃σ ∈ Valt s.t. σ(AtA ) AtE . In the similar way, addi-
tional transformations are needed to reduce containment to simulation as stated
in the following theorem.
Fig. 3. Reducing compliance to simulation.
Theorem 1. Let T 0 be an ELV -terminology and C and D two ELV -patterns in
T and let E be a definition in and EL-terminology T 00 coherent with T 0 . Let
T = T 0 ∪ T 00 . Then there exists guarded variable automata ÂtC , ÃtD , ĀtE and ĀtC
such that:
(i) E 6tT C iff ĀtC ĀtE , and
(ii) C tT D iff ÃtD ÂtC .
The proof of this theorem is given in the extended version of this paper
[13]. We explain below the case (i) (compliance). E 6tT C iff ĀtC ĀtE . Figure
3(b) illustrates the construction of the automata ĀtA and ĀtE corresponding
to the automata of AtA and AtE of figure 3(b). The main idea is to prefix the
automata AtA and AtE with a set of transitions that enable to ensure that: ĀtA
ĀtE iff ∃σ ∈ Valt s.t. σ(AtA ) AtE . The new sri and qri states correspond to
states where all the variables are refreshed. Simulation can be viewed as a game
between a player PE , which moves in the automaton ĀtE with an assigned goal
to prove simulation, and a player PA , which moves in the automaton ĀtA with
an assigned goal to prove that there is no simulation. The rational behind the
proposed construction is to enable PE to force a choice of a valuation σt that
satisfy simulation if such a valuation exists. This is achieved by the two first
transitions labeled with the constant symbol c. At the beginning of the game,
PA choose an arbitrary valuation σ0 and moves from the state Ā to q1 . The
player PE have a choice between several transitions c, that goes in the example
from state Ē to one of the states s1 , . . . , s4 . By this deterministic choice, PE
have the possibility to choose between several classes of valuations, each class
being defined w.r.t. to the relation of the variables of the automata AtA with
the constants that appear in AtE . Once such a choice is performed, the player
PA moves upon the constant c to the state qr1 where he has the possibility to
refresh the variables in order to comply with the class of valuation selected by
PE . The rest of the prefix construction enables the player PE to synchronize
his own variables with the variables of PA in order to be aware of the valuation
chosen by PA . These variables are then used in the guards that enable PE to
enter a ’universal’ final state su in the cases where the player PA cheats (i.e.,
at the state qr1 , the player PA picks a valuation that do not belong to the class
selected by PE ). Hence, ĀtA ĀtE iff there is a valuation σt (that belongs to the
class of valuations picked by PE ) such that σt (AtA ) AtE .
Based on the previous theorem, we can provide the following result w.r.t. the
considered reasoning in ELV .
Theorem 2. Let t ∈ {r, nr}. Then:
(i) Compliance in ELV w.r.t. a t-semantics is NP-complete,
(ii) Pattern containment in ELV w.r.t.a t-semantics is in 2-Exptime.
Consider first the case (i). We recall that, E is compliant with C w.r.t. a
t-semantics, noted E 6tT C, iff there exists a valuation σ ∈ Valt such that
E vσ(T ) σ(C). We know from our construction that E 6tT C is equivalent to:
∃σ s.t σ(AtC ) AtE .
The Compliance problem is in NP : given an oracle which guess a valuation
σ, then it is possible to check in polynomial time if σ(AtC ) AtE .
The NP-hardness is proved by a reduction from graph 3-colorability problem
[11]. Let G = (V, E) be a graph. G is 3-colorable if it is possible to assign to
each node in V one of the three colors in such a way that every two nodes
connected by an edge have different colors. Starting from G and the three colors
{r, g, b}, we construct a compliance problem such that the graph G is 3-colorable
iff Ecolor 6tT CG . Where Ecolor is a definition in T 0 and CG a ELV -pattern
definition in T 00 and T = T 0 ∪ T 00 .
Construction of the terminology T 0 . For each color c ∈ {b, r, g}, we include in
T 0 a concept definition Ec as follows:
– Eb ≡ ∃b.ET op
– Er ≡ ∃r.ET op
– Eg ≡ ∃g.ET op
– ET op ≡ T op
In addition, T 0 contains the definition Ecolor ≡ ∃r.Eb u∃g.Eb u∃r.Eg u∃b.Eg u
∃b.Er u ∃g.Er .
Construction of the ELV -terminology T 00 . Given a graph G = (V, E) with V =
{n1 , . . . , nm }, we include in T 00 the following set of ELV -patterns:
– {Ni ≡ ∃Xi .NT op | f or i ∈ [1, m]} and
– NT op ≡ T op
In addition, T 00 includes the pattern: CG ≡
d
∃Xi .Nj .
(ni ,nj )∈E
Let T = T 0 ∪ T 00 . It is then easy to check that G is 3-colorable iff Ecolor 6tT
CG .
Complexity of pattern containment (case (ii)) is obtained from theorem 1
which reduces an ELV -pattern containment test C tT D into a simulation test
ÃtD ÂtC between two GVA. The automaton ÂtC is exponential in the size of
C and D. Hence, knowing from [5] that simulation is in Exptime, we obtain an
immediate 2-Exptime upper bound for the ELV -pattern containment problem.
5 Conclusion
This paper addresses the problems of pattern compliance and containment for
description logics with variables. It considers a framework that cater for cyclic
terminologies and defines two semantics of variables which differ w.r.t. to the
possibility or not to refresh the variables. The paper provides preliminary results
regarding the description logic ELV , obtained from an extension of EL with
variables. Future research work will be devoted to the extension of the approach
to more expressive logics.
References
1. F. Baader, R. Küsters, A. Borgida, and D. McGuinness. Matching in description
logics. Journal of Logic and Computation, 9(3):411–447, 1999.
2. F. Baader and P. Narendran. Unification of concept terms in description logics. In
ECAI’98, pages 331–335, 1998.
3. Franz Baader. Terminological cycles in a description logic with existential restric-
tions. In IJCAI, pages 325–330, 2003.
4. Franz Baader, Stefan Borgwardt, and Barbara Morawska. Extending unification
in EL towards general TBoxes. In KR’12, pages 568–572, 2012.
5. Walid Belkhir, Yannick Chevalier, and Michael Rusinowitch. Guarded Variable
Automata over Infinite Alphabets. October 2013.
6. F. Baader and R. Küsters. Matching in description logics with existential restric-
tions. In DL’99, Sweden, 1999.
7. Georg Gottlob, Giorgio Orsi, and Andreas Pieris. Ontological queries: Rewriting
and optimization (extended version). CoRR, abs/1112.0343, 2011.
8. Orna Grumberg, Orna Kupferman, and Sarai Sheinvald. Variable automata over
infinite alphabets. In LATA, pages 561–572, 2010.
9. J.E. Hopcroft and J.D. Ullman. Formal languages and their relation to automata.
ACM Classic Books Series, 1969.
10. Michael Kaminski and Daniel Zeitlin. Finite-memory automata with non-
deterministic reassignment. Int. J. Found. Comput. Sci., 21(5):741–760, 2010.
11. R.M. Karp. Reducibility among combinatorial problems. In R.E. Miller and J.W.
Thatcher, editors, Complexity of Computer Computations. Plenum Press, 1972.
12. R. Küsters. Characterizing the Semantics of Terminological Cycles in ALN using
Finite Automata. In KR’98, pages 499–510, 1998.
13. L.Akroun, L. Nourine, and F. Toumani. Reasoning in description logics with vari-
ables: preliminary results (extended version). Technical report, Blaise Pascal Uni-
versity, http://www.isima.fr/ftoumani/dlvextended2015.pdf, 2015.