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. [1]. A first step is to verify abstraction based heuristics like pattern databases [2,3] and/or merge-and-shrink [4].
- 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.
Prerequisites:
Experience with Isabelle/HOL is required.
Advisor:
Mohammad Abdulaziz, email {mansour} AT [in.tum.de]
Supervisor:
Prof. Tobias Nipkow, Raum MI 00.09.055, email {nipkow} AT [in.tum.de]
Material to read:
[1]
A textbook on planning by Malik Ghallab, Dana Nau, and Paolo Traverso: http://projects.laas.fr/planning/book.pdf
[2]
Paper on pattern databases: https://pdfs.semanticscholar.org/f17a/8d6aaa9a876cc1e48afb22ba6d312f14d307.pdf
[3]
Paper on pattern databases: http://idm-lab.org/bib/abstracts/papers/aaai07b.pdf
[4]
Papers on Merge-and-shrink https://dl.acm.org/citation.cfm?id=2559951