文献类型：期刊文章

作　　者：张斌[1] 罗贵明[1] 王平[2]

机构地区：[1]清华大学软件学院,北京100084 [2]沈阳军区装备部,辽宁沈阳110021

出　　处：《计算机应用》

基　　金：国家973规划项目(2004CB719400);国家自然科学基金(60474026);清华大学基础基金资助

年　　份：2006

卷　　号：26

期　　号：10

起止页码：2490-2493

语　　种：中文

收录情况：AJ、BDHX、BDHX2004、CSA、CSA-PROQEUST、CSCD、CSCD2011_2012、IC、INSPEC、JST、RCCSE、ZGKJHX、ZMATH、核心刊

摘　　要：模型检测的一个主要方法是构建线性与时序逻辑(LTL)公式φ的否定形式等价的B櫣chi自动机Aφ和系统模型M的正交积,并检测正交积的可接受语言是否为空。通过对GeneralizedB櫣chi自动机进行化简,可以减小自动机的状态空间,从而提高模型检测的效率。根据所提出的方法设计并实现的基于LTL和Petri网进行模型检测的工具包,可以有效地对基于Petri网表示的系统模型进行模型检测。

关 键 词：模型检测  线性时序逻辑 自动机 PETRI网

分 类 号：TP311.13]