中国科学院软件研究所机构知识库
Advanced  
ISCAS OpenIR  > 软件所图书馆  > 期刊论文
Title:
线性时序逻辑转换Buchi自动机的按需即时算法
Alternative Title: On-the-fly translation algorithm from linear temporal logic to Büchi automata
Author: 单来祥 ; 覃征 ; 卢欣晔 ; 卢正才
Corresponding Author: Qin, Z.(qingzh@mail.tsinghua.edu.cn)
Keyword: 线性时序逻辑 ; 基于迁移的Buchi自动机 ; 按需即时
Source: 清华大学学报. 自然科学版
Issued Date: 2014
Volume: 54, Issue:2, Pages:281-288
Indexed Type: EI ; CSCD
Department: 单来祥, 清华大学计算机科学与技术系, 清华信息科学与技术国家实验室, 北京 100084, 中国. 覃征, 清华大学计算机科学与技术系, 清华信息科学与技术国家实验室, 北京 100084, 中国. 卢正才, 清华大学计算机科学与技术系, 清华信息科学与技术国家实验室, 北京 100084, 中国. 卢欣晔, 中国科学院软件研究所, 北京 100190, 中国.
Abstract: 将线性时序逻辑公式转换成Buchi自动机是显式模型检测中的关键环节,Tableau规则是常用转换算法。该文提出了基于Tableau规则的改进算法 ,将线性时序逻辑公式转换成基于迁移的Buchi自动机。通过在状态和迁移中加入公式的满足信息,实现了用一个接受条件集合判断执行序列是否可接受,避免 了使用多个接受条件集合进行判断。改进算法引入了按需即时(on-the-fly)去扩展化机制,算法展开状态节点的同时进行状态有效性检测,删除无效节 点,合并等价状态和迁移,避免了后置化简。与其他转换工具进行比较实验表明,该算法具有执行速度快、生成自动机的状态数和迁移数少的特征。
English 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.
Language: 中文
Citation statistics:
Content Type: 期刊论文
URI: http://ir.iscas.ac.cn/handle/311060/16736
Appears in Collections:软件所图书馆_期刊论文

Files in This Item:

There are no files associated with this item.


Recommended Citation:
单来祥,覃征,卢欣晔,等. 线性时序逻辑转换Buchi自动机的按需即时算法[J]. 清华大学学报. 自然科学版,2014-01-01,54(2):281-288.
Service
Recommend this item
Sava as my favorate item
Show this item's statistics
Export Endnote File
Google Scholar
Similar articles in Google Scholar
[单来祥]'s Articles
[覃征]'s Articles
[卢欣晔]'s Articles
CSDL cross search
Similar articles in CSDL Cross Search
[单来祥]‘s Articles
[覃征]‘s Articles
[卢欣晔]‘s Articles
Related Copyright Policies
Null
Social Bookmarking
Add to CiteULike Add to Connotea Add to Del.icio.us Add to Digg Add to Reddit
所有评论 (0)
暂无评论
 
评注功能仅针对注册用户开放,请您登录
您对该条目有什么异议,请填写以下表单,管理员会尽快联系您。
内 容:
Email:  *
单位:
验证码:   刷新
您在IR的使用过程中有什么好的想法或者建议可以反馈给我们。
标 题:
 *
内 容:
Email:  *
验证码:   刷新

Items in IR are protected by copyright, with all rights reserved, unless otherwise indicated.

 

 

Valid XHTML 1.0!
Copyright © 2007-2019  中国科学院软件研究所 - Feedback
Powered by CSpace