基于吴方法的符号模型检验

摘要：

模型检验技术广泛应用于验证并发系统的性质.它的瓶颈一直是内存爆炸问题,将BDD技术引入到模型检验中的方法能有效地缓和状态组合爆炸问题.然而,随着系统规模的增大,BDD的大小仍呈指数增长.吴方法是一种处理多项式的符号计算方法,能有效地求解代数方程组并成功地应用于几何定理机器证明.给出应用吴方法计算表示Kripke结构和CTL公式的多项式的特征列的方法,从而实现对较大规模的系统性质的验证,进一步缓和状态组合爆炸问题.

关键词：符号模型检验、吴方法、特征列

所属期刊栏目：44

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

资助基金：国家重点基础研究发展规划973the National Grand Fundamental Research 973 Program of China under Grant 2004CB318003;成都信息工程学院科研基金资助CBF200623

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

页数：共4页

页码：46-48,64