吉林大学学报(工学版)

• • Previous Articles     Next Articles

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

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

  1. 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

PDF (PC)

506

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

CLC Number: 

  • TP301
[1] MA Jian, FAN Jian-ping, LIU Feng, LI Hong-hui. The evolution model of objective-oriented software system [J]. 吉林大学学报(工学版), 2018, 48(2): 545-550.
[2] LUO Yang-xia, GUO Ye. Software recognition based on features of data dependency [J]. 吉林大学学报(工学版), 2017, 47(6): 1894-1902.
[3] YING Huan, WANG Dong-hui, WU Cheng-gang, WANG Zhe, TANG Bo-wen, LI Jian-jun. Efficient deterministic replay technique on commodity system environment [J]. 吉林大学学报(工学版), 2017, 47(1): 208-217.
[4] LI Yong, HUANG Zhi-qiu, WANG Yong, FANG Bing-wu. New approach of cross-project defect prediction based on multi-source data [J]. 吉林大学学报(工学版), 2016, 46(6): 2034-2041.
[5] WANG Nian-bin, ZHU Guan-wen, ZHOU Lian-ke, WANG Hong-wei. Novel dataspace index for efficient processing of path query [J]. 吉林大学学报(工学版), 2016, 46(3): 911-916.
[6] TE Ri-gen, JIANG Sheng, LI Xiong-fei, LI Jun. Document compression scheme based on integer data [J]. 吉林大学学报(工学版), 2016, 46(1): 228-234.
[7] CHEN Peng-fei, TIAN Di, YANG Guang. Design and implementation of LIBS software based on MVC architecture [J]. 吉林大学学报(工学版), 2016, 46(1): 242-245.
[8] LIU Lei, WANG Yan-yan, SHEN Chun, LI Yu-xiang, LIU Lei. Performance portable GPU parallel optimization technique on Bellman-Ford algorithm [J]. 吉林大学学报(工学版), 2015, 45(5): 1559-1564.
[9] FENG Xiao-ning, WANG Zhuo, ZHANG Xu. Formal method for routing protocol of WSN based on L-π calculus [J]. 吉林大学学报(工学版), 2015, 45(5): 1565-1571.
[10] LI Ming-zhe, WANG Jin-lin, CHEN Xiao, CHEN Jun. Architecture model of streaming media applications on network processors(VPL) [J]. 吉林大学学报(工学版), 2015, 45(5): 1572-1580.
[11] WANG Ke-chao, WANG Tian-tian, SU Xiao-hong, MA Pei-jun. Plagiarism detection in student programs based on frequent closed sequence mining [J]. 吉林大学学报(工学版), 2015, 45(4): 1260-1265.
[12] HUANG Hong-tao,WANG Jing,YE Hai-zhi,HUANG Shao-bin. Lazy slicing based method for verifying linear temporal logic property [J]. 吉林大学学报(工学版), 2015, 45(1): 245-251.
[13] FAN Da-juan, HUANG Zhi-qiu, XIAO Fang-xiong, ZHU Yi, WANG Jin. Compatibility analysis and adaptor generation for multi-service interaction [J]. 吉林大学学报(工学版), 2014, 44(4): 1094-1103.
[14] HE Qin-lu, LI Zhan-huai, WANG Le-xiao, WANG Rui. Testing technology for aggregate bandwidth of cloud storage system [J]. 吉林大学学报(工学版), 2014, 44(4): 1104-1111.
[15] LIU Guo-qi, LIU Hui, GAO Yu, LIU Ying, ZHU Zhi-liang. Resource dynamic pricing strategy based on utility in cloud computing [J]. 吉林大学学报(工学版), 2013, 43(06): 1631-1637.
Viewed
Full text


Abstract

Cited
  Shared   
  Discussed   
No Suggested Reading articles found!
Copyright © Journal of Jilin University(Engineering and Technology Edition), All Rights Reserved.
Tel: +86-431-85095297　Fax: +86-431-85094074　E-mail: xbgxb@jlu.edu.cn
Powered by Beijing Magtech Co. Ltd