Bi-Weekly Talk: Daxin Liu: Verification of Belief Programs

Wednesday, August 26, 2020, 10:30am

Location: Online session

Speaker: Daxin Liu

 

Abstract: 

Belief program is an extension of the GOLOG program family, a logical programming language for dynamic domains that encompass the feature of stochastic effectors and noisy sensors.
Its action-central style makes it extremely suitable for high-level robot control. Before deploying such a program, it is desirable and essential to verifying such a program to ensure
it meets certain properties. Nevertheless, the verification problem is non-trivial. It is observed that the complexity of GOLOG program verification mainly subjects to the logic used,
the program structures, and the domain specifications. Properly containing the programs in these aspects suggests a decidable result. It is interesting to see how the three aspects will affect the decidability in the context of belief program.

In this talk, we propose a new semantics for the belief program which allows us to express PCTL like temporal properties.
Thereafter, we study the factors that influence the decidability of the program, particularly, in the dimension of domain specification.
As it turns out, a huge expressiveness of the domain specification needs to be sacrificed to reach decidability.