基于LTL Tableau的自动机构造

吉林大学学报(工学版)

基于LTL Tableau的自动机构造

刘万伟，王戟，陈火旺

国防科技大学计算机学院，长沙 410073

收稿日期:2006-06-26 修回日期:2006-10-23 出版日期:2007-01-01 发布日期:2007-01-01
通讯作者: 王戟

Automata construction based on lineartime temporal logic(LTL) Tableau

Liu Wan-wei，Wang Ji，Chen Huo-wang

School of Computer,National University of Defense Technology, Changsha,410073，China

Received:2006-06-26 Revised:2006-10-23 Online:2007-01-01 Published:2007-01-01
Contact: Wang Ji

摘要/Abstract

摘要： 基于线性时序逻辑（LTL）的模型检验是使用较为广泛的技术。该种模型检验最终归结为有穷自动机的判空问题，其复杂性来源于性质和模型乘积自动机的状态空间膨胀。作者提出了一种构造迟滞交换Co-Büchi自动机（Stuffer Alternating CoBüchi）的具有线性复杂度的方法，该方法
能够降低最终乘积自动机的空间复杂度。

关键词: 计算机软件, 模型检验, LTLTableau, Co-Büchi自动机

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.

Key words: computer software, model checking, LTL Tableau, Co-Büchi automata

中图分类号:

TP301

刘万伟，王戟，陈火旺 . 基于LTL Tableau的自动机构造[J]. 吉林大学学报(工学版), 2007, 37(01): 132-135.

Liu Wan-wei，Wang Ji，Chen Huo-wang . Automata construction based on lineartime temporal logic(LTL) Tableau[J]. 吉林大学学报(工学版), 2007, 37(01): 132-135.

参考文献

相关文章 15

[1]	马健, 樊建平, 刘峰, 李红辉. 面向对象软件系统演化模型[J]. 吉林大学学报(工学版), 2018, 48(2): 545-550.
[2]	罗养霞, 郭晔. 基于数据依赖特征的软件识别[J]. 吉林大学学报(工学版), 2017, 47(6): 1894-1902.
[3]	应欢, 王东辉, 武成岗, 王喆, 唐博文, 李建军. 适用于商用系统环境的低开销确定性重放技术[J]. 吉林大学学报(工学版), 2017, 47(1): 208-217.
[4]	李勇, 黄志球, 王勇, 房丙午. 基于多源数据的跨项目软件缺陷预测[J]. 吉林大学学报(工学版), 2016, 46(6): 2034-2041.
[5]	王念滨, 祝官文, 周连科, 王红卫. 支持高效路径查询的数据空间索引方法[J]. 吉林大学学报(工学版), 2016, 46(3): 911-916.
[6]	特日跟, 江晟, 李雄飞, 李军. 基于整数数据的文档压缩编码方案[J]. 吉林大学学报(工学版), 2016, 46(1): 228-234.
[7]	康辉, 王家琦, 梅芳. 基于Pi演算的并行编程语言[J]. 吉林大学学报(工学版), 2016, 46(1): 235-241.
[8]	陈鹏飞, 田地, 杨光. 基于MVC架构的LIBS软件设计与实现[J]. 吉林大学学报(工学版), 2016, 46(1): 242-245.
[9]	刘磊, 王燕燕, 申春, 李玉祥, 刘雷. Bellman-Ford算法性能可移植的GPU并行优化[J]. 吉林大学学报(工学版), 2015, 45(5): 1559-1564.
[10]	冯晓宁, 王卓, 张旭. 基于L-π演算的WSN路由协议形式化方法[J]. 吉林大学学报(工学版), 2015, 45(5): 1565-1571.
[11]	李明哲, 王劲林, 陈晓, 陈君. 基于网络处理器的流媒体应用架构模型(VPL)[J]. 吉林大学学报(工学版), 2015, 45(5): 1572-1580.
[12]	王克朝, 王甜甜, 苏小红, 马培军. 基于频繁闭合序列模式挖掘的学生程序雷同检测[J]. 吉林大学学报(工学版), 2015, 45(4): 1260-1265.
[13]	黄宏涛，王静，叶海智，黄少滨. 基于惰性切片的线性时态逻辑性质验证[J]. 吉林大学学报(工学版), 2015, 45(1): 245-251.
[14]	范大娟^{1, 2}, 黄志球¹, 肖芳雄¹, 祝义¹, 王进¹. 面向多服务交互的相容性分析与适配器生成[J]. 吉林大学学报(工学版), 2014, 44(4): 1094-1103.
[15]	贺秦禄¹, 李战怀¹, 王乐晓¹, 王瑞². 云存储系统聚合带宽测试技术[J]. 吉林大学学报(工学版), 2014, 44(4): 1104-1111.

Metrics

Viewed

Full text

Abstract

Cited

Shared

Discussed