引用本文
单来祥, 覃征, 卢欣晔, 卢正才. 线性时序逻辑转换Büchi自动机的按需即时算法. 清华大学学报: 自然科学版, 2014, 54(2): 281-288[Laixiang SHAN, Zheng QIN, Xinye LU, et al. On-the-fly translation algorithm from linear temporal logic to Büchi automata[J]. 2014, 54(2): 281-288]  
Permissions
Copyright@2014, 《清华大学学报（自然科学版）》编辑部
版权所有
线性时序逻辑转换Büchi自动机的按需即时算法
单来祥1, 覃征1,2, 卢欣晔3, 卢正才1
1. 清华大学 计算机科学与技术系, 清华信息科学与技术国家实验室, 北京 100084
2. 清华大学 软件学院, 北京 100084
3. 中国科学院 软件研究所, 北京 100190
覃征, 教授, E-mail:qingzh@mail.tsinghua.edu.cn

作者简介: 单来祥(1977—), 男(汉), 山东, 博士研究生。

基金:国防“十二五”预研基金重点项目 (9140A1550212JW01047); 高等学校博士学科点专项科研基金优先发展领域课题 (20120002130007);
摘要

将线性时序逻辑公式转换成Büchi自动机是显式模型检测中的关键环节, Tableau规则是常用转换算法。该文提出了基于Tableau规则的改进算法,将线性时序逻辑公式转换成基于迁移的Büchi 自动机。通过在状态和迁移中加入U公式的满足信息,实现了用一个接受条件集合判断执行序列是否可接受,避免了使用多个接受条件集合进行判断。改进算法引入了按需即时(on-the-fly)去扩展化机制,算法展开状态节点的同时进行状态有效性检测,删除无效节点,合并等价状态和迁移,避免了后置化简。与其他转换工具进行比较实验表明,该算法具有执行速度快、生成自动机的状态数和迁移数少的特征。

关键词: 线性时序逻辑; 基于迁移的Büchi自动机; 按需即时
中图分类号:TP301.1 文献标志码:A 文章编号:1000-0054(2014)02-0281-08
On-the-fly translation algorithm from linear temporal logic to Büchi automata
Laixiang SHAN1, Zheng QIN1,2, Xinye LU3, Zhengcai LU1
1. Tsinghua National Laboratory for Information Science and Technology, Department of Computer Science and Technology, Tsinghua University, Beijing 100084, China
2. School of Software, Tsinghua University, Beijing 100084, China
3. Institute of Software Chinese Academy of Sciences, Beijing 100190, China
Fund:
Abstract

Translations of linear temporal logic to Büchi automata are key to explicit model checking, with the Tableau-based algorithm commonly used for the translation. This paper describes an improved Tableau-based algorithm which converts linear temporal logic to transition-based Büchi automata. The satisfaction information of the U-formula for the states and transitions is used to judge whether the automata is acceptable using only one acceptance condition set, rather than multiple sets. Thus, the algorithm gives an on-the-fly degeneralization mechanism that can expand the state nodes while detecting their validity and removing invalid nodes. The algorithm combines equivalent states and transitions and avoids simplifications after forming the final automata. Comparisons with other conversion tools show that this algorithm runs faster with less states and transitions in the automaton.

Keyword: linear temporal logic; transition-based Büchi automata; on-the-fly

显式模型检测方法是常用的形式化验证方法之一。它根据系统建立有限状态模型,通过自动遍历模型的状态空间,检查每个状态是否都满足系流要求的属性,以确定该模型是否满足属性要求。显式模型检测基本方法是根据系统模型建立系统自动机 S, 将系统要满足的属性 φ取反,并构建 ¬φ的等价自动机 K, 最后计算 K与 S的正交积 M, 对 M的可接受语言进行空值检测。如果 M的可接受语言不为空,则说明 S与 φ存在冲突,并可以给出反例。由于 M的状态数量是 K与 S状态数量的乘积,在作正交运算时,状态检测空间会急剧增大,因此显式模型检测没有确定的多项式时间算法,最差时间复杂度为指数阶,需要大量的计算时间与存储空间。而计算机可用资源是有限的,无法满足状态空间无限增大的需求。当系统规模较大时, M无法在内存中完整建立而导致检测中断或因检测时间过长,现实中无法应用。通过减少 S和 K的状态数,进而减少 M的状态数,可有效避免“状态爆炸”情况的发生。

