论文标题
关于信仰计划的验证
On the Verification of Belief Programs
论文作者
论文摘要
在最近的一篇论文中，Belle和Levesque提出了一种称为“信仰程序”的程序类型的框架，该程序的概率扩展是Golog sproch的概率扩展，在该程序中，每个动作和感知结果都可能是嘈杂的，每个测试条件都指代理商的主观信念。以基于动作为中心的功能继承了从Golog程序继承，使信仰程序在不确定性下相当适合于高级机器人控制。部署此类程序之前的重要一步是验证它是否满足所需的属性。进行验证至少存在两个问题：如何正式指定程序的属性以及验证的复杂性是什么。在本文中，我们根据行动和信念的模态逻辑提出了一种形式主义。除其他外，这使我们能够平稳地表达类似PCTL的时间属性。此外，我们研究了信仰程序验证问题的可决定性和不确定性。
In a recent paper, Belle and Levesque proposed a framework for a type of program called belief programs, a probabilistic extension of GOLOG programs where every action and sensing result could be noisy and every test condition refers to the agent's subjective beliefs. Inherited from GOLOG programs, the action-centered feature makes belief programs fairly suitable for high-level robot control under uncertainty. An important step before deploying such a program is to verify whether it satisfies properties as desired. At least two problems exist in doing verification: how to formally specify properties of a program and what is the complexity of verification. In this paper, we propose a formalism for belief programs based on a modal logic of actions and beliefs. Among other things, this allows us to express PCTL-like temporal properties smoothly. Besides, we investigate the decidability and undecidability for the verification problem of belief programs.
