Computing Differential Invariants of Hybrid Systems as Fixedpoints

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. With this compositional approach we exploit locality in system designs. 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 and car control.

Original document

The different versions of the original document can be found in:

• http://dx.doi.org/10.1007/s10703-009-0079-8

• http://dx.doi.org/10.1184/r1/6604346

• http://dx.doi.org/10.1184/r1/6604346.v1

• http://dx.doi.org/10.1184/r1/6604349

• http://dx.doi.org/10.1184/r1/6604349.v1

• http://dx.doi.org/10.21236/ada476791

• http://www.dtic.mil/dtic/tr/fulltext/u2/a476791.pdf

• http://www.functologic.com/pub/fpdi.pdf

• https://figshare.com/articles/journal_contribution/Computing_Differential_Invariants_of_Hybrid_Systems_as_Fixedpoints/6604346

• https://figshare.com/articles/journal_contribution/Computing_differential_invariants_of_hybrid_systems_as_fixedpoints/6604349

• https://link.springer.com/content/pdf/10.1007%2F978-3-540-70545-1_17.pdf

• http://link.springer.com/content/pdf/10.1007/978-3-540-70545-1_17.pdf,

http://dx.doi.org/10.1007/978-3-540-70545-1_17

• http://link.springer.com/content/pdf/10.1007/s10703-009-0079-8.pdf,

http://link.springer.com/article/10.1007/s10703-009-0079-8/fulltext.html,

http://link.springer.com/content/pdf/10.1007/s10703-009-0079-8,

http://dx.doi.org/10.1007/s10703-009-0079-8 under the license http://www.springer.com/tdm

• http://reports-archive.adm.cs.cmu.edu/anon/2008/CMU-CS-08-103.pdf,

https://link.springer.com/article/10.1007/s10703-009-0079-8,

http://oai.dtic.mil/oai/oai?verb=getRecord&metadataPrefix=html&identifier=ADA476797,

http://repository.cmu.edu/compsci/1244,

https://users.ece.cmu.edu/~krogh/otherNSFpapers/PlC08.pdf,

https://dblp.uni-trier.de/db/journals/fmsd/fmsd35.html#PlatzerC09,

https://www.researchgate.net/profile/Andre_Platzer/publication/226247835_Computing_differential_invariants_of_hybrid_systems_as_fixedpoints/links/00463537caa7ef05ff000000.pdf,

https://www.scipedia.com/public/Platzer_Clarke_2009a,

https://apps.dtic.mil/dtic/tr/fulltext/u2/a476797.pdf,

https://dl.acm.org/citation.cfm?id=1612944,

https://apps.dtic.mil/docs/citations/ADA476797,

https://doi.org/10.1007/s10703-009-0079-8,

https://rd.springer.com/article/10.1007/s10703-009-0079-8,

https://academic.microsoft.com/#/detail/2106606898

• https://link.springer.com/chapter/10.1007%2F978-3-540-70545-1_17,

https://dblp.uni-trier.de/db/conf/cav/cav2008.html#PlatzerC08,

http://dx.doi.org/10.1007/978-3-540-70545-1_17,

https://rd.springer.com/chapter/10.1007/978-3-540-70545-1_17,

https://dl.acm.org/citation.cfm?id=1427805,

https://doi.org/10.1007/978-3-540-70545-1_17,

https://academic.microsoft.com/#/detail/3021664313

DOIS: 10.1007/s10703-009-0079-8 10.1184/r1/6604346.v1 10.1007/978-3-540-70545-1_17 10.21236/ada476791 10.1184/r1/6604349.v1 10.1184/r1/6604346 10.1184/r1/6604349