TY - GEN
T1 - Counterexample-guided refinement of template polyhedra
AU - Bogomolov, Sergiy
AU - Frehse, Goran
AU - Giacobbe, Mirco
AU - Henzinger, Thomas A.
N1 - Publisher Copyright:
© Springer-Verlag GmbH Germany 2017.
PY - 2017/1/1
Y1 - 2017/1/1
N2 - Template polyhedra generalize intervals and octagons to polyhedra whose facets are orthogonal to a given set of arbitrary directions. They have been employed in the abstract interpretation of programs and, with particular success, in the reachability analysis of hybrid automata. While previously, the choice of directions has been left to the user or a heuristic, we present a method for the automatic discovery of directions that generalize and eliminate spurious counterexamples. We show that for the class of convex hybrid automata, i.e., hybrid automata with (possibly nonlinear) convex constraints on derivatives, such directions always exist and can be found using convex optimization. We embed our method inside a CEGAR loop, thus enabling the time-unbounded reachability analysis of an important and richer class of hybrid automata than was previously possible. We evaluate our method on several benchmarks, demonstrating also its superior efficiency for the special case of linear hybrid automata.
AB - Template polyhedra generalize intervals and octagons to polyhedra whose facets are orthogonal to a given set of arbitrary directions. They have been employed in the abstract interpretation of programs and, with particular success, in the reachability analysis of hybrid automata. While previously, the choice of directions has been left to the user or a heuristic, we present a method for the automatic discovery of directions that generalize and eliminate spurious counterexamples. We show that for the class of convex hybrid automata, i.e., hybrid automata with (possibly nonlinear) convex constraints on derivatives, such directions always exist and can be found using convex optimization. We embed our method inside a CEGAR loop, thus enabling the time-unbounded reachability analysis of an important and richer class of hybrid automata than was previously possible. We evaluate our method on several benchmarks, demonstrating also its superior efficiency for the special case of linear hybrid automata.
U2 - 10.1007/978-3-662-54577-5_34
DO - 10.1007/978-3-662-54577-5_34
M3 - Conference contribution
AN - SCOPUS:85017522066
SN - 9783662545768
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 589
EP - 606
BT - Tools and Algorithms for the Construction and Analysis of Systems - 23rd International Conference, TACAS 2017 held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2017, Proceedings
A2 - Margaria , Tiziana
A2 - Legay, Axel
PB - Springer Verlag
T2 - 23rd International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2017 held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2017
Y2 - 22 April 2017 through 29 April 2017
ER -