Using counterexamples for improving the precision of reachability computation with polyhedra

Chao Wang; Zijiang Yang; Aarti Gupta; Franjo Ivančić

doi:10.1007/978-3-540-73368-3_40

Using counterexamples for improving the precision of reachability computation with polyhedra

Chao Wang, Zijiang Yang, Aarti Gupta, Franjo Ivančić

Computer Science

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

19 Scopus citations

Abstract

We present an extrapolation with care set operator to accelerate termination of reachability computation with polyhedra. At the same time, a counterexample guided refinement algorithm is used to iteratively expand the care set to improve the precision of the reachability computation. We also introduce two heuristic algorithms called interpolate and restrict to minimize the polyhedral representations without reducing the accuracy. We present some promising experimental results from a preliminary implementation of these techniques.

Original language	English (US)
Title of host publication	Computer Aided Verification - 19th International Conference, CAV 2007, Proceedings
Publisher	Springer Verlag
Pages	352-365
Number of pages	14
ISBN (Print)	3540733671, 9783540733676
DOIs	https://doi.org/10.1007/978-3-540-73368-3_40
State	Published - 2007
Event	19th International Conference on Computer Aided Verification, CAV 2007 - Berlin, Germany Duration: Jul 3 2007 → Jul 7 2007

Publication series

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

Other

Other	19th International Conference on Computer Aided Verification, CAV 2007
Country/Territory	Germany
City	Berlin
Period	7/3/07 → 7/7/07

All Science Journal Classification (ASJC) codes

Theoretical Computer Science
General Computer Science

Access to Document

10.1007/978-3-540-73368-3_40

Cite this

Wang, C., Yang, Z., Gupta, A., & Ivančić, F. (2007). Using counterexamples for improving the precision of reachability computation with polyhedra. In Computer Aided Verification - 19th International Conference, CAV 2007, Proceedings (pp. 352-365). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 4590 LNCS). Springer Verlag. https://doi.org/10.1007/978-3-540-73368-3_40

Wang, Chao ; Yang, Zijiang ; Gupta, Aarti et al. / Using counterexamples for improving the precision of reachability computation with polyhedra. Computer Aided Verification - 19th International Conference, CAV 2007, Proceedings. Springer Verlag, 2007. pp. 352-365 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).

@inproceedings{54cda1d621cf4a9b9e3e8ed736b565f0,

title = "Using counterexamples for improving the precision of reachability computation with polyhedra",

abstract = "We present an extrapolation with care set operator to accelerate termination of reachability computation with polyhedra. At the same time, a counterexample guided refinement algorithm is used to iteratively expand the care set to improve the precision of the reachability computation. We also introduce two heuristic algorithms called interpolate and restrict to minimize the polyhedral representations without reducing the accuracy. We present some promising experimental results from a preliminary implementation of these techniques.",

author = "Chao Wang and Zijiang Yang and Aarti Gupta and Franjo Ivan{\v c}i{\'c}",

year = "2007",

doi = "10.1007/978-3-540-73368-3_40",

language = "English (US)",

isbn = "3540733671",

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

publisher = "Springer Verlag",

pages = "352--365",

booktitle = "Computer Aided Verification - 19th International Conference, CAV 2007, Proceedings",

address = "Germany",

note = "19th International Conference on Computer Aided Verification, CAV 2007 ; Conference date: 03-07-2007 Through 07-07-2007",

}

Wang, C, Yang, Z, Gupta, A & Ivančić, F 2007, Using counterexamples for improving the precision of reachability computation with polyhedra. in Computer Aided Verification - 19th International Conference, CAV 2007, Proceedings. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 4590 LNCS, Springer Verlag, pp. 352-365, 19th International Conference on Computer Aided Verification, CAV 2007, Berlin, Germany, 7/3/07. https://doi.org/10.1007/978-3-540-73368-3_40

Using counterexamples for improving the precision of reachability computation with polyhedra. / Wang, Chao; Yang, Zijiang; Gupta, Aarti et al.
Computer Aided Verification - 19th International Conference, CAV 2007, Proceedings. Springer Verlag, 2007. p. 352-365 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 4590 LNCS).

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

TY - GEN

T1 - Using counterexamples for improving the precision of reachability computation with polyhedra

AU - Wang, Chao

AU - Yang, Zijiang

AU - Gupta, Aarti

AU - Ivančić, Franjo

PY - 2007

Y1 - 2007

N2 - We present an extrapolation with care set operator to accelerate termination of reachability computation with polyhedra. At the same time, a counterexample guided refinement algorithm is used to iteratively expand the care set to improve the precision of the reachability computation. We also introduce two heuristic algorithms called interpolate and restrict to minimize the polyhedral representations without reducing the accuracy. We present some promising experimental results from a preliminary implementation of these techniques.

AB - We present an extrapolation with care set operator to accelerate termination of reachability computation with polyhedra. At the same time, a counterexample guided refinement algorithm is used to iteratively expand the care set to improve the precision of the reachability computation. We also introduce two heuristic algorithms called interpolate and restrict to minimize the polyhedral representations without reducing the accuracy. We present some promising experimental results from a preliminary implementation of these techniques.

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

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

U2 - 10.1007/978-3-540-73368-3_40

DO - 10.1007/978-3-540-73368-3_40

M3 - Conference contribution

AN - SCOPUS:38149095659

SN - 3540733671

SN - 9783540733676

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

SP - 352

EP - 365

BT - Computer Aided Verification - 19th International Conference, CAV 2007, Proceedings

PB - Springer Verlag

T2 - 19th International Conference on Computer Aided Verification, CAV 2007

Y2 - 3 July 2007 through 7 July 2007

ER -

Wang C, Yang Z, Gupta A, Ivančić F. Using counterexamples for improving the precision of reachability computation with polyhedra. In Computer Aided Verification - 19th International Conference, CAV 2007, Proceedings. Springer Verlag. 2007. p. 352-365. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). doi: 10.1007/978-3-540-73368-3_40

Using counterexamples for improving the precision of reachability computation with polyhedra

Abstract

Publication series

Other

All Science Journal Classification (ASJC) codes

Access to Document

Other files and links

Fingerprint

Cite this