LTL 到 Büchi 自动机的转换

表达对应定理 ​

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

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

自动机状态数最坏为 $2^{O(|\phi |)}$。反方向并非每个$\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，使否定只作用于原子命题。定义 closure $cl(\phi )$，包含公式的全部子公式，以及分析下一步义务所需的相应否定。

候选自动机状态是 closure 的一致子集 $M$。它们至少满足布尔局部约束：

$${\psi }_1\wedge {\psi }_2\in M⟺{\psi }_1\in M\wedge {\psi }_2\in M,$$

并对每个命题选择相容真值。因为 $|cl(\phi )|=O(|\phi |)$，候选集合数自然出现指数上界。

一致性筛掉明显矛盾，却不单独保证所有无限时间义务兑现。尤其 $Fq$ 或 $pUq$ 不能只靠当前状态标记判断，需要接受条件跟踪。

next 与 until 的转移责任 ​

从宏状态 $M$ 到 $M^{\prime }$ 的转移要求

$$X\psi \in M⟹\psi \in M^{\prime }.$$

until 公式按展开

$$pUq\equiv q\vee (p\wedge X(pUq))$$

处理：若 $q$ 当前未兑现而 $pUq$ 仍在 $M$，则 $p$ 当前成立，并把 $pUq$ 作为下一状态义务继续携带。

若只允许义务永远延期，公式 $Fq=trueUq$ 会在从不出现 $q$ 的字上产生伪运行。Büchi 接受集合必须确保每个 until 承诺不是永久 pending。

generalized Büchi 接受集 ​

对每个 $pUq$，建立接受集合

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

接受运行需无限多次访问每个这样的集合，表示义务反复被兑现或不再有效。自然构造得到 generalized Büchi automaton；再用计数器状态轮流等待各接受集，可转成普通 Büchi 自动机。

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

公式轨迹示例 ​

取

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

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

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

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

构造边界与优化 ​

不同翻译使用 tableau、alternating automata、very weak automata 或 formula progression；生成图大小和接受条件形式可不同，但都必须保存完整无限词语言。

实践中 on-the-fly 只生成与系统产品可达的自动机状态，常避免最坏全量指数图。它改善实际成本，不改变公式族的指数下界。

有限 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。
• 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。