Scalable algorithms for safety verification and reachability analysis of hybrid systems

在过去的几十年里，微处理器技术和数字控制器在物理工厂自动化中的使用取得了巨大的进步。这种控制器的日益集成导致涉及连续和离散事件动态的高度复杂的系统。除了由计算机引入的不连续性之外，大多数物理过程由于机电系统中的阀门、齿轮和开关到遗传和代谢网络中的转录调节器等元件的作用而表现出离散动力学。混合系统是一种既具有离散特征又具有连续特征的系统，形式化验证是系统设计中的一个重要问题。它的目标是证明系统按预期运行。 随着自动化系统的规模和复杂性不断增长，细微错误的可能性也越来越大。该项目开发可扩展的，可证明正确的算法和软件工具，用于混合系统的安全验证和可达性分析。首先，该项目研究离散抽象的构造。在这样做的同时，这项工作试图扩大类已知的可判定的混合系统。其次，通过半代数方法和凸优化的最新进展，该项目研究了一种新的安全验证方法，该方法不需要明确计算轨迹或可达集，并提供了一个嵌套的系统安全性的充分条件族，这些条件是多项式时间可检查的。第三，从基于随机技术的运动规划的思想，该项目开发了一个算法的测试用例生成。在这个项目中开发的算法实现为一个可达性分析和VErification（Rave）工具包，并考虑到两个非常困难的问题，在多智能体机器人系统的安全性进行测试。该项目的结果也对混合系统用于建模的广泛领域产生了直接影响，例如自动化高速公路系统，空中交通管理系统，遗传和代谢网络，嵌入式汽车和航空电子控制器，机器人和实时通信网络。

In the past few decades, there have been tremendous advances in microprocessor technology and the use of digital controllers in the automation of physical plants. The increasing integration of such controllers results in highly complex systems involving both continuous and discrete event dynamics. In addition to discontinuities introduced by the computer, most physical processes exhibit discrete dynamics due to the action of elements ranging from valves, gears and switches in electromechanical systems to transcriptional regulators in genetic and metabolic networks. Such systems combining discrete and continuous features are called hybrid systems.Formal verification is a very important issue during system design. Its goal is to prove that the system performs as expected. As the automated systems are growing in scale and complexity, the possibility of subtle errors is much greater. This project develops scalable, provably correct algorithms and software tools for safety verification and reachability analysis of hybrid systems. First, the project investigates the construction of discrete abstractions. While doing this, this work attempts to enlarge the class of known decidable hybrid systems. Second, enabled by recent advances in semialgebraic methods and convex optimization, the project investigates a new method for safety verification that does not require explicit calculation of trajectories or reachable sets, and provides a nested family of sufficient conditions for system safety that are polynomial-time checkable. Third, bringing ideas from motion planning based on randomized techniques, the project develops an algorithm for test case generation.The algorithms developed in this project are implemented as a Reachability Analysis and VErification (Rave) toolkit and tested by considering two very difficult problems arising in the safety of multi-agent robotic systems. The results of this project also have an immediate impact in a wide range of areas where hybrid systems are used for modeling, such as automated highway systems, air-traffic management systems, genetic and metabolic networks, embedded automotive and avionic controllers, robotics, and real-time communication networks.