Abstraction for model checking robot behaviour
Ryan Fraser Kirwan, Alice Ann Miller · ENLIGHTEN (Jurnal Bimbingan dan Konseling Islam) · 2011
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.