A Toolbox for the Reachability Analysis of Hybrid Systems using Geometric Approximations

混杂系统是具有离散-连续混合行为的系统，典型的例子是由离散控制器控制的物理系统。由于这类系统通常是安全关键的，因此为其安全分析的算法和工具的开发投入了大量精力。然而，尽管在过去的十年中取得了巨大的成就，但现有技术的适用性仍然受到限制，需要进一步改进。在我们的HyPro项目的第一阶段，我们开发了一个编程库，以简化计算混合系统可达状态集的新算法的实现。此外，我们开发了Flow*工具，该工具因其处理由非线性微分方程指定的系统动力学的能力而在社区中获得了相当大的关注。最后，我们创建了一个基准库，并使用它对可用的混合系统可达性分析工具进行了广泛的评估和比较。在第一个项目阶段，我们确定了阻碍使用现有技术进行混合系统成功分析的几个障碍。有了这份提案，我们申请继续我们的HyPro项目，以使用我们第一个项目阶段的HyPro库为一些具有挑战性的问题提供解决方案。虽然大多数技术使用静态搜索启发式，但我们的目标是开发动态搜索策略，允许对搜索参数进行上下文敏感的适配。除了开发一个通用框架外，我们还将开发专门的反例生成策略，用于分析具有Zeno行为的模型，以及分析概率混合系统。为了进一步提高效率，我们还将解决并行化和组合性问题。

Hybrid systems are systems with mixed discrete-continuous behaviour, typical examples being physical systems controlled by discrete controllers. As such systems are often safety-critical, much effort was put into the development of algorithms and tools for their safety analysis. However, despite great achievements in the last decade, the applicability of current technologies is still restricted and needs further improvements.In the first phase of our HyPro project we developed a programming library to ease the implementation of novel algorithms for the computation of the set of reachable states of hybrid systems. Furthermore, we developed the Flow* tool, which gained considerable attention in the community due to its ability to handle system dynamics specified by non-linear differential equations. Finally, we created a benchmark library and used it for an extensive evaluation and comparison of available hybrid systems reachability analysis tools.During the first project phase we identified several obstacles that hinder the successful analysis of hybrid systems with available technologies. With this proposal we apply for the continuation of our HyPro project to provide solutions for some of those challenging problems, using our HyPro library from the first project phase. Whereas most technologies work with static search heuristics, we aim at developing dynamic search strategies, which allow the context-sensitive adaptation of search parameters. Besides the development of a general framework, we will develop dedicated strategies for counterexample generation, for the analysis of models with Zeno behaviour, and for the analysis of probabilistic hybrid systems. To further increase efficiency, we will also address parallelisation and compositionality issues.