Petri网系统合成操作的活性保持性研究

合成操作是Petri网系统建模中一种重要的自底向上建模方法,而在Petri网系统的合成过程中,保性性质是一个重要的研究问题.本文综述了我们对Petri网系统两种合成操作(共享合成、同步合成)活性保持性的研究工作.与以往研究不同,侧重从并发语言的角度讨论.定义了相应合成操作的路径并发合成运算,以此建立两种合成操作Petri网系统的并发语言关系式.这些语言关系式可用于判定相应合成操作Petri网系统的活性与无死锁性,同时给出合成的Petri网系统活性与无死锁性的充要条件.最后分别给出条件使得合成的Petri网系统有活性保持性质.

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.