Reasoning about high-level robot programs by model checking and local validity tests

Giuseppe De Giacomo, Riccardo Rosati.
In Proceedings of the AAAI 1998 Fall Symposium on Cognitive Robotics, AAAI-Press, 1998.

Abstract:

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.

Bibtex entry:

@Inproceedings{DeRo98,
author = "De Giacomo, Giuseppe and Rosati, Riccardo",
title = "Reasoning about high-level robot programs by model checking and local validity tests",
booktitle = "Proceedings of the AAAI 1998 Fall Symposium on Cognitive Robotics",
publisher = "AAAI-Press",
year = 1998,
}