系统属性常用线性时序逻辑(linear temporal logic, LTL)表示,在LTL转换成等价的Büchi自动机(Büchi automata, BA)的问题上,已有大量的研究成果发表。Gerth等[1]提出的GPVW(Gerth- Peled-Vardi-Wolper)算法是基于Tableau规则的按需即时(on-the-fly)转换方法,在检测过程中按需生成自动机,避免了无效时间和空间的消耗,该算法被模型检测工具SPIN[2]采用。Daniele等[3]通过识别公式的蕴含关系避免冗余计算,利用扩展状态等价关系减少状态数量。Giannakopoulou等[4,5]利用基于迁移的扩展Büchi 自动机(transition-based generalized Büchi automata, TGBA)作为中间转换自动机,减少最终生成的BA的状态数量。Duret-Lutz 等[5,6]使用二分决策图(binary decision diagram, BDD)表示公式和覆盖,以实现快速的公式化简。Gastin等[7,8,9]通过先将LTL公式转换为极弱交替自动机(very weak alternating automata, VWAA), 再去交替化(alternation removal)将其转换为扩展的Büchi 自动机(generalized Büchi automata, GBA)。利用VWAA作为中间自动机,能够在线性时间内完成转换,但去交替化过程的最差时间复杂度是 Ο( n2 n)[10], 与基于Tableau规则的算法处于同一数量级。在GBA化简方面, Juvekar等[11]改进了基于自动机理论的化简,如计算公平(互)模拟关系(fair (bi)simulation)或延迟(互)模拟关系(delayed (bi)simulation)。Somenzi 等[12,13]也提出了一些公式化简规则,在公式转换之前先将时序算子数量尽可能减少。殷翀元等[14]提出与DFA填表化简法类似的方法,应用于GBA的化简。Sebastiani等[15]提出使迁移更确定化的方法,该算法被模型检测工具SPOT[5]采用。Ehlers等[16]提出不把LTL公式转换为自动机,而是在所有的自动机中寻找与LTL公式等价的自动机,这样可以保证一定能够得到与LTL公式等价的最小自动机,但需要大量计算时间。该方法常用于公式的预处理,或者用于建立常用LTL公式的自动机库,而不能被直接整合到模型检测算法中。罗贵明等[17]避开转换的中间步骤,通过跟踪转换过程中∪公式的满足信息,即时按需化简公式,并利用BDD描述公式的方法,直接将LTL公式转换为TBA。

本文提出基于Tableau规则的改进算法,递归展开LTL公式,生成基于迁移的Büchi 自动机(transition-based Büchi automata, TBA)。由于传统的Tableau方法仅适用于构造GBA(如GPVW算法), 无法从任意LTL公式直接构造TBA。本文对传统的Tableau方法进行改进,通过在状态和迁移上加入∪公式的满足信息,不再使用多重接受条件集合判断执行序列是否可接受,而是使用一个接受条件(即TBA的接受条件)替代一组接受条件集合的集合 (TGBA接受条件)作为判断条件。这相当于在构造TGBA 的同时执行去扩展化操作,避免了传统方法中TGBA 去扩展化时状态空间指数阶增长。本文算法利用“即时按需(on-the-fly)”的思想,在生成自动机的同时化简自动机,消除冗余状态与迁移,减少生成自动机中的无效状态。与LTL3BA和SPOT的最新版本相比,利用本文提出的算法生成的自动机更小,耗费时间更少。

1 预备知识

LTL是描述系统约束的形式化方法,是模态逻辑的一种,其中的模态算子用于指示时间的顺序,而非精确的时间。每个LTL公式都描述了一组2AP上的 ω字,即原子命题(atomic proposition,AP)集合的无穷序列,用于表达某种可能的将来情况。

定义1 (LTL的语法) LTL公式由有限原子命题集合AP, Boole运算符¬、 ∧、 ∨, 时序操作符Χ(next)、 ∪(until)、 R(release)、 F(eventually)、 G(always)组成。LTL公式语法定义如下:

