The image computation problem in hybrid systems model checking

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.

@inproceedings{DBLP:conf/hybrid/PlatzerC07,
	pdf = {pub/happroximation.pdf},
	slides = {pub/happroximation-slides.pdf},
	author = {['André Platzer', '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', 'Antonio Bicchi', '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.}
}