The Preservation of Liveness in Self-Loops Connection of Petri Net Systems

In study of Petri net systems, the approach of synthesis process is playing an increasingly significant role. In a synthesis process, the properties of subsystems must be preserved in the global system in order to reduce the high complexity of analyzing. This paper focuses on such property as live ness in self-loops connection of Petri net systems. The system behavior relation i.e. language relation in self-loops connection process is stressed studied. The corresponding concurrent language formula is presented and proved, and it can be applied to judge the live ness in self-loops connection operation. Moreover, some criteria are introduced, which are necessary and sufficient for live ness preservation. Then, under these conditions, the live ness of global system can be determined by the same properties of local systems. Contrasted with other works, our approaches can synthesize Petri net systems beyond asymmetric choice nets and are based on concurrent behavior of systems.