线性时序逻辑转换Buchi自动机的按需即时算法
文献类型：期刊论文
| 作者 | 单来祥 ; 覃征 ; 卢欣晔 ; 卢正才 |
| 刊名 | 清华大学学报. 自然科学版
 |
| 出版日期 | 2014 |
| 卷号 | 54期号:2页码:281-288 |
| 关键词 | 线性时序逻辑 基于迁移的Buchi自动机 按需即时 |
| ISSN号 | 10000054 |
| 其他题名 | On-the-fly translation algorithm from linear temporal logic to Büchi automata |
| 通讯作者 | Qin, Z.(qingzh@mail.tsinghua.edu.cn) |
| 中文摘要 | 将线性时序逻辑公式转换成Buchi自动机是显式模型检测中的关键环节,Tableau规则是常用转换算法。该文提出了基于Tableau规则的改进算法 ,将线性时序逻辑公式转换成基于迁移的Buchi自动机。通过在状态和迁移中加入公式的满足信息,实现了用一个接受条件集合判断执行序列是否可接受,避免 了使用多个接受条件集合进行判断。改进算法引入了按需即时(on-the-fly)去扩展化机制,算法展开状态节点的同时进行状态有效性检测,删除无效节 点,合并等价状态和迁移,避免了后置化简。与其他转换工具进行比较实验表明,该算法具有执行速度快、生成自动机的状态数和迁移数少的特征。 |
| 英文摘要 | Translations of linear temporal logic to Bu¨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 Bu¨chi automata. The satisfaction information of the ∪-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. |
| 收录类别 | EI ; CSCD |
| 语种 | 中文 |
| CSCD记录号 | CSCD:5158215 |
| 公开日期 | 2014-12-16 |
| 源URL | [http://ir.iscas.ac.cn/handle/311060/16736]  |
| 专题 | 软件研究所_软件所图书馆_期刊论文 |
| 推荐引用方式 GB/T 7714 | 单来祥,覃征,卢欣晔,等. 线性时序逻辑转换Buchi自动机的按需即时算法[J]. 清华大学学报. 自然科学版,2014,54(2):281-288. |
| APA | 单来祥,覃征,卢欣晔,&卢正才.(2014).线性时序逻辑转换Buchi自动机的按需即时算法.清华大学学报. 自然科学版,54(2),281-288. |
| MLA | 单来祥,et al."线性时序逻辑转换Buchi自动机的按需即时算法".清华大学学报. 自然科学版 54.2(2014):281-288. |
入库方式： OAI收割
来源：软件研究所
浏览0
下载0
收藏0
其他版本
除非特别说明，本系统中所有内容都受版权保护，并保留所有权利。