hide
Free keywords:
-
Abstract:
There is increasing awareness that planning and model checking are closely
related fields. Abstraction means to perform search in an over-approximation of
the original problem instance, with a potentially much smaller state space.
This is the most essential method in model checking. One would expect that it
can also be made successful in planning. We show, however, that this is likely
to not be the case. The main reason is that, while in model checking one
traditionally uses blind search to exhaust the state space and prove the
absence of solutions, in planning informed search is used to find solutions. We
give an exhaustive theoretical and practical account of the use of abstraction
in planning. For all abstraction (over-approximation) methods known in
planning, we prove that they cannot improve the best-case behavior of informed
search. While this is easy to see for heuristic search, we were quite surprised
to find that it also holds, in most cases, for the resolution-style proofs of
unsolvability underlying SAT-based optimal planners. This result is potentially
relevant also for model checking, where SAT-based techniques have recently been
combined with abstraction. Exploring the issue in planning practice, we find
that even hand-made abstractions do not tend to improve the performance of
planners, unless the attacked task contains huge amounts of irrelevance. We
relate these findings to the kinds of application domains that are typically
addressed in model checking.
