A Box-Based Distance between Regions for Guiding the Reachability Analysis of SpaceEx.*

S. Bogomolov, G. Frehse, R. Grosu, H. Ladan, A. Podelski, and M. Wehrle.

A recent technique used in falsification methods for hybrid systems relies on distance-based heuristics for guiding the search towards a goal state. The question is whether the technique can be carried over to reachability analyses that use regions as their basic data structure. In this paper, we introduce a box-based distance measure between regions. We present an algorithm that, given two regions, efficiently computes the box-based distance between them. We have implemented the algorithm in SpaceEx and use it for guiding the region-based reachability analysis of SpaceEx. We illustrate the practical potential of our approach in a case study for the navigation benchmark.

In Proc. of CAV'12, the 24th International Conference on Computer Aided Verification, Berkeley, California, USA, July, Springer, LNCS.

*This work was partially supported by the NSF Expeditions Award CNS-09-26190, the and the AFOSR FA-0550-09-1-0481 Award.