LTL 到 Büchi 自动机的转换

LTL 公式用“下一步”“最终”“一直”“直到”等词描述无限执行。把它转成 Büchi 自动机，就是把这些时间要求改写成一台有限状态机器，让机器沿执行序列读取每一步发生的事，并用无限运行的接受条件判断要求是否真的兑现。

转换中最重要的一点是：局部转移只能说明一项义务怎样被推迟，接受条件才能保证它没有永远被推迟。 如果省掉后者，“最终发生”就会被错误地理解成“每一步都说下一步再发生”。

形式陈述

输入是什么，自动机要接受什么

设原子命题集合为有限集 $AP$ ，每个字母 $a_i\subseteq AP$ 表示第 $i$ 个时刻哪些命题成立。一个无限词为

w=a_0a_1a_2\cdots\in(2^{AP})^\omega.

LTL 语义 $w,i\models\varphi$ 表示公式 $\varphi$ 在这个词的第 $i$ 个位置成立。例如

w,i\models\alpha\,\mathrm U\,\beta

表示存在某个 $j\ge i$ ，使 $\beta$ 在 $j$ 成立，而且 $\alpha$ 在 $i,\ldots,j-1$ 都成立。这里允许 $j=i$ ：如果 $\beta$ 现在成立，就不要求 $\alpha$ 现在也成立。

目标是构造非确定性 Büchi 自动机 $A_\varphi$ ，使

L(A_\varphi)=\{w:w,0\models\varphi\}.

它由有限状态集、初态集、按字母标记的转移和接受条件组成。一次运行是否接受，取决于某些状态是否被无限次访问，而不是是否走到了某个有限的“终点”。[1]

一个完整的闭包—原子构造

下面给出便于核对正确性的教科书式构造。它不追求立即得到最少状态，而是把布尔一致性、下一步约束和无限接受三部分明确分开。

闭包：只跟踪有限多个子公式

先把公式化成否定范式：否定只出现在原子命题前，使用 $\land,\lor,\mathrm X,\mathrm U,\mathrm R$ 。记 $\bar\psi$ 为 $\neg\psi$ 化成否定范式后的公式，并采用 $\bar{\bar\psi}=\psi$ 的规范化约定。

构造有限闭包 $\mathrm{cl}(\varphi)$ ，包含公式的子公式及其对偶；对闭包中的每个 Until 或 Release 公式 $\chi$ ，再加入 $\mathrm X\chi$ 及其对偶，并闭合于子公式。只需要这些有限的后继义务，闭包大小仍为 $O(|\varphi|)$ ，不需要不断加入 $\mathrm{XX}\chi,\mathrm{XXX}\chi,\ldots$ 。

原子：对“现在为真”作局部一致的猜测

状态取闭包中的一个集合 $M$ ，表示此刻为真的公式。这里只保留满足以下要求的集合，称作原子：每对 $\psi,\bar\psi$ 恰选一个，真常量必选、假常量不选；布尔联结满足通常的真值关系；Until 与 Release 满足上述展开式。

例如对 $\chi=\alpha\,\mathrm U\,\beta$ ，要求

\chi\in M \iff \beta\in M\ \lor\ (\alpha\in M\land\mathrm X\chi\in M).

对 $\chi=\alpha\,\mathrm R\,\beta$ ，要求

\chi\in M \iff \beta\in M\ \land\ (\alpha\in M\lor\mathrm X\chi\in M).

“恰选一个”保证状态不是随意列出部分愿望，而是对闭包作一份完整、互不矛盾的局部赋值。不过，局部一致仍然不能排除无限拖延，接受条件还没有加入。

转移：现在的 Next 必须成为下一状态的事实

初态集为 $I=\{M:\varphi\in M\}$ 。采用源状态匹配当前字母的约定：存在转移 $M\xrightarrow{a}M'$ ，当且仅当

p\in M\iff p\in a \quad\text{对公式涉及的所有原子命题 }p,

并且

\mathrm X\psi\in M\iff\psi\in M' \quad\text{对闭包中的所有 }\mathrm X\psi.

于是读取 $a_i$ 之前的状态 $M_i$ 表示第 $i$ 个位置的真值信息，边消耗 $a_i$ 后进入 $M_{i+1}$ 。也可以采用目标状态匹配字母的另一种约定，但初态和所有下标必须一起移动；混用两种约定会使 Next 偏移一个位置。

接受集合：排除无限期不兑现的 Until

对闭包中每个 $\chi=\alpha\,\mathrm U\,\beta$ ，定义

F_\chi=\{M:\chi\notin M\ \lor\ \beta\in M\}.

要求运行对每一个 $F_\chi$ 都访问无限多次。得到的是广义 Büchi 自动机，而不是只带一个接受集合的普通 Büchi 自动机。

这里包括闭包中由否定 Release 产生的 Until。因为状态对公式及其对偶都声明真假，这些对偶的无限语义也必须受到约束。只为原公式表面上出现的几个 Until 加条件，却保留完整对偶状态系统，可能允许错误的真值猜测。

直觉

