Quantified differential dynamic logic for distributed hybrid systems

@INPROCEEDINGS{DBLP:conf/csl/Platzer10,
	pdf = {pub/QdL.pdf},
	slides = {pub/QdL-slides.pdf},
	ref = {DBLP:journals/lmcs/Platzer12b},
	refname = {LMCS'12},
	TR = {DBLP:conf/csl/Platzer10:TR},

  author    = {Andr{\'e} Platzer},
  title     = {Quantified Differential Dynamic Logic
               for Distributed Hybrid Systems},
  booktitle = {CSL},
  year      = {2010},
  pages     = {469-483},
  editor    = {Anuj Dawar and
               Helmut Veith},
  longbooktitle = {Computer Science Logic
               24th International Workshop, CSL 2010,
               19th Annual Conference of the EACSL, Brno,
               Czech Republic, August 23-27, 2010.
               Proceedings},
  publisher = {Springer},
  series    = {LNCS},
  volume    = {6247},
  doi       = {10.1007/978-3-642-15205-4_36},
  isbn      = {978-3-642-15204-7},
  keywords  = {Dynamic logic, Distributed hybrid systems,
               Axiomatization, Theorem proving,
               Quantified differential equations},
  abstract  = {
    We address a fundamental mismatch between the
    combinations of dynamics that occur in complex physical
    systems and the limited kinds of dynamics supported in
    analysis. Modern applications combine communication,
    computation, and control. They may even form dynamic
    networks, where neither structure nor dimension stay
    the same while the system follows mixed discrete and
    continuous dynamics.

     We provide the logical foundations for closing this
    analytic gap. We develop a system model for distributed
    hybrid systems that combines quantified differential
    equations with quantified assignments and dynamic
    dimensionality-changes. We introduce a dynamic logic
    for verifying distributed hybrid systems and present a
    proof calculus for it. We prove that this calculus is a
    sound and complete axiomatization of the behavior of
    distributed hybrid systems relative to quantified
    differential equations. In our calculus we have proven
    collision freedom in distributed car control even when
    new cars may appear dynamically on the road.}
}```