基于LTL TableaU的自动机构造

刘万伟; 王戟; 陈火旺

首页> 中文期刊> 《吉林大学学报（工学版）》 >基于LTL TableaU的自动机构造

基于LTL TableaU的自动机构造

开具论文收录证明 >>

期刊封面封底目录下载 >>

文献代查 >>

页面导航

摘要
著录项
相似文献
相关主题

摘要

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

著录项

来源
《吉林大学学报（工学版）》 |2007年第1期|132-135|共4页
作者
刘万伟; 王戟; 陈火旺;
展开▼
作者单位

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

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

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

展开▼
原文格式 PDF
正文语种 chi
中图分类理论、方法;
关键词
计算机软件; 模型检验; LTL Tableau; Co-Büchi自动机;

相似文献

中文文献
外文文献
专利

1. 时态描述逻辑ALC-LTL的Tableau判定算法 [J] . 常亮 ,王娟 ,古天龙 . 计算机科学 . 2011,第008期
2. 一种基于Büchi自动机的LTL程序模型检测方法 [J] . 罗清胜 . 计算机与现代化 . 2010,第008期
3. 一种基于离散时间自动机的LTL性质检测工具 [J] . 张文亮 ,彭云全 . 计算机仿真 . 2008,第004期
4. 一种基于自动机理论的LTL检验符号优化方法 [J] . 钱俊彦 ,赵岭忠 ,古天龙 . 计算机工程 . 2005,第023期
5. 时间自动机的LTL性质模型检测研究 [J] . 彭云全 ,魏绪凯 ,李广元 . 计算机仿真 . 2009,第005期
6. 面向参数化LTL的预测监控器构造方法 [C] . 赵常智 ,董威 ,隋平 . 中国计算机学会全国软件与应用学术会议（NASAC2009） . 2009
7. LTLNFBA:LTL公式到Büchi自动机的转换 [A] . 宋俊 . 2014

基于LTL TableaU的自动机构造

摘要

著录项

相似文献

相关主题

期刊订阅