通过神经Lyapunov函数实现分段仿射系统的认证集合收敛

在有界加性扰动下，分段仿射（PWA）系统的安全关键控制需要的不是对单个状态的保证，而是对整个状态集合同时成立的保证：单个控制动作必须将集合中的每个状态引导至目标，即使跨越模式边界的集合会分裂并在不同的仿射动力学下演化。通过神经Lyapunov函数认证此类集合收敛，需要耦合值函数和策略的Lipschitz常数，但表达力强的网络的认证界与真实值相差数个数量级，从而形成了认证障碍。我们通过一个三阶段流水线来解决这一问题，该流水线将验证与策略解耦。一个通过强化学习训练的Hamilton-Jacobi后向可达性值函数作为Lyapunov候选。一个通过遗憾最小化蒸馏的排列不变Deep Sets控制器产生一个通用动作。验证通过值网络传播zonotopes，得出在整个集合上的经验证Lyapunov上界，而无需界定策略的Lipschitz常数。在四个高达六维的基准系统上，包括具有每模式算子范数超过1的系统，该框架在每个系统上都以正余量认证了集合收敛。一个谱约束的局部证书完成了终端保证，而集合-actor是唯一在恒定在线成本下实现完全严格集合包含的测试方法。