A vector matching method for analysing logic Petri nets

被引:61
作者
Du, YuYue [1 ,2 ]
Qi, Liang [2 ]
Zhou, MengChu [1 ,3 ,4 ]
机构
[1] Tongji Univ, Minist Educ, Key Lab Embedded Syst & Serv Comp, Shanghai 200092, Peoples R China
[2] Shandong Univ Sci & Technol, Coll Informat Sci & Engn, Qingdao 266510, Peoples R China
[3] New Jersey Inst Technol, ECE, Newark, NJ 07102 USA
[4] Chinese Acad Sci, Inst Automat, Lab Complex Syst & Intelligence Sci, Beijing 100080, Peoples R China
基金
中国国家自然科学基金;
关键词
logic Petri nets; enabling vector sets; vector matching; state equation; reachable tree; net state space explosion; DEADLOCK PREVENTION POLICIES; SYSTEMS; LIVENESS; DIAGRAMS;
D O I
10.1080/17517575.2010.541943
中图分类号
TP [自动化技术、计算机技术];
学科分类号
0812 ;
摘要
Batch processing function and passing value indeterminacy in cooperative systems can be described and analysed by logic Petri nets (LPNs). To directly analyse the properties of LPNs, the concept of transition enabling vector sets is presented and a vector matching method used to judge the enabling transitions is proposed in this article. The incidence matrix of LPNs is defined; an equation about marking change due to a transition's firing is given; and a reachable tree is constructed. The state space explosion is mitigated to a certain extent from directly analysing LPNs. Finally, the validity and reliability of the proposed method are illustrated by an example in electronic commerce.
引用
收藏
页码:449 / 468
页数:20
相关论文
共 45 条
[1]   Stepwise rigorous development of distributed agile information systems: from UML-diagrams to component-based Petri Nets [J].
Aoumeur, Nasreddine .
ENTERPRISE INFORMATION SYSTEMS, 2008, 2 (02) :125-160
[2]   Analysis issues in Petri nets with inhibitor arcs [J].
Busi, N .
THEORETICAL COMPUTER SCIENCE, 2002, 275 (1-2) :127-177
[3]  
Chen LQ, 2008, PROCEEDINGS OF 2008 IEEE/ASME INTERNATIONAL CONFERENCE ON MECHATRONIC AND EMBEDDED SYSTEMS AND APPLICATIONS, P476, DOI 10.1109/MESA.2008.4735673
[4]   Preserving languages and properties in stepwise refinement-based synthesis of Petri nets [J].
Ding, ZhiJun ;
Jiang, ChangJun ;
Zhou, MengChu ;
Zhang, YaYing .
IEEE TRANSACTIONS ON SYSTEMS MAN AND CYBERNETICS PART A-SYSTEMS AND HUMANS, 2008, 38 (04) :791-801
[5]   A Petri-net-based correctness analysis of Internet stock trading systems [J].
Du, YuYue ;
Jiang, ChangJun ;
Zhou, MengChu .
IEEE TRANSACTIONS ON SYSTEMS MAN AND CYBERNETICS PART C-APPLICATIONS AND REVIEWS, 2008, 38 (01) :93-99
[6]   Modeling and analysis of real-time cooperative systems using Petri nets [J].
Du, YuYue ;
Jiang, ChangJun ;
Zhou, MengChu .
IEEE TRANSACTIONS ON SYSTEMS MAN AND CYBERNETICS PART A-SYSTEMS AND HUMANS, 2007, 37 (05) :643-654
[7]   A Petri Net-Based Model for Verification of Obligations and Accountability in Cooperative Systems [J].
Du, YuYue ;
Jiang, ChangJun ;
Zhou, MengChu .
IEEE TRANSACTIONS ON SYSTEMS MAN AND CYBERNETICS PART A-SYSTEMS AND HUMANS, 2009, 39 (02) :299-308
[8]  
Du YY, 2002, LECT NOTES COMPUT SC, V2495, P221
[9]  
Duan Y. Y., 2009, Information Technology Journal, V8, P95, DOI 10.3923/itj.2009.95.100
[10]  
Hruz B., 2007, MODELING CONTROL DIS