⚡ electrical engineering

Co-Buchi Barrier Certificates for Discrete-time Dynamical Systems

本文引入了 co-Büchi 屏障证书 (CBBCs)，这是一种受有界合成启发并对经典屏障证书进行的推广，旨在通过迭代地搜索具有递增访问边界的合适函数，来验证离散时间动力系统在给定谓词下被访问的有界次数。

原作者： Vishnu Murali, Ashutosh Trivedi, Majid Zamani

发布于 2026-01-22

📖 1 分钟阅读☕ 轻松阅读

原作者： Vishnu Murali, Ashutosh Trivedi, Majid Zamani

原始论文采用 CC BY 4.0 许可（http://creativecommons.org/licenses/by/4.0/）。 ✨ 这是对下方论文的AI生成解释。它不是由作者撰写或认可的。如需技术准确性，请参阅原始论文。阅读完整免责声明

想象一下你正在观察一个机器人在房间里移动。你的任务是确保机器人永远不会做出危险的行为。在计算机科学和工程领域，我们通常会问一个简单的问题：“机器人是否会进入‘危险区域’？”

如果我们能证明机器人永远不会进入该区域，我们就称该系统是“安全”的。我们使用一种叫做**障碍证书（Barrier Certificate）**的数学工具来进行证明。把障碍证书想象成一道无形的、神奇的墙：

机器人从“安全侧”开始。
这道墙的形状确保随着机器人的移动，它永远无法跨越到“不安全侧”。
如果我们能画出这道墙，我们就知道机器人永远是安全的。

新问题：“不要待太久”

然而，有些规则比单纯的“绝不进入”要复杂得多。有时候，规则是：“你可以进入危险区域，但你只能进去几次。你不能永远待在那里。”

例如，想象一个机器人被允许窥视一个受限房间，但它必须离开，并且进入该房间的次数不得超过 5 次。如果它不停地进进出出，这就是一种违规。旧有的“无形墙”（障碍证书）在这里行不通，因为机器人确实被允许跨越那条线，只是次数有限。

解决方案：“Co-Büchi 障碍证书”

这篇论文介绍了一种更聪明的新工具，叫做Co-Büchi 障碍证书 (CBBC)。

把这个新工具想象成一个附着在机器人身上的神奇计数器：

计数器： 每当机器人踏入受限区域时，计数器就会加 1。
限制： 我们设定一个限制，比如 $k=5$ 。
新的墙： CBBC 是一种新型的无形墙，它不仅观察机器人在哪里，还观察其计数器上的数字是多少。
- 如果机器人在起始位置（计数器 = 0），它必须处于安全侧。
- 如果机器人达到了限制（计数器 = 5）并试图再次进入受限区域，CBBC 将证明这是不可能发生的。这就像是一道墙，随着机器人尝试访问坏地方的次数增加，墙会变得越来越高。

如果我们能找到这样一道“感知计数器的墙”，我们就从数学上证明了机器人访问受限区域的次数是有限的（具体来说，不超过我们设定的限制）。

在实践中如何运作

作者提出了一种类似于调频收音机的“尝试并观察”法：

从小开始： 他们首先尝试寻找一个针对 0 次访问限制的“墙”。如果失败了，他们就尝试 1 次访问。
增加限制： 如果他们无法证明机器人会在 1 次访问后停止，他们就会将限制增加到 2、3，以此类推。
搜索过程： 他们使用强大的计算机数学（如“平方和”（Sum-of-Squares）或 SMT 求解器）来搜索这道神奇之墙的形状。
结果： 一旦他们找到了一道适用于特定限制（例如 3 次访问）的墙，他们就会停止。这时他们已经证明了机器人访问坏地方不会超过 3 次。

为什么这比旧方法更好

这篇论文将其与一种称为**“状态三元组法”（State Triplet Approach）**的旧方法进行了对比：

旧方法： 想象一下，试图通过封锁机器人可能采取的所有路径来阻止它。如果机器人可以绕过一个转角两次，旧方法就会感到困惑并放弃。这就像试图通过在水流可能流过的每一个点都筑起大坝来阻挡河流一样——如果水流存在循环，这是不可能实现的。
新方法 (CBBC)： 新方法更聪明。它不仅封锁路径，还会计算循环次数。它意识到：“好吧，机器人可以绕行一次，也许两次，但如果它尝试第三次，数学逻辑就会说‘没门’。”

