Efficient query answering over Description Logic (DL) ontologies with very large datasets is becoming increasingly vital. Recent years have seen the development of various approaches to ABox partitioning to enable parallel processing. Instance checking using the enhanced most specific concept (MSC) method is a particularly promising approach. The applicability of these distributed reasoning methods to typical ontologies has been shown mainly through anecdotal observation. In this paper, we present an analysis method that makes use of random graph theory to show that the enhanced MSC method results in very small, tractable concepts provided that the number of role assertions removed from consideration is large enough. We also present execution time and efficiency of a parallel implementation deployed over computing clusters of various sizes, showing the ability of the method to process instance checking for large scale datasets.
Description Logics (DL) are increasingly being
used to model and represent structured and
semistructured data in different applications
In the last few years, methods for parallel and
distributed reasoning over expressive ontologies
have been published
2.1
A Description Logics (DL) knowledge base, also referred to as an ontology, is typically defined a tuple, denoted K = (T , A), where the terminological component or TBox T contains definitions of concepts and roles, and the assertional component or ABox A contains assertions about membership of individuals in concepts and about role relations between individuals. The set of roles, concepts, and individual instances in an ontology are denoted respectively by R, C, and I. The discussion
TBox
takesCourse.MagicCourse v Wizard
ABox
School(hogwarts)
Professor(albus)
Professor(severus)
MagicCourse(potions)
MagicCourse(transfiguration)
Course(math)
Student(harry)
Muggle(dudley)
isHeadOf(hogwarts, albus)
takesCourse(harry, transfiguration)
taughtBy(transfiguration, albus)
taughtBy(potions, severus)
in this paper assumes that the reader is familiar
with DL concepts and notations; refer to
1990; Donini and Era, 1992) Let K = {T , A} be an ontology, and a be an individual in I. The most specific concept for a w.r.t. A, written MSCT (A, a), is a concept such that for every concept D where K |= D(a), T |= MSCT (A.a) v D.
If MSCT (A, a) can be derived, then, to test whether K |= Q(a) holds for an arbitrary concept Q it suffices to test if (T [ { Q}) |= MSCT [{ Q}(A, a) v Q. We call the concept Q the query. Note that Q needs to be inserted into the TBox in simple form, which may require in turn the insertion of additional named concepts as well as general concept inclusion (GCI) axioms to express the necessary equivalences for these inserted concepts. In the remainder of this paper, we will assume that the query Q has been inserted into the TBox so that MSCT (A, a) denotes the MSC calculated considering Q.
Computation of the MSC for a given
individual a as defined above can be performed using a
rolling up procedure adapted from the one first
introduced in
Provided that the ABox does not contain assertion cycles, computation of the MSC can be performed recursively as follows: 1. for a given individual a, start with an empty
MSCT (A, a); 2. for every concept assertion C(a) ,
MSCT (A, a) MSCT (A, a) u C; 3. for every role assertion R(a, b),
MSCT (A, a) MSCT (A, a)
u 9 R.MSCT (A\{R(a, b)}, b); 4. for every individual equality assertion a = a0, MSCT (A, a) MSCT (A, a)
u MSCT (A, a0).
So, in the example ABox above, the MSC for severus is
(1)
It is important to note that while class assertions generate relatively simple concepts, role assertions are capable of generating very complex concepts. Suppose for example that ABox An consists of role assertions R0(a0, a1), R1(a1, a2), . . . , Rn(an, an+1); then: MSCT (An, a0) =
9 R1.(9 R2.(. . . (9 Rn.MSCT (an+1)) . . . )) (2) Thus, in the example ABox of Table 1, the MSC for harry is
Two main issues preclude this basic MSC method from proving fully useful with expressive ontologies. First, if assertion cycles are present in the ABox, the method does not terminate. For example, consider what would happen if
isProtegeOf(albus, harry) is inserted into the ABox, then a cycle forms among the individuals harry, transfiguration, and albus.
Second, unless the ABox is highly disconnected, the method has the potential to generate very large concepts, of size in the same order of the ABox itself. Consider what happens if the following assertion is added to the ABox:
takesCourse(harry, potions)
In this case, all individuals become connected with each other, and the MSC of every individual ends up being the same size of the ABox. (3) (4) (5)
Xu et.al. (2015a) define a set of improvements that result in the Enhanced MSC Method. This enhancement consists of two parts: a mechanism to address assertion cycles, and a set of syntactic conditions to reduce the size of the MSCs in practical ontologies. 2.2
To address assertion cycles, Xu et.al. (2015a) use
nominals to indicate the joint node of a cycle, as
previously suggested in
When a cycle is found starting and ending at individual ac, the individual is represented by its corresponding nominal class {ac}, and the conversion of role assertions within the cycle requires modification of the rollup method as follows: If ac is an individual where a cycle is found, select a direction to go through the cycle and: • for R(ac, x), x 6= ac
MSCT (A, ac) MSCT (A, ac)u
({ac} u 9 R.MSCT (A\{R(ac, x)}, x)) • for R(y, ac), y 6= ac
MSCT (A, y) MSCT (A, y) u 9 R.{ac} • for R(ac, ac),
MSCT (A, ac) MSCT (A, ac) u {ac} u9 R.{ac} • for any other R(x, y) in the cycle, for x 6= ac and y 6= ac,
MSCT (A, x) MSCT (A, x)
u9 R.MSCT (A\{R(x, y)}, y) Thus, if an ABox Ac = {R0(a0, a1), R1(a1, a2), . . . , Rn(an, a0)} the MSC of an assertion cycle is obtained as follows:
MSCT (Ac, a0) =
{a0} u 9 R1.(9 R2.(. . . (9 Rn.{a0}) . . . )) (6) So, suppose that the ABox in Table 1 is augmented with the assertion in equation (4), then the MSC for harry becomes {harry} u Student u 9 takesCourse .
(Professor u isHeadOf .School u isProtegeOf .{harry})) (7)
Use of the MSC method to perform instance retrieval is straightforward. Suppose it is desired to query an ABox to retrieve all instances of a concept Q. It suffices to generate MSCT (A, a) for every individual a in the ABox, and then accept every individual where (T [ Q) |= MSCT (A, a) v Q. Note that the query concept Q is added to the TBox being verified.
In
K |= 9 R.B u A0 v A where K |= B(b) and where A0 6v A summarizes information about a not contained in A. Proposition 1 Let K = (T , A) be a SHI ontology containing named concept A, concepts A0 and B, and role R. If equation (8) holds, there must exist some GCIs in T of the form
9 R0.C1 ./ C2 v C3 where R v R0, ./ is a placeholder for either u or t, and Ci’s are concepts.
Proof of this proposition can be found in
Proposition 1 directly leads to a first syntactic condition denoted SYN COND.
the form R(a, b) are said to be true for SYN COND if role R participates in at least one axiom that can be logically converted to the form of equation 9 for some R v R0, false otherwise. Assertions R(a, b) with SYN COND = false do not affect the classification of a unless either R or some R0 such that R ✓ R0 exist in the query, and can be safely removed from the calculation of MSCT (A, a). By symmetry to the inverse role R , this condition also applies to b. In practice, the axioms more likely to be found are of the form C v 9 R.D, which is equivalent to C u > v 9 R.D. Also note that (C v 8 R.D) ⌘ (9 R.¬C v ¬D). In the example in Table 1, assertions with (8) (9) role isHeadOf have SYN COND=true, while assertions with roles takesCourse and taughtBy have SYN COND=false and can be safely removed from consideration, unless the roles exist in the query itself. Note that in this case, the MSC for harry is reduced to
(10)
A second syntactic condition presented in
R(a, b) with SYN COND= true are said to be true for SYN COND DJ if there do not exist any of: • an explicit concept assertion B0(b) such that
K |= B0 v ¬C1; • an explicit concept assertion A0(a) such that
K |= A0 v ¬C3; or • an explicit concept assertion A0(a) such that
K |= A0 v ¬(C3 t ¬C2) for C1, C2, an C3 as in Eq.(9) and R v R0. Role assertions with SYN COND DJ=false can be safely removed from the calculation of the MSC of any individual, since they do not affect classification of either a or b. For example, in Table 1, role assertions with role takesCourse have SYN COND=true due to the assertion
takesCourse.MagicCourse v Wizard.
However, suppose that the following assertion were inserted into the ABox: takesCourse(dudley, math) (11) This assertion has SYN COND DJ=false, since dudley is an instance of Muggle, which in turn is disjoint with Wizard, the filler concept in the assertion above.
R(a, b) with SYN COND= true are said to be true for SYN COND SC if, for every GCI of the form in Eq.(9) there exists an explicit concept assertion A0(a) such that K |= A0 v C3.
Role assertions with SYN COND SC=true are redundant for the classification of a, and can therefore be safely removed from the calculation of the MSC of any individual. For example, the role assertion
Headmaster(albus) (12) would have SYN COND SC=true.
Application of these three syntactic conditions to the computation of the MSC of a given individual results in a significant reduction in the size of the MSC for practical ontologies. The reasons for this reduction will be established in more detail in the next section, but first we provide a definition for the parallelization of the algorithm.
Remark 1 The MSC method is guaranteed to be
sound and complete for SHI DL
The MSC method, including the syntactic conditions detailed above, is highly parallelizable, due to the following: Proposition 2 For a given knowledge base K = (T , A), computation of MSCT (A, a) for an individual a can be performed independently of the computation of the MSC of any other individual. Proof of this proposition follows directly from the definition of the MSC computation in Definitions 2 and 3, as well as in the definition of the syntactic conditions, where it should be clear that MSC computation depends only on the initial state of the knowledge base. This means that the calculation of the MSCs for all individuals can be done in parallel. Instance checking then needs to be performed against T [ MSCT (A, a) for every individual a.
Note that naive parallelized processing of individual equality assertions (i.e., owl:sameAs expressions) using the procedures outlined in Definition 2 results in redundant computations. Precomputation of the reflexive-transitive closure of these equalities avoids such redundancy. Note also that anonymous individuals, typically presented as blank nodes in OWL, are processed in the same way as named individuals for calculation purposes.
As is shown later in Section 4, parallelization of the MSC method allows for the processing of extremely large ABoxes within clusters of commodity hardware. The resulting computational complexity is sublinear with respect to the size of the ABox, which indicates linear complexity for single-machine implementation. In the next section, we present an analysis of the expected computational complexity of the enhanced MSC method, and show why it has tractable expected performance for practical ontologies. 3 3.1
Typically, the size of the ABox as measured by
the number of facts it contains is orders of
magnitude greater than the size of the TBox, and also
much larger than the size of the query. While it has
been shown that, even with exponential time
complexity, TBoxes of realistic size can be processed
in realistic time
It is clear that the MSC method for instance
checking is EXPTIME-complete for SHI. Since
the computation of the MSC is PTIME, as it is
essentially depth-first search, complexity of
checking depends on TBox reasoning. From Definition
1, it should be clear that for a connected ABox,
the size of the MSC is the size of the ABox
itself. Since testing for the subsumption of the
MSC against a concept in the TBox is reducible
to satisfiability testing of the union of the TBox
and the MSC, instance checking with the MSC
method is equivalent to satisfiability testing for
SHI DLs, which is EXPTIME-complete
From a practical standpoint, it seems more interesting to study the performance of the enhanced MSC method when used with typical ABoxes. Graph theory, and particularly random graph theory, provide methods and tools for the study of typical graphs. 3.2
Random graph theory is concerned with the study
of graphs as probabilistic random variables with a
defined probability distribution. Here we provide
a short summary of the points of interest to this
paper; the reader is referred to
Many real-world network structures are
socalled scale-free, that is, they exhibit power-law
degree distributions
It is important to note that random power-law graphs do not contain nodes with degree of 0, since at this value the distribution is undefined; therefore, analysis of random power-law graphs discards all zero-degree nodes. Where it is necessary to make the distinction, we will denote the number of non-zero-degree nodes the effective order of the graph.
It has been shown that a phase transition
occurs as the average node degree increases (where
the degree of a node is the number of edges
connected to it.), so that at a critical value a giant
component forms with high probability 1
The set of role assertions in a SHI ABox define an unlabeled, undirected graph GA, where the nodes represent the individuals in the ABox, and where there is an edge between nodes if there is at least one role assertion between the underlying individuals.
In other words, the ABox graph GA replaces multiple parallel edges between two nodes with a single, unlabeled edge. Self-loops are still allowed. Note that with respect to the MSC method, parallel edges result in only a small increase in MSC size, equivalent to the number of parallel edges. Suppose multiple role assertions R1(a, b), R2(a, b), . . . , Rn(a, b) exist in between individuals a and b in the ABox A; application of the rollup procedure for assertion cycles in Definition 3 results in the following:
MSCT (A, a)
MSCT (A, a) u {a} u 9 R1.(9 R2 {a} u · · · u 9 Rn {a} u MSCT (A\{R1(a, b), R2(a, b) . . . Rn(a, b)}, b)) (16)
Thus, collapsing parallel edges into a single unlabeled edge results in minimal reduction in the complexity of MSC calculations.
Certain properties in the role assertion graph GA can be readily related to expected characteristics of the MSCs calculated for the underlying ABox. Specifically: • the size of MSCT (A, a), as measured by number of simple form concepts that it contains, is equivalent to the order of the connected component that contains the node that represents the individual a. • the number of conjuncts at the top level of MSCT (A, a) is proportional to the degree of the node representing a. • the maximum quantification depth of MSCT (A, a) is given by the diameter of the connected component containing the node corresponding to a.
It is clear that the appearance of a giant component then means that the MSC for a significant number of individuals is in O(n), and that therefore the complexity of MSC instance checking is exponential in n.
The application of the syntactic conditions outlined in subsection 2.3 can be reflected in the role assertion graph through the removal of assertions that do not satisfy the conditions. An important question to ask is how such removal affects the characteristics of the resulting graph. Since random graphs are generative processes, it is reasonable to assume that removal of edges follows the same degree distribution as the original generation of the graphs themselves. If this is the case, the resulting graphs retain their power-law degree distribution. Thus, if the original ABox role assertion graph had a giant component of size O(n), for n the number of nodes, w.h.p. the modified graph will also show a giant component.
Note however that the reduction in the number
of edges necessarily results also in a reduction in
the effective order of the graph, that is, in the
number of non-zero-degree nodes. It is in fact possible
to calculate both the number of nodes n and
number of edges E in the graph based on the volume
and log growth rate parameters from equation 13.
For ↵ > 2, the equations are as follows
X C · k ↵ ⇡ C · ⇣ (↵ ) (17)
E = 12 X1 k · C · k ↵ ⇡ which depends only on ↵ . Therefore, if ↵ remains constant, a reduction in the number of edges necessarily results in a proportional reduction in the number of (non-zero-degree) nodes, that is, in the effective order of the graph. As will be shown in Section 4, it is this property that enables the enhanced MSC method to provide extremely good performance for very large ABoxes. To test both the accuracy and to measure parallelization speedup of the enhanced MSC method, we set up clusters of compute-optimized instances through Amazon Web Services (AWS)2. The enhanced MSC method with syntactic condition correction was implemented in Java and Scala to work over Apache Spark3, installed over Hadoop HDFS and YARN.
For the accuracy tests, we used an in-memory
version of our enhanced MSC implementation.
We set up clusters of two c4.xlarge machines, each
containing 4 virtual CPUs and 7.5GB of
memory, to run the enhanced MSC method, and
compared the results against the HermiT reasoner
version 3.8.14, running on a single c4.xlarge
machine; HermiT was chosen as a comparison
standard due to its stability and speed; future tests will
2aws.amazon.com
3https://spark.apache.org/
4http://www.hermit-reasoner.com
be done against other reasoners such as Pellet5 and
Konclude6. These tests were performed against a
single department dataset for the University
Ontology Benchmark (UOBM)
To test the parallelization of the MSC method,
we used the c3.8xlarge instances,which provide 32
virtual CPUs and 60 GBs of storage. We used
the Lehigh University Benchmark (LUBM)
A test was performed to evaluate the scalability of the parallel MSC method over the number of triples in the ABox. This test was performed over 5https://github.com/stardog-union/pellet 6http://derivo.de/produkte/konclude/ 7http://thinkaurelius.github.io/titan/ 8http://hbase.apache.org/ a cluster of 10 c3.8xlarge machines in AWS. The results are shown in the log-log diagram in Figure 1. As can be observed, the method shows clear sub-linear performance with respect to the size of the data set, as expected from an algorithm with linear performance in a sequential machine.
The performance with respect to the number of machines was evaluated in two parts. First, to evaluate under small cluster conditions, a 500,000 triple set was assembled and used to test against 1 to 10 machines. The execution time and the efficiency with respect to single-machine execution are shown in Figure 2a. To obtain evaluation for large numbers of machines, we used the ABox with 500 million triples and ran it against 10 to 50 machines; to provide a more realistic estimation, the efficiency value was corrected against the result for 500,000 triples in 10 machines. These higher scalability results are shown in Figure 2b.
In terms of raw performance, the parallel
enhanced MSC algorithm was capable of performing
instance checking for a dataset with 500 million
triples and over 110 million individual instances
in about 1,240 seconds, or around 20 min., using
a cluster of 10 machines and a total of 320
execution cores. Using 50 machines, the execution time
was 346 seconds, or somewhat less than 6
minutes. As a comparison, although the difference
in algorithms means that execution times are not
directly comparable, Oracle reports full ABox
inference over 869 million triples in 62 minutes, and
query performance over this pre-reasoned ABox in
about 4.3 min., using specialized hardware (
These results demonstrate that the enhanced
MSC method is inherently parallelizable, enabling
it to work with large scale ABoxes. They also
show that the fact that in the worst case the
enhanced MSC method is in EXPTIME does not
preclude its usefulness with practical ontologies.
In the next section, we evaluate the characteristics
of typical ABoxes that support this assertion using
random graph models.
For this purpose, we have created ABox role
assertion graphs for the same set of ontologies used
for the empirical evaluation in
the respective organisms; the TBox and both ABoxes can be provided upon request.
We have performed the least-squares fit up to
a maximum degree of 100, which accounts for
over 99.8% of all nodes in every graph considered.
Since there usually are discrepancies when the
degree is very small or very large
We have then calculated the effective order and log-growth rate of the degree distribution of the ABox role assertion graphs for all ontologies after application of SYN COND, SYN COND DJ, and SYN COND SC; the results, shown in Table 4, demonstrate that these conditions indeed produce a drastic reduction in the effective order of the role assertion graph and thus in the size of the resulting connected components, even if a giant component still appears. Observe in particular that for the LUBM ontologies, the reduction is so significant that only a very small number of individuals remain connected to others.
It is interesting to examine the relative impact of the various syntactic conditions. Note that SYN COND must always be applied, since without it, the other conditions do not make sense. Table 5 shows the impact for the application of LUBM1 LUBM4 AT CE
LUBM1 LUBM4 AT CE
# the different conditions on the AT ABox; similar trends can be seen with the other data sources. As can be seen, the initial SYN COND condition accounts for a significant portion of the reduction, but still leaves highly connected components, and is therefore not sufficient on its own to enable processing of instance checking in realistic time. Both the disjointness and subclass conditions contribute to a further reduction, resulting finally in a realistic component size for TBox reasoning purposes. In general, SYN COND SC contributes more of the reduction in size, for all studied ontologies. It should be also noted that a very large number of resulting components are singletons, which in the MSC method result in subsumption checking based only on class assertions; this can be performed very fast since the class hierarchy of the TBox can be precomputed.
Up to now, we have assumed that the power law exponent remains constant after application of the various syntactic conditions. It is interesting then to evaluate the behavior of the exponent in the power law distribution of equation 13. Figure 3 shows this for the AT data source on a log-log scale; as can be seen, other than significant deviations at very low degree values, the exponent remains relatively constant. 5
The enhanced MSC method is inherently parallelizable, since instance checking for every individual in the ABox can be performed independently. Coupled with recent advances in cluster computing such as Apache Spark, large triple SYN COND SYN COND DJ SYN COND SC SYN COND ALL
Graph size stores can be queried efficiently using commodity hardware clusters or cloud platforms.
Even as worst-case complexity of the method is in exponential time for a single sequential machine, and thus intractable for parallelization, the method performs within realistic time in practical, real-world ontologies, which typically present a power-law degree distribution. As discussed in our random graph theory analysis, this is due to the ability of the method to reduce the size of the connected components formed within the ABox Role Assertion Graph, which in turn means a reduction in the size of the MSCs generated for the individuals in the ABox. Our method is thus most effective when the different syntactic conditions can be applied to effect this reduction, and will possibly prove less beneficial if most of the roles in the TBox are engaged in axioms of the form of equation (9).
We are currently exploring the use of the
method to address full conjunctive queries over
DL knowledge bases expressed in the SPARQL
query language. This requires the expansion of the
MSC method to retrieve individuals a and b that
can be inferred to be in a relation R(a, b). This
extension is being implemented based on Theorem
4.1 in
SPARQL query answering will also enable us to perform tests with other existing benchmarks such as the DBPedia SPARQL Benchmark (DBPSB). In addition, we are working on improvements in the efficiency of the parallelization of the MSC method. In particular, we are looking into combining multiple individuals that form part of the same connected component in the ABox role assertion graph in the same parallel task, since it can be seen in Definitions 2 and 3 that portions of the MSC computation can be shared among individuals provided that they are connected to each other. 6
In this paper, we have presented a parallel implementation of the enhanced MSC method, and we have evaluated execution time and efficiency as we varied the size of the data and the number of processors used. Since the method performs independent checking for every individual in the ABox, it is inherently parallelizable. The results show sublinear performance with respect to the size of the ABox, which stems from its performance in linear time in the computation of the MSCs, and almost constant time for reasoning due to the small size of the resulting MSC.
This work is supported by grant # R44GM097851 from the National Institute of General Medical Sciences (NIGMS), part of the U.S. National Institutes of Health (NIH).