Institutional Repository
| 线性时序逻辑转换Buchi自动机的按需即时算法 | |
| Alternative Title | On-the-fly translation algorithm from linear temporal logic to Büchi automata |
| 单来祥; 覃征; 卢欣晔; 卢正才; Qin, Z.(qingzh@mail.tsinghua.edu.cn) | |
| 2014 | |
| Source | 清华大学学报. 自然科学版
 |
| ISSN | 10000054 |
| Volume | 54Issue:2Pages:281-288 |
| English Abstract | 将线性时序逻辑公式转换成Buchi自动机是显式模型检测中的关键环节,Tableau规则是常用转换算法。该文提出了基于Tableau规则的改进算法 ,将线性时序逻辑公式转换成基于迁移的Buchi自动机。通过在状态和迁移中加入公式的满足信息,实现了用一个接受条件集合判断执行序列是否可接受,避免 了使用多个接受条件集合进行判断。改进算法引入了按需即时(on-the-fly)去扩展化机制,算法展开状态节点的同时进行状态有效性检测,删除无效节 点,合并等价状态和迁移,避免了后置化简。与其他转换工具进行比较实验表明,该算法具有执行速度快、生成自动机的状态数和迁移数少的特征。 |
| Indexed Type | EI ; CSCD |
| Abstract | 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. |
| Keyword | 线性时序逻辑 基于迁移的buchi自动机 按需即时 |
| Department | 单来祥, 清华大学计算机科学与技术系, 清华信息科学与技术国家实验室, 北京 100084, 中国. 覃征, 清华大学计算机科学与技术系, 清华信息科学与技术国家实验室, 北京 100084, 中国. 卢正才, 清华大学计算机科学与技术系, 清华信息科学与技术国家实验室, 北京 100084, 中国. 卢欣晔, 中国科学院软件研究所, 北京 100190, 中国. |
| Language | 中文 |
| CSCD ID | CSCD:5158215 |
| Content Type | 期刊论文 |
| URI | http://ir.iscas.ac.cn/handle/311060/16736 |
| Collection | 中国科学院软件研究所 |
| Corresponding Author | Qin, Z.(qingzh@mail.tsinghua.edu.cn) |
| Recommended Citation GB/T 7714 | 单来祥,覃征,卢欣晔,等. 线性时序逻辑转换Buchi自动机的按需即时算法[J]. 清华大学学报. 自然科学版,2014,54(2):281-288. |
| APA | 单来祥,覃征,卢欣晔,卢正才,&Qin, Z..(2014).线性时序逻辑转换Buchi自动机的按需即时算法.清华大学学报. 自然科学版,54(2),281-288. |
| MLA | 单来祥,et al."线性时序逻辑转换Buchi自动机的按需即时算法".清华大学学报. 自然科学版 54.2(2014):281-288. |
| Files in This Item: | There are no files associated with this item. | |||||
Items in the repository are protected by copyright, with all rights reserved, unless otherwise indicated.
Edit Comment