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

doi:10.1007/978-3-642-22110-1_30

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

Verimag
New York University
LTHE (UMR 5564 CNRS/IRD/Université de Grenoble)

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

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 over-approximation 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 verification 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.

Original language	English
Title of host publication	Computer Aided Verification - 23rd International Conference, CAV 2011, Proceedings
Publisher	Springer Verlag
Pages	379-395
Number of pages	17
ISBN (Print)	9783642221095
DOIs	https://doi.org/10.1007/978-3-642-22110-1_30
Publication status	Published - 1 Jan 2011
Externally published	Yes

Publication series

Name	Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume	6806 LNCS
ISSN (Print)	0302-9743
ISSN (Electronic)	1611-3349

Access to Document

10.1007/978-3-642-22110-1_30

Cite this

Frehse, G., Le Guernic, C., Donzé, A., Cotton, S., Ray, R., Lebeltel, O., Ripado, R., Girard, A., Dang, T., & Maler, O. (2011). SpaceEx: Scalable verification of hybrid systems. In Computer Aided Verification - 23rd International Conference, CAV 2011, Proceedings (pp. 379-395). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 6806 LNCS). Springer Verlag. https://doi.org/10.1007/978-3-642-22110-1_30

@inproceedings{020f7ad126e44c3da6b2e94638102c63,

title = "SpaceEx: Scalable verification of hybrid systems",

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 over-approximation 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 verification 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.",

author = "Goran Frehse and \{Le Guernic\}, Colas and Alexandre Donz{\'e} and Scott Cotton and Rajarshi Ray and Olivier Lebeltel and Rodolfo Ripado and Antoine Girard and Thao Dang and Oded Maler",

year = "2011",

month = jan,

day = "1",

doi = "10.1007/978-3-642-22110-1\_30",

language = "English",

isbn = "9783642221095",

series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

publisher = "Springer Verlag",

pages = "379--395",

booktitle = "Computer Aided Verification - 23rd International Conference, CAV 2011, Proceedings",

}

Frehse, G, Le Guernic, C, Donzé, A, Cotton, S, Ray, R, Lebeltel, O, Ripado, R, Girard, A, Dang, T & Maler, O 2011, SpaceEx: Scalable verification of hybrid systems. in Computer Aided Verification - 23rd International Conference, CAV 2011, Proceedings. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 6806 LNCS, Springer Verlag, pp. 379-395. https://doi.org/10.1007/978-3-642-22110-1_30

SpaceEx: Scalable verification of hybrid systems. / Frehse, Goran; Le Guernic, Colas; Donzé, Alexandre et al.
Computer Aided Verification - 23rd International Conference, CAV 2011, Proceedings. Springer Verlag, 2011. p. 379-395 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 6806 LNCS).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

TY - GEN

T1 - SpaceEx

T2 - Scalable verification of hybrid systems

AU - Frehse, Goran

AU - Le Guernic, Colas

AU - Donzé, Alexandre

AU - Cotton, Scott

AU - Ray, Rajarshi

AU - Lebeltel, Olivier

AU - Ripado, Rodolfo

AU - Girard, Antoine

AU - Dang, Thao

AU - Maler, Oded

PY - 2011/1/1

Y1 - 2011/1/1

N2 - 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 over-approximation 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 verification 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.

AB - 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 over-approximation 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 verification 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.

U2 - 10.1007/978-3-642-22110-1_30

DO - 10.1007/978-3-642-22110-1_30

M3 - Conference contribution

AN - SCOPUS:79960348872

SN - 9783642221095

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 379

EP - 395

BT - Computer Aided Verification - 23rd International Conference, CAV 2011, Proceedings

PB - Springer Verlag

ER -

Frehse G, Le Guernic C, Donzé A, Cotton S, Ray R, Lebeltel O et al. SpaceEx: Scalable verification of hybrid systems. In Computer Aided Verification - 23rd International Conference, CAV 2011, Proceedings. Springer Verlag. 2011. p. 379-395. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). doi: 10.1007/978-3-642-22110-1_30

SpaceEx: Scalable verification of hybrid systems

Abstract

Publication series

Access to Document

Fingerprint

Cite this