1) 原子命题 p和命题常量True(⊥)、 False(⊥)是LTL公式;

2) 若 φ和 ψ是LTL公式,则 ¬φ、 φ∧ ψ、 φ∨ ψ、 X φ、 F p、 G p、 φ∪ ψ和 φR ψ也是LTL公式。

若 π=π[0] π[1] π[2] …∈ (2AP)ω是AP的字符序列,则 π[ i]是字符序列 π上的第 i个字符, πi表示字符序列 π上自 π[ i]开始的后续序列。包含R、 F、 G操作符的LTL公式可以通过恒等式(1)—(3)转换成只包含 Χ和∪的LTL公式:

φRψ≡¬(¬φ⋃¬ψ),(1)Fφ≡T⋃φ,(2)Gφ≡⊥Rφ≡¬F¬φ)≡¬(T⋃¬φ).(3)

定义2 (LTL的语义) LTL语义定义如下:

π⊧ p iff p∈ π[0],其中 p∈AP;

π⊧ ¬φ iff π⊧ /φ;

π⊧ φ∧ ψ iff π⊧ φ且 π⊧ ψ;

π⊧ φ∨ ψ iff π⊧ φ或 π⊧ ψ;

π⊧X φ iff π1⊧ φ;

π⊧F φ iff ∃ i≥0, πi⊧ φ;

π⊧G φ iff ∀ i≥0, πi⊧ φ;

π⊧ φ∪ ψ iff ∃ j≥0, πj⊧ ψ, 且∀0≤ i<j, πi⊧ φ.

如果LTL公式中只含有∧、 ∨、 ¬、 Χ、 ∪、 R等操作符,且 ¬操作符只出现在原子命题之前,这种LTL公式称为否定范式(negation normal form, NNF)。

定义3 (Büchi自动机) BA是一种 ω自动机,定义为五元组B =( Q,AP, δ, I, F)。其中: Q为有限状态集合; AP为自动机的有限字母表,即原子命题集合; δ⊆ Q×2AP ×Q是一个迁移函数; I⊆ Q为初始状态集合; F⊆ Q是一组接受状态的集合。

π=π[0] π[1] π[2]…∈ (2AP)ω是B的字符序列,如果存在状态序列 σ=q0 q1 q2…( q0∈ I), 满足 qi+1∈ δ( qi, π[ i]), 则 σ是B的执行路径。若存在一个执行路径 σ=q0 q1 q2… qi …, 如果∀ i≥0,∃ j≥ i, σ满足 qj∈ F, 则 σ是B上的一个可接受执行路径。若 π上至少存在一个 σ是B上的可接受执行路径,则 π是可接受的。

定义4 (TGBA) TGBA是在迁移上标记多个接受条件Büchi自动机,接受条件是一组接受条件集合的集合。TGBA定义为五元组G =( Q,AP, δ, I, F)。其中: Q为有限状态集合;AP为自动机的有限字母表,即原子命题集合; δ⊆ Q× 22AP ×2 F×Q是一个迁移函数,每个迁移包含一组Boole公式和一个接受条件的集合; I⊆ Q初始状态集合; F={ f1, f2,…, fm}是一组接受条件集合的集合。

π=π[0] π[1] π[2]…∈(2AP) ω是G的字符序列, σ=( q0, l0, A0, q1)( q1, l1, A1, q2)…∈ δω是G的执行序列。如果∀ i≥0, 存在 πi∈ li, 则∀ f∈ F, ∃ j≥ i, σ满足 f∈ Aj, 即 σ无限次地满足每一个接受条件,则 σ是G上的一个可接受执行序列。若 π上至少存在一个 σ是G上的可接受执行序列,则 π是可接受的。

定义5 (TBA) TBA的接受条件是一组接受迁移的集合,定义为五元组T =( Q,AP, δ, I, F)。其中: Q为有限状态集合; AP为自动机的有限字母表; δ⊆ Q× 22AP ×Q是一个有限迁移的集合; I⊆ Q为初始状态集合; F是接受条件。 σ=( q0, l( t0), q1)…( qi, l( ti), qi+1)…∈ δω是对应T的执行序列,其中 l( ti)∈2AP是迁移 ti上的标签,且 qi⊧ l( ti)。若存在无穷多的 i使得 ti∈ F, 则 σ称为T上的可接受执行运行。