先理解一个义务：最终看到 q

公式 $\mathrm Fq$ 表示现在或未来某个位置出现 $q$ 。它可以由两态自动机识别：初态 $W$ 表示尚未见到 $q$ ，接受态 $D$ 表示要求已经兑现。

当前状态	读到的字母	下一状态
$W$	$q$ 不成立	$W$
$W$	$q$ 成立	$D$
$D$	任意字母	$D$

只有 $D$ 是接受态。对词 $\neg q,\neg q,q,(\neg q)^\omega$ ，状态依次为 $W,W,W,D,D,\ldots$ ，因此接受；对 $(\neg q)^\omega$ ，运行永远停在 $W$ ，因此拒绝。

一旦 $q$ 出现一次，后面永远没有 $q$ 也不影响 $\mathrm Fq$ 为真。接受条件“无限次访问 $D$ ”表达的是义务已经被永久解除，不是要求 $q$ 本身无限次出现；要求后者的公式是 $\mathrm{GF}q$ 。

对 Fq，W 表示仍在等待，D 表示义务已经完成。D 是接受态，见过一次 q 后即可一直停留。

为什么只展开 Until 还不够

Until 满足局部展开式

\alpha\,\mathrm U\,\beta \equiv \beta\lor\bigl(\alpha\land\mathrm X(\alpha\,\mathrm U\,\beta)\bigr).

含义是：要么终点条件 $\beta$ 现在兑现，要么现在满足 $\alpha$ ，并把同一项 Until 义务带到下一步。

但这个方程允许一个虚假的无限解：让 $\alpha$ 永远为真、 $\beta$ 永远为假，同时在每个位置都宣称 Until 为真。每一步的局部展开都能自圆其说，却违背了强 Until 必须最终出现 $\beta$ 的语义。

因此自动机还要为每个 Until 设置一个接受集合：运行必须无限次处于“这项义务当前不活跃”或“它的终点条件已经出现”的状态。持续活跃却永不兑现的义务，就会被排除在接受运行之外。

Release 是 Until 的对偶：

\alpha\,\mathrm R\,\beta \equiv \neg(\neg\alpha\,\mathrm U\,\neg\beta),

局部展开为

\alpha\,\mathrm R\,\beta \equiv \beta\land\bigl(\alpha\lor\mathrm X(\alpha\,\mathrm R\,\beta)\bigr).

它允许 $\beta$ 永远成立而 $\alpha$ 永不出现。Until 与 Release 分别带有“最终必须兑现”与“可以永久维持”的不同无限语义，不能仅因展开式相似就使用相同的终止要求。

为什么这个构造确实识别原公式

从满足公式的词到接受运行。 对给定词 $w$ ，让

M_i=\{\psi\in\mathrm{cl}(\varphi):w,i\models\psi\}.

真实语义自动满足布尔关系、Until／Release 展开和 Next 转移。如果 $w,0\models\varphi$ ， $M_0$ 也是合法初态。对每个 Until，若某一时刻起始终不进入 $F_\chi$ ，就意味着义务始终成立、 $\beta$ 始终不成立，与 Until 的语义矛盾。因此每个接受集合都被无限次访问。

从接受运行到满足公式。 证明状态中的公式与词的真实语义相符。原子、布尔和 Next 情况由字母匹配与转移条件处理。关键仍是 Until：若 $\chi\in M_i$ ，且 $\beta\notin M_i$ ，局部展开强迫 $\alpha\in M_i$ 和 $\chi\in M_{i+1}$ 。

若一直见不到 $\beta$ ，这项义务就一直活跃，运行从此不再进入 $F_\chi$ ，与接受矛盾。因此必有有限的兑现位置，其前面所有位置都满足 $\alpha$ 。反方向则可从 $\beta$ 的兑现位置沿展开式向前回推。Release 通过它的否定 Until 对偶得到对应结论。

最后 $\varphi\in M_0$ 给出 $w,0\models\varphi$ 。这份证明说明三个组件各自承担什么：闭包限定需要记忆的信息，转移保证相邻时刻一致，接受条件选择正确的无限解，而不是任意满足递推等式的解。[1][2]

补充示意图

LTL 公式 Fq 的两态 Büchi 自动机及在 ¬q,¬q,q,(¬q)^ω 上的接受运行 — Fq 到 Büchi 自动机

例子与边界

复杂度与表达能力的边界

从 LTL 到非确定性 Büchi 自动机，最坏情况需要指数级状态，构造规模的上界并非完全来自某个实现不够聪明。非确定性有时也不可避免：例如“最终一直满足 $p$ ”适合猜测最后一次违反之后的位置，并不能对所有 LTL 公式都改用等价的确定性 Büchi 自动机。

需要确定性自动机时，通常使用奇偶或Rabin等更一般的接受条件；Safra确定化解释了Büchi运行历史如何保存在有限树里，一般LTL到确定自动机的最坏规模可达双指数。反过来，Büchi能表达全部 $\omega$ -正则语言，LTL只表达其中一部分，所以“LTL可转Büchi”不是两种表示能力完全相同的等价定理。

