Reasoning on High-Level Robot Behaviors by Model Checking and Local Validity Tests

Contents

In this paper we explore a research direction in reasoning about actions stemming from the Robot-Tino Project at the University of Rome. We introduce a logical formalism that combines a very expressive logic of programs, the modal mu-calculus, with a special use of a minimal knowledge operator. Reasoning in such formalism can be done by integrating model checking for modal mu-calculus and propositional inference. This allows for exploiting existing model checking techniques and systems for reasoning about complex high-level robot behaviors, without renouncing to deal with incomplete information on the initial state and both the preconditions and the effects of actions.