Quantified differential invariants

@INPROCEEDINGS{DBLP:conf/hybrid/Platzer11,
	pdf = {pub/Qdiffind.pdf},
	slides = {pub/Qdiffind-slides.pdf},

  author    = {Andr{\'e} Platzer},
  title     = {Quantified Differential Invariants},
  booktitle = {HSCC},
  year      = {2011},
  pages     = {63-72},
  doi       = {10.1145/1967701.1967713},
  editor    = {Emilio Frazzoli and
               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.}
}```