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

TL;DR

This paper introduces a new logic combining differential dynamic logic with temporal logic to verify both temporal and non-temporal properties of distributed hybrid systems, including dynamic dimensionality changes.

Contribution

It extends QdL with temporal reasoning, providing a modular verification calculus and a complete axiomatization for distributed hybrid systems.

Findings

Verified temporal safety in a distributed air traffic control system

Generalized semantics to hybrid traces for dynamic systems

Proved conservative extension of QdL with temporal logic

Abstract

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.