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.

翻译：本文引入鲁棒微分动态逻辑（微分动态逻辑的一个片段）来规约和推理鲁棒混合系统。具有实际意义的语法限制自然地确保了可定义属性在拓扑上是开放的，从而在构造上对无穷小扰动具有鲁棒性，无需在语法或证明中显式指定定量误差边界。主要成果是证明了鲁棒微分动态逻辑对于一般混合系统可达性属性的绝对完备性。这是首个针对具有精确语义的混合系统的绝对完备性证明。该证明是构造性的、自包含的，并展示了如何通过证明自动验证鲁棒正确的混合系统可达性规约。