%A 单来祥, 覃征, 卢欣晔, 卢正才 %T 线性时序逻辑转换Büchi自动机的按需即时算法 %0 Journal Article %D 2014 %J 清华大学学报(自然科学版) %R %P 281-288 %V 54 %N 2 %U {http://jst.tsinghuajournals.com/CN/abstract/article_148276.shtml} %8 2014-04-20 %X

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