发表机构
University of California, Berkeley; University of Colorado Boulder; Ludwig-Maximilian University（加州大学伯克利分校; 科罗拉多大学博尔德分校; 路德维希-马克西米利安大学）
机构由 AI 辅助整理，请以论文原文为准。AI 中文总结
针对单调系统，提出阈值函数重构方法，将受控不变集合成转化为并行一维搜索，显著降低计算复杂度，实现大规模网格的实时合成与在线重合成。
AI 中文摘要
自主系统的安全关键控制需要形式化的安全证书，例如受控不变集，这些证书必须在条件变化时在线计算。尽管标准合成算法在状态维度上扩展性较差，但具有下闭安全规格的单调动力系统允许加速计算受控不变集。特别是，惰性不动点算法利用单调性并仅跟踪集合的反链基。然而，针对不断演化的基的成员资格测试和冗余检查仍然是主要瓶颈。我们引入了一种阈值函数重构，其中d维网格上的下闭集由其沿指定轴的列高表示。这将最大不动点迭代重构为独立的一维二分搜索，每个网格列一个，产生了一种令人尴尬的并行迭代，其渐近计算复杂度低于惰性不动点算法。实验在3D网格上合成了具有10^9个单元的不变集，耗时不到50毫秒，以及10^14个单元，耗时不到两分钟。我们进一步在安全信息模型预测控制示例中演示了在线重新合成。
英文摘要
Safety-critical control of autonomous systems requires formal safety certificates, such as controlled invariant sets, that must be computed online as conditions change. Although standard synthesis algorithms scale poorly with state dimension, monotone dynamical systems with lower-closed safety specifications allow for accelerated computation of controlled invariant sets. In particular, lazy fixed-point algorithms exploit monotonicity and track only the antichain basis of the set. However, membership tests and redundancy checks against an evolving basis remain major bottlenecks. We introduce a threshold-function reformulation in which a lower-closed set on a d-dimensional grid is represented by its column heights along a designated axis. This reformulates the greatest-fixed-point iteration as independent one-dimensional binary searches, one per grid column, yielding an embarrassingly parallel iteration with asymptotically lower computational complexity than the lazy fixed-point algorithm. Experiments synthesize invariant sets on 3D grids with 10^9 cells in under 50 ms and 10^14 cells in under two minutes. We further demonstrate online re-synthesis in a safety-informed model predictive controller example.
