Verification of Logical Consistency in Robotic Reasoning
This addresses the need for safe and permitted behavior in autonomous robotic agents, though it is incremental as it builds on existing model checking techniques.
The paper tackles the problem of verifying logical consistency in robotic reasoning by using model checking to examine the consistency of rules, beliefs, and actions, presenting two new algorithms for real-time checks and implementing a computational tool for on-board robots.
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.