A Box-Based Distance between Regions for Guiding the Reachability Analysis of SpaceEx
A Box-Based Distance between Regions for Guiding the Reachability Analysis of SpaceEx
复制标题
DOI：
10.1007/978-3-642-31424-7_35
复制
发表时间：
2012-07
期刊：
影响因子：
--
通讯作者：
Sergiy Bogomolov;Goran Frehse;R. Grosu;Hamed Ladan;A. Podelski;Martin Wehrle
中科院分区：
文献类型：
--
作者：
Sergiy Bogomolov;Goran Frehse;R. Grosu;Hamed Ladan;A. Podelski;Martin Wehrle
最近的一项技术，用于伪造方法的混合动力系统依赖于基于距离的启发式引导搜索到一个目标状态。问题是该技术是否可以用于使用区域作为其基本数据结构的可达性分析。在本文中，我们介绍了一个基于盒的区域之间的距离测量。我们提出了一种算法，给定两个区域，有效地计算它们之间的基于框的距离。我们已经在SpaceEx中实现了该算法，并将其用于指导SpaceEx的基于区域的可达性分析。我们说明了我们的方法在案例研究的导航基准的实际潜力。
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.