# Semantic Consistency Checking in Building Ontology from Heterogeneous Sources

Authors: Shihan Yang; Hongyan Tan; Jinzhao Wu
Journal: Journal of Applied Mathematics
 (2014)

---

## Abstract

Semantic collision is inevitable while building a domain ontology from heterogeneous data sources (semi-)automatically. Therefore, the semantic consistency is indispensable precondition for building a correct ontology. In this paper, a model-checking-based method is proposed to handle the semantic consistency problem with a kind of middle-model methodology, which could extract a domain ontology from structured and semistructured data sources semiautomatically. The method translates the middle model into the Kripke structure, and consistency assertions into CTL formulae, so a consistency checking problem is promoted to a global model checking. Moreover, the feasibility and correctness of the transformation is proved, and case studies are provided.


---

## Body

## 1. Introduction

Semantic web has been a great idea and a promising research area for a dozen years [1]. A main challenge of widening semantic web technologies is lack of semantic data, which is named ontology. So lots of researchers focus on how to transform the legacy mass web data into ontology. The legacy web data in varietal forms can be classified roughly into three types: structured data, such as relational databases; semistructured data, such as XML documents and emails; and nonstructured data, such as general text and video. Recently, technologies of automatically transforming semistructured data or structured data into a domain ontology through mediate modeling are promising [2–6]. In these technologies, some semantic collisions appear inevitably when the same domain ontology has been built from multiple data sources. A domain ontology is a formal expression of a domain knowledge, aiming to unify the general knowledge of a special domain in order to share contents, achieve interoperability, or integrate applications without specific authorization. Unfortunately, the unification is very tough even in the same organization, where the general knowledge exists in very different forms, in very distinct interpretation and in very dissimilar usage for most applications. So automatically creating domain ontology from heterogeneous sources becomes a big challenge. The semantical paradox and ambiguity must be of concern during the process of building the domain ontology, which means the validation of semantic consistency. The semantic consistency guarantees correct and concise specific domain ontology for all kinds of semantic web applications with multiple data sources.In [2, 7–11], researchers transform structured data (relational database schema) into a middle model and then create a domain ontology from the model. They regard that the relational database is the only data source and that the database is well defined (no ambiguity), which is not always practical. Some semantic preserving properties on transforming are proved, but they do not concern the semantic consistency, which is left for the created domain ontology.As for semistructured data sources, in [4–6], researchers employ a mediate model language for modeling semistructured data and then transform middle models into the domain ontology. The validity checking has been provided while collisions happen, which is generally a syntax checking. Semantic consistency checking is also missed.For building domain ontology from heterogeneous data sources, the semantic consistency checking is necessary. In [12, 13], the same middle formal model language has been adopted to model both structured and semistructured data, so the method can be used to build the domain ontology from heterogeneous data sources. In this paper, we focus on the semantic consistency problem based on this method. The literature [14] develops a middle formal language to describe semistructured data for model-checking purpose and [15] employs graph-based formalism to model semistructured data and queries based on the fixed point computation. We are inspired by the model-checking technology [16], translate the mediate model into a Kripke structure, and encode all semantic query problems into CTL formulae and then we transform the semantic consistency checking problem into a global model-checking procedure.The following Section2 recalls the mediate-model-based method of building domain ontologies and the model-checking technology. In Section 3, the mediate model language is introduced, and the model equivalence is analyzed. And the model-checking-based consistency checking technology is proposed in Section 4 in detail. Some cases are studied in Section 5. Section 6 gives a conclusion.


## 2. Mediate-Model-Based Technology and Model Checking

In this section, the method of formally creating domain with the mediate model [12, 13] and a model-checking technology [16, 17] are introduced.


### 2.1. Formally Creating Domain Ontology

W-graph, a kind of graph-based formal language, is used to model semantic aspect of relationship databases [12]. The main idea is to execute SQL procedures to retrieve the semantic information of the database instances, transform the result sets into a W-graph model, and then transform the model into the ontology autocompletely, which not only maps schemata to the middle model, but also populates the model with data stored in databases. This language is also used to model semantically XML documents in [5]. In [5], they provide XML documents for a semantical interpretation by the W-graph language. The W-graph model created from relationship databases or XML documents can be automatically transformed into a domain ontology (expressed in ontology web language—OWL [18]). And a W-graph is defined as follows.Definition 1.
A W-graphG
w is a directed labeled graph 〈
N
,
E
,
ℓ
〉, where N
=
{
N
a
,
N
c
} is a finite set of nodes, N
a is a finite set ofatomic nodes depicted as ellipses, N
c is a finite set ofcomposite nodes depicted as rectangles, E
⊆
N
c
×
(
𝒞
×
ℒ
)
×
N is a set of labeled edges of the form 〈
m
,
attribute
,
n
〉, ℓ is defined as ℓ
:
N
∪
E
→
𝒞
×
(
ℒ
∪
{
⊥
}
), 𝒞
=
{
solid
,
dashed
}, ℒ is a set of labels, and ⊥ is a symbol for nothing (empty label, can be read as bottom).
Nodes in W-graph always represent objects, and edges represent relationships between nodes. There are two types of concrete W-graph: instances and schemata. An instance can be formally defined as follows.Definition 2.
AW-instance
I is a W-graph such that ℓ
𝒞
(
e
)
=
solid for each edge e of I and ℓ
𝒞
(
n
)
=
solid and ℓ
ℒ
(
n
)
≠
⊥ for each node n of I.In Figure1 a W-instance I is depicted.I
=
〈
N
,
E
,
ℓ
〉, where
N
=
〈
{
n
1
,
n
2
,
n
3
,
n
4
}
,
{
n
5
,
n
6
,
n
7
,
n
8
}
〉,
E
=
〈
(
n
1
,
(
solid
,
teaches
)
,
n
3
)
,
(
n
2
,
(
solid
,
teaches
)
,
n
3
),
(
n
4
,
(
solid
,
attends
)
,
n
3
)
,
(
n
1
,
(
solid
,
age
)
,
n
5
),
(
n
2
,
(
solid
,
age
)
,
n
6
)
,
(
n
3
,
(
solid
,
c
Name
)
,
n
7
),
(
n
4
,
(
solid
,
name
)
,
n
8
)
〉
,
ℓ
(
n
1
)
=
ℓ
(
n
2
)
=
(
solid
,
Teacher
),
ℓ
(
n
3
)
=
(
solid
,
Course
)
,
ℓ
(
n
4
)
=
(
solid
,
Student
),
ℓ
(
n
5
)
=
(
solid
,
37
)
,
ℓ
(
n
6
)
=
(
solid
,
40
),
ℓ
(
n
7
)
=
(
solid
,
Database
)
,
ℓ
(
n
8
)
=
(
solid
,
Smith
).Figure 1
A W-instanceI.It describes the information that two teachers, one 37 years old and another 40 years old, teach database course, and the student Smith attends this course. In W-graph, edge attribute consists of two components, thecolor and thelabel, and the function ℓ returns acolor and alabel (possibly empty, ⊥) for each node. Edge labels are stuck close to the corresponding edges, and node labels are written inside the rectangles representing the nodes. The set of colors 𝒞 denotes how the lines of nodes and edges are drawn (solid ordashed), and we also call this information thecolor of a node or edge. On the other hand, the function ℓ can be seen as the composition of the two single valued functions ℓ
𝒞 and ℓ
ℒ, so ℓ can also be implicitly defined on edges: if e
=
〈
m
,
〈
c
,
k
〉
,
n
〉, then ℓ
𝒞
(
e
)
=
c and ℓ
ℒ
(
e
)
=
k. Two nodes may be connected by more than one edge, provided that edgeattributes are different.For two subsets ofN
,
S, and T
,
T isaccessible from S if for each node n in the set T there is a corresponding node m in the set S such that there exists a path from m to n in W-graph G
w. For example, in the W-instance I of Figure 1, the set {
n
3
,
n
5
,
n
6
,
n
7
,
n
8
} is accessible from the set {
n
1
,
n
2
,
n
4
}.The bisimulation semantics of the language is also given as follows.Definition 3.
Given two W-graphsG
0
=
〈
N
0
,
E
0
,
ℓ
0
〉 and G
1
=
〈
N
1
,
E
1
,
ℓ
1
〉, a relation b is said to be a bisimulation between G
0 and G
1 (write G
0
~
b
G
1) if and only if:(1)
fori
=
0,1, ∀
n
i
∈
N
i, ∃
n
1
-
i
∈
N
1
-
i such that n
i
b
n
1
-
i,
(2)
fori
=
0,1,∀
n
i
∈
N
i,   ∀
n
1
-
i
∈
N
1
-
i, s.t. n
i
b
n
1
-
i
→
ℓ
ℒ
i
(
n
i
)
=
ℓ
ℒ
1
-
i
(
n
1
-
i
)
∨
ℓ
ℒ
i
(
n
i
)
=
⊥
∨
ℓ
ℒ
1
-
i
(
n
1
-
i
)
=
⊥, and
(3)
fori
=
0,1, ∀
n
∈
N
i, let  M
i
(
n
)
=
def
{
〈
m
,
label
〉
:
〈
n
,
〈
color
,
label
〉
,
m
〉
∈
E
i
}. Then, ∀
n
i
∈
N
i, ∀
n
1
-
i
∈
N
1
-
i such that n
i
b
n
1
-
i; for i
=
0,1, it holds that ∀
〈
m
i
,
ℓ
i
〉
∈
M
i
(
n
i
), ∃
〈
m
1
-
i
,
ℓ
1
-
i
〉
∈
M
1
-
i
(
n
1
-
i
)
,
s
.
t
.
m
i
b
m
1
-
i
∧
ℓ
i
=
ℓ
1
-
i.


