10.2168/LMCS-8(4:17)2012
Platzer, Andre
Andre
Platzer
A Complete Axiomatization of Quantified Differential Dynamic Logic for
Distributed Hybrid Systems
episciences.org
2012
Computer Science - Logic in Computer Science
Computer Science - Programming Languages
Mathematics - Dynamical Systems
F.3.1, F.4.1, D.2.4, C.1.m, C.2.4, D.4.7
contact@episciences.org
episciences.org
2011-01-07T00:00:00+01:00
2016-11-21T15:27:26+01:00
2012-11-26
eng
Journal article
https://lmcs.episciences.org/720
arXiv:1206.3357
1860-5974
PDF
1
Logical Methods in Computer Science ; Volume 8, Issue 4 ; 1860-5974
We address a fundamental mismatch between the combinations of dynamics that
occur in cyber-physical systems and the limited kinds of dynamics supported in
analysis. Modern applications combine communication, computation, and control.
They may even form dynamic distributed networks, where neither structure nor
dimension stay the same while the system follows hybrid dynamics, i.e., mixed
discrete and continuous dynamics. We provide the logical foundations for
closing this analytic gap. We develop a formal model for distributed hybrid
systems. It 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 this
logic. This is the first formal verification approach for distributed hybrid
systems. We prove that our 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 an unbounded number of new cars may appear dynamically on the
road.
Comment: arXiv admin note: text overlap with arXiv:1205.4788