On efficient consistency checks by robots

Most autonomous robotic agents use logic inference to keep to safe and permitted behaviour. Given a set of rules, it is important that the robot is able to establish the consistency of its rules and its current perception-based beliefs. This paper investigates how a robotic agent can use model checking to examine the consistency of its rules and beliefs. 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, which is crucial for efficient consistency checks by robots.