Quantified differential invariants

We address the verification problem for distributed
hybrid systems with nontrivial dynamics. Consider air
traffic collision avoidance maneuvers, for example.
Verifying dynamic appearance of aircraft during an
ongoing collision avoidance maneuver is a longstanding
and essentially unsolved problem. The resulting systems
are not hybrid systems and their state space is not of
the form R^n. They are distributed hybrid systems with
nontrivial continuous and discrete dynamics in
distributed state spaces whose dimension and topology
changes dynamically over time. We present the first
formal verification technique that can handle the
complicated nonlinear dynamics of these systems. We
introduce quantified differential invariants, which are
properties that can be checked for invariance along the
dynamics of the distributed hybrid system based on
differentiation, quantified substitution, and
quantifier elimination in real-closed fields. This
gives a computationally attractive technique, because
it works without having to solve the
infinite-dimensional differential equation systems
underlying distributed hybrid systems. We formally
verify a roundabout maneuver in which aircraft can
appear dynamically.

@inproceedings{DBLP:conf/hybrid/Platzer11,
	pdf = {pub/Qdiffind.pdf},
	slides = {pub/Qdiffind-slides.pdf},
	author = {['André Platzer']},
	title = {Quantified Differential Invariants},
	booktitle = {HSCC},
	year = {2011},
	pages = {63-72},
	doi = {10.1145/1967701.1967713},
	editor = {['Emilio Frazzoli', 'Radu Grosu']},
	longbooktitle = {Proceedings of the 14th ACM
               International Conference on Hybrid Systems:
               Computation and Control, HSCC 2011, Chicago,
               USA, April 12-14, 2011},
	publisher = {ACM},
	isbn = {},
	keywords = {distributed hybrid systems,
               verification logic,
               quantified differential equations,
               quantified differential invariants},
	abstract = {
    We address the verification problem for distributed
    hybrid systems with nontrivial dynamics. Consider air
    traffic collision avoidance maneuvers, for example.
    Verifying dynamic appearance of aircraft during an
    ongoing collision avoidance maneuver is a longstanding
    and essentially unsolved problem. The resulting systems
    are not hybrid systems and their state space is not of
    the form R^n. They are distributed hybrid systems with
    nontrivial continuous and discrete dynamics in
    distributed state spaces whose dimension and topology
    changes dynamically over time. We present the first
    formal verification technique that can handle the
    complicated nonlinear dynamics of these systems. We
    introduce quantified differential invariants, which are
    properties that can be checked for invariance along the
    dynamics of the distributed hybrid system based on
    differentiation, quantified substitution, and
    quantifier elimination in real-closed fields. This
    gives a computationally attractive technique, because
    it works without having to solve the
    infinite-dimensional differential equation systems
    underlying distributed hybrid systems. We formally
    verify a roundabout maneuver in which aircraft can
    appear dynamically.}
}