定义6 (等价状态) 如果Büchi自动机两个状态合并后不改变自动机的可接受语言,则称这两个状态为等价状态。等价状态要满足以下两个条件: 1) 一致性条件,即两个状态必须同时为终态或非终态; 2) 蔓延性条件,即对于所有输入符号,两个状态必须转换到等价的状态中。

定义7 (等价迁移) TBA的迁移定义为四元组transition(src,des,label, P)。其中: src为迁移的源节点, des为迁移的目标节点, label为原子命题集合, P为当前迁移最终要满足的接受条件。

若两个迁移的src、 des和 P相同时,则这两个迁移是等价迁移。

2 基于Tableau规则的改进算法

LTL公式 φ有与之对应的语言 L( φ), L( φ)表示为字符序列 π=π[0] π[1] π[2] …∈ (2AP)ω。由 φ转换生成的BA必然接受 L( φ), 即BA每接受一个字符 π[ i], 就从 L( φ)中排除第 i个字符不是 π[ i]的所有字符序列,可见每个状态代表正在被接受的字符属于 L( φ)。如果将状态与其后继所代表的可能性连接起来(如式(4)所示), 得到一组 ω字的集合,该集合就是LTL公式按照Tableau规则展开得到的Χ原子命题序列。这就是Tableau规则的工作方式,自动机的状态代表LTL公式的Tableau展开。

φ⋃ψ=φ∧Χ(φ⋃ψ)=φ∧Χφ∧ΧΧφ….(4)

如果将状态定义为完全展开LTL公式的X公式,则生成的是一个基于状态的自动机。如果将状态定义为一次展开之后的X公式,而将展开式中的原子命题作为迁移上的标签,则生成的是一个基于迁移的自动机。

2.1 Tableau构造方法

Tableau构造方法是基于LTL公式的图形分解法,能将LTL公式展开成一个树形结构, Tableau构造方法是“压缩”的Kripke结构,基本算法是将LTL公式用表1列举的Tableau规则进行展开。表1中subf代表子公式集合, next代表下一个状态集合。

表1 Tableau规则

在使用Tableau规则展开 φ∪ ψ公式时,可能出现无限循环的情况。由于 φ∪ ψ确保 ψ最终要成立,如果 φ始终成立而 ψ始终不成立,将会使 φ∪ ψ公式陷入一个无限循环,如式(4)所示。为了避免无限循环,需要添加标记 P(promise)。 P代表一种“承诺”,即“目前没有满足 φ∪ ψ,但是承诺之后要通过满足 ψ来保证 φ∪ ψ最终被满足”,如式(5)所示。

φ⋃ψ=ψ∨(φ∧X(φ⋃ψ)∧Pψ).(5)

将带有 P记号的公式加入到迁移的标签中,对于子公式 φ∪ ψ, 所有不包含 Pψ的迁移都将成为 Fφ∪ ψ中的元素。

2.2 LTTB算法实现

本文提出的算法(LTTB算法)将LTL公式转换成符合LTL输入序列要求的TBA,如图1所示。首先,构造自动机模型,将LTL公式存放在自动机的根节点。然后,采用深度优先探索算法(depth first search, DFS), 利用Tableau规则递归展开自动机的节点,生成新的节点和迁移,节点保存着每次展开后的LTL子公式。如果新生成的节点与自动机中已存在的节点是等价节点则抛弃新节点,如果新生成的迁移与已存在的迁移是等价迁移,则合并迁移,否则将节点和迁移添加到自动机中,将迁移的后继节点作为未处理的LTL公式再次进行展开,递归循环直到所有的LTL公式都已经展开。当迁移上所有的接受条件都已经得到满足,则该迁移是可接受的迁移。LTTB算法采用了on-the-fly的思想,即根据需要展开自动机的状态与迁移,避免生成所有状态与迁移。在利用Tableau规则展开LTL公式过程中,会产生冗余或无效的状态与迁移, LTTB算法进行即时化简,展开LTL公式的同时化简生成的TBA, 避免不必要的状态空间,提高算法的执行效率。

图1 LTTB算法

TBA的迁移上要包含必要的信息确保DFS算法展开,数据域定义如下:

