Model checking for improved adaptive behaviour

Closed loop systems are traditionally analysed using simulation. We show how a formal approach, namely model checking, can be used to enhance and inform this analysis. Specifically, model checking can be used to verify properties for any execution of a system, not just a single experimental path. We describe how model checking has been used to investigate a system consisting of a robot navigating around an environment, avoiding obstacles using sequence learning. We illustrate the power of this approach by showing how a previous assumption about the system, gained though vigorous simulation, was demonstrated to be incorrect, using the formal approach.