Analysing and Explicating Dynamical and Hybrid Systems ((07) A01)

动态自动机模型和混合自动机模型是网络物理系统操作表示的核心。该项目的愿景是为这些模型提供一个算法分析框架，以及相应的解释机制。虽然现有的大多数动态和混合系统的方法要么依赖于半算法(没有终止性保证)，要么依赖于近似技术(没有分析结果的正确性保证)，该项目的重点将是开发可证明正确的和可终止的精确验证算法和相应的技术，用于为验证的系统属性生成证书。

Dynamical and hybrid automata models are at the core of operational representations of cyber-physical systems. The vision of the project is to provide an algorithmic analysis framework for these models, together with corresponding explication mechanisms. While the majority of existing methods for dynamical and hybrid systems rely either on semi-algorithms (without termination guarantees) or on approximation techniques (without guarantees of the correctness of the analysis results), the focus of the project will be on the development of provably correct and terminating exact verification algorithms and corresponding techniques for the generation of certificates for verified system properties.