Quantified Differential Dynamic Logic for Distributed Hybrid Systems

11 years 9 months ago
Quantified Differential Dynamic Logic for Distributed Hybrid Systems
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...
André Platzer
Added 08 Nov 2010
Updated 08 Nov 2010
Type Conference
Year 2010
Where CSL
Authors André Platzer
Comments (0)