Abstract
Generalized planning is about finding plans that
solve collections of planning instances, often infi-
nite collections, rather than single instances. Recently it has been shown how to reduce the planning problem for generalized planning to the planning problem for a qualitative numerical problem;
the latter being a reformulation that simultaneously
captures all the instances in the collection. An
important thread of research thus consists in finding such reformulations, or abstractions, automatically. A recent proposal learns the abstractions inductively from a finite and small sample of transitions from instances in the collection. However, as
in all inductive processes, the learned abstraction is
not guaranteed to be correct for the whole collection. In this work we address this limitation by performing an analysis of the abstraction with respect
to the collection, and show how to obtain formal
guarantees for generalization. These guarantees,
in the form of first-order formulas, may be used
to 1) define subcollections of instances on which
the abstraction is guaranteed to be sound, 2) obtain necessary conditions for generalization under
certain assumptions, and 3) do automated synthesis
of complex invariants for planning problems. Our
framework is general, it can be extended or combined with other approaches, and it has applications
that go beyond generalized planning