Universal Safety Controllers with Learned Prophecies¶

会议: AAAI 2026
arXiv: 2511.11390
代码: UCLearn (uclearn 工具)
领域: others (形式化验证/控制器合成)
关键词: 通用安全控制器, 时序逻辑, CTL学习, 反应式合成, 预言近似

一句话总结¶

提出 UCLearn，通过从少量代表性 plant 模型中学习 CTL (计算树逻辑) 公式作为预言（prophecy）的近似表示，替代精确但计算昂贵的树自动机，实现高效、可扩展且可解释的通用安全控制器合成。

研究背景与动机¶

领域现状: 反应式合成（reactive synthesis）和监督控制（supervisory control）旨在从时序逻辑规范自动构建 correct-by-design 的控制器。传统方法需要将规范自动机与具体的 plant 模型组合求解，面临严重的状态空间爆炸问题。
现有痛点: 先前提出的通用安全控制器（USC）框架虽然可以从规范独立于 plant 进行合成，但其核心组件——预言（prophecy）——使用树自动机表示，计算和验证代价极高，且难以理解。
核心矛盾: USC 需要精确刻画"在什么植物行为条件下，某个控制输出是正确的"，但精确表示（树自动机）不实用，而简单表示可能丧失正确性保证。
本文目标: 在保持正确性的前提下，找到计算高效且人类可读的预言表示。
切入角度: 用 CTL 公式替代树自动机作为预言的表示形式，通过学习算法从少量代表性 plant 中推断出能分离正确/不正确控制输出的 CTL 公式。
核心 idea: 不需要精确刻画所有可能的 plant 行为，只需要从少量样本中学习一个足够好的 CTL 公式来分离正确和错误的控制决策。

方法详解¶

整体框架¶

UCLearn 包含三个循环阶段：(1) 初始化——将安全 LTL 规范转为安全自动机，设置初始近似（under-approximation = 空集，over-approximation = 所有 plant）；(2) 精化循环——对每个新 nominal plant，先尝试用当前控制器，若不正确则合成正确控制器并更新正/负样本，学习新的 CTL 公式；(3) 组合——将学习到的预言控制器与具体 plant 组合，通过 CTL 模型检测验证预言，得到显式控制器。

关键设计¶

Approximation Framework（近似框架）:
- 功能：维护预言的上下界近似，确保正确性和最大容许性
- 核心思路：定义三元组 \(\mathcal{W}=(\mathcal{A}, \underline{\kappa}, \overline{\kappa})\)，其中 \(\underline{\kappa}(q,\alpha) \subseteq \kappa(q,\alpha) \subseteq \overline{\kappa}(q,\alpha)\)。Under-approximation \(\underline{\kappa}\) 保证正确性（保守策略），over-approximation \(\overline{\kappa}\) 保证最大容许性（不遗漏正确 plant）
- 设计动机：精确计算预言（\(\kappa\)）代价太高，维护上下界提供渐进精化的可能性，且任何时刻 under-approximation 都是安全可用的
Refinement via Game Solving（基于博弈求解的精化）:
- 功能：对每个新 plant 更新近似的上下界
- 核心思路：将规范自动机与 plant 组合成博弈图 \(G\)，求解获得获胜区域 \(Win\)。对于每个状态 \(q\) 和输出 \(\alpha\)：如果 sub-plant 保证进入获胜状态则加入 \(\underline{\kappa}\)，否则从 \(\overline{\kappa}\) 中移除（Algorithm 1）。精化是单调的——只增加 under-approximation、减少 over-approximation
- 设计动机：通过与具体 plant 交互获取正负样本，逐步缩小预言的不确定范围
CTL Learning for Prophecies（学习 CTL 预言公式）:
- 功能：将上下界样本集合转化为简洁的 CTL 公式
- 核心思路：以 \(\underline{\kappa}\) 中的 plant 为正样本、\(\mathbb{P} \setminus \overline{\kappa}\) 中的 plant 为负样本，调用 learnCTL 算法学习一个 CTL 公式 \(\phi\) 来分离两类样本（Algorithm 2）。得到的 \(\phi\) 用作预言注解：\(\kappa(q,\alpha) = \mathcal{L}(\phi)\)
- 设计动机：CTL 公式简洁、人类可读、验证高效（多项式时间模型检测），且足以表达大多数实际场景中的 plant 行为条件

损失函数 / 训练策略¶

本文不涉及深度学习，核心算法流程： - 初始化：Safety LTL → 确定性安全自动机（LTLtoDSA） - 精化：博弈求解 → 获胜区域 → 更新上下界 → CTL 学习 - 验证：On-the-fly 组合（Algorithm 3）+ 模型检测验证正确性 - 安全网：Algorithm 4 的 synthesize 过程包含验证步骤——如果学习的预言不够好，会自动精化并重新学习

实验关键数据¶

主实验¶

基准	指标	UCLearn	unicon (精确)	标准合成	提升
Grid World (n×n)	计算时间比	1x	10-100x	10-100x	>10x 提速
Lily 基准	计算时间比	1x	~8x	~8x	最高 8x 提速
SYNTCOMP 安全基准	适应性	极快	较慢	不适用	显著更快适应

消融实验¶

配置	关键指标	说明
从单个 2×2 grid 学习	CTL 公式大小 ≤ 2	从极小 plant 泛化到大 grid
组合时间对比	UCLearn << unicon	CTL 模型检测比树自动机快得多
Lily 参数增大	线性增长 vs 指数增长	UCLearn 扩展性显著优于精确方法

关键发现¶

从单个小规模 plant (grid size 2) 学习的 CTL 公式可以泛化到更大的 grid（公式大小仅 ≤ 2），展示了强泛化能力
CTL 预言公式简洁且人类可读（如负载均衡器的预言：\(\forall \bigcirc (overload \Rightarrow asgn_i)\)）
在 SYNTCOMP 基准上，UCLearn 的适应速度远快于 unicon 和标准合成，因为 CTL 公式的复用成本极低

亮点与洞察¶

以学习换精确性：CTL 公式不如树自动机精确，但在实际场景中足够好（从少量 plant 学到的公式可泛化），同时大幅降低计算成本
可解释的控制器：CTL 预言是人类可读的时序逻辑公式，用户可以理解控制器为什么做出某个决策
渐进式正确性保证：under-approximation 始终正确，遇到不覆盖的 plant 会自动精化——这是一个优雅的 anytime 算法
跨 plant 泛化：控制器不是为特定 plant 定制的，而是通过预言条件化——换新 plant 只需验证 CTL 公式

局限与展望¶

CTL 的表达力弱于树自动机，对某些复杂 plant 行为可能无法找到有效的分离公式
学习质量依赖于 nominal plant 的代表性——如果初始 plant 不够多样，学到的预言可能不够泛化
目前仅支持安全 LTL 规范（safety properties），对 liveness 等其他时序属性不适用
CTL 学习算法本身的可扩展性是潜在瓶颈

评分¶

新颖性: ⭐⭐⭐⭐⭐ 首次将学习方法引入 USC 预言合成，CTL 作为预言表示是创新性的
实验充分度: ⭐⭐⭐⭐ 多个基准测试覆盖可扩展性和适应性，但实际应用场景有限
写作质量: ⭐⭐⭐⭐ 形式化定义清晰，算法伪代码完整，示例贯穿始终
价值: ⭐⭐⭐⭐ 在形式化方法/控制合成领域有重要理论和实践价值