Petri net systems synthesis can construct largesystems without the requirement of reachability analysisso that it can reduce the high complexity of analyzingglobal system. In a synthesis process, such good propertiesof subsystems as liveness and deadlock-freeness etc, mustbe preserved in synthesized system. This paper focusses onliveness preservation in inhibitor-arc connection operations.The systems dynamic, concurrent behavior relation i.e.concurrent language relation in inhibitor-arc connectionsis stressed studied. The corresponding language relationformula is present and proved, and it can be appliedto determine liveness of synthesized system in inhibitorarcconnection operations. Furthermore, some criteria areintroduced, which are necessary and sufficient for liveness, todetermine the liveness of global system by the same ones oflocal systems. Finally, some examples are given, illustratingthe effectiveness of the proposed approach in modeling andanalyzing of large systems.
展开▼
