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

Giuseppe De Giacomo, Riccardo Rosati

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.


This page is copyrighted by AAAI. All rights reserved. Your use of this site constitutes acceptance of all of AAAI's terms and conditions and privacy policy.