Conic abstractions for hybrid systems Conference Paper

Author(s): Bogomolov, Sergiy; Giacobbe, Mirco; Henzinger, Thomas A; Kong, Hui
Title: Conic abstractions for hybrid systems
Title Series: LNCS
Affiliation IST Austria
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.
Keywords: Hybrid system; Reachability analysis; Affine system; conic abstraction, discrete abstraction
Conference Title: FORMATS: Formal Modelling and Analysis of Timed Systems
Volume: 10419
Conference Dates: September 5 - 7, 2017
Conference Location: Berlin, Germany
ISBN: 978-331965764-6
Publisher: Springer  
Date Published: 2017-01-01
Start Page: 116
End Page: 132
Sponsor: This work was partly supported by the Austrian Science Fund (FWF) under grants S11402-N23 (RiSE/SHiNE) and Z211-N23 (Wittgenstein Award) and by the ARC project DP140104219 (Robust AI Planning for Hybrid Systems).
DOI: 10.1007/978-3-319-65765-3_7
Open access: yes (repository)
IST Austria Authors
  1. Thomas A. Henzinger
    415 Henzinger
  2. Hui Kong
    9 Kong
Related IST Austria Work