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在生成自动机的大小、运行时间、确定性等方面具有相对的优势。