Conic abstractions for hybrid systems

S. Bogomolov, M. Giacobbe, T.A. Henzinger, H. Kong, in:, A. Abate, G. Geeraerts (Eds.), Springer, 2017, pp. 116–132.

Download
OA 3.81 MB

Conference Paper | Published | English
Editor
;
Department
Series Title
LNCS
Abstract
Despite researchers’ efforts in the last couple of decades, reachability analysis is still a challenging problem even for linear hybrid systems. Among the existing approaches, the most practical ones are mainly based on bounded-time reachable set over-approximations. For the purpose of unbounded-time analysis, one important strategy is to abstract the original system and find an invariant for the abstraction. In this paper, we propose an approach to constructing a new kind of abstraction called conic abstraction for affine hybrid systems, and to computing reachable sets based on this abstraction. The essential feature of a conic abstraction is that it partitions the state space of a system into a set of convex polyhedral cones which is derived from a uniform conic partition of the derivative space. Such a set of polyhedral cones is able to cut all trajectories of the system into almost straight segments so that every segment of a reach pipe in a polyhedral cone tends to be straight as well, and hence can be over-approximated tightly by polyhedra using similar techniques as HyTech or PHAVer. In particular, for diagonalizable affine systems, our approach can guarantee to find an invariant for unbounded reachable sets, which is beyond the capability of bounded-time reachability analysis tools. We implemented the approach in a tool and experiments on benchmarks show that our approach is more powerful than SpaceEx and PHAVer in dealing with diagonalizable systems.
Publishing Year
Date Published
2017-09-01
Volume
10419
Page
116 - 132
Conference
FORMATS: Formal Modelling and Analysis of Timed Systems
Conference Location
Berlin, Germany
Conference Date
2017-09-05 – 2017-09-07
IST-REx-ID

Cite this

Bogomolov S, Giacobbe M, Henzinger TA, Kong H. Conic abstractions for hybrid systems. In: Abate A, Geeraerts G, eds. Vol 10419. Springer; 2017:116-132. doi:10.1007/978-3-319-65765-3_7
Bogomolov, S., Giacobbe, M., Henzinger, T. A., & Kong, H. (2017). Conic abstractions for hybrid systems. In A. Abate & G. Geeraerts (Eds.) (Vol. 10419, pp. 116–132). Presented at the FORMATS: Formal Modelling and Analysis of Timed Systems, Berlin, Germany: Springer. https://doi.org/10.1007/978-3-319-65765-3_7
Bogomolov, Sergiy, Mirco Giacobbe, Thomas A Henzinger, and Hui Kong. “Conic Abstractions for Hybrid Systems.” edited by Alessandro Abate and Gilles Geeraerts, 10419:116–32. Springer, 2017. https://doi.org/10.1007/978-3-319-65765-3_7.
S. Bogomolov, M. Giacobbe, T. A. Henzinger, and H. Kong, “Conic abstractions for hybrid systems,” presented at the FORMATS: Formal Modelling and Analysis of Timed Systems, Berlin, Germany, 2017, vol. 10419, pp. 116–132.
Bogomolov S, Giacobbe M, Henzinger TA, Kong H. 2017. Conic abstractions for hybrid systems. FORMATS: Formal Modelling and Analysis of Timed Systems, LNCS, vol. 10419. 116–132.
Bogomolov, Sergiy, et al. Conic Abstractions for Hybrid Systems. Edited by Alessandro Abate and Gilles Geeraerts, vol. 10419, Springer, 2017, pp. 116–32, doi:10.1007/978-3-319-65765-3_7.
Main File(s)
Access Level
OA Open Access
Last Uploaded
2018-12-12T10:12:38Z


Export

Marked Publications

Open Data IST Research Explorer

Search this title in

Google Scholar
ISBN Search