### 2.2. Model Checking

Model checking is an automated technique that, given a finite-state model of a system and a formal property, systematically checks whether this property holds for (a given state in) the model. Here the finite-state model is always called Kripke structure (an automata-like state transition system), and the formal properties are always expressed by computation tree logic (CTL, a logic that is based on a branching-time view) formulae.Definition 4.
AKripke structure
K
=
〈
Σ
,
Act
,
R
,
I
〉 is a transition system over a set Π of atomic propositions, where Σ is a set of states, Act is a set of actions, R
⊆
Σ
×
Act
×
Σ is a transition relations, and I
:
Σ
→
2
Π is an interpretation.A pathπ in a Kripke structure K
=
〈
Σ
,
Act
,
R
,
I
〉 is an infinite sequence π
=
〈
π
0
,
a
0
,
π
1
,
a
1
,
π
2
,
a
2
,
…
〉 of states and actions (π
i denotes the ith state in the path π), s.t.. For all i
∈
N it holds that π
i
∈
Σ and either 〈
π
i
,
a
i
,
π
i
+
1
〉
∈
R, with a
i
∈
Act, or there are no outgoing transitions from π
i and for all j
⩾
i it holds that a
j is the special action τ (which is not in Act) and π
j
=
π
i.Definition 5.
Given the setsΠ and Act of atomic propositions and actions, computation tree logic (CTL) formulae are recursively defined as follows: (1)
eachp
∈
Π is a CTL formula;
(2)
ifϕ
1 and ϕ
2 are CTL formulae, a
⊆
Act, then ¬
ϕ
1, ϕ
1
∧
ϕ
2, A
X
a
(
ϕ
1
), E
X
a
(
ϕ
1
), A
U
a
(
ϕ
1
,
ϕ
2
), and E
U
a
(
ϕ
1
,
ϕ
2
) are CTL formulae.A andE are the universal and existential path quantifiers, while neXt (X) and Until (U) are the linear-time modalities. Composition of formulae of the form ϕ
1
∨
ϕ
2
,
ϕ
1
→
ϕ
2 can be, respectively, defined by ¬
(
¬
ϕ
1
∧
¬
ϕ
2
) and ¬
ϕ
1
∨
ϕ
2, and the modalities Finally (F) and Generally (G) can be defined in terms of the CTL formulae: F
(
ϕ
)
=
U
(true,
ϕ
) and G
(
ϕ
)
=
¬
F
(
¬
ϕ
).Definition 6.
Satisfaction of a CTL formula by a states of the Kripke structure K
=
〈
Σ
,
Act
,
R
,
I
〉 is defined recursively as follows: (i)
ifp
∈
Π, then s
⊨
p iff p
∈
I
(
s
). Moreover, s
⊨
true, and s
⊭
false;
(ii)
s
⊨
¬
p iif s
⊭
p;
(iii)
s
⊨
ϕ
1
∧
ϕ
2 iff s
⊨
ϕ
1 and s
⊨
ϕ
2;
(iv)
s
⊨
E
X
a
(
ϕ
) iff there is a path π
=
〈
s
,
x
,
π
1
,
…
〉 s.t. x
∈
a and π
1
⊨
ϕ;
(v)
s
⊨
A
X
a
(
ϕ
) iff for all paths π
=
〈
s
,
x
,
π
1
,
…
〉, x
∈
a implies π
1
⊨
ϕ;
(vi)
s
⊨
E
U
a
(
ϕ
1
,
ϕ
2
) iff there is a path π
=
〈
π
0
,
x
0
,
π
1
,
x
1
,
…
〉, and ∃
j
∈
ℕ s.t. π
0
=
s, π
j
⊨
ϕ
2, and ∀
i
<
j
,
(
π
i
⊨
ϕ
1 and x
i
∈
a
);
(vii)
s
⊨
A
U
a
(
ϕ
1
,
ϕ
2
) iff for all paths π
=
〈
π
0
,
x
0
,
π
1
,
x
1
,
…
〉, s.t. π
0
=
s, ∃
j
∈
ℕ, π
j
⊨
ϕ
2, and ∀
i
<
j
,
(
π
i
⊨
ϕ
1 and x
i
∈
a
).Definition 7 (the model-checking problem).
Local model-checking: given a Kripke structure K, a formula ϕ, and a state s of K, the local model-checking is to verify whether s
⊨
ϕ.Global model-checking: given a Kripke structure K, and a formula ϕ, the global model-checking is to find all states s of K such that s
⊨
ϕ.IfΣ is finite, the global model-checking problem for a CTL formula ϕ can be solved in linear running time on |
ϕ
|
·
(
|
Σ
|
+
|
R
|
), where |
ϕ
| is the length of formula ϕ and |
Σ
| is the number of elements in the set Σ, |
R
| is the elements number of the transition relations set R [16].


## 2.1. Formally Creating Domain Ontology

