%0 Journal Article
%T 一种有效的基于ltl和petri网的模型检测方法
%A 张斌
%A 罗贵明
%A 王平
%J 计算机应用
%D 2006
%X ？模型检测的一个主要方法是构建线性与时序逻辑（ltl）公式φ的否定形式等价的büchi自动机aφ和系统模型m的正交积，并检测正交积的可接受语言是否为空。通过对generalizedbüchi自动机进行化简，可以减小自动机的状态空间，从而提高模型检测的效率。根据所提出的方法设计并实现的基于ltl和petri网进行模型检测的工具包，可以有效地对基于petri网表示的系统模型进行模型检测。
%K 模型检测
%K 线性时序逻辑
%K 自动机
%K petri网
%U http://www.joca.cn/CN/abstract/abstract8759.shtml