一种基于自动机理论的LTL检验符号优化方法

摘要：

模型检验是一种重要的形式化自动验证技术.检验一个模型是否满足LTL公式,可以把LTL公式转换为一个表示相同无穷状态序列的ω自动机,通过转换后的ω自动机与系统自动机的乘积判空来进行模型检验.由于自动机的体积是模型检验的一个关键性问题,为了得到尽可能小的自动机,在LTL公式转换为ω自动机之前,对LTL公式进行预处理来减少冗余,然后基于ROBDD,通过布尔技术优化自动机.

关键词：线性时态逻辑、ω自动机、Büchi自动机、ROBDD

所属期刊栏目：31

分类号：TP301.1(计算技术、计算机技术)

资助基金：国家国防预研基金;广西新世纪十百千人才工程基金0141046

在线出版日期：2006-01-12（万方平台首次上网日期，不代表论文的发表时间）

页数：共3页

页码：20-21,27