AMC: Approximation Refinement Model Checker

Overview

AMC is a model checker for non-linear hybrid systems based on the abstraction refinement framework. In collaboration we Ed Clarke, I have implemented AMC in Mathematica at the Carnegie Mellon University and the University of Oldenburg.

Case Studies

We have worked on model checking collision avoidance protocols in air traffic management. These protocols direct aircraft, which are flying close, to flight paths which respect the protected zones of the aircraft.

Abstract

In this paper, we analyze limits of approximation techniques for (non-linear) continuous image computation in model checking hybrid systems. In particular, we show that even a single step of continuous image computation is not semidecidable numerically even for a very restricted class of functions. Moreover, we show that symbolic insight about derivative bounds provides sufficient additional information for approximation refinement model checking. Finally, we prove that purely numerical algorithms can perform continuous image computation with arbitrarily high probability. Using these results, we analyze the prerequisites for a safe operation of the roundabout maneuver in air traffic collision avoidance.

Keywords: model checking, hybrid systems, image computation

[PC07]

André Platzer and Edmund M. Clarke. The Image Computation Problem in Hybrid Systems Model Checking. In A. Bemporad, A. Bicchi, and G. Buttazzo, editors, Hybrid Systems: Computation and Control, 10th International Conference, HSCC 2007, Pisa, Italy, Proceedings, volume 4416 of LNCS, pages 473-486. Springer, 2007, (c) Springer Verlag
[bib | pdf | slides]