Property analysis of logic Petri nets by marking reachability graphs

Logic Petri nets (LPNs) are suitable to describe and analyze batch processing functions and passing value indeterminacy in cooperative systems. To investigate the dynamic properties of LPNs directly, a new method for analyzing LPNs is proposed based on marking reachability graphs in this paper. Enabled conditions of transitions are obtained and a marking reachability graph is constructed. All reachable markings can be obtained based on the graph; the fairness and reversibility of LPNs are analyzed. Moreover, the computing complexity of the enabled conditions and reachable markings can be reduced by this method. The advantages of the proposed method are illustrated by examples and analysis.