Automatic time-unbounded reachability analysis of hybrid systems

Giacobbe M. 2019. Automatic time-unbounded reachability analysis of hybrid systems. Institute of Science and Technology Austria.

Download
OA giacobbe_thesis.pdf 4.10 MB [Published Version]

Thesis | PhD | Published | English
Series Title
ISTA Thesis
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. Nevertheless, 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. While, previously, directions were given by the user, we introduce (1) the first method for computing template directions from spurious counterexamples, so as to generalize and eliminate them. The method applies naturally to convex hybrid automata, i.e., hybrid automata with (possibly non-linear) convex constraints on derivatives only, while for linear ODE requires further abstraction. Specifically, we introduce (2) the conic abstractions, which, partitioning the state space into appropriate (possibly non-uniform) cones, divide curvy trajectories into relatively straight sections, suitable for polyhedral abstractions. Finally, we introduce (3) space-time interpolation, which, combining interval arithmetic and template refinement, computes appropriate (possibly non-uniform) time partitioning and template directions along spurious trajectories, so as to eliminate them. We obtain sound and automatic methods for the reachability analysis over dense and unbounded time of convex hybrid automata and hybrid automata with linear ODE. We build prototype tools and compare—favorably—our methods against the respective state-of-the-art tools, on several benchmarks.
Publishing Year
Date Published
2019-09-30
Publisher
Institute of Science and Technology Austria
Page
132
eISSN
IST-REx-ID

Cite this

Giacobbe M. Automatic time-unbounded reachability analysis of hybrid systems. 2019. doi:10.15479/AT:ISTA:6894
Giacobbe, M. (2019). Automatic time-unbounded reachability analysis of hybrid systems. Institute of Science and Technology Austria. https://doi.org/10.15479/AT:ISTA:6894
Giacobbe, Mirco. “Automatic Time-Unbounded Reachability Analysis of Hybrid Systems.” Institute of Science and Technology Austria, 2019. https://doi.org/10.15479/AT:ISTA:6894.
M. Giacobbe, “Automatic time-unbounded reachability analysis of hybrid systems,” Institute of Science and Technology Austria, 2019.
Giacobbe M. 2019. Automatic time-unbounded reachability analysis of hybrid systems. Institute of Science and Technology Austria.
Giacobbe, Mirco. Automatic Time-Unbounded Reachability Analysis of Hybrid Systems. Institute of Science and Technology Austria, 2019, doi:10.15479/AT:ISTA:6894.
All files available under the following license(s):
Creative Commons Attribution 4.0 International Public License (CC-BY 4.0):
Main File(s)
File Name
Access Level
OA Open Access
Date Uploaded
2019-09-27
MD5 Checksum
773beaf4a85dc2acc2c12b578fbe1965

Source File
Access Level
Restricted Closed Access
Date Uploaded
2019-09-27
MD5 Checksum
97f1c3da71feefd27e6e625d32b4c75b

Material in ISTA:
Part of this Dissertation
Part of this Dissertation
Part of this Dissertation

Export

Marked Publications

Open Data ISTA Research Explorer

Search this title in

Google Scholar