Reasoning about High-Level Robot Behaviors by Model Checking and Local Validity Tests
Giuseppe De Giacomo, Riccardo Rosati · 1998
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 highlevel robot behaviors, without renouncing to deal with incomplete information on the initial state and both the preconditions and the effects of actions. Introduction In this paper we explore a research direction stemming from the Robot-Tino Project at the University of Rome "La Sapienza" (De Giacomo et al. 1996; 1997). This project aims at integrating deliberative behaviors specified in a logical formalism with reactive behaviors provided by low-level mechanisms, which a...