确定监控器也为LTL控制器综合提供接口。验证寻找一条违反给定系统规格的路径；综合则先选一个只看已知输入的统一输出策略，再要求它应对全部环境输入。把非确定自动机的一次成功猜测直接当作控制器动作，会漏掉这一量词和信息时机的变化。

学习与实现时，最值得检查的仍是三个细节：字母在哪个状态位置被读取，Next 是否准确跨一步，以及所有 Until 义务是否分别接受公平性约束。状态数优化应建立在这三项语义对齐之后，而不能用更小的图替代正确的无限运行含义。

推论与应用

多项义务与普通 Büchi 的转换

对 $\mathrm Fp\land\mathrm Fq$ ，自动机必须兑现两项义务。若只要求进入 $F_p\cup F_q$ 无限次，那么 $p$ 已出现、 $q$ 永不出现的运行仍可能被错误接受，因为它可以一直待在 $F_p$ 中。广义 Büchi 使用的是“对每个集合分别无限访问”，不是把集合并起来。

假设广义接受集合为 $F_1,\ldots,F_k$ ， $k\ge1$ 。可给状态附加计数器 $j\in\{1,\ldots,k\}$ ，表示当前等待访问 $F_j$ 。初始 $j=1$ ；沿源状态 $q$ 的转移时，若 $q\in F_j$ ，就把计数器推进到下一个集合， $k$ 后回到 1，否则保持不变。

普通 Büchi 接受集可以准确地取为

F'=\{(q,k):q\in F_k\}.

它标记一整轮等待将被完成的位置。无限次访问 $F'$ 就意味着完成无限多轮，因而每个 $F_j$ 都被无限次访问。

不能只把“计数器等于 1”设为接受条件：若运行永远没等到 $F_1$ ，计数器也可能永远停在 1，造成假接受。若 $k=0$ ，则没有额外公平性义务，所有状态都可设为接受状态，但仍需存在一条无限运行。

这一转换增加至多 $k$ 倍状态。结合最多 $2^{O(|\varphi|)}$ 个闭包原子，整体仍为单指数规模。实际工具通过按需展开、合并和简化状态，通常不会真的先枚举闭包的所有子集。[2][3]

模型检测时为什么转换的是否定公式

设有限状态系统 $K$ 的所有无限执行构成语言 $L(K)$ 。要检查它是否总满足 $\varphi$ ，等价于检查

L(K)\cap L(A_{\neg\varphi})=\varnothing.

因此常构造的是“坏执行”的自动机，再与系统做乘积，寻找接受运行。若有限图存在接受无限运行，就存在一段有限前缀加非空循环组成的接受见证；这不表示每一条接受运行都最终周期。在广义 Büchi 情形，相关可达强连通区域还需能反复经过每个接受集合，并确实包含可无限运行的循环。

例如响应性质

\mathrm G(\mathrm{request}\to\mathrm F\mathrm{grant})

的否定为

\mathrm F(\mathrm{request}\land\mathrm G\neg\mathrm{grant}).

坏执行自动机可以非确定性地猜测某次请求从此永远得不到授权，然后检查后面始终没有 grant。非确定性不是在有限时间里神奇地预知未来，而是提供多个候选运行，只有猜测与整个无限词一致的那条才会接受。

这里 $\mathrm F$ 包括当前位置，因此请求与授权同一步出现就已经满足该次响应。若业务要求严格在后续步骤授权，应使用 $\mathrm{XF}\mathrm{grant}$ 等相应表达。公式也没有要求不同请求对应不同授权；一个未来授权可以同时满足多项尚未完成的这种布尔响应要求。

参考资料

[1] Moshe Y. Vardi and Pierre Wolper, “An Automata-Theoretic Approach to Automatic Program Verification,” LICS, 1986；链接为作者版本，奠定逻辑到无限自动机的模型检测路线。

[2] Rob Gerth, Doron Peled, Moshe Y. Vardi, and Pierre Wolper, “Simple On-the-fly Automatic Verification of Linear Temporal Logic,” PSTV, 1995, pp. 3–18，按需转换与 Until 接受义务。

[3] Paul Gastin and Denis Oddoux, “Fast LTL to Büchi Automata Translation,” CAV, 2001, pp. 53–65，实用转换与简化。

[4] Christel Baier and Joost-Pieter Katoen, Principles of Model Checking, MIT Press, 2008，LTL、广义 Büchi、空语言检查及其正确性。

形式陈述 ​

输入是什么，自动机要接受什么 ​

一个完整的闭包—原子构造 ​

闭包：只跟踪有限多个子公式 ​

原子：对“现在为真”作局部一致的猜测 ​

转移：现在的 Next 必须成为下一状态的事实 ​

接受集合：排除无限期不兑现的 Until ​

先理解一个义务：最终看到 q ​

为什么只展开 Until 还不够 ​

为什么这个构造确实识别原公式 ​

复杂度与表达能力的边界 ​

多项义务与普通 Büchi 的转换 ​

模型检测时为什么转换的是否定公式 ​

反向链接