基于on-the-fly的Petri网模型检查技术研究与实现

摘要

Petri网是一种应用非常广泛的建模工具,它能深刻、简洁地描述控制系统,特别是能较好地描述并发系统的结构,并能对系统的动态性质进行分析.在探讨了Petri网的模型检查的基础上,采用双DFS算法,对基于Petri网的模型检查的算法进行了改进,提出了针对Petri网的on-the-fly算法,同时给出了基于on-the-fly的Petri网模型检查的实现和测试,从而可以有效地对Petri网表示的系统模型进行模型检查.%Petri net is a very widely used modelling tool ,which can describe the control system in a profound and brief way.In particular,it can better describe the structure of concurrent system,and can analyse the dynamic property of a system.In this paper, based on the discussion of model checking of the Petri net,we adopt double DFS algorithm to improve the Petri net-based model checking algorithm,put forward the on-the-fly algorithm in light to the Petri net.Meanwhile,we also present the realisation and test of model checking of Petri net based on on-the-fly algorithm,so that the model checking on the system model expressed by Petri net can be applied effectively.