Verifying Safety and Persistence Properties of Hybrid Systems Using Flowpipes and Continuous Invariants
Author
Abstract

We propose a method for verifying persistence of nonlinear hybrid systems. Given some system and an initial set of states, the method can guarantee that system trajectories always eventually evolve into some specified target subset of the states of one of the discrete modes of the system, and always remain within this target region. The method also computes a time-bound within which the target region is always reached. The approach combines flowpipe computation with deductive reasoning about invariants and is more general than each technique alone.

Year of Publication
2017
Conference Name
NASA Formal Methods - 9th International Symposium
Date Published
05/2017
Publisher
Springer
Conference Location
Moffett Field, CA, USA
ISBN Number
978-3-319-57287-1
Attachments
Google Scholar | BibTeX | XML