A box-based distance between regions for guiding the reachability analysis of SpaceEx

Sergiy Bogomolov; Goran Frehse; Radu Grosu; Hamed Ladan; Andreas Podelski; Martin Wehrle

doi:10.1007/978-3-642-31424-7_35

A box-based distance between regions for guiding the reachability analysis of SpaceEx

Sergiy Bogomolov^*, Goran Frehse, Radu Grosu, Hamed Ladan, Andreas Podelski, Martin Wehrle

^*Corresponding author for this work

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

12 Citations (Scopus)

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.

Original language	English
Title of host publication	Computer Aided Verification - 24th International Conference, CAV 2012, Proceedings
Pages	479-494
Number of pages	16
DOIs	https://doi.org/10.1007/978-3-642-31424-7_35
Publication status	Published - 2012
Externally published	Yes
Event	24th International Conference on Computer Aided Verification, CAV 2012 - Berkeley, CA, United States Duration: 7 Jul 2012 → 13 Jul 2012

Publication series

Name	Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume	7358 LNCS
ISSN (Print)	0302-9743
ISSN (Electronic)	1611-3349

Conference

Conference	24th International Conference on Computer Aided Verification, CAV 2012
Country/Territory	United States
City	Berkeley, CA
Period	7/07/12 → 13/07/12

Access to Document

10.1007/978-3-642-31424-7_35

Cite this

Bogomolov, S., Frehse, G., Grosu, R., Ladan, H., Podelski, A., & Wehrle, M. (2012). A box-based distance between regions for guiding the reachability analysis of SpaceEx. In Computer Aided Verification - 24th International Conference, CAV 2012, Proceedings (pp. 479-494). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 7358 LNCS). https://doi.org/10.1007/978-3-642-31424-7_35

Bogomolov, Sergiy ; Frehse, Goran ; Grosu, Radu et al. / A box-based distance between regions for guiding the reachability analysis of SpaceEx. Computer Aided Verification - 24th International Conference, CAV 2012, Proceedings. 2012. pp. 479-494 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).

@inproceedings{1239332802cb4c75a06bb8baf8d44d52,

title = "A box-based distance between regions for guiding the reachability analysis of SpaceEx",

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.",

author = "Sergiy Bogomolov and Goran Frehse and Radu Grosu and Hamed Ladan and Andreas Podelski and Martin Wehrle",

year = "2012",

doi = "10.1007/978-3-642-31424-7_35",

language = "English",

isbn = "9783642314230",

series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

pages = "479--494",

booktitle = "Computer Aided Verification - 24th International Conference, CAV 2012, Proceedings",

note = "24th International Conference on Computer Aided Verification, CAV 2012 ; Conference date: 07-07-2012 Through 13-07-2012",

}

Bogomolov, S, Frehse, G, Grosu, R, Ladan, H, Podelski, A & Wehrle, M 2012, A box-based distance between regions for guiding the reachability analysis of SpaceEx. in Computer Aided Verification - 24th International Conference, CAV 2012, Proceedings. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 7358 LNCS, pp. 479-494, 24th International Conference on Computer Aided Verification, CAV 2012, Berkeley, CA, United States, 7/07/12. https://doi.org/10.1007/978-3-642-31424-7_35

A box-based distance between regions for guiding the reachability analysis of SpaceEx. / Bogomolov, Sergiy; Frehse, Goran; Grosu, Radu et al.
Computer Aided Verification - 24th International Conference, CAV 2012, Proceedings. 2012. p. 479-494 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 7358 LNCS).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

TY - GEN

T1 - A box-based distance between regions for guiding the reachability analysis of SpaceEx

AU - Bogomolov, Sergiy

AU - Frehse, Goran

AU - Grosu, Radu

AU - Ladan, Hamed

AU - Podelski, Andreas

AU - Wehrle, Martin

PY - 2012

Y1 - 2012

N2 - 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.

AB - 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.

UR - http://www.scopus.com/inward/record.url?scp=84864052497&partnerID=8YFLogxK

U2 - 10.1007/978-3-642-31424-7_35

DO - 10.1007/978-3-642-31424-7_35

M3 - Conference contribution

AN - SCOPUS:84864052497

SN - 9783642314230

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 479

EP - 494

BT - Computer Aided Verification - 24th International Conference, CAV 2012, Proceedings

T2 - 24th International Conference on Computer Aided Verification, CAV 2012

Y2 - 7 July 2012 through 13 July 2012

ER -

Bogomolov S, Frehse G, Grosu R, Ladan H, Podelski A, Wehrle M. A box-based distance between regions for guiding the reachability analysis of SpaceEx. In Computer Aided Verification - 24th International Conference, CAV 2012, Proceedings. 2012. p. 479-494. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). doi: 10.1007/978-3-642-31424-7_35

A box-based distance between regions for guiding the reachability analysis of SpaceEx

Abstract

Publication series

Conference

Access to Document

Other files and links

Fingerprint

Cite this