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.

The visual presentation layer of the AMC model checker can be used to animate traces like these examples of collision avoidance protocols in air traffic management:

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

1. André Platzer and Edmund M. Clarke.
   The image computation problem in hybrid systems model checking.
   In Alberto Bemporad, Antonio Bicchi and Giorgio Buttazzo, editors, Hybrid Systems: Computation and Control, 10th International Conference, HSCC 2007, Pisa, Italy, Proceedings, volume 4416 of LNCS, pp. 473-486. Springer, 2007, © Springer
   [bib | ✂ | pdf | doi | slides | tool | abstract]
   
   

Due to so many requests for my slides, I have decided to put them online under the above link.

We address safety model checking for robust hybrid systems at the decidability borderline of image computation. We present approximation-refinement techniques for uniform piecewise polynomial over-approximations of non-linear dynamics exploiting flow bounds, probabilistic bounds or Lipschitz bounds and robust switching surfaces. We show decidability in the presense of bounds, probabilistic bounds, or Lipschitz bounds using effective Weierstraß approximations. We show that image computation for hybrid systems is undecidable in the general case.

Also see publications on model checking.