线性时序逻辑转换Büchi自动机的按需即时算法 |
| |
引用本文: | 单来祥,覃征,卢欣晔,卢正才.线性时序逻辑转换Büchi自动机的按需即时算法[J].印染,2014(2):281-288. |
| |
作者姓名: | 单来祥 覃征 卢欣晔 卢正才 |
| |
作者单位: | 清华大学计算机科学与技术系,清华信息科学与技术国家实验室;清华大学软件学院;中国科学院软件研究所 |
| |
基金项目: | 国防“十二五”预研基金重点项目(9140A1550212JW01047);高等学校博士学科点专项科研基金优先发展领域课题(20120002130007) |
| |
摘 要: | 将线性时序逻辑公式转换成Büchi自动机是显式模型检测中的关键环节,Tableau规则是常用转换算法。该文提出了基于Tableau规则的改进算法,将线性时序逻辑公式转换成基于迁移的Büchi自动机。通过在状态和迁移中加入∪公式的满足信息,实现了用一个接受条件集合判断执行序列是否可接受,避免了使用多个接受条件集合进行判断。改进算法引入了按需即时(on-the-fly)去扩展化机制,算法展开状态节点的同时进行状态有效性检测,删除无效节点,合并等价状态和迁移,避免了后置化简。与其他转换工具进行比较实验表明,该算法具有执行速度快、生成自动机的状态数和迁移数少的特征。
|
关 键 词: | 线性时序逻辑 基于迁移的Büchi自动机 按需即时 |
本文献已被 CNKI 等数据库收录! |
|