Computing differential invariants of hybrid systems as fixedpoints

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.

@inproceedings{DBLP:conf/cav/PlatzerC08,
	pdf = {pub/fpdi.pdf},
	slides = {pub/fpdi-slides.pdf},
	ref = {DBLP:journals/fmsd/PlatzerC09},
	refname = {FMSD'09},
	study = {pub/fpdi-examples.zip},
	TR = {DBLP:conf/cav/PlatzerC08:TR},
	author = {['André Platzer', 'Edmund M. Clarke']},
	title = {Computing Differential Invariants of Hybrid
               Systems as Fixedpoints},
	booktitle = {CAV},
	longbooktitle = {Computer Aided Verification, 20th
               International Conference, CAV 2008,
               Princeton, NJ, USA, July 7-14, 2008,
               Proceedings},
	year = {2008},
	pages = {176-189},
	month = {},
	editor = {['Aarti Gupta', 'Sharad Malik']},
	publisher = {Springer},
	series = {LNCS},
	volume = {5123},
	isbn = {978-3-540-70543-7},
	doi = {10.1007/978-3-540-70545-1_17},
	keywords = {verification of hybrid systems,
               differential invariants, verification logic,
               fixedpoint engine},
	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.}
}