A Technique for Reachability Graph Generation for the Petri Net Models of Parallel Processes
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.
[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.
[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.
@article{"International Journal of Information, Control and Computer Sciences:63511", author = "Farooq Ahmad and Hejiao Huang and Xiaolong Wang", title = "A Technique for Reachability Graph Generation for the Petri Net Models of Parallel Processes", 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.", volume = "3", number = "3", pages = "808-5", }
