Compositional verification of liveness property in inhibitor-arc connections of Petri net systems

被引：0
作者：
Pu, Fei [1 ,2 ]
机构：
[1] College of Computer and Information Engineering, Zhejiang Gongshang University, Hangzhou
[2] State Key Laboratory of Computer Science, Institute of Software, Chinese Academy of Sciences, Beijing
来源：
Journal of Software | 2012年 / 7卷 / 03期
关键词：
Concurrent language; Dynamic invariance; Inhibitor-arc connections; Liveness preservation;
D O I：
10.4304/jsw.7.3.499-507
中图分类号：
学科分类号：
摘要：
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 inhibitor-arc 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. © 2012 ACADEMY PUBLISHER.
引用
收藏
页码：499 / 507
页数：8
相关论文
共 19 条
  • [1] Simple composition of nets, Proceedings of 30th International Conference On Application and Theory of Petri Nets, pp. 23-42, (2009)
  • [2] Ferrarini L., Narduzzi M., Tassan-Solet M., A new approach to modular liveness analysis conceived for large logic controllers' design, IEEE Transactions On Robotics and Automation, 10, 2, pp. 169-184, (1994)
  • [3] An incremental approach to logic controller design with Petri nets, IEEE Transaction On Systems, Man, and Cybernetics, 22, 3, pp. 461-473, (1992)
  • [4] Wang H.Q., Jiang C.J., Liao S.Y., Behavior relations in synthesis process of Petri net models, IEEE Transsaction On Robotics and Automation, 16, 4, pp. 400-406, (2000)
  • [5] Petri net dynamic invariance, Science China(ScienceE), 27, 6, pp. 605-611, (1997)
  • [6] Souissi Y., On liveness preservation by composition of nets via a set of places, Advances In Petri Nets, Volume 524 of Lecture Notes In Computer Science, pp. 277-295, (1991)
  • [7] Souissi Y., Memmi G., Composition of nets via a communication medium, Advances In Petri Nets, Volume 483 of Lecture Notes In Computer Science, pp. 457-470, (1990)
  • [8] A Petri net synthesis theorey for modeling flexible manufacturing systems, IEEE Transaction On Systems, Man, and Cybernetics, 27, 2, pp. 169-183, (1997)
  • [9] Jeng M.D., Diceare F., A review of synthesis techniquees for Petri nets with appliccations to automated manufacturing systems, IEEE Transaction On Systems, Man, and Cybernetics, 23, 1, pp. 301-312, (1993)
  • [10] Aybar A., Ifar A., Overlapping decompositions and expansions of Petri nets, IEEE Transaction On Automatic Control, 47, 3, pp. 511-515, (2002)
12