LTL to Büchi Automata Translation: Fast and More Deterministic
一、主要问题
二、主要贡献
- 将给定LTL转为一个接受条件为co- Büchi 的very weak alternating automaton （VWAA）；
- 将这个VWAA转为一个transition-based generalized Büchi automaton (TGBA)；
- 将TGBA转为Büchi automaton (BA)。
从线性时序逻辑公式生成Büchi自动机一直是model checking领域的重要问题，早在1995年Moshe Vardi等人就提出了“tableau construction”的方法，但是这个方法在很多情况下会需要较长的运行时间和大量内存，CAV 2001提出的算法先生成一个“very weak alternating automaton”，再将其转为TGBA，可以有效地避免直接生成状态数较多的Büchi自动机。注意这里先构造的是一个“very weak”的alternating automaton，正是由于“very weak”的性质，其每个run的infinite branch上的状态都是递减的（这里其实需要解释如何定义的偏序关系，但是要完全说清楚比较麻烦，有兴趣的读者可以自己看CAV 2001这篇原文Theorem 2的证明），而状态集合有穷，故最终必为常数，于是才有文中very weak alternating co-Büchi automaton和其构造的TGBA的等价性。另外，该算法框架这种将任务分解为一步步完成的结构，也使得作者可以分别在每一步进行自动机的simplification和算法的优化。
本文主要思路：
本文基于上述经典的算法框架，观察到具有“alternating”结构的一类公式，定义这样的“alternating公式”，然后利用alternating公式的性质，来优化上面经典算法框架中每一步的转换过程，下面在本文内容中详细介绍改进优化的方法。
三、本文内容
3.1 Preliminaries：
1) LTL：即线性时序逻辑（Linear Temporal Logic）
语法（Syntax）：
语义（Semantics）：
为了便于表示，增加如下的时序算子（temporal operators）：
2) Büchi自动机：
3) Very Weak Alternating co-Büchi Automata(VWAA)：
3.2 Algorithm：
下面开始介绍LTL到BA的转换算法，对每一步，会先介绍CAV 2001文章中的原始算法，然后介绍本文所进行的改进。
3.2.1 LTL to VWAA Translation:
为了便于解释，先定义一些符号：
3.2.2 VWAA to TGBA Translation
3.3 Experiments
本文的算法用C++实现了一个工具名为LTL3BA，中间数字3是因为前面提到的CAV 2001文章将他们的算法实现为LTL2BA。
如图是对不同的公式与SPOT和LTL2BA的运行时间比较，横轴表示公式中的参数n，纵轴表示运行时间（单位是秒）：
如表，是SPOT，SPOT+WDBA最小化，LTL2BA，以及LTL3BA使用文中不同的优化方法得到的自动机状态、迁移、时间和确定性的比较，可以看到LTL3BA在生成自动机的大小、运行时间、确定性等方面具有相对的优势。