new: 未处理的公式集合;

src: 源节点,已经处理过的LTL公式集合;

des: 目标节点,后继要处理的LTL公式集合;

label: 原子命题集合,用来标记迁移;

curr: 当前正在处理的LTL公式集合。

算法定义了TBA类,其属性与函数定义如下:

new(): 生成一个新BA;

initial(): 初始化BA, 根节点保存要展开的LTL公式;

add_trans(): 向BA中添加一个迁移;

state: BA已经存在的状态;

trans: BA已经存在的迁移;

accept_cond: TBA接受条件的集合。

其他变量定义如下:

p: 原子命题;

f: 初始的LTL公式;

all_pro: 记录所有接受条件的变量;

Neg()函数定义: Neg( p)=¬ p或Neg(¬ p) =p;

∅等价于True(⊥)。

图1所示算法4—7行: 递归的展开LTL公式,直到不再有新的LTL公式产生。

算法8—9行: 生成迁移上的接受条件。

算法15—28行: 利用Tableau规则展开LTL公式。

算法17—18行: 在展开得到新的节点时,检测新节点是否与存在的节点有矛盾,如果存在矛盾,则抛弃新节点。图2所示LTL公式展开过程中出现无效节点{ a, ¬a}, 因此抛弃该节点。

图2 无效节点

算法29—30行: 如果生成的后继节点不在BA存在的节点中,则将该节点加入到未处理节点集合。

算法31—36行: 如果新生成迁移与BA已存在迁移等价,则合并迁移,否则在BA中添加新迁移。检测新生成的迁移与已存在的迁移是否是等价迁移,如果等价则合并迁移。

以LTTB展开( a∪ b)∪ c的过程为例说明LTTB算法的执行过程。先展开( a∪ b)∪ c节点,得到两个新的节点{( a∪ b)∪ c, a∪ b}和 •, 以及节点之间的迁移。然后,对两个节点分别进行递归展开,当没有新的节点出现时,算法结束,得到图3所示的TGBA。

图3 (a∪b)∪c展开为TGBA

由图3得到的TBA如图4所示。该TBA共有两个接受条件,分别是{( a∪ b)∪ c}和{ a∪ b}。图4中带白点的迁移表示该迁移已满足接受条件{ a∪ b};图4中带黑点的迁移表示该迁移已满足接受条件 (a⋃b)⋃c}; 既有白点又有黑点的迁移表示已满足TBA两个接受条件,因此是TBA的接受迁移。

图4 (a∪b)∪c展开为TBA

2.3 算法复杂性

LTTB算法中最耗时的操作是状态展开(expand)操作,这与其他的基于Tableau构造方法的算法相似,在状态展开过程中会导致状态膨胀,最差空间复杂度是 Ο( n2 n)( n是公式的长度,即公式中时序算子的个数)。

由于算法中增加了on-the-fly化简过程,在状态展开过程中会删除无效状态、合并等价状态,但不会增加很大的时间消耗。由于状态数量的减少,LTTB算法的最优空间复杂度为 Ο(2 n)。

3 算法正确性证明

本节将对LTTB算法的正确性进行证明。

引理1 若 σ是自动机T的一个执行序列,如果 φ∪ ψ∈ δ( q0)成立,则下面两式成立:

1) ∀ i≥0: φ∈ δ( qi), φ∪ ψ∈ δ( qi), ψ∉ δ( qi);

2) ∃ j≥0,∀ i,0≤ i<j: φ∈ δ( qi), φ∪ ψ∈ δ( qi), ψ∈ δ( qj) .

证明: 由 φ∪ ψ≡ ψ∨( φ∧X( φ∪ ψ))可知, ψ∈ δ( qi)最终要出现。对于执行序列 σ, 如果 φ∪ ψ∈ δ( q0)蕴含两种情况,如果 ψ∈ δ( q0),则 φ∪ ψ∈ δ( q0); 如果 ψ∉ δ( q0), 则必有( φ, φ∪ ψ)∈ δ( qi), 直到 ψ∈ δ( qj)出现。因此,引理1中的两式成立。■

引理2 若 ξ是T上的接受命题序列, σ=q0 q1 q2…( q0∈ I)是 T执行序列,则 ξ⊧∧ δ( q0)。

