Macro liveness graph and liveness of ω-independent unbounded nets  

作　　者：WANG ShouGuang GAN MengDi ZHOU MengChu 

机构地区：[1]School of Information and Electronic Engineering, Zhejiang Gongshang University [2]Key Laboratory of Embedded System and Service Computing, Ministry of Education,Tongji University [3]Department of Electrical and Computer Engineering, New Jersey Institute of Technology

出　　处：《Science China(Information Sciences)》2015年第3期129-138,共10页中国科学（信息科学）（英文版）

基　　金：supported by the National Science Foundation of USA(Grant No.CMMI-1162482);National Natural Science Foundation of China(Grant Nos.61374148,61472361 and 61100056);Zhejiang Natural Science Foundation for Distinguished Yong Scholars(Grant No.LR14F020001);Zhejiang Science and Technology Project(Grant No.2013C31111);Zhejiang NNST Key Laboratory(Grant No.2013E10012)

摘　　要：Liveness is a basic property of a system and the liveness issue of unbounded Petri nets remains one of the most difficult problems in this field. This work proposes a novel method to decide the liveness of a class of unbounded generalized Petri nets called w-independent unbounded nets, breaking the existing limits to one-place-unbounded nets. An algorithm to construct a macro liveness graph （MLG） is developed and a critical condition based on MLG deciding the liveness of w-independent unbounded nets is proposed. Examples are provided to demonstrate its effectiveness.Liveness is a basic property of a system and the liveness issue of unbounded Petri nets remains one of the most difficult problems in this field. This work proposes a novel method to decide the liveness of a class of unbounded generalized Petri nets called w-independent unbounded nets, breaking the existing limits to one-place-unbounded nets. An algorithm to construct a macro liveness graph （MLG） is developed and a critical condition based on MLG deciding the liveness of w-independent unbounded nets is proposed. Examples are provided to demonstrate its effectiveness.

关 键 词：discrete event system （DES） Petri nets complex systems LIVENESS property analysis 

分 类 号：TP301.1[自动化与计算机技术—计算机系统结构]