Generalized planning is about finding plans that solve collections of
planning instances, often infinite 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.

本研究针对广义规划中的归纳学习过程中模型广化限制的问题，提出基于全量数据的抽象模型和自动化合成方法，并形式化证明了其可行性和正确性。