Conic Abstractions for Hybrid Systems

Bogomolov, Sergiy and Giacobbe, Mirco and Henzinger, Thomas A and Kong, Hui (2017) Conic Abstractions for Hybrid Systems. In: FORMATS: Formal Modeling and Analysis of Timed Systems, September 5-7, 2017, Berlin, Germany. (Submitted)

[img] Text
main.pdf - Submitted Version
Available under License All rights reserved.
Download (3717Kb)


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 \emph{HyTech} or \emph{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 \emph{SpaceEx} and \emph{PHAVer} in dealing with diagonalizable systems.

Item Type: Conference or Workshop Item (Paper)
Subjects: 000 Computer science, knowledge & general works > 000 Computer science, knowledge & systems > 005 Computer programming, programs & data
Research Group: Henzinger Group
Depositing User: Mirco Giacobbe
Date Deposited: 30 Jun 2017 07:19
Last Modified: 30 Aug 2017 14:01

Actions (login required)

View Item View Item