The main focus of this paper is on the discussion of formal rule verication using graph-based approach. XTT2 is a custom rule representation method, that introduces a structured rule base composed of extended decision tables linked in a tree-like structure. Considering the complex nature of the XTT2 structure, only the local, table level verication has been considered so far. However, graph-oriented verication is a powerful solution to the analysis of rule-based systems. It can be applied to provide global verication of the XTT2 knowledge bases. The principal idea consists in representing XTT2 rules as a directed hypergraph. All of rule formulas are transformed into vertices and appropriate hyperarcs are determined. This restructuring of the XTT2 knowledge base allows to provide verication using graph algorithms. Preliminary evaluation of this approach shows that the graph-oriented verication is a promising solution to provide a formal analysis of XTT2 rules.
Rule-based systems (RBS) [
The main focus of the paper is the formal verication of rules [
The approach proposed in this paper uses graph-based representation. Graphoriented verication is a powerful solution to the analysis of rule-based systems. It can be applied to provide global verication of the XTT2 knowledge bases. ? The paper is carried out within the AGH UST Project No. 10.10.120.105. The principal idea consists in representing XTT2 rules as a directed hypergraph. All of rule formulas are transformed into vertices and appropriate hyperarcs are determined. This restructuring of the XTT2 knowledge base allows to provide a verication using graph algorithms. Preliminary evaluation of this approach shows that the graph-oriented verication is a promising solution to provide a formal analysis of XTT2 rules. In the paper a practical example is provided. 2
The formalization for XTT 2 representation is based on ALSV(FD) logic [
A1 ∈ t1 ∧ A2 ∈ t2 ∧ · · · ∧ An ∈ tn −→ retract(B1 = b1, B2 = b2, . . . , Bb = bb) assert(C1 = c1, C2 = c2, . . . , Cc = cc) H1 = h1, H2 = h2, . . . , Hh = hh next(j), else(k) (1)
In (1) a formula ψ describes context. A1 ∈ t1 ∧ A2 ∈ t2 ∧ · · · ∧ An ∈ tn is a precondition formula. Cj (j = 1, . . . , c) and Bi (i = 1, . . . , b) correspond to facts to assert and to retract from the knowledge base. Conclusions (decisions or actions) are represented by H1 = h1, H2 = h2, . . . , Hh = hh. There is also a control statement introducing the next or alternative rule.
In the case of XTT 2 representation, the logical rule format is as follows:
r : (A1 ∝1 V1) ∧ (A2 ∝2 V2) ∧ · · · ∧ (An ∝n Vn) −→ RHS,
(2)
where ∝i∈ {=, 6=, ∈, ∈/} for simple attributes (taking single values) and ∝i∈ {=
, 6=, ⊆, ⊇, ∼, 6∼} for general attributes (taking set values). The form of RHS is
as in (1). For more details on the XTT2 rule formalization using ALSV(FD)
see [
The quality of a rule-based system is dependent on the quality of a knowledge base. What is more important, anomalies in the set of rules could result in serious faults in system’s responses. Therefore the analysis of knowledge base is an important step during development of a rule-based system.
The issues of verication and validation were discussed by many authors.
Dierences in their approaches to V&V start at the denition level. In this
paper verication and validation processes are dened as follows:
Verication is a process in early design phase, aimed at checking if the system
meets its constraints and requirements ([
Testing is a process aimed at analyzing the system work, by comparing system
responses to known responses for special input data ([
Validation is a case of testing, aimed at checking if the system meets user’s
requirements ([
A summary of analysis techniques and tools is presented in [
The classication of potential errors and deformation of knowledge base
was also widely discussed, with some practical taxonomies of anomalies given
(see [
Let the knowledge base be described by rules: r1 : Ψ1 → h1 r2 : Ψ2 → h2 . .
.
rn : Ψn → hn
(3)
Completeness ensures that for any input state the system reacts and
produces some response (conclusion, decision or action) ([
Determinism guarantees that the system always produces the same reaction
for the same input data. In other words for any input state the system
nds a unique solution ([
The system is indeterministic, if there are contradictory rules in knowledge base. Inconsistency also is a cause of indeterminism.
Minimal number of rules indicates a set of rules without redundant, subsumed rules. What is more, the set of rules should produce the same reactions as a overdeveloped set.
All of above features completeness, determinism, minimal number of rules
should be provided to assure reliability, safety and eciency of the rule-base
system ([
All of verication procedures are based on inference rules for ALSV(FD)
introduced in [
φAi is a value from the domain of Ai, where φAi is a value of attribute Ai in formula φ, a formula (Ai = φAi ) is a logical consequence of a formula (Ai ∝i Vi).
The basic idea in the verication of completeness consists in checking all input states. Domains of attributes are considered. The Cartesian product of domains determine all states for the context (table). For every tuple corresponding to an input state, the algorithm checks if preconditions of any rule are satised. If there is no rule to execute, the considered state is reported as uncover. Based on all uncovered states, a proposal of a new rule is given. The analysis ends, when all states are checked. Since domains of attributes are nite, the verication procedure terminates after a nite number of discrete steps.
Verication of contradiction is based on a pairwise comparison of rules. Two rules, executable in the same time (for the same state), are taken into consideration. The comparison concerns the right-hand side of rules. If conclusions are inconsistent, the conict is reported. The verication procedure stops when all possible comparisons are done.
The pairwise comparison of rules is also used to verify subsumption. However, the analysis concerns both sides of rules. One rule is subsumed by another, if its preconditions are more specic, but simultaneously conclusions are more general. The verication procedure nds two rules in the context (table), executable for the same state. Then checks, whether there is relation between conclusions. The algorithm provides all comparisons. This strategy allows to detect identical rules. In this case, a rule is reported as subsuming another and the other subsuming the rst one.
HalVA allows to reduce an overdeveloped set of rules. The reduction can be
done by using the dual resolution ([
Unfortunately, solutions provided by HalVA are limited. The serious issue is computational complexity of provided algorithms. Verication of completeness could cause a combinatorial explosion, if domains of attributes are outsized. The other technique the pairwise comparison of rules is also dependent on a size of the considered case. Generally, to verify a set of n rules, n2 comparisons need to be done. What is most important, all of HalVA verication features are focused on a local analysis. The limitation of the scope indicates a verication of some context (implicitly a table) only. Therefore, HalVA procedures can point out anomalies in some specic area. Unfortunately, the problem of the global quality of the knowledge base remains unsolved. This is where the new approach proves to be useful. 4
Graph-oriented Verication Solution Proposal To verify rule-based systems in global scope the graph-oriented approach is introduced. The main concept consists in representing XTT2 rules as a directed hypergraph. Necessary basic denitions are introduced bellow.
Let X = {x1, x2, . . . , xn} be a nite set, and let E = (Ei|i ∈ I) be a family of subsets of X. The family E is said to be a hypergraph on X if 1. Ei 6= ∅ (i ∈ I) 2. [ Ei = X.
i∈I
The couple H = (X, E ) is called a hypergraph. |X| = n is called the order of
this hypergraph. The elements x1, x2, . . . , xn are called the vertices and the sets
E1, E2, . . . , Em are called the edges ([
A hypergraph is presented in Fig. 1. For directed edges (hyperarcs) initial and terminal endpoints can be pointed out (vide Fig. 2).
Let a hypergraph G = (X, E ) be considered (vide Fig. 3). The outer
demidegree d+G(x) of a vertex x is dened as the number of arcs having x as their
initial endpoint ([
Fig. 2. A hyperarc E = {v1(i), . . . , vn(i), v1(t) . . . , vm(t)}. Vertices: v1(i), . . . , vn(i) are initial endpoints and v1(t), . . . , vm(t) are terminal endpoints of the hyperarcs
For a directed hypergraph H = (X, E ) the incidence matrix is a matrix
((aij ))m×n with m rows that represent the edges of H and n columns that
represent the vertices of H, such that ([
1 if xj ∈ Ei and xj is an terminal endpoint of Ei 0 if xj ∈/ Ei Incidence matrix for the hypergraph in the Fig. 3 is introduced in Table 1.
To provide verication using the graph theory an appropriate transformation of XTT rules needs to be done. The rst step is to determine vertices. If vertices correspond to all possible values from domains of attributes, it causes a combinatorial explosion for outsized domains. Therefore, not single values, but whole formulas are transformed into vertices. However, using formulas to describe vertices results in an additional assumption. The graph-oriented approach can be provided, if the table-level verication of completeness is done.
There are three classes of vertices in the graph representation of rules: sources : the source corresponds to a formula (Ai ∝i Vi), where the attribute Ai is used only in a precondition part of rules. sinks : the sink corresponds to conclusion part of rules. others : all of others vertices, which are neither source nor the sinks, are related to formulas (Ai ∝i Vi), where attribute Ai appears in both a precondition and a conclusion part of rules.
The assumption of local verication of completeness ensures the absence of isolated vertices. Therefore, for the source x: d+G(x) > 0, for the sink x: dG−(x) > 0, and for others x: d+(x) > 0 and d−(x) > 0. In this representation, a rule from the knowledge base is transformed into a hyperarc. The rule also determines the direction of the hyperarc. Therefore, each rule has a unique representation. Initial endpoints of the hyperarc are related to formulas in a precondition part of the rule. The hyperarc is terminated in several ways. Firstly, if a conclusion in the rule is related to a sink, the sink becomes a terminal endpoint of the hyperarc. Secondly, if an attribute in a conclusion appears in a clause in a precondition part of other rule and if the clause is more general than the conclusion, the vertex related to the clause terminates the hyperarc. Finally, if control statements (next, else ) are introduced in the rule, appropriate vertices (clauses) become terminators of the hyperarc. r1 A in [a1, a2] B set b1 C set c1 r2 A eq a3 B set b2 C set c2
The hypergraph for the system is presented in Fig. 4. Let the XTT2 system be described by rules r1, r2 and r3 (vide Table 2). The attribute A appears only in a precondition part. On the other hand, attributes B and D appear in a decision part. Therefore, a hypergraph for the system has vertices: v1: (A in [a1, a2]) v2: (A eq a3) v3: (B set b1) v4: (B set b2) v5: (C eq c1) v6: (C set c2) v7: (D eq d1)
The introduced representation of rules allows to dene anomalies of the
knowledge base as follows ([
Contradiction exists if two paths from vertex X to vertices Y and ¬Y exist in the graph.
Redundancy exists if at least two dierent paths from vertex X to Y exist. Circularity exists if there is a cycle in the graph.
Unreachability exists if a vertex which is not the beginning of a path to any output node and is not the end of a path from any input node can be found in the graph.
Locally veried inconsistency, contradiction and redundancy assure correctness of rules in the table scope only. The new representation of rules allows to examine paths in the graph. Deformed ones are reported. However, the vital question is the global verication of completeness. Local analysis of verication is helpful, but it is not limitative in the global scope. Fortunately, graphoriented approach allows to detect unreachable formula or dead-end formula main sources of incompleteness.
As it was mentioned earlier, if the vertex v ∈ V is neither the source nor the sink, its outer and inner demi-degree are greater than zero. If d+(v) = 0 and d−(v) > 0, the vertex is a dead-end formula. On the other hand, if d+(v) > 0 and d−(v) = 0, the vertex is a unreachable formula.
The graph-oriented verication is a powerful solution to the analysis of
rulebased systems. It can be applied to provide a global verication of the XTT2
knowledge bases ([
Consider the thermostat control system ([
The hypergraph related to the subsystem is presented as an incidence matrix (vide Table 3). Let the deformation during the knowledge acquisition phase be introduced. The altered knowledge base could be described by hypergraph where vertices 3 and 4 are modied as shown in the parentheses. Locally the knowledge base is still valid: it is complete and there is no contradiction or redundancy. However, consider the global scope: vertices 1, 2, 5, 6, 7 and 8 are sources; vertices 9 and 10 are sinks. Demi-degrees (inner and outer) of other vertices 3 and 4 should be greater than zero. Unfortunately, the vertex 4 is deformed. Its inner demi-degree equals zero. There is no path from any source to this vertex. It is an unreachable formula . Therefore, the knowledge base is globally incomplete. 6
In this paper a graph-based representation for XTT2 rules is proposed. It is aimed at the graph-oriented verication, which is a powerful solution to the analysis of rule-based systems. It can be applied to provide global verication of the XTT2 knowledge bases. In the paper a practical example is provided, and a preliminary evaluation of the approach is given.
In the global verication of XTT2, formulas in precondition and decision parts are transformed into vertices. Adequate hyperarcs are determined. The analysis of hypergraph structure allows to detect unreachable and dead-end formulas. This allows for a more ecient analysis of completeness of the rule base.
The research presented in the paper is work in progress. Detection of redundancy or contradiction needs to examine paths in the hypergraph. This is a more dicult problem than the analysis of structure of the hypergraph. The correlation between vertices on a path needs to be checked. Therefore, this method should be improved. Another important question is reconstructing the system from the hypergraph. At the moment the transformation to hypergraph is not entirely reversible. Yet another issue is the global inference support based on the hypergraph structure. Apparently, in this approach the inference can be optimized on both the table level and global level.