Quantified differential dynamic logic for distributed hybrid systems

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.

@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é Platzer']},
	title = {Quantified Differential Dynamic Logic
               for Distributed Hybrid Systems},
	booktitle = {CSL},
	year = {2010},
	pages = {469-483},
	editor = {['Anuj Dawar', '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.}
}