---
title: "A Correctness Result for Reasoning about One-Dimensional Planning Problems"
authors:
  - "Yuxiao Hu"
  - "Hector J. Levesque"
doi: "10.5591/978-1-57735-516-8/IJCAI11-439"
url: "https://ijcai.org/proceedings/2011/439"
pdf: "https://ijcai.org/proceedings/2011/0439.pdf"
venue: "Proceedings of the Twenty-Second International Joint Conference on Artificial Intelligence"
year: 2011
pages: "2638-2642"
track: ""
keywords:
---

# A Correctness Result for Reasoning about One-Dimensional Planning Problems

Yuxiao Hu, Hector J. Levesque

*Proceedings of the Twenty-Second International Joint Conference on Artificial Intelligence*, pages 2638-2642. DOI: [10.5591/978-1-57735-516-8/IJCAI11-439](https://doi.org/10.5591/978-1-57735-516-8/IJCAI11-439)

## Abstract

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 an algorithm that does this verification practically, and a planner based on this verification algorithm efficiently generates provably correct plans for 1d problems.