Complete Robust Hybrid Systems Reachability

TL;DR

This paper develops a new logical framework for verifying the robustness of hybrid systems' reachability, ensuring properties hold under infinitesimal perturbations, and proves its absolute completeness for general hybrid systems.

Contribution

It introduces robust differential dynamic logic with syntactic restrictions that guarantee robustness and provides the first absolute completeness proof for hybrid systems reachability.

Findings

Robust differential dynamic logic is sound and complete for hybrid systems.

Properties are topologically open, ensuring robustness.

Automated verification of robust reachability is possible.

Abstract

This paper introduces robust differential dynamic logic (a fragment of differential dynamic logic) to specify and reason about robust hybrid systems. Practically meaningful syntactic restrictions naturally ensure that definable properties are topologically open and thus by construction robust with respect to infinitesimal perturbations, without explicit quantitative margins of error in the syntax or in proofs. The main result is a proof of absolute completeness of robust differential dynamic logic for reachability properties of general hybrid systems. This is the first absolute completeness proof for hybrid systems with exact semantics. The proof is constructive, self-contained, and demonstrates how robustly correct hybrid systems reachability specifications can be automatically verified through proof.