Preservation of Liveness and Deadlock-Freeness in Synchronous Synthesis of Petri Net Systems
同步合成Petri网系统活性与无死锁性的保持性

Synthesis process is an important bottom-up approach on modeling Petri net systems, and the preservation of certain good properties such as liveness, deadlock-freeness, reversibility and so forth is also a significant problem in the study of synthesis processes. In this paper, the preservation of liveness and deadlock-freeness is discussed for a synchronous synthesis process. The difference from other work is that the presented approaches are based on the concurrent composition of paths using a concurrent language. The concurrent language relation formula is presented and proved in the synchronous synthesis of Petri net systems, and it can be applied to judge the liveness and deadlock-freeness of a synthesized system. Meanwhile, criteria which are necessary and sufficient for the liveness and deadlock-freeness of the resultant system are developed. Finally, conditions under which the preservation of liveness and deadlock-freeness holds for the synchronous synthesis of Petri net systems are proposed.