A Technique for Reachability Graph Generation for the Petri Net Models of Parallel Processes

Authors: Farooq Ahmad, Hejiao Huang, Xiaolong Wang

Abstract:

Reachability graph (RG) generation suffers from the problem of exponential space and time complexity. To alleviate the more critical problem of time complexity, this paper presents the new approach for RG generation for the Petri net (PN) models of parallel processes. Independent RGs for each parallel process in the PN structure are generated in parallel and cross-product of these RGs turns into the exhaustive state space from which the RG of given parallel system is determined. The complexity analysis of the presented algorithm illuminates significant decrease in the time complexity cost of RG generation. The proposed technique is applicable to parallel programs having multiple threads with the synchronization problem.

Keywords: Parallel processes, Petri net, reachability graph, time complexity.

Digital Object Identifier (DOI): doi.org/10.5281/zenodo.1083117

References:

[1] T. Murata, "Petri nets: properties, analysis and application," In Proceedings of IEEE, vol. 77, No. 4, pp. 541-580, 1989.
[2] J. L. Peterson, "Petri Net Theory and the Modeling of Systems", Prentice-Hall: Englewood Cliffs, NJ, 1981.
[3] A. Valmari, "The state explosion problem", In: W. Reisig, G. Rozenberg (Eds.), Lectures on Petri nets I: Basic Models, LNCS 1491, Springer- Verlag, pp. 429-528, 1998.
[4] L. Recalde, "Structural methods for the design and analysis of concurrent systems modeled with Place/Transition nets", PhD Thesis, DIIS, University of Zaragoza, 1998.
[5] H. Huang, "Enhancing the property preserving Petri net process algebra for component-based system design (with application to designing multiagent systems and manufacturing systems)", PhD thesis of City University of Hong Kong, 2004.
[6] K. L. McMillan, "Using unfolding to avoid the state explosion problem in the verification of asynchronous circuits", LNCS 663, Springer- Verlag, pp. 164-177, 1992.
[7] M. Heiner, "Petri net based system analysis without state explosion", In Proceedings of High Performance Computing, Boston, pp. 394-403, 1998.
[8] C. Girault and R. Valk, "Petri Net for System Engineering: A Guide to Modeling, Verification, and Application", Springer-Verlag, Berlin Heidelberg, 2003.
[9] H. Huang, T. Y. Cheung and W. M. Mak, "Structure and behavior preservation by Petri-net-based refinements in system design", Theoretical Computer Science, vol. 328, pp. 245-269, 2004.
[10] X. Ye, J. Zhou, and X. Song, "On reachability graphs of Petri nets", Computers and Electrical Engineering, vol. 29, pp. 263-272, 2003.
[11] P. Godefroid, "Partial-Order Method for the Verification of Concurrent Systems: An Approach to the State-Explosion Problem", LNCS 1032, Springer-Verlag, New York, USA, 1996.
[12] M. Ceska, L. Hasa, and T. Vojnar, "Partial-order reduction in model checking object-oriented Petri nets", Proc. EUROCAST 2003, LNCS 2809, Springer, p.265-278, 2003.
[13] C. Flanagan, and P. Godefroid, "Dynamic partial-order reduction for model checking software", Proc. 32nd ACM symposium on POPL-05, pp. 110-121, 2005.
[14] X. Wang, and M. Kwiatkowska, "Compositional state space reduction using untangled actions", Electronic Notes in Theoretical Computer Science, vol. 175, pp. 27-46, 2007.
[15] A. Valmari, "State of the art report: Stubborn sets", Petri net Newsletter, vol. 46, pp. 6-14, 1994.
[16] K. Schmidt, "Stubborn set for model checking the EF/AG fragment of CTL", Fundamenta Informaticae, vol. 43(1-4), pp. 331-341, 2000.
[17] L. M. Kristensen, K. Schmidt and A. Valmari, "Question-guided stubborn set methods for state properties", Formal Methods in System Design, vol. 29, No. 3, pp. 215-251, 2006.
[18] R. Janicki, and M. Koutny, "Optimal simulations, nets and reachability graphs", In: Rozenberg, G. (Ed.), Advances in Petri Nets: LNCS 524, Springer-Verlag, Berlin, pp. 205-226, 1991.
[19] A. Karatkevich, "Dynamic Analysis of Petri Net-based Discrete Systems", LNCIS, vol. 358, Springer-Verlag, Berlin, 2007.
[20] E. M. Clarke, O. Grumberg, M. Minea and D. A. Peled, "State space reduction using partial order techniques", STTT, vol. 2, No. 3, pp. 279- 287, 1999.
[21] K. Schmidt, "How to calculate symmetries of Petri nets", Acta Informatica, vol. 36, No. 7, pp. 545-590, 2000.
[22] T. Junttila, "New canonical representative marking algorithms for place/transition nets", In: J. Cortadella, W. Reisig (Eds.), ICATPN 2004, LNCS 3099, Springer, Heidelberg, pp. 258-277, 2004.
[23] L. Capra, "Colored Petri nets state-space reduction via symbolic execution", Proc. IEEE International Symposium SYNASC-05, page 231, 2005.
[24] K. Bilinski, "Application of Petri Nets in Parallel Controllers Design", PhD thesis, University of Bristol, 1996.
[25] G. Labiak, "Symbolic state exploration of UML state charts for hardware description", In: A. Adamski, A. Karatkevich, M. Wegrzyn (Eds.), Design of Embedded Control Systems, Springer, NY, pp. 73-83, 2005.
[26] P. Miczulski, "Calculating state space of hierarchical Petri nets using BDD", In: A. Adamski, A. Karatkevich, M. Wegrzyn (Eds.), Design of Embedded Control Systems, Springer, NY, pp. 85-94, 2005.