On Preservation of Liveness in Synthesis Processes of Petri Net Systems

The synthesis process is an important bottom-up approach on modeling Petri net systems, and the preservation of properties also is a significant problem in study of synthesis process of Petri net systems. This paper summarizes our works on preservation of liveness in two synthesis processes, namely, synchronous and sharing processes. The difference from other works is that our approaches are based on concurrent language. An operation is defined to express the concurrent composition of paths, and a concurrent language formula of corresponding synthesis process is established, and it can be applied to judge the liveness and deadlock-freeness of synthesized system. Meanwhile, some criteria are introduced, which are necessary and sufficient for liveness and deadlock-freeness. Finally, some conditions are proposed to preserve the liveness and deadlock-freeness of composite system.