Information Technology Reference

In-Depth Information

Algorithm
CreateHierarchy
(
Γ , G
)

inputs: a set of CSCs
Γ
and a goal state
G

output: an ordered monotonic abstraction hierarchy

begin

graph ← DetermineConstraints
(
{}, Γ , G
)

components ← FindStronglyConnectedComponents
(
graph
)

partialOrder ← ConstructReducedGraph
(
graph, components
)

absHierarchy

TopologicalSort
(
partialOrder
)

return
absHierarchy

end
CreateHierarchy

←

Fig. 2.
Creating an abstraction hierarchy.

extended by observing the succedents of CSCs and in the case it consists only of

1, the CSC would not be considered. Anyway these CSCs may be needed during

reasoning.

3.1

The Role of the Initial State

While building a constraint graph for abstraction, dependencies between literals

are detected. If it should happen that at least one literal
l ∈ S
is not included in

the constraint graph and it does not occur in the goal state
G
either, then there

is no proof for the particular CSA. This applies iff there are no CSCs, which

could consume literal
l
.

Theorem 1.
Given a CSA and a set of edges
D
e

of the constraint graph

D

,

which was constructed for the CSA, and if

∃l.
(
l ∈ S ∧ l ∈ G ∧ l ∈ D
e
∧∀c ∈

Γ.
(
succ
(
c
)

=1)
, then there is no proof for the CSA.

Proof.
While finding dependencies between literals through constraint graph

construction, roughly a way for literal propagation is estimated for reaching the

goal
G
and literals on the way are inserted to the graph. Therefore, if not all

literals
l ∈ S
are included in the constraint graph, then there is no way to find

aprooffor
Γ
;
S G
.

Anyway, some literals in the initial state
S
may be not engaged during PD

and thus they exist in both states
S
and
G
. In that case the missing literal from

a constraint graph does not indicate that the state
G
is not reachable. Similarly,

CSCs
C
with
succ
(
C
)

≡

1 have to be considered, since they only consume literals

and therefore are rejected, when generating a constraint graph.

This case is illustrated in Fig. 3(b), where a constraint graph is generated for

CSA
Γ
;
A ⊗ B ⊗ C F
. As it can be seen in Fig. 3(b) the literal
B
, although

being in the state
S
, is not included in the constraint graph. The same applies

for literal
A
. Therefore the CSA has no proof.

Search WWH ::

Custom Search