We introduce an extension of the Description Logic ℱ ℒ0 that allows us to define concepts in an approximate way. More precisely, we extend ℱ ℒ0 with a threshold concept constructor of the form ◁▷ for ◁▷ ∈ {≤ , <, ≥ , >}, whose semantics is given by using a membership distance function (mdf). A membership distance function assigns to each domain element and concept a distance value expressing how “close” is such element to being an instance of the concept. Based on this, a threshold concept ◁▷ is interpreted as the set of all domain elements that have a distance from such that ◁▷ . We provide a framework to obtain membership distance functions based on functions that compare tuples of languages, and we show how weighted looping tree automata over a semiring can be used to define membership distance functions for ℱ ℒ0 concepts.
Traditional Description Logics (DLs) [
To alleviate this, a considerable amount of research has been directed towards extending
DLs with means that would allow us to model (and reason about) imprecise knowledge. Early
examples of this are fuzzy DLs [
In this paper, we extend the DL ℱ ℒ0 [15] with threshold concepts, by following the general
idea applied to ℰ ℒ in [14]. The resulting family of logics is called ℱ ℒ0at(), where the
parameter now corresponds to a membership distance function. The main diference to [ 14] is
that now we use the notion of distance instead of membership degrees, to measure “how close”
an element is to being an instance of a concept. Obviously, a key aspect of ℱ ℒ0at() is which
distance function to choose. In this work, we provide a general framework to define such
distance functions for ℱ ℒ0, which reduces the definition of membership distance functions
to the definition of functions comparing tuples of formal languages. Moreover, we show that
such measures can be defined by using weighted tree automata, which not only ofers a more
concrete (yet diverse) form of defining membership distance functions, but also provides a
machinery that allows in many cases to actually compute these functions. A distinctive feature
of this framework is that it allows us to define membership distance functions that can take
into account background knowledge stated by GCIs in an ℱ ℒ0 TBox. This is not the case for
the approaches proposed in [
The paper is structured as follows. In the next section, we formally introduce the DL ℱ ℒ0, and recall some related technical notions that are needed in the rest of the paper. In Section 3, we introduce the family of threshold logics ℱ ℒ0at(). We then continue in Section 4, by describing our framework for defining membership distance functions for ℱ ℒ0. In Section 5, we explain how weighted looping tree automata can be used to define and compute membership distance functions. We finish the paper, by summarizing the contributions of the paper and giving some ideas of how to move forward.
Due to space constraints, we provide all proofs and additional technical details in the accompanying technical report [17].
We start by formally introducing the DL ℱ ℒ0. Afterwards, we recall how subsumption (equivalence) between ℱ ℒ0 concepts can be characterized using language inclusion, and show that this idea can also be applied to characterize membership of an individual in an ℱ ℒ0 concept.
Let NC and NR be finite disjoint sets of concept names and role names, respectively. The set ℱℒ0 (NC, NR) of ℱ ℒ0 concept descriptions over NC and NR is obtained by using the concept constructors conjunction (⊓), universal restriction (∀.), and top (⊤) in the following way: ::= ⊤ | | ⊓ | ∀. where ∈ NC, ∈ NR and is an ℱ ℒ0 concept description. We will often write ℱℒ0 in place of ℱℒ0 (NC, NR), if the sets NC and NR are clear from the context or irrelevant.
The semantics of ℱ ℒ0 is defined in the usual way, by using standard first-order interpretations. An interpretation ℐ = (Δℐ , · ℐ ) consists of a non-empty domain Δℐ and an interpretation function · ℐ that assigns subsets ℐ ⊆ Δℐ to concept names ∈ NC and binary relations ℐ ⊆ Δℐ × Δℐ to role names ∈ NR. The function .ℐ is inductively extended to all ℱ ℒ0 concepts in ℱℒ0 (NC, NR) as follows: ⊤ℐ := Δℐ , ( ⊓ )ℐ := ℐ ∩ ℐ , (∀.)ℐ := { ∈ Δℐ | ∀ ∈ Δℐ : (, ) ∈ ℐ ⇒ ∈ ℐ }. Given two ℱ ℒ0 concepts and , we say that is subsumed by (written as ⊑ ) if ℐ ⊆ ℐ for all interpretations ℐ. These two concepts are equivalent (written as ≡ ) if ⊑ and ⊑ . In addition, is satisfiable if ℐ ̸= ∅ for some interpretation ℐ.
An ℱ ℒ0 TBox is a finite set of general concept inclusions (GCIs), which are expressions of the form ⊑ where , ∈ ℱℒ0 . We say that an interpretation ℐ is a model of (written as ℐ |= ) if it satisfies all the GCIs in , meaning that ℐ ⊆ ℐ for all ⊑ in . The subsumption and equivalence relations are now defined modulo the set of models of , and denoted as ⊑ and ≡ , respectively. The notion of satisfiable concept is also defined modulo the set of models of . 2.2. ℱ ℒ0 and formal languages In ℱ ℒ0, subsumption and equivalence can be characterized via a transition to formal languages, by utilizing a certain normal form. In particular, the semantics of ℱ ℒ0 implies that value restrictions distribute over conjunction, i.e, for all ℱ ℒ0 concepts , and roles it holds that ∀.( ⊓ ) ≡ ∀ . ⊓ ∀.. Using this equivalence as a rewrite rule from left to right, every ℱ ℒ0 concept description can be written as a finite conjunction of terms of the form ∀1.∀2. · · · ∀ ., where ≥ 0, {1, . . . , } ⊆ NR, and ∈ NC. We can further abbreviate such a term as ∀., where represents the word 1 . . . over the alphabet NR. In case = 0, is the empty word , and thus ∀. corresponds to . Finally, we can group together value restrictions with the same concept name, i.e., abbreviate ∀1. ⊓ · · · ⊓ ∀ ℓ. by ∀{1, . . . , ℓ}., where {1, . . . , ℓ} is a finite language over NR. In addition, we use the convention that ∀∅. corresponds to ⊤. As a result, any two ℱ ℒ0 concept descriptions , over NC = {1, . . . , } and NR can be rewritten in the normal form: ≡ ∀ 1.1 ⊓ · · · ⊓ ∀ . ≡ ∀ 1.1 ⊓ · · · ⊓ ∀ ., where 1, . . . , , 1, . . . , are finite subsets of NR* . Using this language normal form (LNF), it was shown in [18] that ⊑ if ⊆ for all = 1, . . . , . Since ≡ if ⊑ and ⊑ , it follows that ≡ if = for all = 1, . . . , .
In [19], this characterization of subsumption was extended to non-empty TBoxes, by using the notion of value restriction sets. Given a concept ∈ ℱℒ0 , a concept name ∈ NC, and an ℱ ℒ0 TBox , the value restriction set of w.r.t. and is defined as the language: ℒ (, ) = { ∈ NR* | ⊑ ∀.}.
Using these sets, the above characterizations of subsumption and equivalence can be lifted to take into account the GCIs in a TBox as follows (see [19]): ⊑ ⇐⇒ ℒ (, ) ⊆ ℒ (, ) ( = 1, . . . , ), ≡ ⇐⇒ ℒ (, ) = ℒ (, ) ( = 1, . . . , ).
Essentially, this means that every ℱ ℒ0 concept description can be uniquely represented by the tuple of languages
ℒ () = (ℒ (, 1), . . . , ℒ (, )) and every concept description equivalent to has the same representation.
We will now demonstrate that a similar characterization can be used to describe when an individual is an instance of a concept description in an interpretation ℐ. Given an interpretation ℐ, ∈ Δℐ and ∈ NC, we define the following language:
ℒℐ (, ) = { ∈ NR* | ∈ (∀.)ℐ }.
Using these languages, an individual can be represented as a tuple of languages ℒℐ () := (ℒℐ (, 1), . . . , ℒℐ (, )). Moreover, membership in ℱ ℒ0 can be characterized as follows. Theorem 1. Given an ℱ ℒ0 TBox , a model ℐ = (Δℐ , · ℐ ) of , an ℱ ℒ0 concept , and an element ∈ Δℐ we have that ∈ ℐ ⇐⇒ ℒ (, ) ⊆ ℒ ℐ (, ) for every ∈ .
In this section, we introduce the family of threshold logics ℱ ℒ0().
3.1. The family of logics ℱ ℒ0()
Threshold concepts for ℱ ℒ0 are expressions of the form ◁▷ where is an ℱ ℒ0 concept,
◁▷ ∈ {<, ≤ , >, ≥} , and is an element of a linearly ordered set (, ≤ ) with minimum m. The
purpose of these concept constructors is to define sets of individuals of an interpretation ℐ that
may not belong to ℐ , but still satisfy some of the properties required by . To quantify the
notion of partial satisfaction, we use a value from that expresses “how far” an individual is
from belonging to ℐ , where the m identifies crisp membership, i.e., that ∈ ℐ . For instance, if
we consider (, ≤ ) as the interval [
To provide the semantics for threshold concepts, we introduce the notion of membership distance function. Such a function operates as follows: given an interpretation ℐ, it takes an individual ∈ Δℐ and an ℱ ℒ0 concept as input, and outputs a value in expressing how far is from belonging to ℐ . Membership distance functions are required to satisfy two properties, as stated in the following definition.
Definition 1. Given a linearly ordered set with minimum (, ≤ , m), a membership distance function (mdf) is a family of functions containing for every interpretation ℐ a function ℐ : Δℐ × ℱℒ0 → , such that satisfies the following (for all ℱ ℒ0 concepts and ): M1: for all interpretations ℐ and all ∈ Δℐ : ∈ ℐ ⇔ ℐ (, ) = m,
M2: ≡ ⇔ ℐ (, ) = ℐ (, ) for all interpretations ℐ and all ∈ Δℐ .
The first property expresses the intuition that membership distance functions generalize the notion of classical membership. Regarding M2, it requires equivalence invariance, which means that should behave the same for concepts that are equivalent, regardless of their syntactic definition. We are now ready to define the syntax and semantics of our family of logics ℱ ℒ0(). Given the sets NC and NR of concept and role names, the set of ℱ ℒ0() concepts is defined as follows:
̂︀ ::= ⊤ | | ̂︀ ⊓ ̂︀ | ∀.̂︀ | ◁▷ , where ∈ NC, ∈ NR, ◁▷ ∈ {<, ≤ , >, ≥} , ∈ , is an ℱ ℒ0 concept description, and ̂︀ is a ℱ ℒ0() concept description. Concepts of the form ◁▷ are called threshold concepts.
The semantics of ℱ ℒ0() concept descriptions is defined completely analogously to the semantics of classical ℱ ℒ0 concepts, but additionally using the parameter distance function to interpret threshold concepts in the following way:
[◁▷ ]ℐ := { ∈ Δℐ | ℐ (, ) ◁▷ }.
The following is a direct consequence of requiring property M1.
Proposition 1. For every ℱ ℒ0 concept description it holds that ≤ m ≡ and >m ≡ ¬ , where the semantics of negation is (¬)ℐ = Δℐ ∖ ℐ .
Essentially, this tells us that the addition of threshold concepts allows for expressing the negation of ℱ ℒ0 concept descriptions. Therefore, diferently from ℱ ℒ0, there are unsatisfiable ℱ ℒ0() concept descriptions, e.g., ⊓ >m.
An important aspect when using DLs is to have the possibility to formulate (and take into account) terminological knowledge, which in DLs is expressed by GCIs in a TBox. For the family of logics ℱ ℒ0at(), the most simple and natural form of such TBox is a plain ℱ ℒ0 TBox. For instance, we can define the ℱ ℒ0() concept descriptions ∀.(∀.)< and ∀.(∀.)< w.r.t. the following TBox:
:= {∀. ⊑ ∀., ∀. ⊑ ∀.}.
Note that, although ∀. ̸≡ ∀ ., they are actually equivalent modulo . Therefore, it should be the case that (∀.)< ≡ (∀.)< and ∀.(∀.)< ≡ ∀.(∀.)< hold in any particular logic ℱ ℒ0(). However, this will not always be the case, since the semantics of (∀.)< and (∀.)< depends on the distance function , but need not take into account the GCIs in . Hence, to properly define the semantics of ℱ ℒ0() w.r.t. an ℱ ℒ0 TBox , we need to make aware of the GCIs in . To this end, we slightly extend the definition of membership distance functions given in Definition 1 to a larger family of functions.
Definition 2. Given a linearly ordered set with minimum (, ≤ , m), a membership distance function (mdf) is a family of functions containing for every ℱ ℒ0 TBox and model ℐ of a function ℐ, : Δℐ × ℱℒ0 → , such that satisfies the following (for all TBoxes and ℱ ℒ0 concepts and ):
M1′ : for all ℐ |= and all ∈ Δℐ : ∈ ℐ ⇔ ℐ, (, ) = m,
M2′ : ≡ ⇔ ℐ, (, ) = ℐ, (, ) for all ℐ |= all ∈ Δℐ .
Hence, in the presence of an ℱ ℒ0 TBox , the semantics of ℱ ℒ0() concepts is defined by using ℐ, to interpret threshold concepts ◁▷ in any model ℐ of . In the next sections, we will provide more concrete ways of defining distance functions w.r.t. ℱ ℒ0 TBoxes.
Finally, we would like to be able to state GCIs containing threshold concepts, e.g., ∀.(∀.)≥ ⊑ ∀.. However, as pointed out in [16] for the family of threshold logics ℰ ℒ(), obtaining an appropriate semantics for TBoxes containing threshold concepts is not entirely trivial. We will consider this in future work.
In this section, we introduce a general framework to define membership distance functions for ℱ ℒ0. To this end, we exploit the connection between ℱ ℒ0 and formal languages to obtain a way of defining distance functions in terms of language containment distances, which are functions that compare tuples of languages. Finally, we describe a particular form that such containment distances can have, and provide concrete examples that can be derived from it.
The idea of using tuples of languages to approximate the semantics of ℱ ℒ0 is not new. In [20, 21, 22], the authors exploit the fact that ℱ ℒ0 concepts can be represented as tuples of languages, to use these tuples to define concept comparison measures (CCMs) between ℱ ℒ0 concepts. Intuitively, a CCM generalizes classical equivalence (subsumption), by assigning to a pair of concepts (, ) a degree to which equivalence (subsumption) between and is satisfied. Such measures are defined in [20, 21, 22] by using the following general approach: 1 1. Translate the concepts and into the tuples of languages ℒ () and ℒ (). 2. Compare the tuples ℒ () and ℒ () by using a function c that assigns values from a numerical domain to tuples of languages. 3. The value c(ℒ (), ℒ ()) is then used to define the value of the CCM on and .
Since crisp membership in ℱ ℒ0 can also be characterized by using tuples of languages (see Theorem 1), we employ a similar approach to define membership distance functions for ℱ ℒ0. More precisely, we define membership distance functions as functions that compare tuples of languages, i.e., ℐ, (, ) is defined by comparing the tuples ℒ () and ℒℐ (). Clearly, not every function comparing tuples of languages yields a membership distance function, i.e., a 1In [20, 21], CCMs are only defined w.r.t. the empty TBox, i.e., by using ℒ∅() and ℒ∅(). family of functions satisfying the properties M1′ and M2′. For this reason, we introduce the notion of language containment distance (lcd), which is formally defined as follows. Definition 3. Let l = (, ≤ , m) be a linearly ordered set with minimum m. In addition, let Σ be an alphabet and ℓ a positive integer. An ℓ-language containment distance over Σ and l (ℓ-lcd) is a function c : (2Σ* )ℓ × (2Σ* )ℓ → that satisfies the property c((1, . . . , ℓ), (1, . . . , ℓ)) = m ⇐⇒ ⊆ for all , 1 ≤ ≤ ℓ.
(1)
We can now define a mechanism that, given NC = {1, . . . , } and an -lcd c over Σ = NR and l = (, ≤ , m), yields a distance function c for ℱ ℒ0 concepts defined over NC and NR. Definition 4. Let c be a -lcd over NR and l = (, ≤ , m). Then, for each ℱ ℒ0 TBox and interpretation ℐ that is a model of , the function cℐ, : Δℐ × ℱℒ0 ↦→ is defined as: cℐ, (, ) = c(︀ ℒ (), ℒℐ ())︀ .
The following lemma shows that the family of functions c = {cℐ, | is an ℱ ℒ0 TBox, ℐ |= } induced by an lcd c satisfies the required properties, i.e., M1′ and M2′, and hence the above framework can be used to define membership distance functions. Lemma 1. Let c be an -lcd over NR and l = (, ≤ , m). Then, c is a membership distance function.
One way to define ℓ-language containment distances is, given tuples (1, . . . , ℓ) and (1, . . . , ℓ), to use a 1-language containment distance to compare each pair of languages (, ), and then apply an appropriate function that combines the obtained ℓ values into a single one [21]. A function : ℓ → is called an ℓ-ary combining function if it is commutative: (1, . . . , ℓ) = ( (1), . . . , (ℓ)) for all permutations of indices 1, . . . , ℓ, monotone: 1 ≤ 1, . . . , ℓ ≤ ℓ =⇒ (1, . . . , ℓ) ≤ (1, . . . , ℓ), and m-closed: (1, . . . , ℓ) = m ⇐⇒ 1 = · · · = ℓ = m.
For instance, for the interval [
The following is an easy consequence of the properties required for combining functions and 1-language containment distances.
Lemma 2. Let c1 be a 1-language containment distance over Σ and l, and an ℓ-ary combining function over . Further, let c : (2Σ* )ℓ × (2Σ* )ℓ → be defined as:
c((1, . . . , ℓ), (1, . . . , ℓ)) := (c1(1, 1), . . . , c1(ℓ, ℓ)).
Then, c is an ℓ-language containment distance over Σ and l.
2For the [
We now provide some examples of ℓ-lcds that are obtained by using 1-language containment distances and ℓ-ary combining functions. These are defined over the set of non-negative reals. • c0(, ) = 0 if ⊆ and 1 otherwise. This is the simplest form of a 1-lcd, since it simply checks whether the first language is contained in the second one or not. It can be extended to an ℓ-lcd by using maximum, sum, or average: – c˜0(︀ (1, . . . , ℓ), (1, . . . , ℓ))︀ = 1 ∑︀ℓ
=1 c0(, ). – c¯0(︀ (1, . . . , ℓ), (1, . . . , ℓ))︀ = max(c0(1, 1), . . . , c0(ℓ, ℓ)), – ĉ0︀(︀ (1, . . . , ℓ), (1, . . . , ℓ))︀ = ∑︀=1 c0(, ), Intuitively, the first function checks whether containment is violated in any of the language pairs, the second one counts in how many of them a violation occurs, while the last one gives the percentage of pairs in which a violation of containment occurs. • c1(, ) = 2− , where = min{|| | ∈ ∖ }. Obviously, if ⊆ then ∖ = ∅, and hence = +∞, meaning that 1(, ) = 0. This function searches for the shortest word that occurs in but not in , and assigns a greater value to shorter ones than longer ones. Once again, we can extend c1 to an ℓ-lcd by using any of the functions described for c0. If we use maximum, we are essentially looking for the shortest violation overall, with summing we are aggregating the penalties for the violations in the diferent pairs, while taking the average does not hold much intuitive meaning. • c2(, ) = ( ∖ ), where () = ∑︀∈ (2|Σ|)−| |. This function takes all violations into account, but longer words are penalized less than shorter ones. Extending c2 to an ℓ-lcd by applying maximum yields a containment distance that searches for the “largest” diference in any pair of languages, whereas summing over the diferent pairs of languages corresponds to taking into account all the diferences that occur. Finally, taking the average has the obvious meaning.
It is easy to verify that, by construction, c0, c1, c2 are indeed 1-lcds, since they only output the value m = 0 if the language in their first argument is contained in the one in the second.
Finally, since the main reason we employ lcds is to define membership distance functions, let us examine the meaning of these functions when applied to ℒ () and ℒℐ (). It should be clear that if is a violation of containment, this means that ⊑ ∀. (for some ∈ NC), while ∈/ (∀.)ℐ . As a result, c0 (extended with the max function) simply checks whether ∈ ℐ (see Theorem 1), outputting 0, or not, outputting 1. Furthermore, the idea behind c1 and c2 that longer violations should count less than shorter ones corresponds to the view that diferences “closer” to are more important than ones further away.
In the previous section, we described how to reduce the definition of membership distance functions to defining measures that compare tuples of languages: ℐ, (, ) corresponds to a value that results from comparing the tuples ℒ () and ℒℐ (). In this section, we first demonstrate how to compute and (finitely) represent these tuples of (potentially) infinite languages, and how to assign such a value by making use of tree automata with weights. To this end, after establishing a correspondence between tuples of languages and infinite trees, we exhibit how these tuples can be computed and encoded using looping tree automata (LTAs) accepting the corresponding trees. Subsequently, we discuss how weighted looping tree automata perform the function of assigning values to trees and how they can be combined with the aforementioned LTAs. Overall, we obtain a concrete way to define membership distance functions that can be computed.
The idea of representing tuples of languages using infinite trees has appeared in [ 18, 23, 19, 22]. Initially, we provide the formal definition of infinite trees, before we discuss how they can be used to represent tuples of languages.
Definition 5. Let Σ = { 1, . . . , }be a non-empty, finite set of symbols. Given a finite set of labels , an -labeled Σ-tree is a mapping : Σ* → that assigns a label () ∈ to every node ∈ Σ* . The set of all -labeled Σ-trees is denoted as Σ,.
Intuitively, the nodes of a Σ-tree correspond to finite words in Σ* , where the empty word is represented by the root of and every node has children corresponding to the words 1, . . . , . Furthermore, if we label each node of the tree with either 0 or 1, we can define a language over Σ by considering the words ∈ Σ for which () = 1. If the labels were pairs of 0s and 1s, then two languages can be defined, one for each component, and so on.
More generally, the following mapping makes the connection between tuples of languages and infinite trees explicit. where L : Σ* → {0, 1}ℓ is the Σ-tree such that Definition 6. Let Σ be a finite set of symbols and ℓ ∈ N. We define the mapping ℓ : ︀( 2Σ* )︀ ℓ → Σ,{0,1}ℓ as follows: given a tuple of languages L = (1, . . . , ℓ) over Σ, we set ℓ(L) := L L() := (1, . . . , ℓ), where = 1 if ∈ (for all ∈ Σ* ).
It is easy to see that ℓ is a bijection between tuples of ℓ languages over the alphabet Σ and {0, 1}ℓ-labeled Σ-trees. Given ∈ Σ,{0,1}ℓ , the inverse function yields the tuple ℓ− 1() = (1, . . . , ℓ) where consists of the words for which the -th component of () is 1.
In particular, if we fix Σ = NR and a linear order between the concept names in NC = (1, . . . , ), the tuple of languages ℒ () (likewise for ℒℐ ()) can be represented by the NR-tree ℒ () with labels from {0, 1} defined as:
ℒ ()() := (1, . . . , ), where = 1 if ∈ ℒ (, ) (for all ∈ Σ* ). Note that ℒ () and ℒℐ () can be put together in a single tree, by using labels of length 2.
So far, we have seen how concept descriptions and individuals in an interpretation can be represented as tuples of languages, which in turn correspond to (infinite) trees. Next, we need to represent said trees in a finite way. Obviously, this is not always possible for infinite trees. However, for the needs of our work, the relevant trees are regular (see [22, 19] for ℒ () and the proof of Prop. 3 [17] for ℒℐ () when ℐ is finite). There are diferent ways to represent regular trees in a finite way [24]. Here, we use looping tree automata for this purpose. Definition 7 (Looping tree automaton (LTA)). A looping tree automaton is a tuple = (Σ, , , Δ, ) where Σ = { 1, . . . , } is a finite set of symbols, is a finite set of states, is a finite set of labels, Δ ⊆ × × is the transition relation and ⊆ is a set of initial states. A run of this automaton on a tree ∈ Σ, is a -labeled Σ-tree : Σ* → such that: () ∈ and ( (), (), ( 1), . . . , ( )) ∈ Δ for all ∈ Σ* . The tree language ℒ() recognized by is the set of all trees ∈ Σ, such that accepts , i.e., has a run on . If ℒ() = {0}, then we say that is representing the tree 0.
Essentially, if an LTA is representing a single tree, it is a finite representation of this tree. In [22] it was proved that regular trees can always be represented by an LTA. In particular, for the case of ℒ (), the following result was shown in [19].
Proposition 2 ([19]). Let be an ℱ ℒ0 concept description and an ℱ ℒ0 TBox. Then, one can construct an LTA that represents ℒ () in time exponential in the size of and .
For ℒℐ (), however, one has to be more careful. For infinite interpretations, the languages ℒℐ (, ) need not be regular (and hence also the tree ℒℐ()). Still, for finite interpretations these languages are always regular (as Prop. 3 below shows), and hence can be represented by deterministic finite automata. Intuitively, we can view a finite interpretation as a finite automaton, where the individuals are states and role connections correspond to transitions. It is then not dificult to verify that for an individual and a concept name one can recursively follow the paths in the graph to check whether ∈ (∀.)ℐ or not. The language ℒℐ (, ) will be the solution of a set of language equations. Overall, we have the following result. Proposition 3. Let NC = {1, . . . , }. Given a finite interpretation ℐ = (Δℐ , · ℐ ) and ∈ Δℐ one can construct DFAs that recognize the languages ℒℐ (, 1), . . . , ℒℐ (, ) and a looping tree automaton that is representing the tree ℒℐ() in time exponential in the size of ℐ and NC.
We now want to assign values from a proper (numerical) domain to trees (that correspond to tuples of languages). This is exactly the operation of infinitary tree series, for which the assigned values are usually elements of a semiring, i.e., a domain equipped with two operations, the one traditionally called “addition” and the other “multiplication”, that satisfy certain mathematical properties. Formally, an infinitary tree series ℎ over the alphabet and semiring is a mapping ℎ : Σ, → . The class of all infinitary tree series over and is denoted by ⟨⟨ Σ,⟩⟩.
One way to (finitely) define such series, is using a weighted looping tree automaton (wLTA) ([22]). Intuitively, a wLTA ℳ attributes a weight, i.e., a value from a semiring to every transition, and “multiplies” all the weights accumulated during a certain run on a tree. Finally, it “sums” the weights of all the runs to determine the value that will be assigned to the input tree. For this purpose, it is clear that the underlying semiring should admit suitable infinite sums and products. In totally complete commutative semirings, addition and multiplication can be suitably extended to infinite sums and countably infinite products (see [25] for formal definitions).
Furthermore, since we want the output values to be used for membership distance functions, we require that the domain of is also equipped with a linear order and has a minimum element m. This is not a heavy restriction, since most numeric semirings are already equipped with such an order. Examples are the semiring of natural numbers (N ∪ {+∞}, +, · , 0, 1), the tropical semiring = (N ∪ {+∞}, min, +, +∞, 0), and its real counterpart R = (R≥ 0 ∪ {+∞}, inf, +, +∞, 0), all equipped with the usual order and 0 as the minimum element.
The infinitary tree series ||ℳ|| ∈ ⟨⟨ Σ,⟩⟩ defined by the wLTA ℳ is called the behavior of the wLTA ℳ. It assigns to every tree ∈ Σ, a value (||ℳ||, ). As demonstrated in [22], wLTAs can be used to define functions over tuples of languages, viewed as infinite trees. In fact, the language containment distances described in Section 4 are variations of the functions defined in [22], and they can also be defined by a wLTA by using similar constructions.
It is also shown in [22] that, for certain semirings, a wLTA ℳ can be combined with an LTA representing a tree in order to compute the value (||ℳ||, ) in time polynomial in the size of ℳ and . As a result, given a wLTA ℳ defining a language containment distance c, the LTAs obtained from ℒ () and ℒℐ () can be combined with ℳ in order to compute cℐ, (, ), i.e., the value (||ℳ||, ,ℐ ) where ,ℐ is the single tree representing ℒ () and ℒℐ (). This “computable” family of wLTAs includes the wLTAs defining the language containment distances described in Section 4. Overall we obtain the following result.
Theorem 2. Given a wLTA ℳ that computes a language containment distance c, an ℱ ℒ0 TBox , a finite model ℐ of , ∈ Δℐ , and ∈ ℱℒ0 , the value cℐ, (, ) is computable. In particular, this holds for all concrete language containment distances c defined in Section 4.
We have introduced a family of DLs ℱ ℒ0() that extends the DL ℱ ℒ0 with threshold concepts, whose semantics is defined by using a membership distance function . We have demonstrated how membership of an indvidual in an ℱ ℒ0 concept can be characterized using formal languages, similarly to existing characterizations of subsumption and equivalence between ℱ ℒ0 concepts. Utilizing this characterization, we derived a framework for obtaining membership distance functions by employing functions that compare tuples of formal languages, namely language containment distances. Finally, we exhibited how weighted looping tree automata can be exploited to derive concrete and computable functions through our framework.
The natural continuation in this line of work is to study reasoning problems in ℱ ℒ0() for particular membership distance functions. A powerful tool when reasoning in ℱ ℒ0 is the notion of a functional model of a concept description [19], i.e., an interpretation that has the shape of an infinite tree, where every node has exactly one successor for every ∈ NR, and the root of which belongs to (the interpretation of) . Among others, subsumption ([19]) and instance checking ([26]) can be decided using said models, since every ℱ ℒ0 concept has a functional model. One could reasonably assume that a similar technique could be employed for ℱ ℒ0(). For example, in order to investigate satisfiability of a concept description, the search space could potentially be reduced to the set of functional models. However, this is not possible in ℱ ℒ0(), as a result of Proposition 1. More precisely, the concept description ̂︀ := ∀.( ⊓ >m) is satisfiable but it requires that any individual in the extension of ̂︀ has no successors. As a result, this concept description has no functional model for any membership distance function. It would be interesting to investigate if a such an approach can be used in order to reason in this threshold setting. [14] F. Baader, G. Brewka, O. Fernández Gil, Adding threshold concepts to the description logic ℰ ℒ, in: Proc. of the 10th Int. Symp. on Frontiers of Combining Systems (FroCoS 2015), volume 9322 of Lecture Notes in Computer Science, Springer, 2015, pp. 33–48. [15] F. Baader, Using automata theory for characterizing the semantics of terminological cycles,
Ann. Math. Artif. Intell. 18 (1996) 175–219. [16] F. Baader, O. Fernández Gil, Extending the description logic ℰ ℒ(deg ) with acyclic TBoxes, in: Proc. of the 22nd Eur. Conf. on Artificial Intelligence (ECAI 2016), volume 285 of Frontiers in Artificial Intelligence and Applications , IOS Press, 2016, pp. 1096–1104. [17] O. Fernández Gil, P. Marantidis, Towards Extending the Description Logic ℱ ℒ0 with Threshold Concepts Using Weighted Tree Automata, LTCS-Report 23-04, Chair for Automata Theory, Institute for Theoretical Computer Science, Technische Universität Dresden, Dresden, Germany, 2023. See http://lat.inf.tu-dresden.de/research/reports.html. [18] F. Baader, P. Narendran, Unification of concept terms in description logics, J. of Symbolic
Computation 31 (2001) 277–305. [19] M. Pensel, An automata based approach for subsumption w.r.t. general concept inclusions in the description logic ℱ ℒ0, Master’s thesis, Chair for Automata Theory, TU Dresden, Germany. See http://lat.inf.tu-dresden.de/research/mas., 2015. [20] T. Racharak, B. Suntisrivaraporn, Similarity measures for ℱ ℒ0 concept descriptions from an automata-theoretic point of view, in: 6th International Conference of Information and Communication Technology for Embedded Systems (IC-ICTES), 2015, pp. 1–6. [21] F. Baader, P. Marantidis, A. Okhotin, Approximate unification in the description logic ℱ ℒ0, in: Proc. of the 15th Eur. Conf. on Logics in Artificial Intelligence (JELIA’2016), volume 10021 of Lecture Notes in Computer Science, Springer, 2016, pp. 49–63. [22] F. Baader, O. Fernández Gil, P. Marantidis, Approximation in description logics: How weighted tree automata can help to define the required concept comparison measures in ℱ ℒ0, in: Proceedings of the 11th International Conference on Language and Automata Theory and Applications (LATA 2017), volume 10168 of Lecture Notes in Computer Science, Springer, 2017, pp. 3–26. [23] F. Baader, A. Okhotin, On language equations with one-sided concatenation, Fundamenta
Informaticae 126 (2013) 1–35. [24] W. Thomas, Automata on infinite objects, in: Handbook of Theoretical Computer Science,
Volume B: Formal Models and Sematics (B), The MIT Press, 1990, pp. 133–192. [25] G. Rahonis, Weighted muller tree automata and weighted logics, J. Autom. Lang. Comb.
12 (2007) 455–483. [26] F. Baader, P. Marantidis, M. Pensel, The data complexity of answering instance queries in ℱ ℒ0, in: P. Champin, F. Gandon, M. Lalmas, P. G. Ipeirotis (Eds.), Companion of the The Web Conference 2018 on The Web Conference 2018, WWW 2018, Lyon , France, April 23-27, 2018, ACM, 2018, pp. 1603–1607.