Decomposition of Nets and Verification in terms of Decomposition

Decomposition is an important technique in design and verification based on Petri nets. This paper introduces two kinds of decomposition methods in terms of places and transitions, respectively. For each method, the strategy used in this paper is to require such a decomposition to preserve the desirable properties including liveness and boundedness of the system in the resulting components. Besides, this paper shows that the two decomposition methods may also be used for verifying the properties of a given system