Counterexample guided refinement of template polyhedra Conference Paper


Author(s): Bogomolov, Sergiy; Frehse, Goran; Giacobbe, Mirco; Henzinger, Thomas A
Title: Counterexample guided refinement of template polyhedra
Title Series: LNCS
Affiliation IST Austria
Abstract: 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.
Conference Title: TACAS: Tools and Algorithms for the Construction and Analysis of Systems
Volume: 10205
Conference Dates: April 22 - 29, 2017
Conference Location: Uppsala, Sweden
Publisher: Springer  
Date Published: 2017-01-01
Start Page: 589
End Page: 606
URL:
DOI: 10.1007/978-3-662-54577-5_34
Notes: This research was supported in part by the Austrian Science Fund (FWF) under grants S11402-N23 (RiSE/SHiNE) and Z211-N23 (Wittgenstein Award), by the European Commission under grant 643921 (UnCoVerCPS), and by the ARC project DP140104219 (Robust AI Planning for Hybrid Systems).
Open access: yes (repository)
IST Austria Authors
  1. Thomas A. Henzinger
    415 Henzinger
Related IST Austria Work