|
|||||
|
|
| 基于PPTL的着色Petri网的模型检测方法 | |
| 作者姓名： | 门鹏 |
| 作者单位： | 陕西省烟草专卖局（公司） |
| 基金项目： | 基金项目：国家自然科学基金青年基金(61003079),陕西省工业攻关计划(2009K01-36),教育部博士点基金（新教师计划）(20100203120012);国家教育部博士点基金;国家自然科学基金项目（面上项目,重点项目,重大项目） |
| 摘 要： | 为了提高着色Petri网的描述及验证能力,提出了一种基于投影命题时序逻辑的着色Petri网的模型检测方法。通过构建投影命题时序逻辑公式的否定形式等价的Buchi自动机,将它与着色Petri网的可达图相积,通过检测检测乘积图的可接受语言是否为空,从而判断用时序逻辑公式描述的系统性质是否满足。利用投影命题时序逻辑公式具有更强的表达力,可以有效地提高着色Petri网系统的描述及验证能力。 |
| 关 键 词： | 着色Petri网 模型检测 投影命题时序逻辑 |
| 收稿时间： | 2012-09-25 |
| 修稿时间： | 2012-10-25 |
| 本文献已被 CNKI 等数据库收录！ | |
| 点击此处可从《科学技术与工程》浏览原始摘要信息 | |
| 点击此处可从《科学技术与工程》下载免费的PDF全文 | |