证明: 若 φ∪ ψ∈ δ( q0), 由引理1可知,满足T的接受条件的 ξ只有两种情况,即∃ j≥0, ξj⊧ ψ,或者0≤ i<j, ξi⊧ φ。 由LTL的语义可知, ξ⊧ φ∪ ψ, 即 ξ⊧∧ δ( q0)。

同理可以证明,原子命题 p和 ¬p以及含有Χ操作符的LTL公式也满足 ξ⊧∧ δ( q0), 而其他时序操作符可转换成由∪和Χ表示的LTL公式,故而 ξ⊧∧ δ( q0)成立。■

引理3 T是依据LTL属性 φ构建的自动机,且T接受命题序列 ξ, 则 ξ⊧ φ。

证明: 假设T是依据LTL属性 φ构建的自动机, q∈ I是初始状态集合,由T的定义可知 φ∈ δ( q)。

ξ是T上的接受命题序列, σ=q0 q1 q2…( q0∈ I)是T执行序列,由引理2可知, ξ⊧∧ δ( q0)。

由 ξ⊧∧ δ( q0)和 φ∈ δ( q)成立可知, ξ⊧ φ成立。■

引理4 状态节点 q分裂成两个节点 q1和 q2时,必有下式成立(参见2 .2节算法第21行至25行)。

∧src(q))∧(∧curr(q))∧(X∧des(q))↔∧src(q1))∧(∧curr(q1))∧(X∧des(q1))∨∧src(q2))∧(∧curr(q2))∧(X∧des(q2)).

状态节点 q更新为 q'时,必有下式成立(参见2 .2节算法第26行至27行)。

