同步合成Petri网系统活性与无死锁性的保持性

Preservation of Liveness and Deadlock-Freeness in Synchronous Synthesis of Petri Net Systems

合成操作是Petri网系统建模中一种重要的自底向上建模方法,而在Petri网系统的合成研究中,一些好性质,如活性、无死锁性、可回复性等的保持性,是一个重要的研究问题.研究了Petri网系统同步合成操作活性与无死锁性的保持性.与以往研究工作不同,基于路径的并发合成用并发语言的方法,提出并证明了同步合成Petri网系统的一个并发语言关系式.该语言关系式可用于判定同步合成Petri网系统的活性与无死锁性,同时给出了同步合成Petri网系统活性与无死锁性的充要条件.最后提出一些条件,在这些条件下,同步合成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. 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.