A Correctness Result for Reasoning about One-Dimensional Planning Problems

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 generalized plan representation called an FSA plan, with its semantics defined in the situation calculus. Based on this, we identify a class of infinite planning problems, which we call one-dimensional (1d), and prove a correctness result that 1d problems can be verified by finite means. We show that this theoretical result leads to a practical algorithm that does this verification practically, and a planner based on this verification algorithm efficiently generates provably correct plans for 1d problems.

• Type: Conference
• Year: 2010
• Where: KR
• Authors: Yuxiao Hu, Hector J. Levesque
• Keywords: Automated Reasoning, Generalized Plan, KR 2010, Multiple Planning Instances, Rich Control Structures