Macro liveness graph and liveness of ω-independent unbounded nets

被引：0

作者：

WANG ShouGuang ^{[1
]}

GAN MengDi ^{[2
]}

ZHOU MengChu ^{[2
,3
]}

机构：

[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年 / 58卷 / 03期

关键词：

discrete event system(DES); Petri nets; complex systems; liveness; property analysis;

D O I：

暂无

中图分类号：

TP301.1 [自动机理论];

学科分类号：

081202 ;

摘要：

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ω-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ω-independent unbounded nets is proposed.Examples are provided to demonstrate its effectiveness.

引用

页码：132 / 141

页数：10

共 50 条

[31] Notes on Liveness and Boundedness of Extended Strong Asymmetric Choice Nets Ⅱ [J].

焦莉 ;

陆维明 .

Journal of Computer Science and Technology, 2001, (05) :426-433

[32] Liveness Supervision of AMS with Complex Processes Using Petri Nets [J].

Hu, Hesuan ;

Tang, Ying ;

Zhou, Mengchu ;

Li, Zhiwu .

2011 IEEE INTERNATIONAL CONFERENCE ON SYSTEMS, MAN, AND CYBERNETICS (SMC), 2011, :844-849

[33] Fake fingerprint liveness detection based on micro and macro features [J].

Agrawal, Rohit ;

Jalal, Anand Singh ;

Arya, K. V. .

INTERNATIONAL JOURNAL OF BIOMETRICS, 2019, 11 (02) :177-206

[34] A SUBCLASS OF PETRI NETS WHERE LIVENESS IS PRESERVED UNDER THE EARLIEST FIRING RULE [J].

OHTA, A ;

HISAMURA, T .

ELECTRONICS AND COMMUNICATIONS IN JAPAN PART III-FUNDAMENTAL ELECTRONIC SCIENCE, 1994, 77 (05) :58-67

[35] Design of T-liveness enforcing supervisors in Petri nets [J].

Iordache, MV ;

Antsaklis, PJ .

IEEE TRANSACTIONS ON AUTOMATIC CONTROL, 2003, 48 (11) :1962-1974

[36] Liveness Evaluation of a Cyclo-Static DataFlow Graph [J].

Benazouz, Mohamed ;

Munier-Kordon, Alix ;

Hujsa, Thomas ;

Bodin, Bruno .

2013 50TH ACM / EDAC / IEEE DESIGN AUTOMATION CONFERENCE (DAC), 2013,

[37] TYPE-CHECKING LIVENESS FOR COLLABORATIVE PROCESSES WITH BOUNDED AND UNBOUNDED RECURSION [J].

Debois, Soren ;

Hildebrandt, Thomas ;

Slaats, Tijs ;

Yoshida, Nobuko .

LOGICAL METHODS IN COMPUTER SCIENCE, 2016, 12 (01)

[38] Verifying Liveness for Asynchronous Programs [J].

Ganty, Pierre ;

Majumdar, Rupak ;

Rybalchenko, Andrey .

ACM SIGPLAN NOTICES, 2009, 44 (01) :102-113

[39] Notes on liveness and boundedness of extended strong asymmetric choice nets II [J].

Li Jiao ;

Weiming Lu .

Journal of Computer Science and Technology, 2001, 16 :426-433

[40] Notes on liveness and boundedness of extended Strong Asymmetric Choice Nets II [J].

Jiao, L ;

Lu, WM .

JOURNAL OF COMPUTER SCIENCE AND TECHNOLOGY, 2001, 16 (05) :426-433

← 1 2 3 4 5 →