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.
翻译:在最近的一篇论文中,Belle and Levesque为一种叫作信仰程序的方案提出了一个框架,这是GOLOG方案的一个概率扩展,其中每一种行动和感知结果都会吵闹,而且每个测试条件都指代理人的主观信仰。从GOLOG方案中生来,以行动为中心的特征使得信仰方案在不确定的情况下完全适合高级机器人的控制。在部署这样一个程序之前的一个重要步骤是核实它是否满足了期望的特性。在进行核查时至少存在两个问题:如何正式指定一个程序的特性以及核查的复杂性。在本文中,我们建议基于行动和信仰模式逻辑的信仰方案的形式主义。这使我们能够顺利地表达PCTL相似的时间属性。此外,我们还要调查信仰程序核查问题的可衰减性和不可衰减性。