The image computation problem in hybrid systems model checking

@INPROCEEDINGS{DBLP:conf/hybrid/PlatzerC07,
	pdf = {pub/happroximation.pdf},
	slides = {pub/happroximation-slides.pdf},

  author    = {Andr{\'e} Platzer and
               Edmund M. Clarke},
  title     = {The Image Computation Problem in Hybrid
               Systems Model Checking},
  booktitle = {HSCC},
  longbooktitle = {Hybrid Systems: Computation and Control,
               10th International Conference, HSCC 2007,
               Pisa, Italy, Proceedings},
  year      = {2007},
  pages     = {473-486},
  doi       = {10.1007/978-3-540-71493-4_37},
  editor    = {Alberto Bemporad and
               Antonio Bicchi and
               Giorgio Buttazzo},
  publisher = {Springer},
  series    = {LNCS},
  volume    = {4416},
  isbn      = {978-3-540-71492-7},
  keywords  = {model checking, hybrid systems, image
               computation},
  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.},
}```