高达十亿维仿射系统的数值验证
数值分析
2019-03-07 v3 系统与控制
摘要
仿射系统可达性是许多验证方法的基础。通过进一步计算，现有方法可推理具有输入、非线性微分方程和混合动力学的更丰富模型。因此，仿射系统验证的可扩展性是更复杂系统可扩展分析的先决条件。在本文中，我们提升了仿射系统验证的可扩展性，就系统中的维数（变量）而言。仿射系统的可达状态可用矩阵指数表示，安全性检查可在特定时间步通过线性规划执行。遗憾的是，对于具有许多状态变量的大型系统，这种直接方法需要难以承受的内存量和计算时间。我们通过结合几种利用常见问题结构的方法来克服这些挑战。通过利用非满维的初始状态和关于状态变量少数线性投影的安全属性（输出）来减少内存。通过计算仅与验证问题相关的矩阵指数投影，利用数值模拟节省计算时间。由于大型系统通常具有稀疏动力学，我们使用基于 Arnoldi 或 Lanczos 迭代的 Krylov 子空间模拟方法。我们的方法在属性被违反时产生准确的反例，并且在具有充分问题结构的极端情况下，可分析具有十亿个实值状态变量的系统。
引用
@article{arxiv.1804.01583,
title = {Numerical Verification of Affine Systems with up to a Billion Dimensions},
author = {Stanley Bak and Hoang-Dung Tran and Taylor T. Johnson},
journal= {arXiv preprint arXiv:1804.01583},
year = {2019}
}