Information Technology Reference
In-Depth Information
Theorem 4. If the preconditions of Proposition 1 are satisfied, then our algo-
rithm in Fig. 2 gives us an optimal abstraction hierarchy.
Proof. The proof follows from Proposition 1 and Definition 21.
The last theorem identifies that in order to take advantage of optimal ab-
straction hierarchies, we have to constrain heavily the CSCs in a CSA. However,
even if an optimal abstraction hierarchy is not constructed for a CSA, the non-
optimal one may still help to reduce the complexity of PD.
5
An Abstraction Example
In order to demonstrate PD with abstraction, let us consider the following CSA:
CSA 0 ::= E ⊗ M ⊗ X 3
!( E ⊗ N H )
!( H E ⊗ I ⊗ M )
!( M N )
!( I 7
!( F ⊗ X Y 2 )
!( Y 2
⊗ X 2
X 2 )
E ⊗ M ⊗ X 2
F )
The corresponding constraint graph, achieved by using the algorithm in
Fig. 1, is presented in Fig. 5(a). A directed edge from node A to node B in the
graph indicates that A cannot occur lower in the abstraction hierarchy than B .
F
Y
I
E M
N
X
IMNEH
F
XY
H
(a)
(b)
Fig. 5. The constraint graph (a) and the abstraction hierarchy derived from it (b).
One corresponding abstraction hierarchy derived from the graph presented in
Fig. 5(a) is depicted in Fig. 5(b). Using this abstraction hierarchy, we introduce 2
new abstracted CSAs
CSA 1 and
CSA 2 for abstraction levels 1 and 2 respectively:
CSA 1 ::= X 3
!( Y 2
⊗ X 2
X 2 )
!( F ⊗ X Y 2 )
X 2
!(1
F )
CSA 2 ::= X 3
!( Y 2
⊗ X 2
X 2 )
!( X Y 2 )
X 2
The literals and CSCs available at different abstraction levels are represented
inTable1.Thevalue“—”thererepresents that a CSC was abstracted to
1
1
and was thus then discarded, because this axiom is already included in HLL.
In Table 1 the CSCs at abstraction level 2 are obtained by substituting all
literals except X and Y with constant 1. For instance,
H E ⊗I ⊗M is first
abstracted to
1
1
1
1, because literals H , E , I and M are not allowed at

Search WWH ::

Custom Search