Verification of Logical Consistency in Robotic Reasoning

TL;DR

This paper presents a method for robotic agents to verify the logical consistency of their rules, beliefs, and actions using model checking techniques, ensuring safe and reliable autonomous behavior.

Contribution

It introduces a novel approach modeling rule sets as Boolean evolution systems and develops algorithms for real-time consistency and stability verification in robots.

Findings

Algorithms enable real-time consistency checks

Model checking formulations for stability and consistency

Implementation supports on-board robotic verification

Abstract

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.