A box-based distance between regions for guiding the reachability analysis of SpaceEx
ConferencePaper (Artikel, die in Tagungsbänden erschienen sind)
 
ID 1422628
Author(s) Bogomolov, Sergiy; Frehse, Goran; Grosu, Radu; Ladan, Hamed; Podelski, Andreas; Wehrle, Martin
Author(s) at UniBasel Wehrle, Martin
Year 2012
Title A box-based distance between regions for guiding the reachability analysis of SpaceEx
Editor(s) Madhusudan, P.; Seshia, Sanjit A.
Book title (Conference Proceedings) Computer Aided Verification : 24th International Conference (CAV 2012)
Place of Conference Berkeley, California, USA
Year of Conference 2012
Publisher Springer
Place of Publication Belin
Pages S. 479-494
ISSN/ISBN 978-3-642-31424-7 (E-Book) ; 978-3-642-31423-0 (Print)
Abstract 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.
Series title Lecture Notes in Computer Science
Number 7358
edoc-URL http://edoc.unibas.ch/dok/A6043736
Full Text on edoc No
Digital Object Identifier DOI 10.1007/978-3-642-31424-7_35
ISI-Number INSPEC:12867865
 
   

MCSS v5.8 PRO. 0.456 sec, queries - 0.000 sec ©Universität Basel  |  Impressum   |    
11/08/2020