10.1184/R1/6604346.v1
Andre Platzer
Andre
Platzer
Edmund M Clarke
Edmund M
Clarke
Computing Differential Invariants of Hybrid Systems as Fixedpoints
Carnegie Mellon University
1999
verification of hybrid systems
differential invariants
verification logic
fixedpoint engine
1999-09-01 00:00:00
Journal contribution
https://kilthub.cmu.edu/articles/journal_contribution/Computing_Differential_Invariants_of_Hybrid_Systems_as_Fixedpoints/6604346
We introduce a fixedpoint algorithm for verifying safety properties of hybrid systems with differential
equations that have right-hand sides that are polynomials in the state variables. In order
to verify non-trivial 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.