SpaceEx: Scalable Verification of Hybrid Systems
Goran Frehse, Colas Le Guernic, Alexandre Donzé, Scott Cotton, Rajarshi Ray, Olivier Lebeltel, Rodolfo Ripado, Antoine Girard, Thao Dang, Oded Maler
CAV'11 (2011)
LNCS, Springer, 2011
Abstract
We present a scalable reachability algorithm for hybrid systems with piecewise affine, non-deterministic dynamics. It combines polyhedra and support function representations of continuous sets to compute an overapproximation of the reachable states. The algorithm improves over previous work by using variable time steps to guarantee a given local error bound. In addition, we propose an improved approximation model, which drastically improves the accuracy of the algorithm. The algorithm is implemented as part of SpaceEx, a new veri cation platform for hybrid systems, available at spaceex.imag.fr. Experimental results of full fixed-point computations with hybrid systems with more than 100 variables illustrate the scalability of the approach.
Below the paper as well as the conference presentation are available for download.
| Download | Size |
|---|---|
| paper_55.pdf | 696.38 KB |
| cav11_frehselgdcrlrgdm_presentation_v1.0.pdf | 914.73 KB |
| cav2011_appendix.pdf | 147.51 KB |
Bibtex:
@inproceedings{FrehseLGDCRLRGDM11,
title = {SpaceEx: Scalable Verification of Hybrid Systems},
author = {Frehse, Goran and Le Guernic, Colas and Donz\'e, Alexandre and Cotton, Scott and Ray, Rajarshi and Lebeltel, Olivier and Ripado, Rodolfo and Girard, Antoine and Dang, Thao and Maler, Oded},
editor = {Ganesh Gopalakrishnan, Shaz Qadeer},
booktitle = {Proc. 23rd International Conference on Computer Aided Verification (CAV)},
publisher = {Springer},
series = {LNCS},
team = {TEMPO},
year = {2011},
abstract = {We present a scalable reachability algorithm for hybrid systems with piecewise affine, non-deterministic dynamics. It combines polyhedra and support function representations of continuous sets to compute an overapproximation of the reachable states. The algorithm improves over previous work by using variable time steps to guarantee a given local error bound. In addition, we propose an improved approximation model, which drastically improves the accuracy of the algorithm. The algorithm is implemented as part of SpaceEx, a new veri cation platform for hybrid systems, available at spaceex.imag.fr. Experimental results of full fixed-point computations with hybrid systems with more than 100 variables illustrate the scalability of the approach. }