作者在三个不同的场景中测试了该方法：

房间温度模型： 一个控制热量的系统。他们证明了温度只会进入“过热”区域几次，然后就会趋于稳定。
二维振荡器： 一个摆动单摆的数学模型。他们证明了它进入特定“危险区域”的次数是有限的。
三维振荡器： 一个具有三个运动部分的更复杂的系统。他们成功证明了相同的访问次数限制。

核心结论

这篇论文为工程师提供了一种新方法，用以证明一个系统不会陷入“坏行为循环”。他们不再仅仅说“绝不要去那里”，而是可以说：“你可以去那里，但只能去几次，然后你必须停止。”他们通过在安全证明中加入一个“计数器”，将一个复杂的“无限”问题转化为了一个可处理的“有限”问题。

技术摘要：离散时间动力系统的 Co-Büchi 屏障证书

问题定义

本文解决了验证离散时间动力系统是否满足 $\omega$ -正则属性的挑战，特别是那些要求证明特定状态集（或区域）仅被有限次访问的属性。传统的安全性验证确保系统永不进入不安全集合。然而，许多时序逻辑属性（例如由通用 Co-Büchi 自动机或 Büchi 自动机的补集所指定的属性）需要证明系统不会无限次地访问接受状态。

现有方法面临显著的局限性：

状态三元组方法： 先前的研究方法（如 Wongpiromsarn 等人）使用屏障证书通过打破状态三元组来“切断”自动机的路径。虽然这种方法对于有限词自动机或 co-safe 语言有效，但它是保守的，并且对于一般的无限词自动机往往会失效。它无法验证那些即使总访问次数有限、但轨迹会多次（例如超过两次）到达接受状态的系统。
有界合成的局限性： 虽然有界合成通过限制状态访问次数将 LTL 规范转换为安全性问题，但标准技术通常需要展开自动机或处理缺乏增量保证的复杂乘积构造。
复杂度： 连续空间上的传统模型检测受制于维度灾难，而现有的针对时序逻辑的屏障证书方法往往依赖于特定的模板，或者缺乏必要性保证。

核心问题在于开发一种函数式过近似（即证书），用以证明系统的轨迹对特定区域的访问次数是受限的，且无需显式构建完整的乘积系统或无限展开自动机。

方法论

作者提出了 Co-Büchi 屏障证书 (CBBCs)，这是经典屏障证书的一种推广。该方法论依赖于以下概念和计算步骤：

1. 概念框架：将有限访问视为安全性

其核心洞察是：虽然“有限次访问一个区域”本身不是直接的安全性属性，但可以通过为系统添加一个计数器将其转化为安全性问题。

扩展系统： 原系统 $S$ 在概念上通过附加一个计数器 $\ell$ 扩展为 $S'$ ，每当系统进入目标区域 $X_{VF}$ 时，计数器 $\ell$ 就会递增。
安全性归约： 证明 $X_{VF}$ 被访问有限次，等价于证明扩展系统 $S'$ 永远不会达到计数器超过固定界限 $k$ 的状态。这通过将问题转化为在扩展状态空间上的标准安全性验证问题。

2. CBBC 的定义

Co-Büchi 屏障证书是一个函数 $B: X \times [0..k] \to \mathbb{R}$ ，它满足特定的条件以确保计数器不会超过 $k$ ：

初始条件： 对于所有初始状态， $B(x, 0) \le 0$ 。
不安全条件： 对于所有在目标区域 $X_{VF}$ 中的状态， $B(x, k) > 0$ （表明以计数器为 $k$ 到达该区域是“不安全”的）。
归纳步骤：
- 如果系统不在 $X_{VF}$ 中，则 $B$ 的值必须是非递增的（计数器保持不变）。
- 如果系统在 $X_{VF}$ 中，则下一步（计数器增加后）的 $B$ 值相对于当前步必须是非递增的。