W-graph, a kind of graph-based formal language, is used to model semantic aspect of relationship databases [12]. The main idea is to execute SQL procedures to retrieve the semantic information of the database instances, transform the result sets into a W-graph model, and then transform the model into the ontology autocompletely, which not only maps schemata to the middle model, but also populates the model with data stored in databases. This language is also used to model semantically XML documents in [5]. In [5], they provide XML documents for a semantical interpretation by the W-graph language. The W-graph model created from relationship databases or XML documents can be automatically transformed into a domain ontology (expressed in ontology web language—OWL [18]). And a W-graph is defined as follows.Definition 1.
A W-graphG
w is a directed labeled graph 〈
N
,
E
,
ℓ
〉, where N
=
{
N
a
,
N
c
} is a finite set of nodes, N
a is a finite set ofatomic nodes depicted as ellipses, N
c is a finite set ofcomposite nodes depicted as rectangles, E
⊆
N
c
×
(
𝒞
×
ℒ
)
×
N is a set of labeled edges of the form 〈
m
,
attribute
,
n
〉, ℓ is defined as ℓ
:
N
∪
E
→
𝒞
×
(
ℒ
∪
{
⊥
}
), 𝒞
=
{
solid
,
dashed
}, ℒ is a set of labels, and ⊥ is a symbol for nothing (empty label, can be read as bottom).
Nodes in W-graph always represent objects, and edges represent relationships between nodes. There are two types of concrete W-graph: instances and schemata. An instance can be formally defined as follows.Definition 2.
AW-instance
I is a W-graph such that ℓ
𝒞
(
e
)
=
solid for each edge e of I and ℓ
𝒞
(
n
)
=
solid and ℓ
ℒ
(
n
)
≠
⊥ for each node n of I.In Figure1 a W-instance I is depicted.I
=
〈
N
,
E
,
ℓ
〉, where
N
=
〈
{
n
1
,
n
2
,
n
3
,
n
4
}
,
{
n
5
,
n
6
,
n
7
,
n
8
}
〉,
E
=
〈
(
n
1
,
(
solid
,
teaches
)
,
n
3
)
,
(
n
2
,
(
solid
,
teaches
)
,
n
3
),
(
n
4
,
(
solid
,
attends
)
,
n
3
)
,
(
n
1
,
(
solid
,
age
)
,
n
5
),
(
n
2
,
(
solid
,
age
)
,
n
6
)
,
(
n
3
,
(
solid
,
c
Name
)
,
n
7
),
(
n
4
,
(
solid
,
name
)
,
n
8
)
〉
,
ℓ
(
n
1
)
=
ℓ
(
n
2
)
=
(
solid
,
Teacher
),
ℓ
(
n
3
)
=
(
solid
,
Course
)
,
ℓ
(
n
4
)
=
(
solid
,
Student
),
ℓ
(
n
5
)
=
(
solid
,
37
)
,
ℓ
(
n
6
)
=
(
solid
,
40
),
ℓ
(
n
7
)
=
(
solid
,
Database
)
,
ℓ
(
n
8
)
=
(
solid
,
Smith
).Figure 1
A W-instanceI.It describes the information that two teachers, one 37 years old and another 40 years old, teach database course, and the student Smith attends this course. In W-graph, edge attribute consists of two components, thecolor and thelabel, and the function ℓ returns acolor and alabel (possibly empty, ⊥) for each node. Edge labels are stuck close to the corresponding edges, and node labels are written inside the rectangles representing the nodes. The set of colors 𝒞 denotes how the lines of nodes and edges are drawn (solid ordashed), and we also call this information thecolor of a node or edge. On the other hand, the function ℓ can be seen as the composition of the two single valued functions ℓ
𝒞 and ℓ
ℒ, so ℓ can also be implicitly defined on edges: if e
=
〈
m
,
〈
c
,
k
〉
,
n
〉, then ℓ
𝒞
(
e
)
=
c and ℓ
ℒ
(
e
)
=
k. Two nodes may be connected by more than one edge, provided that edgeattributes are different.For two subsets ofN
,
S, and T
,
T isaccessible from S if for each node n in the set T there is a corresponding node m in the set S such that there exists a path from m to n in W-graph G
w. For example, in the W-instance I of Figure 1, the set {
n
3
,
n
5
,
n
6
,
n
7
,
n
8
} is accessible from the set {
n
1
,
n
2
,
n
4
}.The bisimulation semantics of the language is also given as follows.Definition 3.
Given two W-graphsG
0
=
〈
N
0
,
E
0
,
ℓ
0
〉 and G
1
=
〈
N
1
,
E
1
,
ℓ
1
〉, a relation b is said to be a bisimulation between G
0 and G
1 (write G
0
~
b
G
1) if and only if:(1)
fori
=
0,1, ∀
n
i
∈
N
i, ∃
n
1
-
i
∈
N
1
-
i such that n
i
b
n
1
-
i,
(2)
fori
=
0,1,∀
n
i
∈
N
i,   ∀
n
1
-
i
∈
N
1
-
i, s.t. n
i
b
n
1
-
i
→
ℓ
ℒ
i
(
n
i
)
=
ℓ
ℒ
1
-
i
(
n
1
-
i
)
∨
ℓ
ℒ
i
(
n
i
)
=
⊥
∨
ℓ
ℒ
1
-
i
(
n
1
-
i
)
=
⊥, and
(3)
fori
=
0,1, ∀
n
∈
N
i, let  M
i
(
n
)
=
def
{
〈
m
,
label
〉
:
〈
n
,
〈
color
,
label
〉
,
m
〉
∈
E
i
}. Then, ∀
n
i
∈
N
i, ∀
n
1
-
i
∈
N
1
-
i such that n
i
b
n
1
-
i; for i
=
0,1, it holds that ∀
〈
m
i
,
ℓ
i
〉
∈
M
i
(
n
i
), ∃
〈
m
1
-
i
,
ℓ
1
-
i
〉
∈
M
1
-
i
(
n
1
-
i
)
,
s
.
t
.
m
i
b
m
1
-
i
∧
ℓ
i
=
ℓ
1
-
i.


## 2.2. Model Checking

Model checking is an automated technique that, given a finite-state model of a system and a formal property, systematically checks whether this property holds for (a given state in) the model. Here the finite-state model is always called Kripke structure (an automata-like state transition system), and the formal properties are always expressed by computation tree logic (CTL, a logic that is based on a branching-time view) formulae.Definition 4.
AKripke structure
K
=
〈
Σ
,
Act
,
R
,
I
〉 is a transition system over a set Π of atomic propositions, where Σ is a set of states, Act is a set of actions, R
⊆
Σ
×
Act
×
Σ is a transition relations, and I
:
Σ
→
2
Π is an interpretation.A pathπ in a Kripke structure K
=
〈
Σ
,
Act
,
R
,
I
〉 is an infinite sequence π
=
〈
π
0
,
a
0
,
π
1
,
a
1
,
π
2
,
a
2
,
…
〉 of states and actions (π
i denotes the ith state in the path π), s.t.. For all i
∈
N it holds that π
i
∈
Σ and either 〈
π
i
,
a
i
,
π
i
+
1
〉
∈
R, with a
i
∈
Act, or there are no outgoing transitions from π
i and for all j
⩾
i it holds that a
j is the special action τ (which is not in Act) and π
j
=
π
i.Definition 5.
Given the setsΠ and Act of atomic propositions and actions, computation tree logic (CTL) formulae are recursively defined as follows: (1)
eachp
∈
Π is a CTL formula;
(2)
ifϕ
1 and ϕ
2 are CTL formulae, a
⊆
Act, then ¬
ϕ
1, ϕ
1
∧
ϕ
2, A
X
a
(
ϕ
1
), E
X
a
(
ϕ
1
), A
U
a
(
ϕ
1
,
ϕ
2
), and E
U
a
(
ϕ
1
,
ϕ
2
) are CTL formulae.A andE are the universal and existential path quantifiers, while neXt (X) and Until (U) are the linear-time modalities. Composition of formulae of the form ϕ
1
∨
ϕ
2
,
ϕ
1
→
ϕ
2 can be, respectively, defined by ¬
(
¬
ϕ
1
∧
¬
ϕ
2
) and ¬
ϕ
1
∨
ϕ
2, and the modalities Finally (F) and Generally (G) can be defined in terms of the CTL formulae: F
(
ϕ
)
=
U
(true,
ϕ
) and G
(
ϕ
)
=
¬
F
(
¬
ϕ
).Definition 6.
Satisfaction of a CTL formula by a states of the Kripke structure K
=
〈
Σ
,
Act
,
R
,
I
〉 is defined recursively as follows: (i)
ifp
∈
Π, then s
⊨
p iff p
∈
I
(
s
). Moreover, s
⊨
true, and s
⊭
false;
(ii)
s
⊨
¬
p iif s
⊭
p;
(iii)
s
⊨
ϕ
1
∧
ϕ
2 iff s
⊨
ϕ
1 and s
⊨
ϕ
2;
(iv)
s
⊨
E
X
a
(
ϕ
) iff there is a path π
=
〈
s
,
x
,
π
1
,
…
〉 s.t. x
∈
a and π
1
⊨
ϕ;
(v)
s
⊨
A
X
a
(
ϕ
) iff for all paths π
=
〈
s
,
x
,
π
1
,
…
〉, x
∈
a implies π
1
⊨
ϕ;
(vi)
s
⊨
E
U
a
(
ϕ
1
,
ϕ
2
) iff there is a path π
=
〈
π
0
,
x
0
,
π
1
,
x
1
,
…
〉, and ∃
j
∈
ℕ s.t. π
0
=
s, π
j
⊨
ϕ
2, and ∀
i
<
j
,
(
π
i
⊨
ϕ
1 and x
i
∈
a
);
(vii)
s
⊨
A
U
a
(
ϕ
1
,
ϕ
2
) iff for all paths π
=
〈
π
0
,
x
0
,
π
1
,
x
1
,
…
〉, s.t. π
0
=
s, ∃
j
∈
ℕ, π
j
⊨
ϕ
2, and ∀
i
<
j
,
(
π
i
⊨
ϕ
1 and x
i
∈
a
).Definition 7 (the model-checking problem).
Local model-checking: given a Kripke structure K, a formula ϕ, and a state s of K, the local model-checking is to verify whether s
⊨
ϕ.Global model-checking: given a Kripke structure K, and a formula ϕ, the global model-checking is to find all states s of K such that s
⊨
ϕ.IfΣ is finite, the global model-checking problem for a CTL formula ϕ can be solved in linear running time on |
ϕ
|
·
(
|
Σ
|
+
|
R
|
), where |
ϕ
| is the length of formula ϕ and |
Σ
| is the number of elements in the set Σ, |
R
| is the elements number of the transition relations set R [16].


## 3. Modeling Semantic Inconsistency

