JSW 2012 Vol.7(3): 499-507 ISSN: 1796-217X
doi: 10.4304/jsw.7.3.499-507
doi: 10.4304/jsw.7.3.499-507
Compositional Verification of Liveness Property in Inhibitor-arc Connectio
Fei Pu1, 2
1College of Computer and Information Engineering
Zhejiang Gongshang University, Hangzhou, China
2State Key Laboratory of Computer Science, Institute of Software Chinese Academy of Sciences, Beijing, China
Abstract—Petri net systems synthesis can construct large systems without the requirement of reachability analysis so that it can reduce the high complexity of analyzing global system. In a synthesis process, such good properties of subsystems as liveness and deadlock-freeness etc, must be preserved in synthesized system. This paper focusses on liveness preservation in inhibitor-arc connection operations. The systems dynamic, concurrent behavior relation i.e. concurrent language relation in inhibitor-arc connections is stressed studied. The corresponding language relation formula is present and proved, and it can be applied to determine liveness of synthesized system in inhibitorarc connection operations. Furthermore, some criteria are introduced, which are necessary and sufficient for liveness, to determine the liveness of global system by the same ones of local systems. Finally, some examples are given, illustrating the effectiveness of the proposed approach in modeling and analyzing of large systems.
Index Terms—liveness preservation, concurrent language, dynamic invariance, inhibitor-arc connections
2State Key Laboratory of Computer Science, Institute of Software Chinese Academy of Sciences, Beijing, China
Abstract—Petri net systems synthesis can construct large systems without the requirement of reachability analysis so that it can reduce the high complexity of analyzing global system. In a synthesis process, such good properties of subsystems as liveness and deadlock-freeness etc, must be preserved in synthesized system. This paper focusses on liveness preservation in inhibitor-arc connection operations. The systems dynamic, concurrent behavior relation i.e. concurrent language relation in inhibitor-arc connections is stressed studied. The corresponding language relation formula is present and proved, and it can be applied to determine liveness of synthesized system in inhibitorarc connection operations. Furthermore, some criteria are introduced, which are necessary and sufficient for liveness, to determine the liveness of global system by the same ones of local systems. Finally, some examples are given, illustrating the effectiveness of the proposed approach in modeling and analyzing of large systems.
Index Terms—liveness preservation, concurrent language, dynamic invariance, inhibitor-arc connections
Cite: Fei Pu, "Compositional Verification of Liveness Property in Inhibitor-arc Connections of Petri Net Systems," Journal of Software vol. 7, no. 3, pp. 499-507, 2012.
PREVIOUS PAPER
First page
General Information
ISSN: 1796-217X (Online)
Frequency: Quarterly
Editor-in-Chief: Prof. Antanas Verikas
Executive Editor: Ms. Yoyo Y. Zhou
Abstracting/ Indexing: DBLP, EBSCO, CNKI, Google Scholar, ProQuest, INSPEC(IET), ULRICH's Periodicals Directory, WorldCat, etc
E-mail: jsweditorialoffice@gmail.com
-
Mar 01, 2024 News!
Vol 19, No 1 has been published with online version [Click]
-
Jan 04, 2024 News!
JSW will adopt Article-by-Article Work Flow
-
Apr 01, 2024 News!
Vol 14, No 4- Vol 14, No 12 has been indexed by IET-(Inspec) [Click]
-
Apr 01, 2024 News!
Papers published in JSW Vol 18, No 1- Vol 18, No 6 have been indexed by DBLP [Click]
-
Nov 02, 2023 News!
Vol 18, No 4 has been published with online version [Click]