∧src(q))∧(∧curr(q))∧(X∧des(q))↔∧src(q'))∧(∧curr(q'))∧(X∧des(q')).

证明: 依据表1列出的Tableau规则,可以得到上式成立。■

引理5 T是依据LTL属性 φ构建的自动机,则必有 φ↔ ∨q∈I((∧ δ( q))∧Χ(∧next( q)))成立。

证明: 假设 p是T的根节点, q1, q2,… qn是 p的后继节点。令 Θ表示按照Tableau规则生成的新节点的集合。由Tableau规则可知式(6)成立,

∧Θ↔∨1≤i≤n((∧δ(qi))∧Χ(∧next(qi))).(6)

T是依据LTL属性 φ构建的自动机, Θ是T的初始值,可知式(7)成立。

Θ∈φ.(7)

由式(6)和(7)可知, φ↔ ∨q∈I((∧ δ( q))∧Χ(∧next( q)))成立。■

引理6 T是接受命题序列 ξ的自动机,如果存在 ξ⊧ φ, 则T必定存在一个执行序列 σ接受 ξ。

证明: 假设 q∈ I是T的初始节点,由引理5可知, ξ⊧∧ δ( q)∧Χ(∧next( q))。若T存在 q→ q'的迁移,则 ξ⊧∧ δ( q')∧Χ(∧next( q'))成立。由此可知,若 ξi⊧∧ δ( qi)∧Χ(∧next( qi)), qi+1是 qi的后继节点,则 ξi+1⊧∧ δ( qi+1)∧Χ(∧next( qi+1))。

由题意知, ξ⊧ φ, 因此T必定存在一个执行序列 σ接受 ξ。■

引理7 依据LTL属性 φ构建的自动机T接受满足属性 φ的所有序列 (2AP)ω。

证明: 由引理3和引理6可知LTTB算法是正确的成立。■

引理8 T存在迁移 t=( s, l( ci), d), 如果∀ si, sj, di, dj∈ Q, l( ci)≠ l( cj), 即不存在相同Label的迁移,则该自动机不存在等价迁移。

证明: 假设 ti=( si, l( ci), di)与 tj=( sj, l( cj), dj)为等价迁移,则经过 si的执行序列 ρi与经过 sj的执行序列为 ρj等价,可知 l( ci) =l( cj), 这与原命题 l( si)≠ l( sj)矛盾,故而假设不成立, ti, tj不是等价迁移。■

引理9 T存在迁移 t=( s, l( ci), d), 如果∀ si, sj∈ S, l( si) =l( sj)且dest( si) =dest( sj), 则 ti, tj是等价迁移。

证明: 假设 ti, tj不是等价迁移,且经过 si的可接受执行序列为 α1 si α2, 经过 sj的可接受执行序列为 β1 sj β2。由假设可知: ( α1 si α2)≠( α1 sj α2)且( β1 si β2)≠( β1 sj β2)成立,可知 l( si)≠ l( sj)或者dest( si)≠dest( sj), 这与原命题矛盾,故而假设不成立, ti, tj是等价迁移。■

4 实验结果

本节将LTTB与LTL3BA (v1.0.2)和SPOT(v1.0.2)进行实验对比。LTL3BA和SPOT是目前技术领先的两种LTL公式转换BA的工具。LTL3BA[8]是通过中间自动机实现LTL公式到BA的转换,即LTL先转换成VWAA, 再转换成TGBA, 最后去扩展化生成BA, LTL3BA性能优于LTL2BA[7]。SPOT[5]基于Tableau规则展开LTL公式,利用BDD表示公式和覆盖,实现公式化简,性能优于Wring[12]、 GPVW[1]和LTL2AUT[3]等工具。

针对LTL公式的保证属性、安全属性、责任属性、持续属性和重复属性5个层次,分别取出一类公式进行对比测试,对比生成TBA的状态数与迁移数和执行时间。实验平台配置如下: Intel Core i5-3470 CPU @3.2 GHz, 4 GB内存,操作系统为Ubuntu 12.04 LTS。

保证属性指其否定范式中只能包含Χ、 ∪和F等时序操作符的LTL公式,如: φGn =F( p1∧F( p2∧…F pn))∧F( q1∧F( q2∧…F qn))。

安全属性指其否定范式中只能包含Χ、 R和G的LTL公式,如 φSn =(…( p1R p2)…)R pn-1)R pn)。

责任属性指保证属性与安全属性的Boole组合,如 φOn =( p1∪( p2∪… pn)…)∧( q1R( q2R… qn)…)。

持续属性指∪ -R的单次嵌套,如 φPn =FG p1∨…∨FG pn。

重复属性指R -∪的单次嵌套,如 φCn =GF p1∧…∧GF pn。

对 φGn、 φSn、 φOn、 φPn和 φCn5种属性取 n=5,6,7,8,9进行实验。实验结果(如表2所示)记录了在30 s内3种工具分别将LTL公式转换成BA得到的状态数和迁移数。

表2 LTL3BA、SPOT与LTTB比较实验结果

从状态数和迁移数进行比较, LTTB生成自动机的状态数和迁移数不多于LTL3BA和SPOT这两个工具生成的结果。其中, LTTB生成重复属性 φCn自动机的状态数和迁移数略少于LTL3BA和SPOT得到的结果。

从生成自动机使用的转换时间进行比较, LTTB使用时间明显少于LTL3BA和SPOT。LTTB内嵌计时模块,可记录转换时间。但是, LTL3BA和SPOT没有在工具中内嵌计时功能,无法进行精确时间比较。实验以30 s为转换时间限制,超过30 s认为转换过程失败。从实验结果可见,在转换保证属性 φGn和责任属性 φOn时,若 n≥9, LTL3BA和SPOT均不能在30 s以内计算出结果,而LTTB使用时间明显少于其他两个工具,而且 n值越大时LTTB优势越明显。

5 结论与下一步工作

本文提出了基于Tableau规则的改进算法LTTB, 将LTL公式转换成TBA。通过跟踪转换过程中∪公式最终要满足的接受条件,在状态和迁移上加入∪公式的满足信息,将原本由TGBA接受条件区分执行序列是否可接受的功能,转换成使用TBA接受条件判断执行序列是否可接受,不再需要多重接受条件集合作为判断条件。采用on-the-fly方法删除生成过程中产生的冗余状态节点和等价迁移,减少了生成BA的状态数和迁移数。通过与LTL3BA和SPOT的比较可以看出,本文提出的方法生成的TBA的状态数和迁移数较少,执行速度更快。

LTTB算法在执行LTL公式展开操作时还存在重复计算的问题,需要进一步优化递归算法。同时,生成的TBA还需要进一步转换成BA, 以便与其他模型检测工具(如SPIN)配合使用,因此本文提出的方法还可以作进一步改进。

The authors have declared that no competing interests exist.

参考文献
[1] Gerth R, Peled D, Vardi M Y, et al. Simple on-the-fly automatic verification of linear temporal logic [C]//Proceedings of the 15th IFIP WG6. 1 International Symposium on Protocol Specification, Testing and Verification. Seneca, USA: IFIP, 1995. [本文引用:2]
[2] Holzmann G J. The model checker SPIN[J]. IEEE Transactions on Software Engineering, 1997, 23(5): 279-295. [本文引用:1] [JCR: 2.292]
[3] Daniele M, Giunchiglia F, Vardi M Y. Improved automata generation for linear temporal logic [C]//Computer Aided Verification. Berlin, Heidelberg, Germany: Springer1999: 249-260. [本文引用:2]
[4] Giannakopoulou D, Lerda F. From states to transitions: Improving translation of LTL formulae to Büchi automata [C]//Formal Techniques for Networked and Distributed Sytems, FORTE 2002. Berlin, Heidelberg, Germany: Springer, 2002: 308-326. [本文引用:1]
[5] Duret-Lutz A. LTL translation improvements in spot [C]//Proceedings of the 5th International Conference on Verification and Evaluation of Computer and Communication Systems. Swinton, UK: British Computer Society, 2011: 72-83. [本文引用:4]
[6] Shoshmina I V, Belyaev A B. Symbolic algorithm for generation Büchi automata from LTL formulas [C]//Parallel Computing Technologies. Berlin, Heidelberg, Germany: Springer, 2011: 98-109. [本文引用:1]
[7] Gastin P, Oddoux D. Fast LTL to Büchi automata translation [C]//Computer Aided Verification. Berlin, Heidelberg, Germany: Springer, 2001: 53-65. [本文引用:2]
[8] Babiak T, Kretínsky M, Rehák V, et al. LTL to Büchi automata translation: Fast and more deterministic [C]//Tools and Algorithms for the Construction and Analysis of Systems. Berlin, Heidelberg, Germany: Springer, 2012: 95-109. [本文引用:1]
[9] Fritz C. Concepts of automata construction from LTL [C]//Logic for Programming, Artificial Intelligence, and Reasoning. Berlin, Heidelberg, Germany: Springer, 2005: 728-742. [本文引用:1]
[10] Boker U, Kupferman O, Rosenberg A. Alternation removal in Büchi automata [C]//Automata, Languages and Programming. Berlin, Heidelberg, Germany: Springer, 2010: 76-87. [本文引用:1]
[11] Juvekar S, Piterman N. Minimizing generalized Büchi automata [C]//Computer Aided Verification. Berlin, Heidelberg, Germany: Springer, 2006: 45-58. [本文引用:1]
[12] Somenzi F, Bloem R. Efficient Büchi automata from LTL formulae [C]//Computer Aided Verification. Berlin, Heidelberg, Germany: Springer, 2000: 248-263. [本文引用:2]
[13] Etessami K, Holzmann G J. Optimizing Büchi automata [C]//CONCUR 2000: Concurrency Theory. Berlin, Heidelberg, Germany: Springer, 2000: 153-168. [本文引用:1]
[14] Yin C, Luo G. Efficient translation of LTL to Büchi automata[J]. Tsinghua Science & Technology, 2009, 14(1): 75-82. [本文引用:1] [CJCR: 0.609]
[15] Sebastiani R, Tonetta S. “More deterministic” vs. “smaller” Büchi automata for efficient LTL model checking [C]//Correct Hardware Design and Verification Methods. Berlin, Heidelberg, Germany: Springer, 2003: 126-140. [本文引用:1]
[16] Ehlers R, Finkbeiner B. On the virtue of patience: Minimizing Büchi automata [C]//Model Checking Software. Berlin, Heidelberg, Germany: Springer, 2010: 129-145. [本文引用:1]
[17] Lu X, Luo G. Direct translation of LTL formulas to Büchi automata [C]//2012 IEEE 11th International Conference on Cognitive Informatics & Cognitive Computing (ICCI*CC). Bratislava, Slovak: IEEE Press, 2012: 323-328. [本文引用:1]