Sciweavers

KR
2010
Springer

A Correctness Result for Reasoning about One-Dimensional Planning Problems

13 years 8 months ago
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.
Yuxiao Hu, Hector J. Levesque
Added 19 Jul 2010
Updated 19 Jul 2010
Type Conference
Year 2010
Where KR
Authors Yuxiao Hu, Hector J. Levesque
Comments (0)