Quantified Differential Temporal Dynamic Logic for Verifying Properties of Distributed Hybrid Systems

We combine quantified differential dynamic logic (QdL) for reasoning about the possible behavior of distributed hybrid systems with temporal logic for reasoning about the temporal behavior during their operation. Our logic supports verification of temporal and non-temporal properties of distributed hybrid systems and provides a uniform treatment of discrete transitions, continuous evolution, and dynamic dimensionality-changes. For our combined logic, we generalize the semantics of dynamic modalities to refer to hybrid traces instead of final states. Further, we prove that this gives a conservative extension of QdL for distributed hybrid systems. On this basis, we provide a modular verification calculus that reduces correctness of temporal behavior of distributed hybrid systems to non-temporal reasoning, and prove that we obtain a complete axiomatization relative to the non-temporal base logic QdL. Using this calculus, we analyze temporal safety properties in a distributed air traffic control system where aircraft can appear dynamically.