| 基于LTL Tableau的自动机构造 |
| |
| 引用本文： | 刘万伟,王戟,陈火旺.基于LTL Tableau的自动机构造[J].吉林大学学报(工学版),2007,37(1):132-135. |
| |
| 作者姓名： | 刘万伟 王戟 陈火旺 |
| |
| 作者单位： | 国防科技大学,计算机学院,长沙,410073 |
| |
| 基金项目： | 国家重点基础研究发展计划(973计划)
,
国家自然科学基金
,
国家高技术研究发展计划(863计划)
,
教育部跨世纪优秀人才培养计划 |
| |
| 摘 要： | 基于线性时序逻辑(LTL)的模型检验是使用较为广泛的技术。该种模型检验最终归结为有穷自动机的判空问题,其复杂性来源于性质和模型乘积自动机的状态空间膨胀。作者提出了一种构造迟滞交换Co-Büchi自动机(Stuffer Alternating Co-Büchi)的具有线性复杂度的方法,该方法能够降低最终乘积自动机的空间复杂度。
|
| 关 键 词： | 计算机软件 模型检验 LTLTableau Co-Büchi自动机 |
| 文章编号： | 1671-5497(2007)01-0132-04 |
| 收稿时间： | 2006-06-26 |
| 修稿时间： | 2006年6月26日 |
Automata construction based on linear-time temporal logic(LTL) Tableau |
| |
| Liu Wan-wei,Wang Ji,Chen Huo-wang.Automata construction based on linear-time temporal logic(LTL) Tableau[J].Journal of Jilin University:Eng and Technol Ed,2007,37(1):132-135. |
| |
| Authors: | Liu Wan-wei Wang Ji Chen Huo-wang |
| |
| Abstract: | In software model checking technology,the selection of stipulating language significantly affects the complexity of verification.Linear-time temporal logic(LTL) is widely used in such technology.This model checking method comes down to the space estimation of finite automata.Its complexity is originated from the state space expansion of the automaton which is the production of the property and the model.This paper presents an approach in constructing Stuffer Alternating Co-Büchi automata based on Tableau theory.The complexity of this approach is linear and it may reduce the size of state space of the production automaton used in model checking. |
| |
| Keywords: | computer software model checking LTL Tableau Co-Büchi automata |
| 本文献已被 CNKI 万方数据 等数据库收录！ |
| 点击此处可从《吉林大学学报(工学版)》浏览原始摘要信息 |
|
点击此处可从《吉林大学学报(工学版)》下载全文 |
