LTL 到 Büchi 自动机的转换

形式陈述 ​

表达对应定理 ​

对每个LTL公理库线性时序逻辑 LTLLinear temporal logic · LTL · Propositional temporal logic在单条无限状态序列上解释 next、until 及其派生算子，并以全路径量词规定系统满足关系。 公式 $\phi$，都能有效构造Büchi 自动机公理库Büchi 自动机Büchi automaton · Nondeterministic Büchi automaton · NBA在无限字上运行，并以接受状态被无限多次访问作为接受条件的有限状态自动机。 ${\mathcal{A}}_{\phi }$，使

$$L_{\omega }({\mathcal{A}}_{\phi })=\{w\in (2^{AP}{)}^{\omega }:w\models \phi \}.$$

自动机状态数最坏为 $2^{O(|\phi |)}$。这一阶在最坏情形是紧的：存在长度为 $n$ 的 LTL 公式族，使任何等价 nondeterministic Büchi automaton 都需要 $2^{\mathrm{\Omega }(n)}$ 个状态。反方向并非每个$\omega$-正则语言公理库ω-正则语言Omega-regular language · ω-regular language · Regular language of infinite words由 Büchi 等价自动机形式识别的无限字语言，以及其有限前缀与无限重复结构。都可由 LTL 定义，因此结论是“LTL 语言属于 $\omega$-regular”，不是两个表达系统完全等价。

模型检查通常构造的是 ${\mathcal{A}}_{\mathrm{\neg }\phi }$。它接受违反规格的状态词；与系统取积后，非空接受运行就是反例。若误构造 ${\mathcal{A}}_{\phi }$，找到的会是满足行为而非违反行为。

closure、初态与完整一致性 ​

先把公式化为 negation normal form（仍记为 $\phi$），使否定只作用于原子命题。对 closure 中的公式 $\psi$，记 $\overline{\psi }$ 为 $\mathrm{\neg }\psi$ 化到 NNF 后的对偶。$cl(\phi )$ 对子公式、单一对偶以及时间展开所需的 $X(\alpha U\beta )$、$X(\alpha R\beta )$ 封闭，因而大小仍为 $O(|\phi |)$。

候选宏状态 $M\subseteq cl(\phi )$ 是最大一致、完备的局部类型：对每个 $\psi$，$\psi$ 与 $\overline{\psi }$ 恰有一个属于 $M$；布尔联结满足

$$\alpha \wedge \beta \in M⟺\alpha \in M\wedge \beta \in M,$$$$\alpha \vee \beta \in M⟺\alpha \in M\vee \beta \in M.$$

满足这些完备一致性条件以及下述 $U/R$ 局部展开的宏状态构成 $Q$，初始宏状态集合明确取为

$$Q_0=\{M\in Q:\phi \in M\}.$$

因此自动机不能从一个没有承担 $\phi$ 的局部类型开始。候选宏状态至多有 $2^{O(|\phi |)}$ 个。

字母读取、next 与 U/R 展开 ​

沿用本库 Büchi 自动机的运行约定，边

$$M_i\stackrel{a_i}{\to }{M}_{i+1}$$

读取当前位置字母 $a_i\in 2^{AP}$。它要求每个出现在 $\phi$ 中的原子命题与当前字母完全匹配，并把所有 next 义务精确传到下一宏状态：

$$\mathrm{\forall }p\in AP(\phi ),p\in M_i⟺p\in a_i,$$$$\mathrm{\forall }X\psi \in cl(\phi ),X\psi \in M_i⟺\psi \in M_{i+1}.$$

每个宏状态还满足 until 与 release 的局部展开等价：

$$\alpha U\beta \in M_i⟺\beta \in M_i\vee (\alpha \in M_i\wedge X(\alpha U\beta )\in M_i),$$$$\alpha R\beta \in M_i⟺\beta \in M_i\wedge (\alpha \in M_i\vee X(\alpha R\beta )\in M_i).$$

结合 next 等价，未兑现的 $U/R$ 义务恰好延续到 $M_{i+1}$。这些局部规则仍允许 $Fq=trueUq$ 永远等待，因此还需要接受条件选择 until 的最小不动点语义。

generalized Büchi 接受集 ​

对 closure 中每个 $\alpha U\beta$，建立接受集合

$$F_{\alpha U\beta }=\{M:\beta \in M\text{或}\alpha U\beta \notin M\}.$$

接受运行需无限多次访问每个这样的集合，表示义务反复被兑现或不再有效。closure 已包含 release 的否定对偶 until，故 $R$ 不需要另一套独立接受条件。自然构造得到 generalized Büchi automaton；再用计数器状态轮流等待各接受集，可转成普通 Büchi 自动机。

转换计数器增加状态，却保持语言。若把“访问所有接受集”错误改成“访问其中一个”，多个 until 义务中只兑现一项也会被接受。

正确性的两向证明骨架 ​

