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

摘要

为了提高着色Petri网的描述及验证能力,提出了一种基于投影命题时序逻辑的着色Petri网的模型检测方法.通过构建投影命题时序逻辑公式的否定形式等价的Buchi自动机,将它与着色Petri网的可达图相积,通过检测检测乘积图的可接受语言是否为空,从而判断用时序逻辑公式描述的系统性质是否满足.利用投影命题时序逻辑公式具有更强的表达力,可以有效地提高着色Petri网系统的描述及验证能力.%To improve the description and verification ability of the Colored Petri Net, one model-checking method for colored Petri nets which is based on the Prepositional projection temporal logic is proposed.Initially, Buchi automata is constructed, which is equivalent to the negative form of propositional projection temporal logic.Followed by the product graph of the Buchi automata and the ratability graph of colored Petri nets are created.This will detect whether the acceptable language of product graph is null.Subsequently, whether the system property is satisfied which is described by PPTL formula can be judged.PPTL is more expressive, so the method can effectively improve the description and verification ability of the colored Petri nets.