论文证明了，在满足预设假设（oracle assumptions）的情况下，存在这样一个函数对于系统最多访问该区域 $k$ 次是充分且必要的。

3. 自动机理论验证

为了验证由通用 Co-Büchi 自动机 (UCA) $A_{c,k}$ 指定的属性：

系统 $S$ 与自动机同步以形成乘积系统。
CBBC 的“不安全”区域被定义为乘积状态中自动机处于接受状态的集合。
验证算法搜索具有界限 $k$ 的 CBBC。如果找到，则系统满足该属性。如果未找到，则增加 $k$ 并重复搜索。这提供了一种增量式验证方法。

4. 计算方法

论文提出了两种计算 CBBC 的方法：

平方和 (SOS) 方法： 假设系统动力学和状态集是半代数形式的（由多项式不等式定义）。寻找屏障证书的过程被转化为一个半正定规划 (SDP) 问题。其复杂度对于状态空间的维度（假设固定多项式阶数模板）是多项式级的，并且对于界限 $k$ 是线性级的。
基于 SMT 的方法 (CEGIS)： 使用反例引导的归纳合成 (Counterexample-Guided Inductive Synthesis)。它从状态空间中采样点，将 CBBC 约束编码为关于线性实算术的满足性模理论 (SMT) 查询，并迭代地利用反例来精炼候选证书，直到找到有效的函数或达到超时。

核心贡献

新颖的证书定义： 引入了 Co-Büchi 屏障证书 (CBBCs)，通过将计数器变量直接整合进证书函数中，将其推广到处理“有限访问”属性。
理论保证： 论文确立了 CBBC 不仅是验证有限访问属性的充分条件，也是必要条件，这比许多现有的时序验证方法提供了更强的声明。
对状态三元组方法的泛化： 作者证明了 CBBC 方法涵盖了“状态三元组”方法。他们提供了一个构造性证明，表明如果一个系统可以通过状态三元组方法进行验证，那么它也可以通过 CBBC 进行验证；但反之则不然（CBBC 可以验证三元组方法无法验证的系统）。
增量验证策略： 提出的方法允许对界限 $k$ 进行增量搜索。算法从 $k=0$ 开始，仅在找不到证书时才增加 $k$ ，从而在计算成本和验证能力之间提供实用的权衡。
计算框架： 提供了用于合成这些证书的两种算法：基于 SOS（针对多项式系统）和基于 SMT（针对一般系统）。

结果与案例研究

论文通过三个案例研究验证了该方法：

室温模型（状态三元组法的失效）： 该系统由于自动机边上存在重叠标签（具体表现为无法通过重复标签切断路径），导致状态三元组方法失效。CBBC 方法成功找到了一个 $k=4$ 的证书，证明了在该处属性成立，而此前的方法无法得出结论。
二维 Van der Pol 振荡器： 一个针对 UCA 验证的非线性系统。使用 SOS 方法，在约 5 分钟内找到了一个 6 阶 CBBC ( $k=3$ )，证明了接受状态最多被访问 3 次。
三维 Kuramoto 振荡器： 一个具有三角函数动力学的更高维系统（通过泰勒级数近似）。找到了一个 4 阶 CBBC ( $k=2$ )，耗时约 20 分钟，验证了特定区域的有限访问性。

意义与主张

论文声称 CBBCs 为离散时间动力系统的 $\omega$ -正则属性验证提供了一个鲁棒且无需抽象的框架。其重要性在于：

克服保守性： 它解决了状态三元组方法的局限性，后者对于一般的无限词自动机往往过于保守。
可扩展性： 通过避免显式构建具有庞大状态空间的复杂乘积自动机，并依赖函数式过近似，该方法在（固定模板下）随状态维度呈多项式级扩展，缓解了维度灾难。
必要性： 不同于许多启发式方法，论文强调了这些证书的必要性，这意味着如果一个系统满足该属性，理论上必然存在一个 CBBC。

作者指出，虽然 CBBCs 在验证方面非常有效，但由于处理非确定性和实现问题中对确定性自动机的需求，其在合成（控制器设计）方面的应用仍具挑战。他们将此列为未来的研究方向，包括将该方法扩展到加权、随机和定时自动机。