Using counterexamples for improving the precision of reachability computation with polyhedra

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

Research output: Chapter in Book/Report/Conference proceedingConference contribution

14 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 languageEnglish (US)
Title of host publicationComputer Aided Verification - 19th International Conference, CAV 2007, Proceedings
PublisherSpringer Verlag
Pages352-365
Number of pages14
ISBN (Print)3540733671, 9783540733676
DOIs
StatePublished - Jan 1 2007
Externally publishedYes
Event19th International Conference on Computer Aided Verification, CAV 2007 - Berlin, Germany
Duration: Jul 3 2007Jul 7 2007

Publication series

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

Other

Other19th International Conference on Computer Aided Verification, CAV 2007
CountryGermany
CityBerlin
Period7/3/077/7/07

All Science Journal Classification (ASJC) codes

  • Theoretical Computer Science
  • Computer Science(all)

Fingerprint Dive into the research topics of 'Using counterexamples for improving the precision of reachability computation with polyhedra'. Together they form a unique fingerprint.

  • 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