Abstraction for model checking robot behaviour

Abstract

We use model checking to verify properties of real systems. These systems consist of robots interacting with obstacles
\nwithin an environment and learning to avoid collision. We describe an approach to abstract environments so that all
\nfeasible scenarios are represented, and properties are still applicable. The abstraction is necessary for the verification (and ultimately, comparison) of learning algorithms and, although currently applied to Promela specifications, is applicable to other specification formalisms.