| 一种有效的基于LTL和Petri网的模型检测方法 |
| |
| 引用本文： | 张斌,罗贵明,王平.一种有效的基于LTL和Petri网的模型检测方法[J].计算机应用,2006,26(10):2490-2493. |
| |
| 作者姓名： | 张斌 罗贵明 王平 |
| |
| 作者单位： | 1. 清华大学,软件学院,北京,100084
2. 沈阳军区装备部,辽宁,沈阳,110021 |
| |
| 基金项目： | 国家重点基础研究发展计划(973计划);国家自然科学基金;清华大学校科研和教改项目 |
| |
| 摘 要： | 模型检测的一个主要方法是构建线性与时序逻辑（LTL）公式φ的否定形式等价的Büchi自动机Aφ和系统模型M的正交积，并检测正交积的可接受语言是否为空。通过对Generalized Büchi自动机进行化简，可以减小自动机的状态空间，从而提高模型检测的效率。根据所提出的方法设计并实现的基于LTL和Petri网进行模型检测的工具包，可以有效地对基于Petri网表示的系统模型进行模型检测。
|
| 关 键 词： | 模型检测 线性时序逻辑 自动机 Petri网 |
| 文章编号： | 1001-9081（2006）10-2490-04 |
| 收稿时间： | 2006-04-24 |
| 修稿时间： | 2006-04-242006-06-19 |
Efficient method of model checking based on LTL and Petri net |
| |
| ZHANG Bin,LUO Gui-ming,WANG Ping.Efficient method of model checking based on LTL and Petri net[J].journal of Computer Applications,2006,26(10):2490-2493. |
| |
| Authors: | ZHANG Bin LUO Gui-ming WANG Ping |
| |
| Abstract: | 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. |
| |
| Keywords: | model checking Linear Temporal Logic(LTL) automata Petri net |
| 本文献已被 CNKI 万方数据 等数据库收录！ |
| 点击此处可从《计算机应用》浏览原始摘要信息 |
|
点击此处可从《计算机应用》下载全文 |
