Property analysis of logic Petri nets by marking reachability graphs

Abstract

Logic Petri nets (LPNs) are suitable to describe and analyze batch processing functions and passing value indeterminacy in cooperative systems. To investigate the dynamic properties of LPNs directly, a new method for analyzing LPNs is proposed based on marking reachability graphs in this paper. Enabled conditions of transitions are obtained and a marking reachability graph is constructed. All reachable markings can be obtained based on the graph; the fairness and reversibility of LPNs are analyzed. Moreover, the computing complexity of the enabled conditions and reachable markings can be reduced by this method. The advantages of the proposed method are illustrated by examples and analysis.

Keywords

logic Petri nets / enabled condition / reachable marking graph / fairness / reversibility

References

[1] Hruz B, Zhou M C. Modeling and control of discrete event dynamic systems. London: Springer, 2007

[2] Du Y Y, Jiang C J, Zhou M C. A Petri net-based model for verification of obligations and accountability in cooperative systems. IEEE Transactions on Systems, Man and Cybernetics, Part A: Systems and Humans, 2008, 39(2): 299-308

[3] Du Y Y, Jiang C J, Zhou M C. A Petri net based correctness analysis of internet stock trading systems. IEEE Transactions on Systems, Man, and Cybernetics, Part C: Applications and Reviews, 2008, 38(1): 93-99

[4] Deng S Y, Du Y Y. Logic Petri net based model for Web service cluster. Journal of Computer Applications, 2012, 32(8): 2328-2337

[5] Du Y Y, Jiang C J, Zhou M C. A Petri net-based model for verifi-cation of obligations and accountability in cooperative systems. IEEE Transactions on Systems, Man, and Cybernetics, Part A: Systems and Humans, 2009, 39(2): 299-308

[6] Kusiak A, Yang H H. Modeling design cycles with stochastic Petri nets. American Society of Mechanical Engineers. Production Engineering Division PED, 1992, 59(8): 375-385

[7] Tan W, Fan Y S, Zhou M C, Tian Z. Data-driven service composition in building SOA solutions: a Petri net approach. IEEE Transactions on Automation Science and Engineering, 2010, 7(3): 686-694

[8] Xiong P C, Fan Y, Zhou M C. A Petri net approach to analysis and composition of web services. IEEE Transactions on Systems, Manand Cybernetics, Part A: Systems and Humans, 2010, 40(2): 376-387

[9] Du Y Y, Guo B Q. Logic Petri nets and equivalency. Information Technology Journal, 2009, 8(1): 95-100

[10] Du Y Y, Jiang C J. Formal representation and analysis of batch stock trading systems by logical Petri net workflows. Lecture Notes in Computer Science, 2002, 2495: 221-225

[11] Busi N. Analysis issues in Petri nets with inhibitor arcs. Theoretical Computer Science, 2002, 275(1): 127-177

[12] Du Y Y, Qi L, Zhou M C. A vector matching method for analyzing logic Petri nets. Enterprise Information Systems, 2011, 5(4): 449-468

[13] Robidoux R, Xu H, Xing L D, Zhou M C. Automated verification of dynamic reliability block diagrams using colored Petri nets. IEEE Transactions on Systems, Man, and Cybernetics, Part A: Systems and Humans, 2010, 40(4): 337-351

[14] Hu H, Zhou M C, Li Z. Liveness enforcing supervision of video streaming systems using non-sequential Petri nets. IEEE Transactions on Multimedia, 2009, 11(8): 1446-1456

[15] Li J, Zhou M, Dai X. Algebraic reduction and refinement of Petri nets. IEEE Transactions on Systems, Man and Cybernetics: Part A: Systems and Humans, 2012, 42(7): 1244-1255

[16] Liu D, Li ZW, Zhou M C. Liveness of an extended S3PR. Automatica, 2010, 46(6): 1008-1018

[17] Liu G, Jiang C, Zhou M C. Two simple deadlock prevention policies for S3PR based on key resource/operation-place pairs. IEEE Transactions on Automation Science and Engineering, 2010, 7(4): 945-957

RIGHTS & PERMISSIONS

2014 Higher Education Press and Springer-Verlag Berlin Heidelberg