206
21 December 2017 - 14h00
Counterexample-guided Refinement of Template Polyhedra
by Mirco Giacobbe from IST Austria
Abstract: Template polyhedra generalize intervals and octagons to polyhedra whose facets are orthogonal to a given set of arbitrary directions. They offer a very powerful framework for the reachability analysis of hybrid automata, as an appropriate choice of directions allows an effective tuning between accuracy and precision. In this talk, I will present a method for the automatic discovery of directions that generalize and eliminate spurious counterexamples, task which was previously left to the user or a heuristic. I will show that for the class of convex hybrid automata, i.e. hybrid automata with (possibly non-linear) convex constraints on derivatives, such directions can be found using convex optimization. Finally, I will show our experimental results on several bechmarks, demonstrating an effective time-unbounded reachability analysis for a richer class of hybrid automata than was previously possible, and superior performance for the special case of linear hybrid automata.
Guest researcher invited by the TEMPO Team
