M.Sc. Verifying Belief Program by Symbolic Dynamic Programming

Wednesday, Jun 9, 2021

Belief program is a member of the GOLOG programming language family where each test refers to the agent’s subjective belief and actions and sensing could be noisy. Due to its action-centered properties, it is extremely suitable for high-level robot control in a partial-observable environment. Verifying such a program to ensure it meets certain properties like safety is crucial before deployment. The verification of belief programs is known to be closely related to model-checking in the Partial-Observable Markov Decision Process(POMDP). In this thesis, we will study how to exploit Symbolic Dynamic Programming, an algorithm used in solving first-order Markov Decision Process(FOMDP), to verify belief programs.


  • (Mandatory) a satisfactory score of the course Introduction to Artificial Intelligence;
  • (Preferable) a good score of the course The Logic of Knowledge Base; a good score of the course Introduction to Knowledge Representation; some knowledge about model-checking and verification.

Further Information

If you are interested in it or have questions, please feel free to contact Daxin Liu via email “liu@kbsg.rwth-aachen.de”.