Counterexample-guided refinement of template Polyhedra

Bogomolov, Sergiy and Frehse, Goran and Giacobbe, Mirco and Henzinger, Thomas A (2017) Counterexample-guided refinement of template Polyhedra. In: TACAS: Tools and Algorithms for the Construction and Analysis of Systems, April 24, 2017, Uppsala, Sweden.

This is the latest version of this item.

[img] Text
Download (550Kb)
Official URL:


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.

Item Type: Conference or Workshop Item (Paper)
Subjects: 000 Computer science, knowledge & general works > 000 Computer science, knowledge & systems
Research Group: Henzinger Group
Depositing User: Mirco Giacobbe
Date Deposited: 12 Feb 2018 13:41
Last Modified: 12 Feb 2018 13:41

Available Versions of this Item

Actions (login required)

View Item View Item