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.