---
res:
bibo_abstract:
- "Hybrid automata combine finite automata and dynamical systems, and model the
interaction of digital with physical systems. Formal analysis that can guarantee
the safety of all behaviors or rigorously witness failures, while unsolvable in
general, has been tackled algorithmically using, e.g., abstraction, bounded model-checking,
assisted theorem proving.\r\nNevertheless, very few methods have addressed the
time-unbounded reachability analysis of hybrid automata and, for current sound
and automatic tools, scalability remains critical. We develop methods for the
polyhedral abstraction of hybrid automata, which construct coarse overapproximations
and tightens them incrementally, in a CEGAR fashion. We use template polyhedra,
i.e., polyhedra whose facets are normal to a given set of directions.\r\nWhile,
previously, directions were given by the user, we introduce (1) the first method\r\nfor
computing template directions from spurious counterexamples, so as to generalize
and\r\neliminate them. The method applies naturally to convex hybrid automata,
i.e., hybrid\r\nautomata with (possibly non-linear) convex constraints on derivatives
only, while for linear\r\nODE requires further abstraction. Specifically, we introduce
(2) the conic abstractions,\r\nwhich, partitioning the state space into appropriate
(possibly non-uniform) cones, divide\r\ncurvy trajectories into relatively straight
sections, suitable for polyhedral abstractions.\r\nFinally, we introduce (3) space-time
interpolation, which, combining interval arithmetic\r\nand template refinement,
computes appropriate (possibly non-uniform) time partitioning\r\nand template
directions along spurious trajectories, so as to eliminate them.\r\nWe obtain
sound and automatic methods for the reachability analysis over dense\r\nand unbounded
time of convex hybrid automata and hybrid automata with linear ODE.\r\nWe build
prototype tools and compare—favorably—our methods against the respective\r\nstate-of-the-art
tools, on several benchmarks.@eng"
bibo_authorlist:
- foaf_Person:
foaf_givenName: Mirco
foaf_name: Giacobbe, Mirco
foaf_surname: Giacobbe
foaf_workInfoHomepage: http://www.librecat.org/personId=3444EA5E-F248-11E8-B48F-1D18A9856A87
orcid: 0000-0001-8180-0904
bibo_doi: 10.15479/AT:ISTA:6894
dct_date: 2019^xs_gYear
dct_isPartOf:
- http://id.crossref.org/issn/2663-337X
dct_language: eng
dct_publisher: IST Austria@
dct_title: Automatic time-unbounded reachability analysis of hybrid systems@
...