On Liveness Analysis And Verification For Petri Nets

Petri net is a graphical modeling tool.Liveness is the main content of Petri net theory.In this thesis,structural analysis and reachability analysis are used to study the liveness of general Petri net system.The main research contents and results are as follows:Firstly,we propose the definition of non-pre-blocked Siphon and study the relationship between the liveness and non-pre-blocking properties of Petri net.We introduce the concept of stable marking,and prove that any Petri net has stable marking.By discussing the structural characteristics related to dead transition in non-liveness and non-pre-blocking Petri nets under stable marking,the necessary and sufficient conditions on liveness for four subclasses of Petri net,namely simple net,asymmetric choice nets,homogeneous quasi-strongly connected joinfree nets and -nets,are obtained.Secondly,when discussing sufficient conditions for the general Petri net to remain liveness,the structure of Petri net is not restricted.If the bounded Petri net is weakly-live,then the constraint condition – a mathematical homogeneous linear system with only positive integer solutions is added,then the Petri net is live.Then,when judging the liveness of the Petri net,the extended Petri net is constructed by adding a place with with sufficiently large but bounded number of tokens to the Petri net to ensure that the behavior of the extended Petri net is close to the behavior of the original Petri net,so as to deduce the liveness of the original net from the liveness of the extended net.In addition,as for how to determine non-pre-blocked Siphon,two structures of Siphon non-pre-blocking are given respectively from Trap control and invariant control,and a linear programming method is given to determine Siphon non-pre-blocking by means of the state equation.Finally,the validity of the method is verified by some common examples in literature.Compared with controlled Siphon,non-pre-blocked Siphon is proposed in this paper,and a new method for determining non-pre-blocking Siphon is proposed by using linear programming theory.Based on the non-pre-blocked Siphon,this paper not only gives the necessary and sufficient conditions for the common simple nets,HQJF nets and AC nets to remain liveness,but also gives the necessary and sufficient conditions for the liveness of -nets,a subclass of Petri net whose structure is opposite to AC nets.In addition,unlike most literatures that are limited to the liveness decison of Petri net with special structures,this paper constructed an extended Petri net to determine the liveness of the original Petri net without limiting the structure of the Petri net,which can be applied to more classes of Petri net.