Name
Abstract | ||
|---|---|---|
To decide whether a set of states is reachable in a hybrid system, over-approximative symbolic successor computations can be used, where the symbolic representation of state sets as well as the successor computations have several parameters which determine the efficiency and the precision of the computations. Naturally, faster computations come with less precision and more spurious counterexamples. To remove a spurious counterexample, the only possibility offered by current tools is to reduce the error by re-starting the complete search with different parameters. In this paper we propose a CEGAR approach that takes as input a user-defined ordered list of search configurations, which are used to dynamically refine the search tree along potentially spurious counterexamples. Dedicated datastructures allow to extract as much useful information as possible from previous computations in order to reduce the refinement overhead. |
Year | DOI | Venue |
|---|---|---|
2018 | 10.1007/978-3-319-89963-3_17 | Lecture Notes in Computer Science |
Field | DocType | Volume |
Computer science,Successor cardinal,Reachability,Theoretical computer science,Counterexample,Hybrid system,Spurious relationship,Computation,Search tree | Conference | 10806 |
ISSN | Citations | PageRank |
0302-9743 | 2 | 0.39 |
References | Authors | |
15 | 2 | |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Stefan Schupp | 1 | 27 | 2.20 |
| Erika Ábrahám | 2 | 830 | 63.17 |