论文分享_08_01

LTL to Büchi Automata Translation: Fast and More Deterministic

一、主要问题

二、主要贡献

       针对LTL转Büchi自动机的问题,本文在Fast LTL to Büchi Automata Translation(CAV 2001)这篇文章的经典算法基础上进行了改进,能够更快的生成更小、更有确定性的自动机。CAV 2001中提出的算法框架如下:

  1. 将给定LTL转为一个接受条件为co- Büchi 的very weak alternating automaton (VWAA);
  2. 将这个VWAA转为一个transition-based generalized Büchi automaton (TGBA);
  3. 将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

        首先简单介绍TGBA的定义,即接受状态为多个transition集合的自动机:

3.3 Experiments

本文的算法用C++实现了一个工具名为LTL3BA,中间数字3是因为前面提到的CAV 2001文章将他们的算法实现为LTL2BA。

如图是对不同的公式与SPOT和LTL2BA的运行时间比较,横轴表示公式中的参数n,纵轴表示运行时间(单位是秒):

如表,是SPOT,SPOT+WDBA最小化,LTL2BA,以及LTL3BA使用文中不同的优化方法得到的自动机状态、迁移、时间和确定性的比较,可以看到LTL3BA在生成自动机的大小、运行时间、确定性等方面具有相对的优势。