Generating and Verifying Planning Sketches using Temporal Logic

Publication date

DOI

Document Type

Master Thesis

Collections

Open Access logo

License

CC-BY-NC-ND

Abstract

Sketches express the subgoal structure of a set of planning problems with a similar goal. A sketch consists of sketch rules that indicate how the environment has to change in a particular situation to reach the goal. Using sketches effectively speeds up the search for a solution to a planning problem. While a previous technique for learning sketches has been investigated, this thesis proposes a novel, modular approach to automatically find all `good' sketches with n rules and m features given a set of domain instances with similar goals. Our approach involves lazily generating a pool of potential sketches and verifying them using temporal logic constraints. We show that our method can find good sketches for eight domains, including those learned in previous research. Because our approach allows us to generate all good sketches with a certain number of rules, we can analyze patterns of equivalent sketches, which opens up a wide range of future work.

Keywords

planning; sketches; temporal logic; model-checking; finite CTL-star

Citation