论文标题
PIRK：高维非线性系统的可扩展间隔可及性分析
PIRK: Scalable Interval Reachability Analysis for High-Dimensional Nonlinear Systems
论文作者
论文摘要
可及性分析是对动态系统形式验证和为其合成控制器的关键工具。由于其计算复杂性，许多可及性分析方法仅限于具有相对较小的系统的系统。这种限制的一个重要原因是，这些方法及其实施并非旨在利用并行性。他们使用设计用于在一个计算单元中串行运行的算法，并且无法利用广泛可用的高性能计算（HPC）平台，例如多核CPU，GPU，GPU和云计算服务。 本文提出了PIRK，这是一种有效计算具有极高尺寸的一般非线性系统的可触及套件的工具。 PIRK已在多个系统上进行了测试，州维度从10到40亿。 PIRK并行实现的可伸缩性非常有利。
Reachability analysis is a critical tool for the formal verification of dynamical systems and the synthesis of controllers for them. Due to their computational complexity, many reachability analysis methods are restricted to systems with relatively small dimensions. One significant reason for such limitation is that those approaches, and their implementations, are not designed to leverage parallelism. They use algorithms that are designed to run serially within one compute unit and they can not utilize widely-available high-performance computing (HPC) platforms such as many-core CPUs, GPUs and Cloud-computing services. This paper presents PIRK, a tool to efficiently compute reachable sets for general nonlinear systems of extremely high dimensions. PIRK has been tested on several systems, with state dimensions ranging from ten up to 4 billion. The scalability of PIRK's parallel implementations is found to be highly favorable.
