Abstraction in Planning via Model Checking

Planning via Model Checking is a novel approach to planning. It is based on the reformulation of a planning problem to the exploration of a finite state automaton. Automata exploration can be efficiently performed with Model Checking, a formal verification technique widely applied in design of industrial systems. For very large domains, however, a state explosion can arise. Abstractions can be used to tackle the problem. In this paper we show how Abstraction techniques developed in classical planning can be lifted to the Planning via Model Checking paradigm