利用库普曼谱进行动力学系统可达性验证的时间到达界

在本工作中，我们提出了一种基于库普曼谱的非线性系统可达性验证新方法。与传统方法关注在预设时间跨度内刻画动力学系统的所有可能状态不同，我们的方法通过评估估计的时间到达区间的非空性来验证可达性，而不涉及显式计算可达集。基于库普曼算子的谱分析，我们将验证可达轨迹存在的问题重新表述为确定系统可达性所需的可行时间到达界的问题。通过求解线性规划问题，我们的算法能够有效估计动力学系统从给定初始集进入（和离开）目标集的所有潜在时间区间，时间范围无界。最后，我们在具有挑战性的设置中展示了我们的方法，例如验证非凸甚至不连通集合之间的可达性，以及反向可达性和多次进入目标集。此外，通过验证推车-摆系统和多智能体共识系统的可达性案例研究，我们验证了其在解决现实世界挑战和高维系统可扩展性方面的适用性。