给定字 $w=a_0{a}_1\cdots$ 及接受运行 $M_0\stackrel{a_0}{\to }{M}_1\stackrel{a_1}{\to }\cdots$，初态条件先给出 $\phi \in M_0$。再对 closure 中公式作结构归纳：字母匹配处理原子命题，完备一致性处理否定和布尔联结，next 等价处理位置推进，$U/R$ 展开处理局部时间递归；generalized Büchi 条件排除“永远携带 $\alpha U\beta$ 却从不出现 $\beta$”的伪解。由此得到 truth lemma

$$\psi \in M_i⟺w,i\models \psi ,$$

特别有 $w,0\models \phi$；这是 soundness 方向。

反过来，若 $w\models \phi$，令

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

每个 $M_i$ 都是完备一致的局部类型，且 $\phi \in M_0$；LTL 语义保证字母匹配、next 等价以及 $U/R$ 展开成立，所以 $M_i\stackrel{a_i}{\to }{M}_{i+1}$。对任一 $\alpha U\beta$：若它在无限多个位置不属于 $M_i$，相应接受集已被无限访问；否则它从某处起持续出现，而 strong-until 语义迫使 $\beta$ 此后反复兑现，也会无限访问接受集。于是该宏状态序列是接受运行；这是 completeness 方向。

直觉

公式轨迹示例 ​

取

$$\phi =G(request\to Fgrant).$$

反例自动机针对 $\mathrm{\neg }\phi =F(request\wedge G\mathrm{\neg }grant)$。它先非确定等待某个 request，随后进入监控阶段，要求以后每个位置都没有 grant。

若词中请求后第三步出现授权，进入监控的该次猜测会失败；自动机也可等待另一个请求。只有存在某次请求永远得不到后续授权，才有接受运行。

这说明非确定性用于猜测违反见证的位置，Büchi 循环用于证明义务在无限后缀上持续失败。

例子与边界

可复算构造：$Fq$ ​

把 $Fq$ 看成 $trueUq$。相关 closure 义务包括 $q,\mathrm{\neg }q,Fq$ 以及未兑现时传给下一位置的 $XFq$。约简后的等价 Büchi 自动机可用两个状态表示：初态 $W$ 表示“仍在等待 $q$”，状态 $D$ 表示“这次 eventually 已兑现”。转移为

$$W\stackrel{\mathrm{\neg }q}{\to }W,W\stackrel{q}{\to }D,D\stackrel{q\text{ 或 }\mathrm{\neg }q}{\to }D,$$

且只有 $D$ 接受。一般公式中的接受集合

$$F_{Fq}=\{M:q\in M\text{ 或 }Fq\notin M\}$$

正好排除“$Fq$ 一直 pending 且 $q$ 从未出现”的 waiting 状态。

对词 $a_0{a}_1\cdots =\mathrm{\neg }q,\mathrm{\neg }q,q,(\mathrm{\neg }q{)}^{\omega }$，采用 $r_{i+1}\in \delta (r_i,a_i)$ 且 $r_0=W$ 的运行约定，状态序列是

$$W,W,W,D,D,\dots .$$

读完位置 $0,1$ 后仍在等待，读完位置 $2$ 的 $q$ 才进入 $D$，随后接受态被无限访问。对 $(\mathrm{\neg }q{)}^{\omega }$，唯一运行是 $W^{\omega }$，从不访问接受态，故拒绝。这与 $Fq$ 要求存在某个 $j\ge 0$ 满足 $q$ 的量词完全对应。

构造路线与边界 ​

不同翻译使用 tableau、alternating automata、very weak automata 或 formula progression；生成图大小、非确定分支和接受条件形式可以不同，但必须保存完整无限词语言。on-the-fly 只生成与系统产品可达的部分，常显著减少实际状态，却不取消上述最坏指数下界。

普通 Büchi 适合非确定反例搜索；若后续算法要求确定自动机，LTL 到 deterministic parity/Rabin automata 的最坏增长更高，不能把 NBA 的单指数结论原样搬用。

推论与应用

模型检查实际构造 ${\mathcal{A}}_{\mathrm{\neg }\phi }$，再与系统同步取积并寻找接受环。翻译的非确定状态记录尚未排除的公式义务，产品中的系统分量则保证每个接受字确由真实执行产生；两者缺一都不能给出反例。

有限 trace、past operators 与 fairness 扩展需要相应变体。把经典无限词翻译直接用于终止日志，可能因末端 next/until 语义不同而给出错误接受结果。

参考资料

• Moshe Y. Vardi and Pierre Wolper, “An Automata-Theoretic Approach to Automatic Program Verification,” LICS, 1986, pp. 332–344。
• Rob Gerth, Doron Peled, Moshe Vardi, and Pierre Wolper, “Simple On-the-fly Automatic Verification of Linear Temporal Logic,” PSTV, 1995, pp. 3–18。
• Paul Gastin and Denis Oddoux, “Fast LTL to Büchi Automata Translation,” CAV, 2001, pp. 53–65。
• Javier Esparza and Jan Křetínský, “From LTL to Deterministic Automata: A Safraless Compositional Approach,” Formal Methods in System Design 49, 2016, pp. 219–271。