bstract

A plan with rich control structures like branches and loops can usually serve as a general solution that solves multiple planning instances in a domain.However, the correctness of such generalized plans is non-trivial to define and verify, especially when it comes to whether or not a plan works for all of the infinitely many instances of the problem.  In this paper, we give a precise definition of a gen-eralized plan representation called an FSA plan,with its semantics defined in the situation calcu-lus. Based on this, we identify a class of infinite planning problems, which we call one-dimensional (1d), and prove a correctness result that 1d prob-lems can be verified by finite means.  We show that this theoretical result leads to an algorithm that does this verification practically, and a plan-ner based on this verification algorithm efficiently generates provably correct plans for 1d problems