基于LTL Tableau的自动机构造  

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

作　　者：刘万伟[1] 王戟[1] 陈火旺[1] 

机构地区：[1]国防科技大学计算机学院,长沙410073

出　　处：《吉林大学学报（工学版）》2007年第1期132-135,共4页Journal of Jilin University:Engineering and Technology Edition

基　　金：'973'国家重点基础研究计划项目(2005CB321802);国家自然科学基金重点资助项目(60233020);'863'国家高技术研究发展计划项目(005AA113130);教育部新世纪优秀人才支持计划项目(NCET-04-0996)

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

关 键 词：计算机软件 模型检验 LTL TABLEAU Co—Büchi自动机 

分 类 号：TP301[自动化与计算机技术—计算机系统结构]