线性时序逻辑转换Büchi自动机的按需即时算法  

On-the-fly translation algorithm from linear temporal logic to Büchi automata

作　　者：单来祥[1] 覃征[1,2] 卢欣晔 卢正才[1] 

机构地区：[1]清华大学计算机科学与技术系,清华信息科学与技术国家实验室,北京100084 [2]清华大学软件学院,北京100084 [3]中国科学院软件研究所,北京100190

出　　处：《清华大学学报（自然科学版）》2014年第2期281-288,共8页Journal of Tsinghua University(Science and Technology)

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

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

关 键 词：线性时序逻辑 基于迁移的Büchi自动机 按需即时 

分 类 号：TP301.1[自动化与计算机技术—计算机系统结构]