On-the-fly Model Checking Based On Petri Nets

As an important mathematics tool,the Petri nets are effectively applied in the description and making model of the concurrent systems.Meanwhile,linear temporal logic(LTL for short)is one of the most significant formal tools,which could exactly describe and check the properties of the concurrent systems,and describe the important properties of the concurrent system accurately,such as safety and liveness.The theory of automaton play an important role in model checking,whose cornerstone is temporal logic and the theory of automaton.In fact,model checking is a formal verification technique to detect whether a computing model,by searching the state spaces,satisfies a given property described by an appropriate temporal logic. However,the main disadvantage of model checking is the state explosion problem.This article described the Petri nets,linear temporal logic,Büchi automaton and the intersection of the reachable graph of the Petri net and the automaton,an efficient model checking policy of the reachable graph of the Petri net are detailed discussed based on the linear temporal logic and the theory of automaton,and compared to the other polices,this policy is based on the on-the-fly technique.In on-the-fly model checking,we only need to construct the automaton correspondence to the verified property and the Petri net model of the system,through the search of the state spaces,if new state is needed,then the intersection of the reachable graph of the Petri net and the property automaton is constructed dynamically,at the same time,we use the property automaton to guide the procedure of the constructing of the reachable graph of the Petri net dynamically.Thus,after finding a counter-example of the verified property,it is possible that we only need to construct a small part of state spaces of the reachable graph of the Petri net and the intersection of the automaton, thus we can avoid searching the entire state spaces of the intersection of the automaton, and this policy can reduce the search spaces,and can slow down the state explosion problem.And the memory we needed to save the reachable graph of the Petri net as well as the synchronous product will be reduced,thus it is solved the insufficient of the memory.