Generating and Verifying Planning Sketches using Temporal Logic
Publication date
Authors
DOI
Document Type
Master Thesis
Metadata
Show full item recordCollections
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