Affordable Access

Abstraction for model checking robot behaviour

Department of Computing Science, University of Glasgow
Publication Date
  • Computer Science


We use model checking to verify properties of real systems. These systems consist of robots interacting with obstacles within an environment and learning to avoid collision. We describe an approach to abstract environments so that all feasible 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.

There are no comments yet on this publication. Be the first to share your thoughts.