A Complete Axiomatization of Quantified Differential Dynamic Logic for Distributed Hybrid Systems
The authors 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 stays the same while the system follows hybrid dynamics, i.e., mixed discrete and continuous dynamics. They provide the logical foundations for closing this analytic gap. They develop a formal model for distributed hybrid systems. It combines quantified differential equations with quantified assignments and dynamic dimensionality-changes.