可重写Petri网:位置可重写及性质分析

摘要

To solve problems of dynamic modeling capabilities of Petri nets on the dynamic system reconfiguration, rewritable Petri nets and rewritable place of Petri nets is presented in this paper. Some properties of the rewritable place of Petri nets, such as structural boundedness, conservation, repetitiveness, and liveness are analyzed and verified. A necessary and sufficient condition for the liveness of the rewritable place of Petri nets is presented. The paper shows that the sharing synthesis Petri net is an instance of rewritable place of Petri net, and a simulation algorithm the degraded rewritable place of Petri nets simulates sharing synthesis Petri nets is established. The results provide a theoretical method for Petri net formal modeling of dynamic reconfiguration systems, and provide an effective way for the formal verification of large-scale dynamic distributed systems.%针对Petri网对动态系统重构形式化描述和建模能力的不足,提出了可重写Petri网和位置可重写Petri网的基本概念.分析了位置可重写Petri网保持有界性、保守性、可重复性及活性等性质.给出了位置可重写Petri网保持活性的一个充要条件.证明了共享合成Petri网是位置可重写Petri网的一个实例,建立了退化的位置可重写Petri网模拟共享合成Petri网的算法.所得结果能够为动态重构系统的Petri网形式化建模提供理论方法,为大规模动态分布式系统的形式化验证提供有效途径.