QQ客服 官方微博 反馈留言

	一种有效的基于LTL和Petri网的模型检测方法
	张斌 ; 罗贵明 ; 王平 ; ZHANG Bin ; LUO Gui-ming ; WANG Ping
	2010-06-09 ; 2010-06-09
关键词	模型检测 线性时序逻辑 自动机 Petri网 model checking Linear Temporal Logic(LTL) automata Petri net TP301.1
其他题名	Efficient method of model checking based on LTL and Petri net
中文摘要	模型检测的一个主要方法是构建线性与时序逻辑(LTL)公式φ的否定形式等价的B櫣chi自动机Aφ和系统模型M的正交积,并检测正交积的可接受语言是否为空。通过对GeneralizedB櫣chi自动机进行化简,可以减小自动机的状态空间,从而提高模型检测的效率。根据所提出的方法设计并实现的基于LTL和Petri网进行模型检测的工具包,可以有效地对基于Petri网表示的系统模型进行模型检测。; An import method of model checking is constructing the product of automata A_ φ from the negation of Linear Temporal Logic(LTL) formula and the model of system, and checking the emptiness of the product. A method to reduce the state-space of the Generalized Büchi automaton was presented, which can improve the efficiency of model checking. The toolkit for model checking which was designed and implemented based on LTL and Petri net can check the model described by Petri net very well.; 国家973规划项目(2004CB719400); 国家自然科学基金(60474026); 清华大学基础基金资助
语种	中文 ; 中文
内容类型	期刊论文
源URL	[http://hdl.handle.net/123456789/56590]
专题	清华大学
推荐引用方式 GB/T 7714	张斌,罗贵明,王平,等. 一种有效的基于LTL和Petri网的模型检测方法[J],2010, 2010.
APA	张斌,罗贵明,王平,ZHANG Bin,LUO Gui-ming,&WANG Ping.(2010).一种有效的基于LTL和Petri网的模型检测方法..
MLA	张斌,et al."一种有效的基于LTL和Petri网的模型检测方法".(2010).

个性服务

查看访问统计

相关权益政策

暂无数据

收藏/分享

除非特别说明，本系统中所有内容都受版权保护，并保留所有权利。