Verifying Belief-Based Programs via Symbolic Dynamic Programming

Frontiers in artificial intelligence and applications

Abstract

Belief-based programming is a probabilistic extension of the Golog programming language family, where every action and sensing could be noisy and every test refers to the subjective beliefs of the agent. Such characteristics make it rather suitable for robot control in a partial-observable uncertain environment. Recently, efforts have been made in providing formal semantics for belief programs and investigating the hardness of verifying belief programs. Nevertheless, a general algorithm that actually conducts the verification is missing. In this paper, we propose an algorithm based on symbolic dynamic programming to verify belief programs, an approach that generalizes the dynamic programming technique for solving (partially observable) Markov decision processes, i.e. (PO)MDP, by exploiting the symbolic structure in the solution of first-order (PO)MDPs induced by belief program execution.

Authors 4

1. Daxin Liu corresponding Aachen

   RWTH Aachen University · University of Edinburgh

   Affiliation as printed

   RWTH-Aachen University, Germany

   University of Edinburgh, the United Kingdom

2. Qinfei Huang Aachen

   RWTH Aachen University

   Affiliation as printed

   RWTH-Aachen University, Germany

3. Vaishak Belle

   University of Edinburgh

   Affiliation as printed

   University of Edinburgh, the United Kingdom

4. Gerhard Lakemeyer Aachen

   RWTH Aachen University

   Affiliation as printed

   RWTH-Aachen University, Germany