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

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

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.