Verification of logical consistency in robotic reasoning
Verification of logical consistency in robotic reasoning
复制标题
DOI：
10.1016/j.robot.2016.06.005
复制
发表时间：
2016-09
期刊：
影响因子：
--
通讯作者：
Hongyang Qu;S. Veres
中科院分区：
文献类型：
--
作者：
Hongyang Qu;S. Veres
大多数自主机器人代理使用逻辑推理来保持自己的安全和允许的行为。给定一组规则，重要的是机器人能够建立其规则，其基于感知的信念，其计划的行动及其后果之间的一致性。本文研究了机器人智能体如何使用模型检测来检查其规则、信念和动作的一致性。一个规则集是由一个布尔演化系统与同步语义，它可以被转换成一个标记的转换系统（LTS）。证明了稳定性和一致性可以表示为计算树逻辑（CTL）和线性时态逻辑（LTL）性质。提出了两种新的算法，分别进行实时一致性和稳定性检查。他们的实现为我们提供了一个计算工具，它可以形成有效的一致性检查的基础上，船上的机器人。
Most autonomous robotic agents use logic inference to keep themselves to safe and permitted behaviour. Given a set of rules, it is important that the robot is able to establish the consistency between its rules, its perception-based beliefs, its planned actions and their consequences. This paper investigates how a robotic agent can use model checking to examine the consistency of its rules, beliefs and actions. A rule set is modelled by a Boolean evolution system with synchronous semantics, which can be translated into a labelled transition system (LTS). It is proven that stability and consistency can be formulated as computation tree logic (CTL) and linear temporal logic (LTL) properties. Two new algorithms are presented to perform realtime consistency and stability checks, respectively. Their implementation provides us a computational tool, which can form the basis of efficient consistency checks on-board robots.