Differential Dynamic Logics Automated Theorem Proving for Hybrid Systems

摘要

Designing and analyzing hybrid systems, which are models for complex physical systems, is expensive and error-prone. The dissertation presented in this article introduces a verification logic that is suitable for analyzing the behavior of hybrid systems. It presents a proof calculus and a new deductive verification tool for hybrid systems that has been used successfully to verify aircraft and train control.