Computing Differential Invariants of Hybrid Systems as Fixedpoints Export

@inproceedings{PlatzerFixpoint, abstract = {We introduce a fixedpoint algorithm for verifying safety properties of hybrid systems with differential equations whose right-hand sides are polynomials in the state variables. In order to verify nontrivial systems without solving their differential equations and without numerical errors, we use a continuous generalization of induction, for which our algorithm computes the required differential invariants . As a means for combining local differential invariants into global system invariants in a sound way, our fixedpoint algorithm works with a compositional verification logic for hybrid systems. To improve the verification power, we further introduce a saturation procedure that refines the system dynamics successively with differential invariants until safety becomes provable. By complementing our symbolic verification algorithm with a robust version of numerical falsification, we obtain a fast and sound verification procedure. We verify roundabout maneuvers in air traffic management and collision avoidance in train control.}, address = {Berlin, Heidelberg}, author = {Platzer, Andr\'{e} and Clarke, Edmund M.}, booktitle = {CAV '08: Proceedings of the 20th international conference on Computer Aided Verification}, citeulike-article-id = {3053212}, citeulike-linkout-0 = {http://portal.acm.org/citation.cfm?id=1427805}, citeulike-linkout-1 = {http://dx.doi.org/10.1007/978-3-540-70545-1_17}, doi = {10.1007/978-3-540-70545-1_17}, isbn = {978-3-540-70543-7}, journal = {Computer Aided Verification}, keywords = {cps, model\_checking}, location = {Princeton, NJ, USA}, pages = {176--189}, posted-at = {2009-11-05 18:07:34}, priority = {2}, publisher = {Springer-Verlag}, title = {Computing Differential Invariants of Hybrid Systems as Fixedpoints}, url = {http://dx.doi.org/10.1007/978-3-540-70545-1_17}, year = {2008} }

TY - CONF ID - PlatzerFixpoint L3 - citeulike-article-id:3053212 N2 - We introduce a fixedpoint algorithm for verifying safety properties of hybrid systems with differential equations whose right-hand sides are polynomials in the state variables. In order to verify nontrivial systems without solving their differential equations and without numerical errors, we use a continuous generalization of induction, for which our algorithm computes the required differential invariants . As a means for combining local differential invariants into global system invariants in a sound way, our fixedpoint algorithm works with a compositional verification logic for hybrid systems. To improve the verification power, we further introduce a saturation procedure that refines the system dynamics successively with differential invariants until safety becomes provable. By complementing our symbolic verification algorithm with a robust version of numerical falsification, we obtain a fast and sound verification procedure. We verify roundabout maneuvers in air traffic management and collision avoidance in train control. CY - Princeton, NJ, USA JF - Computer Aided Verification SN - 978-3-540-70543-7 AD - Berlin, Heidelberg EP - 189 TI - Computing Differential Invariants of Hybrid Systems as Fixedpoints PB - Springer-Verlag T2 - CAV '08: Proceedings of the 20th international conference on Computer Aided Verification SP - 176 KW - cps KW - model_checking AU - Platzer, André AU - Clarke, Edmund PY - 2008/// UR - http://dx.doi.org/10.1007/978-3-540-70545-1_17 ER -