Verified planning under uncertainty (i.e. (PO)MDP planning)

Chair for Logic and Verification

Master’s practical course, Master’s thesis, or IDP

AI planning is the discipline aiming at building agents (i.e. computer programs) that act to achieve a certain goal, given a declarative description of the environment and the actions available to it. In practical applications, like autonomous vehicles driving, it is not possible to model the exact effects of actions. Planning in settings with uncertainty has been explored in the areas of AI, control, and operations research. In those settings the environment is commonly modelled as a factored Markov decision process (MDP) or a partially observable MDP. Tasks in this project include

Experience with Isabelle/HOL is required.

Mohammad Abdulaziz, email {mansour} AT []

Prof. Tobias Nipkow, Raum MI 00.09.055, email {nipkow} AT []

Material to read:

Chapter 6 in this book offers an overview of value/policy iteration:

Detailed description of policy/value iteration convergence:

An overview of the formalisation of MDPs in Isabelle:

Isabelle Refinement Framework