一种有效的基于LTL和Petri网的模型检测方法

作     者：张斌 罗贵明 王平 ZHANG Bin;LUO Gui-ming;WANG Ping

作者机构：清华大学软件学院北京100084 沈阳军区装备部辽宁沈阳110021 

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

出 版 物：《计算机应用》 (journal of Computer Applications)

年 卷 期：2006年第26卷第10期

页      码：2490-2493页

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

主 题 词：模型检测 线性时序逻辑 自动机 Petri网 

学科分类：12[管理学] 1201[管理学-管理科学与工程类] 

核心收录：

馆 藏 号：203162822...