--- _id: '631' abstract: - lang: eng text: 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. acknowledgement: 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). alternative_title: - LNCS author: - first_name: Sergiy full_name: Bogomolov, Sergiy id: 369D9A44-F248-11E8-B48F-1D18A9856A87 last_name: Bogomolov orcid: 0000-0002-0686-0365 - first_name: Goran full_name: Frehse, Goran last_name: Frehse - first_name: Mirco full_name: Giacobbe, Mirco id: 3444EA5E-F248-11E8-B48F-1D18A9856A87 last_name: Giacobbe orcid: 0000-0001-8180-0904 - first_name: Thomas A full_name: Henzinger, Thomas A id: 40876CD8-F248-11E8-B48F-1D18A9856A87 last_name: Henzinger orcid: 0000−0002−2985−7724 citation: ama: 'Bogomolov S, Frehse G, Giacobbe M, Henzinger TA. Counterexample guided refinement of template polyhedra. In: Vol 10205. Springer; 2017:589-606. doi:10.1007/978-3-662-54577-5_34' apa: 'Bogomolov, S., Frehse, G., Giacobbe, M., & Henzinger, T. A. (2017). Counterexample guided refinement of template polyhedra (Vol. 10205, pp. 589–606). Presented at the TACAS: Tools and Algorithms for the Construction and Analysis of Systems, Uppsala, Sweden: Springer. https://doi.org/10.1007/978-3-662-54577-5_34' chicago: Bogomolov, Sergiy, Goran Frehse, Mirco Giacobbe, and Thomas A Henzinger. “Counterexample Guided Refinement of Template Polyhedra,” 10205:589–606. Springer, 2017. https://doi.org/10.1007/978-3-662-54577-5_34. ieee: 'S. Bogomolov, G. Frehse, M. Giacobbe, and T. A. Henzinger, “Counterexample guided refinement of template polyhedra,” presented at the TACAS: Tools and Algorithms for the Construction and Analysis of Systems, Uppsala, Sweden, 2017, vol. 10205, pp. 589–606.' ista: 'Bogomolov S, Frehse G, Giacobbe M, Henzinger TA. 2017. Counterexample guided refinement of template polyhedra. TACAS: Tools and Algorithms for the Construction and Analysis of Systems, LNCS, vol. 10205, 589–606.' mla: Bogomolov, Sergiy, et al. Counterexample Guided Refinement of Template Polyhedra. Vol. 10205, Springer, 2017, pp. 589–606, doi:10.1007/978-3-662-54577-5_34. short: S. Bogomolov, G. Frehse, M. Giacobbe, T.A. Henzinger, in:, Springer, 2017, pp. 589–606. conference: end_date: 2017-04-29 location: Uppsala, Sweden name: 'TACAS: Tools and Algorithms for the Construction and Analysis of Systems' start_date: 2017-04-22 date_created: 2018-12-11T11:47:36Z date_published: 2017-03-31T00:00:00Z date_updated: 2023-09-07T12:53:00Z day: '31' ddc: - '000' department: - _id: ToHe doi: 10.1007/978-3-662-54577-5_34 file: - access_level: open_access checksum: f395d0d20102b89aeaad8b4ef4f18f4f content_type: application/pdf creator: system date_created: 2018-12-12T10:11:41Z date_updated: 2020-07-14T12:47:27Z file_id: '4897' file_name: IST-2017-741-v1+1_main.pdf file_size: 569863 relation: main_file - access_level: open_access checksum: f416ee1ae4497b23ecdf28b1f18bb8df content_type: application/pdf creator: system date_created: 2018-12-12T10:11:42Z date_updated: 2020-07-14T12:47:27Z file_id: '4898' file_name: IST-2018-741-v2+2_main.pdf file_size: 563276 relation: main_file file_date_updated: 2020-07-14T12:47:27Z has_accepted_license: '1' intvolume: ' 10205' language: - iso: eng month: '03' oa: 1 oa_version: Submitted Version page: 589 - 606 project: - _id: 25F5A88A-B435-11E9-9278-68D0E5697425 call_identifier: FWF grant_number: S11402-N23 name: Moderne Concurrency Paradigms - _id: 25F42A32-B435-11E9-9278-68D0E5697425 call_identifier: FWF grant_number: Z211 name: The Wittgenstein Prize publication_identifier: isbn: - 978-366254576-8 publication_status: published publisher: Springer publist_id: '7162' pubrep_id: '966' quality_controlled: '1' related_material: record: - id: '6894' relation: dissertation_contains status: public scopus_import: 1 status: public title: Counterexample guided refinement of template polyhedra type: conference user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87 volume: 10205 year: '2017' ...