A Complete Axiomatization of Quantified Differential Dynamic Logic for Distributed Hybrid Systems

摘要

We address a fundamental mismatch between the combinations of dynamics thatoccur in cyber-physical systems and the limited kinds of dynamics supported inanalysis. Modern applications combine communication, computation, and control.They may even form dynamic distributed networks, where neither structure nordimension stay the same while the system follows hybrid dynamics, i.e., mixeddiscrete and continuous dynamics. We provide the logical foundations forclosing this analytic gap. We develop a formal model for distributed hybridsystems. It combines quantified differential equations with quantifiedassignments and dynamic dimensionality-changes. We introduce a dynamic logicfor verifying distributed hybrid systems and present a proof calculus for thislogic. This is the first formal verification approach for distributed hybridsystems. We prove that our calculus is a sound and complete axiomatization ofthe behavior of distributed hybrid systems relative to quantified differentialequations. In our calculus we have proven collision freedom in distributed carcontrol even when an unbounded number of new cars may appear dynamically on theroad.