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

作者：单来祥; 覃征; 卢欣晔; 卢正才

来源：清华大学学报, 2014, 54(02): 281-288.

DOI：10.16511/j.cnki.qhdxxb.2014.02.025

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

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

• 单位
  清华大学; 中国科学院软件研究所; 清华信息科学与技术国家实验室