摘要
Petri网是一种对并发系统进行描述和建模的重要数学工具,可达图是Petri网模型的主要分析方法。为了解决由于系统参数化造成的Petri模型可达图难以构造并且无法进行模型性质检验的问题,在分析现有参数化可达图方法的基础上,利用参数化标识提出一种新的Petri网模型完全参数化可达图构造方法。同时给出了这种可达图的有关特性及其证明,并举例说明了如何利用这种参数化可达图对系统进行模型性质检测。
Petri net is an important mathematical tool for concurrent systems description and modeling, and reachability graph analysis is one of the most effective methods for Petri net models, In order to solve the problem of constructing teachability graphs and verifying properties of parameterized system Petri net models, a novel completely parameterized reachability graph （PRG） based on parameterized markings is presented. Constructing algorithm for the PRG is introduced, and some primary properties of this kind of PRG are given and proved, An example is presented to illustrate how to use the PRG for modeling property verification.
出处
《系统仿真学报》
CAS
CSCD
北大核心
2007年第A01期38-43,共6页
Journal of System Simulation
基金
国家自然科学基金(60673187
90412012)
关键词
PETRI网
参数化
可达图
模型性质检测
petri net
parameterized
teachability graph
modeling property verification
