Shared P-Type Logic Petri Net Composition and Property Analysis: A Vector Computational Method

Petri net (PN) is an effective modeling and analysis tool for discrete event systems. By attaching a first-order logic predicate logic formula to a transition in a PN, a high-level Petri net named Logic Petri Net (LPN) is obtained. LPN has been proved to have equivalent modeling capability with inhibition Petri nets but keeps simpler net structures than the latter. It has the advantage of modeling the cooperative systems with the function to process batch and indeterminate resources. This paper proposes a vector computational method for LPN compositional analysis. It studies the composition of LPNs with the shared P-type subnets. Each logical expression is transformed into a unique disjunctive normal one and then into a unique set of vectors. A vector computational method is proposed such that the properties of the composition of the shared P-type subnets such as liveness, boundedness, and reversibility are verified. An E-commerce system with customers, merchants, and a third-party is constructed to illustrate the method. This paper can improve the state of the art in the theory of LPNs.