CMU-CS-08-103
Computer Science Department
School of Computer Science, Carnegie Mellon University



CMU-CS-08-103

Computing Differential Invariants of Hybrid Systems as Fixedpoints

André Platzer*, Edmund M. Clarke
February 2008

CMU-CS-08-103.pdf


Keywords: Verification of hybrid systems, differential invariants, verification logic, fixedpoint engine

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.

34 pages

*Department of Computing Science, University of Oldenburg, Germany


Return to: SCS Technical Report Collection
School of Computer Science

This page maintained by reports@cs.cmu.edu