Information Technology Reference
In-Depth Information
we plan to derive the definition of those heuristic functions automatically. A
simple distance heuristic can be derived if the goal of the model checking is to
find specific values for certain variables of the machine (such as
on = ongoal
).
Basically, for current state
s
=
s
1
,...,s
n
and a target state
t
=
t
1
,...,t
n
we
use as heuristic
h
(
s
)=
Σ
1
≤i≤n
Δ
(
s
i
,t
i
)where
-
Δ
(
x, target
)=
abs
(
x
−
target
)if
x
integer
-
Δ
(
x, target
)=
card
(
x
−
TARGET
)
−
card
(
TARGET
∩
A
)if
x
aset
-
Δ
((
x, y
)
,
(
t
1
,t
2)) =
Δ
(
x, t
1) +
Δ
(
y, t
2) for pairs,
-
in all other cases:
Δ
(
x, target
)=0if
x
=
target
and 1 otherwise
If the value of a particular variable is not relevant, then we simply set
Δ
(
s
i
,t
i
)=
0 for that variable.
This defines a kind of Hamming distance for B states. We have applied this
(manually) in the BlocksWorld example above.
We have only evaluated this approach for finding goals. Here, it obtained
the best overall geometric mean of 0.34. For Puzzle8 and Abrial press m13,
this approach yielded by far the best solution. For RussianPostal, TrainTorch,
Blocksworld, Abrial Queue m1 it obtains the best result. There was one exper-
iment were it is markedly worse than ProB in the reference settings: Syste-
mOnChip Router. Here the heuristic did not pay off at all. Indeed, here the last
event changes all of the four variables, relevant for the model checking GOAL,
in one step. This only confirms the fact that we are working with
heuristic
func-
tions, which are not guaranteed to always improve the performance.
Summary of the Directed Model Checking Experiments:
We have sum-
marised the main findings of our experiments in Table 8 in Appendix A. We can
conclude that:
-
for invariant checking, the random hash heuristic fared best.
2
This seems to
indicate that it is maybe useful to combine some more random component
into the depth-first/breadth-first techniques of Section 3, e.g., to also ran-
domly permute the operation order. Indeed, the approaches from Section 3
always process the operations in the same order, and do not shue the states
inside the pending list.
-
for deadlock checking, the out-degree-hash heuristic is the best. It should
provide a good basis for further improved deadlock checking techniques.
-
for goal finding, a custom heuristic function provides (except in one case)
by far the best result. The next step is to derive those heuristic functions
automatically.
The out-degree-hash heuristic also provides reasonably good performance
(its geometric mean is 0.41, which is better than the best mixed-depth-first
one of 0.57 for DF75).
2
However, note that DF50 had an overall geometric mean of 0.58, and was hence
better overall than random hash.
Search WWH ::
Custom Search