| 基于PPTL的着色Petri网的模型检测方法 |
| |
| 引用本文： | 门鹏. 基于PPTL的着色Petri网的模型检测方法[J]. 科学技术与工程, 2013, 13(5): 1362-1367 |
| |
| 作者姓名： | 门鹏 |
| |
| 作者单位： | 陕西省烟草专卖局（公司） |
| |
| 基金项目： | 基金项目：国家自然科学基金青年基金(61003079)，陕西省工业攻关计划(2009K01-36)，教育部博士点基金（新教师计划）(20100203120012);国家教育部博士点基金;国家自然科学基金项目（面上项目，重点项目，重大项目） |
| |
| 摘 要： | 为了提高着色Petri网的描述及验证能力,提出了一种基于投影命题时序逻辑的着色Petri网的模型检测方法。通过构建投影命题时序逻辑公式的否定形式等价的Buchi自动机,将它与着色Petri网的可达图相积,通过检测检测乘积图的可接受语言是否为空,从而判断用时序逻辑公式描述的系统性质是否满足。利用投影命题时序逻辑公式具有更强的表达力,可以有效地提高着色Petri网系统的描述及验证能力。
|
| 关 键 词： | 着色Petri网 模型检测 投影命题时序逻辑 |
| 收稿时间： | 2012-09-25 |
| 修稿时间： | 2012-10-25 |
Model-checking Method of PPTL-based Colored Petri Nets |
| |
| menpeng. Model-checking Method of PPTL-based Colored Petri Nets[J]. Science Technology and Engineering, 2013, 13(5): 1362-1367 |
| |
| Authors: | menpeng |
| |
| Affiliation: | MENG Peng (Shaanxi Tobacco Monopoly Bureau,Xi’an 710061,P.R.China) |
| |
| Abstract: | |
| |
| Keywords: | Colored Petri Nets Model checking Propositional projection temporal logic |
| 本文献已被 CNKI 等数据库收录！ |
| 点击此处可从《科学技术与工程》浏览原始摘要信息 |
|
点击此处可从《科学技术与工程》下载全文 |
|
