Scalable algorithms for safety verification and reachability analysis of hybrid systems

在过去的几十年里，微处理器技术和数字控制器在物理工厂自动化中的使用取得了巨大的进步。这些控制器的日益集成导致了涉及连续和离散事件动态的高度复杂的系统。除了计算机引入的间断外，由于机电系统中的阀门、齿轮和开关，以及遗传和新陈代谢网络中的转录调节因素的作用，大多数物理过程都表现出离散的动力学。这种将离散和连续特性结合在一起的系统称为混合系统，形式化验证是系统设计中非常重要的问题。它的目标是证明系统的性能符合预期。随着自动化系统在规模和复杂性上的增长，出现细微错误的可能性要大得多。该项目开发可扩展的、可证明正确的算法和软件工具，用于混合系统的安全性验证和可达性分析。首先，该项目研究了离散抽象的构造。在这样做的同时，这项工作试图扩大已知的可判定混合系统的类别。其次，在半代数方法和凸优化方法的最新进展的推动下，该项目研究了一种新的安全验证方法，该方法不需要显式地计算轨迹或可达集，并提供了一族嵌套的系统安全的多项式时间可检查的充分条件。第三，借鉴基于随机化技术的运动规划思想，提出了一种测试用例生成算法，并以可达性分析与验证(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.