When a language has been used to semantically model different data sources for building the same domain ontology, the semantic collision becomes prominent, so the consistency checking is inevitable. Even from a single data source, the incremental procedure of building the semantical model may fail when a new snippet collides semantically with some model segments that existed. Therefore, ambiguities should be detected in order to get correct semantical model during building a domain ontology. The semantic consistency checking is a mechanism for checking whether the model is semantic unambiguity or paradox.Two kinds of problems would be of concern: redundancy and paradox. The redundancy-free can reduce the size of the model and accelerate modeling procedure. For the middle-model language W-graph, according to Definition3, two equivalent models (or model segments) cause a redundancy.As far as the paradox is concerned, there are four types of inconsistency: concept inconsistency, relationship inconsistency, attribute inconsistency, and fact inconsistencies. Before discussing details of these inconsistencies, another special W-graph, so-called W-schema, will be presented. The schema gives a pattern to organize data for an instance. The schema of W-instance is also a W-graph, and it could be defined formally as follows.Definition 8.
AW-schema
S is a W-graph such that ℓ
𝒞
(
e
)
=
solid for each edge e of S and ℓ
𝒞
(
n
)
=
solid and ℓ
ℒ
(
n
)
=
⊥ for each node n of S; that is, a schema has no values.For example, Figure2 depicts the W-schema of the W-instance I in Figure 1. So the W-graph language can be used to model semantic aspects of the knowledge, nodes for concepts, edges for relationships between them, W-schemata for the patterns of the knowledge, and W-instances for the concrete contents of that knowledge. Now we will discuss the details of each inconsistency based on the W-graph.Figure 2
A W-schemaS of I.Concept Redundancy. During the procedure of building semantic model, if a new concept occurs, then we add this concept to the model (add a new node to the W-schema). If a concept paradox occurs, then we also add a new concept to the model. But concepts redundancy will occur if we find two concepts (different names, of course) getting the same attribute set and relationship set. Concepts redundancy always occurs in the W-schema. For example, Figure 3 shows thatTeacher andTutor are the same concepts here. There is not a new conceptTutor to be added into the model, but a new synonym ofTeacher can be annotated by only one edge labeled “synonym.”Figure 3
A concept redundancy.We define concept redundancy as follows.Definition 9.
In the W-graph〈
N
,
E
,
ℓ
〉, two concepts C
1 and C
2 (expressed as nodes n
1
,
n
2) are redundancy when they get the same adjacent nodes set and edges set:C
1
≈
C
2
iff
|
{
n
∣
(
n
,
n
1
)
∈
E
}
|
=
|
{
m
∣
(
m
,
n
2
)
∈
E
}
|, |
{
n
∣
(
n
1
,
n
)
∈
E
}
|
=
|
{
m
∣
(
n
2
,
m
)
∈
E
| and for all m and corresponding n such that m
~
n.Here,m
~
n means that after omitting concepts nodes n
1, n
2 and their adjacent edges the subgraph M including node m bisimulates the subgraph N including node n. Computing m
~
n is an iterative process. For deciding whether m
~
n, we delete node m and its adjacent edges from M and node n and its adjacent edges from N and then decide whether the two smaller subgraphs are bisimulation. The iterative process will terminate because the nodes and edges are finite.Relationships Inconsistency. When a new relationship between concepts during modeling process is found, the relationship cannot be added directly into the model, because sometimes the inconsistency will occur. Firstly, if the relationship is redundant according to the bisimulation, it should be ignored. Secondly, if the relationship is added into the model, we must ensure not to introduce some paradox into the model; otherwise, the relationship inconsistency occurs. For example, Figure 4 shows that the relationship “Student teaches Teacher” should cause a paradox. The relationship may be found from XML documents “Teacher teaches students knowledge, and meanwhile teacher also learns something from students.” The relationship “teacher learns from students” may be understood as “Student teaches Teacher,” but this contradicts “Teacher teaches Student” relationship, which is reasoned from “Teacher teaches Course” and “Student attends the Course.”Figure 4
A relationship inconsistency.The paradox relationship can be formally defined as follows.Definition 10.
In the W-graph〈
N
,
E
,
ℓ
〉, a paradox relationship between node n
1 and node n
2 is that (
n
1
,
n
2
)
∈
E and (
n
2
,
n
1
)
∈
E, where ℓ
(
(
n
1
,
n
2
)
)
=
ℓ
(
(
n
2
,
n
1
)
).Attribute Inconsistency. The attributes of concepts are another kind of relationship, so-called “isa” or “hasa” relationship. So attribute inconsistency is a kind of relationship inconsistency, but simpler.Fact Inconsistency. This kind of inconsistency occurs in the W-instance. Facts are the individuals of concepts or attributes. When creating W-instance by populating data from the heterogeneous sources, lots of facts inconsistencies may occur. In Figure 5(a), an attribute fact inconsistency will happen if the fact “age is 40” is added into the model, where the teacher named Charley gets two different ages. And in Figure 5(b), the Teacher2 gets all the same value set of attributes, so Teacher1 and Teacher2 are the concept fact inconsistency. Therefore, the two facts “age is 40” and “Teacher2” cannot be added into the model.A fact inconsistency.
(a)
(b)The fact inconsistency is formally defined as follows.Definition 11.
In the W-instance〈
N
,
E
,
ℓ
〉 where N
=
{
N
a
,
N
c
}, two facts n
1
,
n
2
∈
N are said to be inconsistent if (1)
forn
1
,
n
2
∈
N
a, ∃
m
∈
N
c s.t. ℓ
(
(
m
,
n
1
)
)
=
ℓ
(
(
m
,
n
2
)
) and ℓ
(
n
1
)
≠
ℓ
(
n
2
) or
(2)
forn
1
,
n
2
∈
N
c, ∀
m
1
∈
N
a
,
(
n
1
,
m
1
)
∈
E and m
2
∈
N
a
,
(
n
2
,
m
2
)
∈
E s.t. ℓ
(
(
n
1
,
m
1
)
)
=
ℓ
(
(
n
2
,
m
2
)
) and ℓ
(
m
1
)
=
ℓ
(
m
2
).For all these inconsistencies, the core problem is how to discovery the redundancy and paradox in the model. In fact, the procedure of discovery is a subgraph query problem in W-graph.Definition 12.
For a W-graphG
=
〈
N
,
E
,
ℓ
〉, a subgraph of G is also a W-graph G
s
=
〈
N
s
,
E
s
,
ℓ
s
〉, where N
s
=
{
n
∈
N
:
ℓ
𝒞
(
n
)
=
solid
} and E
s
=
{
(
m
,
(
solid
,
ℓ
)
,
n
)
:
m
,
n
∈
N
s
}. Furthermore, given two sets of nodes S
,
T
⊆
N, T is accessible from S if for each n
∈
T there is a node m
∈
S such that there is a path in G from m to n.Definition 13.
A W-query is a pointed W-graph, namely, a pair〈
G
,
ν
〉 with ν as a node of G (the point). A W-query 〈
G
,
ν
〉 is accessible if the set N of nodes of G is accessible from {
ν
}.For example, in Figure6 three W-queries are depicted. The thick arrows are theirpoints, and they are W-queries. Intuitively, the meaning of the first query is to collect all the teachers aged 37. The second query asks for all the teachers that have declared an age (observe the use of an undefined node). The third query, instead, requires collecting all the teachers that teach some courses but not Database, where dashed nodes and lines are introduced to allow a form of negation.Three W-queries.
(a)
(b)
(c)According to Definition13, an inconsistency checking problem is indeed a query problem in the partial W-graph model. Meanwhile, the semantic equivalence must be of concern during query processing. We call this asemantical equivalence query problem. For the incremental procedure of building domain ontology, a semantical equivalence querying should be executed as soon as each new element (concept, relationship, attribute or fact) is added into the model. So, the semantic equivalence querying problem is the basic problem for the consistency checking.However, the semantical equivalence querying problem for a W-graph model is the subgraph-isomorphism problem, which is NP problem in general. In this paper, we employ model-checking technology to handle semantical equivalence query problem in order to avoid computing subgraph isomorphism.


## 4. Consistency Checking

In order to employ model-checking technology, we can see a W-graph model as a Kripke structure and a semantical equivalency query as a formula of the temporal logic CTL. In this way, the inconsistency checking problem is reduced to the problem of finding out the states of the model which satisfy the formula (the model-checking problem) that can be done in linear time.


### 4.1. W-Graph as Kripke Structure

With the following definition, we can build Kripke structure from W-graph.Definition 14.
LetG
=
〈
N
,
E
,
ℓ
〉 be a W-graph, the Kripke structure K
G
=
〈
Σ
G
,
Ac
t
G
,
R
G
,
I
G
〉 over the set of atomic properties Π
G is defined as follows: (i)
Π
G is the set of all node labels of G, Π
G
=
{
p
∣
∀
n
∈
N
,
p
=
ℓ
(
n
)
}.
(ii)
The set of statesΣ
G
=
N.
(iii)
The set of actionsAc
t
G
=
{
p
∣
∃
m
,
n
∈
N
,
(
m
,
p
,
n
)
∈
E
}
∪
{
p
-
1
∣
∃
m
,
n
∈
N
,
(
m
,
p
,
n
)
∈
E
}
∪
{
p
¯
∣
∃
m
,
n
∈
N
,
(
m
,
p
,
n
)
∈
E
}; that is, the set of actions includes all the edge labels, negative labels (express as p
¯), and their inverse labels (express as p
-
1
,
p
¯
-
1); note that negative labels are very different from inverse labels. A negative label edge expresses that there is no special relationship (i.e., “label” relationship) between two nodes, but an inverse label edge expresses that there is a special relationship (i.e., inverse relationship) between this two nodes.
(iv)
The ternary transition relationR
G
=
E
∪
{
(
n
,
p
-
1
,
m
)
∣
(
m
,
p
,
n
)
∈
E
}. Moreover, assume that, for each state s with no outgoing edge in E (a leaf in G), a self-loop edge labeled by the special action τ is added.
(v)
The interpretation functionI
G
(
n
)
=
{
true
,
ℓ
ℒ
(
n
)
}, where n
∈
N. That is, in each state n the only formulae that hold are the unary atom ℓ
ℒ
(
n
) and true.For instance, consider the W-graph of Figure1. It holds the following:(i)
Π
G
=
{
Teacher, Course, Student, 37, 40, Databases, Smith
},
(ii)
Σ
G
=
{
n
1, n
2, …, n
8
},
(iii)
Ac
t
G
=
{
age,ag
e
-
1, age
¯, age
¯
-
1, teaches, teache
s
-
1, teaches
¯, teaches
¯
-
1, attends
,
attend
s
-
1, attends
¯
,
attends
¯
-
1, name
,
nam
e
-
1, name
¯, nam
e
-
1, c
Name, c
Nam
e
-
1, c
Name
¯, c
Name
¯
-
1
},
(iv)
R
G
=
{
(
n
1, age, n
5
), (
n
5, ag
e
-
1
,
n
1
), (
n
1, teaches
,
n
3
), (
n
3, teache
s
-
1, n
1
), (
n
2, age, n
6
), (
n
6
,
ag
e
-
1
,
n
2
), (
n
2, teaches, n
3
), (
n
3, teache
s
-
1,n
2
), (
n
4, attends,n
3
),(
n
3, attend
s
-
1,n
4
), (
n
3,c
Name,n
7
), (
n
7, c
Nam
e
-
1, n
3
), (
n
4, name, n
8
), (
n
8, nam
e
-
1, n
4
), (
n
5, τ, n
5
), (
n
6, τ, n
6
), (
n
7, τ,n
7
),(
n
8, τ, n
8
)
},
(v)
I
G
=
{
I
G
(
n
1
)
=
{
true, Teacher
}, I
G
(
n
2
)
=
{
true, Teacher
}, I
G
(
n
3
)
=
{
true
,
Course
}, I
G
(
n
4
)
=
{
true, Student
}, I
G
(
n
5
)
=
{
true, 37
}, I
G
(
n
6
)
=
{
true, 40
}, I
G
(
n
7
)
=
{
true, Database
}, I
G
(
n
8
)
=
{
true, Smith
}
}.And this Kripke structure is shown in Figure 7.Figure 7
The Kripke structure of Figure1.


### 4.2. Query as CTL Formula

Reviewing the W-query in Figure6(a), intuitively, the CTL formula must express the statement “the state Teacher formula is true and there is one next state reachable by an edge labeled age, where the 37 formula is true,” this is to say
(1)
Teacher
∧
E
X
age
(
37
)
.
For the query in Figure 6(b), the CTL formula should be written as
(2)
Teacher
∧
E
X
age
(
true
)
,
For the query of Figure 6(c), we get the following formula:
(3)
Teacher
∧
E
X
teaches
(
Course
)
∧
A
X
c
name
(
¬
Database
)
.
This formula is true if “there is a node labeled Teacher and there exists one next node labeled Course, which is reachable by an edge labeled teaches, such that for all next to Course nodes labeled Database, the relation cName is not fulfilled”. Let us then consider how to encode W-queries in CTL formulae. We study the situation that W-graph and W-query are both acyclic. Firstly, we define an auxiliary function to simply handle labels of nodes and edges in W-graph.Definition 15.
LetG
=
〈
N
,
E
,
ℓ
〉 be a W-graph, for all nodes n
∈
N and for all edges e
=
〈
n
1
,
(
c
,
p
)
,
n
2
〉
∈
E; an auxiliary function φ is defined as
(4)
φ
(
n
)
=
{
ℓ
ℒ
(
n
)
,
if
ℓ
ℒ
(
n
)
≠
⊥
t
r
u
e
,
otherwise
φ
(
e
)
=
{
p
,
if
ℓ
𝒞
(
e
)
=
ℓ
𝒞
(
n
2
)
,
p
¯
,
otherwise
.And the query translation can be formally defined as follows.Definition 16.
LetG
=
〈
N
,
E
,
ℓ
〉 be a acyclic W-graph, ν
∈
N, and let Q
=
〈
G
,
ν
〉 be an accessible query. The formula associated with Q is Ψ
ν
(
G
), where Ψ
ν
(
G
) is defined recursively as follows: (i)
letb
1
,
…
,
b
h
(
h
≥
0
) be the successors of ν, s.t. ℓ
𝒞
(
b
i
)
=
solid,
(ii)
letc
1
,
…
,
c
k
(
k
≥
0
) be the successors of ν, s.t. ℓ
𝒞
(
c
i
)
=
dashed
(iii)
fori
=
1
,
…
,
h and j
=
1
,
…
,
k, let e
i be the edge which links ν to b
i and e
i
′ the one which links ν to c
j. If ℓ
𝒞
(
ν
)
=
solid, then
(5)
Ψ
ν
(
G
)
=
φ
(
ν
)
∧
⋀
i
=
1
,
…
,
h
E
X
φ
(
e
i
)
(
Ψ
b
i
(
G
)
)
∧
⋀
j
=
1
,
…
,
k
A
X
φ
(
e
j
′
)
(
Ψ
c
j
(
G
)
)
else
(
ℓ
𝒞
(
ν
)
=
dashed
)
Ψ
ν
(
G
)
=
¬
φ
(
ν
)
∨
⋁
i
=
1
,
…
,
h
A
X
φ
(
e
i
)
(
Ψ
b
i
(
G
)
)
∨
⋁
j
=
1
,
…
,
k
E
X
φ
(
e
j
′
)
(
Ψ
c
j
(
G
)
)
.The construction of the formula involves the unfolding of a directed acyclic graph; the size of the formulaΨ
ν
(
G
) (written as |
Ψ
ν
(
G
)
|) can grow exponentially with respect to|
G
|. Although that, it is easy to compute the formula without repetitions of subformulae and keep the memory allocation linear w.r.t. |
G
|, so it is natural to compactly represent the formula using a linear amount of memory. This compact representation is allowed by the model-checker NuSMV [19].Theorem 17.
Given a W-instanceI and a W-query 〈
G
,
ν
〉, let K
I be the Kripke structure associated with I and Ψ
ν
(
G
) the CTL formula associated with 〈
G
,
ν
〉. Consistency checking I with 〈
G
,
ν
〉 can be done in linear time on |
I
|
·
|
Ψ
ν
(
G
)
|.Proof.
For achieving the consistency checking procedure, there are three steps to follow, translating the W-graph into a Kripke structure, encoding the W-query into a CTL formula, and executing a model-checking process.
Assuming that|
I
|
=
|
N
|
+
|
E
|, where |
N
| is the number of nodes in W-instance I and |
E
| is the number of edges in this graph, notating K
I
=
〈
Σ
I
,
Ac
t
I
,
R
I
,
I
I
〉, expressing |
Σ
I
|
,
|
Ac
t
I
|
,
|
R
I
| as the number of states, actions, and transition relations in |
K
I
|, and writing |
Ψ
ν
(
G
)
| as the length of the CTL formula Ψ
ν
(
G
), then the complexity issues can be analyzed.
Firstly, when creating the Kripke structure, for each node, action, and transitional relation that must be created one by one, the time complexity should be|
Σ
I
|
+
|
Ac
t
I
|
+
|
R
I
|
≤
|
N
|
+
4
|
E
|
+
3
|
E
|
=
O
(
|
I
|
), according to Definition 14. Secondly, we consider the length of the encoded CTL formula |
Ψ
ν
(
G
)
|
≤
|
G
|
=
O
(
|
G
|
), because the worst situation is to encode the whole W-graph into a formula, where |
G
| is the total number of edges and nodes in this query. The last step is to execute model-checking procedure; the time complexity is |
Ψ
ν
(
G
)
|
·
(
|
Σ
I
|
+
|
R
I
|
)
=
O
(
|
G
|
·
|
I
|
) according to [16]. So the total time complexity is O
(
|
I
|
)
+
O
(
|
G
|
)
+
O
(
|
G
|
·
|
I
|
), which is a linear time on |
I
|
·
|
Ψ
ν
(
G
)
|.
If we think that the|
G
| is always less than or equal to |
I
| (intuitively, it is always so), then O
(
|
I
|
)
+
O
(
|
G
|
)
+
O
(
|
G
|
·
|
I
|
)
≤
O
(
|
I
|
2
)
+
O
(
|
I
|
), which is a polynomial time over |
I
|.The equivalence between two segments of W-graph is the equivalence between two CTL formulae, which can be formally proved in linear time. The consistency checking problem for the W-graph model is promoted to the equivalence proof problem for the CTL formulae with a Kripke structure.


### 4.3. Checking Consistency

During the procedure of extracting a domain ontology gradually from heterogeneous data sources, semantic consistency has to be checked. According to Definitions14 and 16, after encoding a W-graph to a Kripke structure and a W-query to a CTL formula, the semantic equivalent query problem on the W-graph has been promoted to a global model-checking problem.Definition 18.
Given a W-instanceI and a W-query 〈
G
,
ν
〉, let K
I be the Kripke structure associated with I and Ψ
ν
(
G
) the CTL formula associated with 〈
G
,
ν
〉. The Consistency checking I with 〈
G
,
ν
〉 amounts to solve the global model-checking problem with the Kripke structure K
I and the CTL formula Ψ
ν
(
G
), namely, to find all the states s of K
I such that s
⊨
Ψ
ν
(
G
). Algorithm 1 describes this procedure.Algorithm 1:Semantic consistency checking.
Require:  I, // W-graph semantic model
〈
G
,
ν
〉 // semantic segment expressed by W-query
Ensure:  consistent or inconsistent
encoding  I  to  K
I; // according to Definition 14
encoding  〈
G
,
ν
〉  to  Ψ
ν
(
G
); // according to Definition 16
S
=
{
s∣s
⊨
Ψ
ν
(
G
)
}; // model checking
if  S is emptyset  then
return  consistent;
else
return  inconsistent;
end ifSo semantic consistency checking can be done with model-checking technology. Let us consider each type of inconsistency defined above. As for concepts inconsistency, it is to find out whether there is another concept (equivalent toC) in W-schema S, which has been built to be extended, when a new concept C has been added into the W-schema S. This is to say, a W-query Q
=
〈
S
,
C
〉 should be imposed on the S for consistency checking. Let K
S be the Kripke structure of S and let Ψ
C
(
S
)
=
φ
(
C
) be the CTL formula of Q and we should find all states s of K
S such that s
⊨
φ
(
C
).As far as relationship inconsistency is concerned, it is to query a W-graphG with a W-query Q
=
〈
G
,
n
1
〉 before a new relationship (
n
1
,
n
2
) is added into the W-graph model. Let K
G be the Kripke structure of G, and the CTL formula is
(6)
Ψ
n
1
(
G
)
=
φ
(
n
1
)
∧
E
X
φ
(
(
n
1
,
n
2
)
)
(
n
2
)
.
The consistency checking is to find all states s of K
G such that s
⊨
Ψ
n
1
(
G
). If the states like this cannot be found, then the model is consistent after adding the new relationship (
n
1
,
n
2
); if any state has been found, then the model will be inconsistent and the new relationship cannot be added into the model. This is the relationship redundant inconsistency. As for paradox relationship paradox inconsistency, the CTL formula is
(7)
Ψ
n
2
(
G
)
=
φ
(
n
2
)
∧
E
X
φ
(
(
n
1
,
n
2
)
)
(
n
1
)
.As for fact consistency checking, the Kripke structure of the W-instanceI is K
I, and the CTL formula for the attribute fact (the instance m of a concept has the concrete attribute value n, i.e., (
m
,
n
)) inconsistency is
(8)
Ψ
m
(
I
)
=
φ
(
m
)
∧
E
X
φ
(
(
m
,
n
)
)
(
n
)
.
The CTL formula for the concept fact (the instance m of one concept to be added into the model) inconsistency is
(9)
Ψ
m
(
I
)
=
φ
(
m
)
∧
⋀
j
=
1
,
…
,
k
A
X
φ
(
(
m
,
n
j
)
)
(
Ψ
n
j
(
I
)
)
,
where n
j
,
j
=
1
,
…
,
k are all successors of m. If some states of K
I satisfy the above formula, then the inconsistency occurs. This is to say, a fact m cannot be added into the model if an equivalent fact has already existed in the model.


## 4.1. W-Graph as Kripke Structure

With the following definition, we can build Kripke structure from W-graph.Definition 14.
LetG
=
〈
N
,
E
,
ℓ
〉 be a W-graph, the Kripke structure K
G
=
〈
Σ
G
,
Ac
t
G
,
R
G
,
I
G
〉 over the set of atomic properties Π
G is defined as follows: (i)
Π
G is the set of all node labels of G, Π
G
=
{
p
∣
∀
n
∈
N
,
p
=
ℓ
(
n
)
}.
(ii)
The set of statesΣ
G
=
N.
(iii)
The set of actionsAc
t
G
=
{
p
∣
∃
m
,
n
∈
N
,
(
m
,
p
,
n
)
∈
E
}
∪
{
p
-
1
∣
∃
m
,
n
∈
N
,
(
m
,
p
,
n
)
∈
E
}
∪
{
p
¯
∣
∃
m
,
n
∈
N
,
(
m
,
p
,
n
)
∈
E
}; that is, the set of actions includes all the edge labels, negative labels (express as p
¯), and their inverse labels (express as p
-
1
,
p
¯
-
1); note that negative labels are very different from inverse labels. A negative label edge expresses that there is no special relationship (i.e., “label” relationship) between two nodes, but an inverse label edge expresses that there is a special relationship (i.e., inverse relationship) between this two nodes.
(iv)
The ternary transition relationR
G
=
E
∪
{
(
n
,
p
-
1
,
m
)
∣
(
m
,
p
,
n
)
∈
E
}. Moreover, assume that, for each state s with no outgoing edge in E (a leaf in G), a self-loop edge labeled by the special action τ is added.
(v)
The interpretation functionI
G
(
n
)
=
{
true
,
ℓ
ℒ
(
n
)
}, where n
∈
N. That is, in each state n the only formulae that hold are the unary atom ℓ
ℒ
(
n
) and true.For instance, consider the W-graph of Figure1. It holds the following:(i)
Π
G
=
{
Teacher, Course, Student, 37, 40, Databases, Smith
},
(ii)
Σ
G
=
{
n
1, n
2, …, n
8
},
(iii)
Ac
t
G
=
{
age,ag
e
-
1, age
¯, age
¯
-
1, teaches, teache
s
-
1, teaches
¯, teaches
¯
-
1, attends
,
attend
s
-
1, attends
¯
,
attends
¯
-
1, name
,
nam
e
-
1, name
¯, nam
e
-
1, c
Name, c
Nam
e
-
1, c
Name
¯, c
Name
¯
-
1
},
(iv)
R
G
=
{
(
n
1, age, n
5
), (
n
5, ag
e
-
1
,
n
1
), (
n
1, teaches
,
n
3
), (
n
3, teache
s
-
1, n
1
), (
n
2, age, n
6
), (
n
6
,
ag
e
-
1
,
n
2
), (
n
2, teaches, n
3
), (
n
3, teache
s
-
1,n
2
), (
n
4, attends,n
3
),(
n
3, attend
s
-
1,n
4
), (
n
3,c
Name,n
7
), (
n
7, c
Nam
e
-
1, n
3
), (
n
4, name, n
8
), (
n
8, nam
e
-
1, n
4
), (
n
5, τ, n
5
), (
n
6, τ, n
6
), (
n
7, τ,n
7
),(
n
8, τ, n
8
)
},
(v)
I
G
=
{
I
G
(
n
1
)
=
{
true, Teacher
}, I
G
(
n
2
)
=
{
true, Teacher
}, I
G
(
n
3
)
=
{
true
,
Course
}, I
G
(
n
4
)
=
{
true, Student
}, I
G
(
n
5
)
=
{
true, 37
}, I
G
(
n
6
)
=
{
true, 40
}, I
G
(
n
7
)
=
{
true, Database
}, I
G
(
n
8
)
=
{
true, Smith
}
}.And this Kripke structure is shown in Figure 7.Figure 7
The Kripke structure of Figure1.


## 4.2. Query as CTL Formula

Reviewing the W-query in Figure6(a), intuitively, the CTL formula must express the statement “the state Teacher formula is true and there is one next state reachable by an edge labeled age, where the 37 formula is true,” this is to say
(1)
Teacher
∧
E
X
age
(
37
)
.
For the query in Figure 6(b), the CTL formula should be written as
(2)
Teacher
∧
E
X
age
(
true
)
,
For the query of Figure 6(c), we get the following formula:
(3)
Teacher
∧
E
X
teaches
(
Course
)
∧
A
X
c
name
(
¬
Database
)
.
This formula is true if “there is a node labeled Teacher and there exists one next node labeled Course, which is reachable by an edge labeled teaches, such that for all next to Course nodes labeled Database, the relation cName is not fulfilled”. Let us then consider how to encode W-queries in CTL formulae. We study the situation that W-graph and W-query are both acyclic. Firstly, we define an auxiliary function to simply handle labels of nodes and edges in W-graph.Definition 15.
LetG
=
〈
N
,
E
,
ℓ
〉 be a W-graph, for all nodes n
∈
N and for all edges e
=
〈
n
1
,
(
c
,
p
)
,
n
2
〉
∈
E; an auxiliary function φ is defined as
(4)
φ
(
n
)
=
{
ℓ
ℒ
(
n
)
,
if
ℓ
ℒ
(
n
)
≠
⊥
t
r
u
e
,
otherwise
φ
(
e
)
=
{
p
,
if
ℓ
𝒞
(
e
)
=
ℓ
𝒞
(
n
2
)
,
p
¯
,
otherwise
.And the query translation can be formally defined as follows.Definition 16.
LetG
=
〈
N
,
E
,
ℓ
〉 be a acyclic W-graph, ν
∈
N, and let Q
=
〈
G
,
ν
〉 be an accessible query. The formula associated with Q is Ψ
ν
(
G
), where Ψ
ν
(
G
) is defined recursively as follows: (i)
letb
1
,
…
,
b
h
(
h
≥
0
) be the successors of ν, s.t. ℓ
𝒞
(
b
i
)
=
solid,
(ii)
letc
1
,
…
,
c
k
(
k
≥
0
) be the successors of ν, s.t. ℓ
𝒞
(
c
i
)
=
dashed
(iii)
fori
=
1
,
…
,
h and j
=
1
,
…
,
k, let e
i be the edge which links ν to b
i and e
i
′ the one which links ν to c
j. If ℓ
𝒞
(
ν
)
=
solid, then
(5)
Ψ
ν
(
G
)
=
φ
(
ν
)
∧
⋀
i
=
1
,
…
,
h
E
X
φ
(
e
i
)
(
Ψ
b
i
(
G
)
)
∧
⋀
j
=
1
,
…
,
k
A
X
φ
(
e
j
′
)
(
Ψ
c
j
(
G
)
)
else
(
ℓ
𝒞
(
ν
)
=
dashed
)
Ψ
ν
(
G
)
=
¬
φ
(
ν
)
∨
⋁
i
=
1
,
…
,
h
A
X
φ
(
e
i
)
(
Ψ
b
i
(
G
)
)
∨
⋁
j
=
1
,
…
,
k
E
X
φ
(
e
j
′
)
(
Ψ
c
j
(
G
)
)
.The construction of the formula involves the unfolding of a directed acyclic graph; the size of the formulaΨ
ν
(
G
) (written as |
Ψ
ν
(
G
)
|) can grow exponentially with respect to|
G
|. Although that, it is easy to compute the formula without repetitions of subformulae and keep the memory allocation linear w.r.t. |
G
|, so it is natural to compactly represent the formula using a linear amount of memory. This compact representation is allowed by the model-checker NuSMV [19].Theorem 17.
Given a W-instanceI and a W-query 〈
G
,
ν
〉, let K
I be the Kripke structure associated with I and Ψ
ν
(
G
) the CTL formula associated with 〈
G
,
ν
〉. Consistency checking I with 〈
G
,
ν
〉 can be done in linear time on |
I
|
·
|
Ψ
ν
(
G
)
|.Proof.
For achieving the consistency checking procedure, there are three steps to follow, translating the W-graph into a Kripke structure, encoding the W-query into a CTL formula, and executing a model-checking process.
Assuming that|
I
|
=
|
N
|
+
|
E
|, where |
N
| is the number of nodes in W-instance I and |
E
| is the number of edges in this graph, notating K
I
=
〈
Σ
I
,
Ac
t
I
,
R
I
,
I
I
〉, expressing |
Σ
I
|
,
|
Ac
t
I
|
,
|
R
I
| as the number of states, actions, and transition relations in |
K
I
|, and writing |
Ψ
ν
(
G
)
| as the length of the CTL formula Ψ
ν
(
G
), then the complexity issues can be analyzed.
Firstly, when creating the Kripke structure, for each node, action, and transitional relation that must be created one by one, the time complexity should be|
Σ
I
|
+
|
Ac
t
I
|
+
|
R
I
|
≤
|
N
|
+
4
|
E
|
+
3
|
E
|
=
O
(
|
I
|
), according to Definition 14. Secondly, we consider the length of the encoded CTL formula |
Ψ
ν
(
G
)
|
≤
|
G
|
=
O
(
|
G
|
), because the worst situation is to encode the whole W-graph into a formula, where |
G
| is the total number of edges and nodes in this query. The last step is to execute model-checking procedure; the time complexity is |
Ψ
ν
(
G
)
|
·
(
|
Σ
I
|
+
|
R
I
|
)
=
O
(
|
G
|
·
|
I
|
) according to [16]. So the total time complexity is O
(
|
I
|
)
+
O
(
|
G
|
)
+
O
(
|
G
|
·
|
I
|
), which is a linear time on |
I
|
·
|
Ψ
ν
(
G
)
|.
If we think that the|
G
| is always less than or equal to |
I
| (intuitively, it is always so), then O
(
|
I
|
)
+
O
(
|
G
|
)
+
O
(
|
G
|
·
|
I
|
)
≤
O
(
|
I
|
2
)
+
O
(
|
I
|
), which is a polynomial time over |
I
|.The equivalence between two segments of W-graph is the equivalence between two CTL formulae, which can be formally proved in linear time. The consistency checking problem for the W-graph model is promoted to the equivalence proof problem for the CTL formulae with a Kripke structure.


## 4.3. Checking Consistency

During the procedure of extracting a domain ontology gradually from heterogeneous data sources, semantic consistency has to be checked. According to Definitions14 and 16, after encoding a W-graph to a Kripke structure and a W-query to a CTL formula, the semantic equivalent query problem on the W-graph has been promoted to a global model-checking problem.Definition 18.
Given a W-instanceI and a W-query 〈
G
,
ν
〉, let K
I be the Kripke structure associated with I and Ψ
ν
(
G
) the CTL formula associated with 〈
G
,
ν
〉. The Consistency checking I with 〈
G
,
ν
〉 amounts to solve the global model-checking problem with the Kripke structure K
I and the CTL formula Ψ
ν
(
G
), namely, to find all the states s of K
I such that s
⊨
Ψ
ν
(
G
). Algorithm 1 describes this procedure.Algorithm 1:Semantic consistency checking.
Require:  I, // W-graph semantic model
〈
G
,
ν
〉 // semantic segment expressed by W-query
Ensure:  consistent or inconsistent
encoding  I  to  K
I; // according to Definition 14
encoding  〈
G
,
ν
〉  to  Ψ
ν
(
G
); // according to Definition 16
S
=
{
s∣s
⊨
Ψ
ν
(
G
)
}; // model checking
if  S is emptyset  then
return  consistent;
else
return  inconsistent;
end ifSo semantic consistency checking can be done with model-checking technology. Let us consider each type of inconsistency defined above. As for concepts inconsistency, it is to find out whether there is another concept (equivalent toC) in W-schema S, which has been built to be extended, when a new concept C has been added into the W-schema S. This is to say, a W-query Q
=
〈
S
,
C
〉 should be imposed on the S for consistency checking. Let K
S be the Kripke structure of S and let Ψ
C
(
S
)
=
φ
(
C
) be the CTL formula of Q and we should find all states s of K
S such that s
⊨
φ
(
C
).As far as relationship inconsistency is concerned, it is to query a W-graphG with a W-query Q
=
〈
G
,
n
1
〉 before a new relationship (
n
1
,
n
2
) is added into the W-graph model. Let K
G be the Kripke structure of G, and the CTL formula is
(6)
Ψ
n
1
(
G
)
=
φ
(
n
1
)
∧
E
X
φ
(
(
n
1
,
n
2
)
)
(
n
2
)
.
The consistency checking is to find all states s of K
G such that s
⊨
Ψ
n
1
(
G
). If the states like this cannot be found, then the model is consistent after adding the new relationship (
n
1
,
n
2
); if any state has been found, then the model will be inconsistent and the new relationship cannot be added into the model. This is the relationship redundant inconsistency. As for paradox relationship paradox inconsistency, the CTL formula is
(7)
Ψ
n
2
(
G
)
=
φ
(
n
2
)
∧
E
X
φ
(
(
n
1
,
n
2
)
)
(
n
1
)
.As for fact consistency checking, the Kripke structure of the W-instanceI is K
I, and the CTL formula for the attribute fact (the instance m of a concept has the concrete attribute value n, i.e., (
m
,
n
)) inconsistency is
(8)
Ψ
m
(
I
)
=
φ
(
m
)
∧
E
X
φ
(
(
m
,
n
)
)
(
n
)
.
The CTL formula for the concept fact (the instance m of one concept to be added into the model) inconsistency is
(9)
Ψ
m
(
I
)
=
φ
(
m
)
∧
⋀
j
=
1
,
…
,
k
A
X
φ
(
(
m
,
n
j
)
)
(
Ψ
n
j
(
I
)
)
,
where n
j
,
j
=
1
,
…
,
k are all successors of m. If some states of K
I satisfy the above formula, then the inconsistency occurs. This is to say, a fact m cannot be added into the model if an equivalent fact has already existed in the model.


## 5. Cases Study

In this section, we will test the semantic consistency checking technique presented above by using the model checker NuSMV 2.5.4 [20]. NuSMV allows for the representation of finite-state machines (FSMs) and for the analysis of specifications expressed in computation tree logic (CTL) using symbol model-checking techniques. For using the tool, we first rewrite the Kripke structure into a finite-state machine, where edges are not labeled, as follows:given a Kripke structure related to a W-instance, replace every labeled edgem
→
action
n by the two edges m
→
μ, μ
→
n, where μ is a new node labeled action.The input of the NuSMV tool is represented by a SMV program, which can express both the FSMs and CTL formulae. The Algorithm2 is the SMV program to describe the Kripke structure of the W-instance in Figure 7 and some CTL specification of consistency checking mentioned above, where the line started with symbol “- -” is comment.Algorithm 2
-
-
SMV
program
for
consistency
checking
MODULE
main
VAR
state:{n1,n2,n3,n4,n5,n6,n7,n8,teaches,inv_teaches,attends,
inv_attends,age,inv_age,name,inv_name,cName,inv_cName,tao};
label:{Teacher,Course,Student,Database,Smith,37,40};
ASSIGN
init(state)
:=
n1;
next(state)
:=
case
state
=
n1
∣
state
=
n2
:
{teaches,age};
state
=
teaches
:
n3;
state
=
age
:
{n5,n6};
state
=
n3:{inv_attends,inv_teaches,cName};
state
=
inv_attends
:
n4;
state
=
inv_teaches
:
{n1,n2};
state
=
cName
:
n7;
state
=
n4
:
{attends,name};
state
=
attends
:
n3;
state
=
name
:
n8;
state
=
n5
:
{inv_age,tao};
state
=
inv_age
:
{n1,n2};
state
=
tao
:
{n5,n6,n7,n8};
state
=
n6
:
{inv_age,tao};
state
=
n7
:
{inv_cName,tao};
state
=
inv_cName
:
n3;
state
=
n8
:
{inv_name,tao};
state
=
inv_name
:
n4;
TRUE
:
state;
esac;
DEFINE
nl
:=
case
state
=
n1
∣
state
=
n2
:
Teacher;
state
=
n3
:
Course;
state
=
n4
:
Student;
state
=
n5
:
37;
state
=
n6
:
40;
state
=
n7
:
Database;
state
=
n8
:
Smith;
TRUE
:
state;
esac;
-
-
concept
redundancy
checking
CTLSPEC
(nl=Teacher)
&
EX(state=age)
&
EX(state=teaches
&
EX(nl=Course))
-
-
relationship
inconsistency
checking
-
-
need
to
be
changed
to
‘init(state)
:=
n4;’
CTLSPEC
(nl=Student)
&
EX(state=attends
&
EX(nl=Course))
-
-
attribute
inconsistency
checking
CTLSPEC
(nl=Teacher)
&
EX(state=age
&
EX(nl=40))
-
-
fact
inconsistency
checking
CTLSPEC
(nl=Teacher)
&
EX(state=age
&
EX(nl=37))
&
EX(state=teaches
&
EX(nl=Course
&
EX(state=cName
&
EX(nl=Database))))In this SMV program, the set of states of the Kripke structure is chosen by declaring the state variablestate to assume values {
n
0
,
…
,
n
8
,
t
e
a
c
h
e
s
,
…
,
t
a
o
}, where actions have also been seen as states. The transition relation of the Kripke structure is expressed by assigning (ASSIGN), for each value of the variable state, the list of nodes that can be reached from it through one edge. The variables label and nl are introduced to define the node label of each state identified by the value of the variable state. And CTL formulae have been defined by CTLSPEC. The formula(
n
l
=
T
e
a
c
h
e
r
) & E
X
(
s
t
a
t
e
=
a
g
e
) & E
X
(
s
t
a
t
e
=
t
e
a
c
h
e
s
&
E
X
(
n
l
=
C
o
u
r
s
e
)
)says when a new conceptTeacher, which has anage attribute, has a teaches action, and can teach some Course, is to be added into the model whether there exists an inconsistency. And (
n
l
=
S
t
u
d
e
n
t
) & E
X
(
s
t
a
t
e
=
a
t
t
e
n
d
s
&
E
X
(
n
l
=
C
o
u
r
s
e
)
)expresses whether a new relationship Student
→
attends
Course can be added into the model without semantic inconsistency. And (
n
l
=
T
e
a
c
h
e
r
) & E
X
(
s
t
a
t
e
=
a
g
e
&
E
X
(
n
l
=
40
)
)says whether the attribute relationship “the Teacher is 40 years old” can be added into the model without any redundancy and paradox. And (
n
l
=
T
e
a
c
h
e
r
) & E
X
(
s
t
a
t
e
=
a
g
e
&
E
X
(
n
l
=
37
)
) & E
X
(
s
t
a
t
e
=
t
e
a
c
h
e
s
&
E
X
(
n
l
=
C
o
u
r
s
e
&
E
X
(
s
t
a
t
e
=
c
N
a
m
e
&
E
X
(
n
l
=
D
a
t
a
b
a
s
e
)
)
)
)expresses whether the fact “the 37-year Teacher teaches Database Course” can be added into the model.The results we have obtained on the 64-bit windows 7 operation system are shown in Figure8. The outputtrue for a CTL formula says that at least one inconsistency exists when checking the W-graph model with the new semantic segment (expressed by this formula), so the new segment cannot be added into the model. Otherwise, we can choose another initiate state to check again, until we finish all elements of initiated state set. If we always get a finalfalse output, then the inconsistency has not occurred, and the new semantic segment can be added into the model.Figure 8
Experiment results.This test confirms the possibility of solving semantic consistency checking problem by using model-checking on polynomial time methods.


## 6. Conclusion

For validating semantic consistency during the increasing procedure of building a domain ontology from heterogeneous sources, we employ the model-checking technology to avoid subgraph isomorphism problem, which is NP hard. In order to adopt model-checking method, we formally transform the semantic model into a Kripke structure and the semantic equivalent querying problem into CTL formulae and then the semantic consistency is promoted to the global model-checking problem. The effective experiment with the model-checking tool NuSMV has also been introduced. In the future, the reasoning problem should be considered clearly; for example, some implicative semantic elements would be reasoned from the existing model. If a new semantic segment is equivalent to some implicative semantic elements, the inconsistency also occurs. In the near future, this type of consistency checking should also be regarded.



---

*Source: 181938-2014-04-15.xml*