Language Recursiveness and Liveness in Sharing Synthesis of Petri Net Systems

The determination of such good properties as liveness, deadlock-freeness of a global system is an important field in the study of Petri net systems synthesis. In this paper, the sharing synthesis of Petri net systems, a significant synthesis process, is discussed. The language recursiveness in sharing synthesis process is proposed and proved, and then the language relation formula based on the concurrent language is obtained. These results present a formal tool for the analysis of a large system which contains concurrent behavior. Moreover, this language relation formula can be applied to judge the liveness and deadlock-freeness of the synthesized systems. Necessary and sufficient conditions are developed. Finally, under the given conditions, the liveness of a global system can be determined by the sublanguage of the local systems, and thus can be studied by means of local systems.