Reasoning about Robot Actions: A Model Checking Approach

Abstract

Mobile robot control remains a di#cult challenge in changing and unpredictable environments. Reacting to unanticipated events, interacting and coordinating with other agents, and acquiring information about the world remain di#cult problems. These actions should be the direct products of the robot's capabilities to perceive, act, and process information intelligently, taking into account its state, that of the environment, and the goals to be achieved. This paper discusses the use of model-checking to reason about robot actions in this context. The approach proposed is to study behaviors that allow abstract, but informative models, so that a computer program can reason with them e#ciently. Model-checking can then be used as a means for verifying and planning robot actions with respect to such behaviors.