%0 Journal Article
%T Efficient method of model checking based on LTL and Petri net<br>一种有效的基于LTL和Petri网的模型检测方法
%A ZHANG Bin
%A LUO Gui-ming
%A WANG Ping
%A <br>张斌
%A 罗贵明
%A 王平
%J 计算机应用
%D 2006
%I 
%X 模型检测的一个主要方法是构建线性与时序逻辑(LTL)公式φ的否定形式等价的B櫣chi自动机Aφ和系统模型M的正交积,并检测正交积的可接受语言是否为空。通过对GeneralizedB櫣chi自动机进行化简,可以减小自动机的状态空间,从而提高模型检测的效率。根据所提出的方法设计并实现的基于LTL和Petri网进行模型检测的工具包,可以有效地对基于Petri网表示的系统模型进行模型检测。
%K model checking
%K Linear Temporal Logic(LTL)
%K automata
%K Petri net<br>模型检测
%K 线性时序逻辑
%K 自动机
%K Petri网
%U http://www.alljournals.cn/get_abstract_url.aspx?pcid=5B3AB970F71A803DEACDC0559115BFCF0A068CD97DD29835&cid=8240383F08CE46C8B05036380D75B607&jid=831E194C147C78FAAFCC50BC7ADD1732&aid=08DD0E9BC435CFCF&yid=37904DC365DD7266&vid=96C778EE049EE47D&iid=F3090AE9B60B7ED1&sid=991A1B87C8CBBB34&eid=8A7870C868F44860&journal_id=1001-9081&journal_name=计算机应用&referenced_num=0&reference_num=7