基于证书函数的形式化分析
Lyapunov 函数、障碍函数与超鞅类证书为稳定性、安全性和可达—规避性质提供了形式化分析工具。对随机系统而言，证书函数能够把系统局部期望演化条件与整体概率性质联系起来。
Background
学习型控制能够处理复杂任务，但经验性能不等于形式化保证。
机器人、自主系统和其他网络物理系统在运行时常常受到随机扰动、传感噪声与模型误差的影响。即使从同一个初始状态出发，控制器也可能产生不同的系统轨迹。对安全关键任务而言，平均性能或少量成功轨迹不足以刻画系统风险。
可达—规避任务把目标可达性与安全性放在同一个要求中：系统最终需要进入指定的目标区域，并在到达目标之前始终避开不安全区域。由于系统轨迹具有随机性，这一要求通常以任务完成的概率表达，而不是假设每次运行都必然成功。
学习型控制可以利用数据处理复杂、非线性和高维系统，但训练数据与有限次仿真只能覆盖部分状态和扰动样本。较高的经验成功率并不自动意味着控制器对整个初始集合、给定扰动分布和无限时间范围都满足要求，因此还需要形式化分析明确保证成立的条件、范围与概率下界。
Core problem
在随机扰动下，能否合成一个使系统以可证明概率完成可达—规避任务的控制器？
考虑如下离散时间随机系统：
xt+1 = f(xt, ut, ωt),
ut = π(xt).
给定状态空间 Ψ、初始集合 Θ、目标集合 Xg、不安全集合 Xu 与扰动分布 𝒫，目标是合成策略 π，使每个 x0 ∈ Θ 都满足：
Prπx₀ [
∃ t ≥ 0 : xt ∈ Xg
∧ ∀ 0 ≤ τ ≤ t, xτ ∉ Xu
] ≥ δ.
δ 是经过形式化验证的可达—规避概率下界。这里要回答的不只是控制器在有限次仿真中的经验成功率，而是这一概率下界能否对整个初始集合和无限时间范围成立。
- Θ 初始集合
- Xg 目标集合
- Xu 不安全集合
- 成功轨迹
- 不安全轨迹
- 随机分支
- 01
随机系统可达—规避控制
面向非线性随机系统，研究怎样设计控制策略，使闭环系统在随机扰动下获得良好的可达—规避性能。
- 02
形式化概率保证
研究怎样为整个初始集合证明控制器满足可达—规避要求，并计算具有实际意义的概率下界。
- 03
学习型控制的形式化验证
研究怎样协调学习型控制器的表达能力与后续形式化验证的可计算性。
- 04
计算可扩展性
研究怎样让控制器合成与形式化验证扩展到更高维、更强非线性以及具有更一般扰动分布的随机系统。
Research landscape
现有研究已经建立了形式化保证的基本框架，但仍受到可扩展性限制。
随机系统可达—规避控制的形式化分析通常依赖证书函数，把难以直接处理的无限时间概率性质转化为可检查的函数条件。随着学习方法进入控制领域，“学习候选控制器或证书，再进行形式化验证”也成为重要研究路线。
学习辅助的控制与证书构造
强化学习和神经网络可以为复杂非线性系统获得控制策略，也可以帮助构造候选证书函数。它们提高了控制性能与表达能力，但学习结果通常首先由训练样本提供经验支持，仍需要额外的形式化验证。
对学习结果进行形式化后验证
现有方法常通过区间界、Lipschitz 界与状态空间划分验证学习得到的控制器和证书。系统维度上升时，分区数量会快速增长；部分方法还假设扰动空间有界，使具有无界支撑的分布更难直接处理。
Why it matters
研究目标不是只判断若干次实验是否成功，而是明确系统在什么条件下至少有多大概率完成任务。
- 01
从经验成功率走向可验证概率下界
仿真描述控制器在抽样场景中的表现；形式化概率保证进一步说明，在给定系统模型、初始集合和扰动分布下，任务完成概率至少是多少，使风险具有明确的数学含义。
- 02
把可达—规避要求纳入控制器设计
可达—规避控制把到达目标、避开不安全区域和概率要求一起纳入控制器合成，使形式化保证成为设计目标，而不只是控制器完成后的附加检查。
- 03
扩展形式化方法的适用范围
提高非线性、高维和一般随机扰动下合成与验证的可扩展性，有助于让形式化概率保证从低维示例走向更复杂的控制任务。
Research outcomes
科研经历与成果
以下条目与当前研究方向直接相关。对于在投稿件，仅展示可以公开的研究主题与投稿状态，不披露匿名稿件、方法、实验或审稿信息。
科研项目国家自然科学基金面上项目
面向神经网络控制系统安全验证的多项式代数方法研究
研究神经网络控制策略在非线性系统中的形式化安全验证。
论文与投稿
- 已接收 · 2026Learning-Aided Reach-Avoid Controller Synthesis with Formal Guarantees for Stochastic Systems
MEMOCODE 2026 · CCF C 类会议
第一作者 - 在投Safety Guarantees for Nonlinear Systems with Bayesian Neural Network Control Policies
Formal Aspects of Computing · CCF B 类期刊
导师一作，本人二作 - 在投
一篇关于随机系统可达—规避控制器合成与形式化概率保证的工作
CCF A 类会议