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. 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.

@article{DBLP:journals/fmsd/PlatzerC09,
	pdf = {pub/cdifp.pdf},
	ref = {DBLP:conf/cav/PlatzerC08},
	refname = {CAV'08},
	study = {pub/cdifp-examples.zip},
	author = {['André Platzer', 'Edmund M. Clarke']},
	title = {Computing Differential Invariants of Hybrid
               Systems as Fixedpoints},
	journal = {Form. Methods Syst. Des.},
	longjournal = {Formal Methods in System Design},
	year = {2009},
	volume = {35},
	number = {1},
	pages = {98-120},
	doi = {10.1007/s10703-009-0079-8},
	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. 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.}
}