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.
If you are interested in it or have questions, please feel free to contact Daxin Liu via email “firstname.lastname@example.org”.