基于PPTL的着色Petri网的模型检测方法

摘要：

为了提高着色Petri网的描述及验证能力,提出了一种基于投影命题时序逻辑的着色Petri网的模型检测方法.通过构建投影命题时序逻辑公式的否定形式等价的Buchi自动机,将它与着色Petri网的可达图相积,通过检测检测乘积图的可接受语言是否为空,从而判断用时序逻辑公式描述的系统性质是否满足.利用投影命题时序逻辑公式具有更强的表达力,可以有效地提高着色Petri网系统的描述及验证能力.

关键词：着色Petri网、模型检测、投影命题时序逻辑

所属期刊栏目：13

分类号：TP391.41(计算技术、计算机技术)

资助基金：国家自然科学基金青年基金61003079;陕西省工业攻关计划2009K01036;教育部博士点基金新教师计划20100203120012

在线出版日期：2013-04-18（万方平台首次上网日期，不代表论文的发表时间）

页数：共6页

页码：1362-1367