Master’s practical course, Master’s thesis, or IDP
State space search is a successful technique to solve classical AI planning problems, i.e. deterministic problems with finite states. The main task of this project is to (partially) build a formally verified A* based planning algorithm. Tasks in this project include
- formalising existing heuristics for classical planning in Isabelle/HOL and verifying that they are admissible. There are many such heuristics, and they are reviewed in sections 2.3 and 2.7.9 in a book by Gallab et al. . A first step is to verify abstraction based heuristics like pattern databases [2,3] and/or merge-and-shrink .
- integrating an existing Isabelle formalisation of A* with 1) already formalised semantics of planning problems to obtain a version of A* that operates on planning state spaces and 2) planning heuristics that are verified.
- refining the integrated A* to executable code.
Experience with Isabelle/HOL is required.
Material to read:
A textbook on planning by Malik Ghallab, Dana Nau, and Paolo Traverso: http://projects.laas.fr/planning/book.pdf
Paper on pattern databases: https://pdfs.semanticscholar.org/f17a/8d6aaa9a876cc1e48afb22ba6d312f14d307.pdf
Paper on pattern databases: http://idm-lab.org/bib/abstracts/papers/aaai07b.pdf
Papers on Merge-and-shrink https://dl.acm.org/citation.cfm?id=2559951