具有十亿维的仿射系统的数值验证
Numerical Verification of Affine Systems with up to a Billion Dimensions
AI总结：
本文提出了一种方法，通过利用问题结构来提高仿射系统验证的可扩展性，能够处理具有十亿个状态变量的系统，以确保安全性和正确性。
摘要：
仿射系统可达性是许多验证方法的基础。随着计算能力的提升，方法能够处理更复杂的模型，包括输入、非线性微分方程和混合动态。因此，仿射系统验证的可扩展性是更复杂系统可扩展分析的前提。在本文中，我们提高了仿射系统验证的可扩展性，特别是在系统中的变量数量（维度）方面。仿射系统的可达状态可以表示为矩阵指数，安全检查可以在特定时间步长上通过线性规划进行。不幸的是，对于具有许多状态变量的大系统，这种方法需要不可行的内存和计算时间。我们通过结合几种利用常见问题结构的方法来克服这些挑战。通过利用非全维的初始状态和安全属性（输出）在几个线性投影上的状态变量，减少了内存。通过使用数值模拟来计算仅与验证问题相关的矩阵指数的投影，节省了计算时间。由于大系统通常具有稀疏动态，我们使用基于Arnoldi或Lanczos迭代的Krylov子空间模拟方法。我们的方法在属性被违反时能够产生准确的反例，并且在问题结构足够的情况下，可以分析具有十亿个实值状态变量的系统。
英文摘要：
Affine systems reachability is the basis of many verification methods. With further computation, methods exist to reason about richer models with inputs, nonlinear differential equations, and hybrid dynamics. As such, the scalability of affine systems verification is a prerequisite to scalable analysis for more complex systems. In this paper, we improve the scalability of affine systems verification, in terms of the number of dimensions (variables) in the system. The reachable states of affine systems can be written in terms of the matrix exponential, and safety checking can be performed at specific time steps with linear programming. Unfortunately, for large systems with many state variables, this direct approach requires an intractable amount of memory while using an intractable amount of computation time. We overcome these challenges by combining several methods that leverage common problem structure. Memory is reduced by exploiting initial states that are not full-dimensional and safety properties (outputs) over a few linear projections of the state variables. Computation time is saved by using numerical simulations to compute only projections of the matrix exponential relevant for the verification problem. Since large systems often have sparse dynamics, we use Krylov-subspace simulation approaches based on the Arnoldi or Lanczos iterations. Our method produces accurate counter-examples when properties are violated and, in the extreme case with sufficient problem structure, can analyze a system with one billion real-valued state variables.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
