Structural Place Invariants for Analyzing the Behavioral Properties of Nested Petri Nets

  • Leonid W. Dworzanski
  • Irina A. LomazovaEmail author
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 9698)


Nested Petri nets (NP-nets) is an extension of the Petri nets formalism within the “nets-within-nets” approach. Due to tokens with individual behavior and the mechanism of synchronization NP-nets are convenient for modeling multi-agent and adaptive systems, flexible workflow nets, and other systems with mobile interacting components and dynamic structure.

In contrast to classical Petri nets, there is still a lack of analysis methods for NP-nets. In this paper we show, that the classical Petri nets analysis technique based on place invariants can be extended to NP-nets. This paper defines place invariants of NP-nets, which link several NP-net components and allow to prove crucial behavioral properties directly from the NP-net structure. An algorithm for computing NP-net invariants is presented and illustrated with an example of EJB system verification.


Nested Petri nets Place invariants Behavioral properties Structural analysis methods 


  1. 1.
    Bednarczyk, M.A., Bernardinello, L., Pawłowski, W., Pomello, L.: Modelling mobility with Petri hypernets. In: Fiadeiro, J.L., Mosses, P.D., Orejas, F. (eds.) WADT 2004. LNCS, vol. 3423, pp. 28–44. Springer, Heidelberg (2005). doi: 10.1007/978-3-540-31959-7_2CrossRefGoogle Scholar
  2. 2.
    Bloem, R., et al.: Decidability of parameterized verification. Synth. Lect. Distrib. Comput. Theory 6(1), 1–170 (2015). doi: 10.2200/S00658ED1V01Y201508DCT013CrossRefzbMATHGoogle Scholar
  3. 3.
    Chang, L. et al.: Applying a nested Petri net modeling paradigm to coordination of sensor networks with mobile agents. In: Proceedings of Workshop on Petri Nets and Distributed Systems, Xian, China, pp. 132–145 (2008)Google Scholar
  4. 4.
    Cristini, F., Tessier, C.: Nets-within-nets to model innovative space system architectures. In: Haddad, S., Pomello, L. (eds.) PETRI NETS 2012. LNCS, vol. 7347, pp. 348–367. Springer, Heidelberg (2012). doi: 10.1007/978-3-642-31131-4_19CrossRefGoogle Scholar
  5. 5.
    Desel, J., Neuendorf, K.-P., Radola, M.-D.: Proving nonreachability by modulo-invariants. Theoret. Comput. Sci. 153(1–2), 49–64 (1996). doi: 10.1016/0304-3975(95)00117-4MathSciNetCrossRefzbMATHGoogle Scholar
  6. 6.
    Dworzański, L.W., Lomazova, I.: CPN tools-assisted simulation and verification of nested Petri nets. Autom. Control Comput. Sci. 47(7), 393–402 (2013). doi: 10.3103/S0146411613070201CrossRefGoogle Scholar
  7. 7.
    Dworzański, L.W., Lomazova, I.A.: On compositionality of boundedness and liveness for nested Petri nets. Fundamenta Informaticae 120(3–4), 275–293 (2012). doi: 10.3233/FI-2012-762MathSciNetCrossRefzbMATHGoogle Scholar
  8. 8.
    Genrich, H.J., Lautenbach, K.: The analysis of distributed systems by means of predicate/transition-nets. In: Kahn, G. (ed.) Semantics of Concurrent Computation. LNCS, vol. 70, pp. 123–146. Springer, Heidelberg (1979)CrossRefGoogle Scholar
  9. 9.
    van Hee, K.M., Lomazova, I.A., Oanea, O., Serebrenik, A., Sidorova, N., Voorhoeve, M.: Nested nets for adaptive systems. In: Donatelli, S., Thiagarajan, P.S. (eds.) ICATPN 2006. LNCS, vol. 4024, pp. 241–260. Springer, Heidelberg (2006). doi: 10.1007/11767589_14CrossRefzbMATHGoogle Scholar
  10. 10.
    van Hee, K.M., et al.: Checking properties of adaptive workflow nets. Fundamenta Informaticae 79(3–4), 347–362 (2007)MathSciNetzbMATHGoogle Scholar
  11. 11.
    Hoffmann, K., Ehrig, H., Mossakowski, T.: High-level nets with nets and rules as tokens. In: Ciardo, G., Darondeau, P. (eds.) ICATPN 2005. LNCS, vol. 3536, pp. 268–288. Springer, Heidelberg (2005)CrossRefGoogle Scholar
  12. 12.
    Jensen, K.: Coloured Petri nets and the invariant-method. Theoret. Comput. Sci. 14, 317–336 (1981)MathSciNetCrossRefGoogle Scholar
  13. 13.
    Jensen, K., Kristensen, L.M.: Coloured Petri Nets - Modelling and Validation of Concurrent Systems. Springer, Heidelberg (2009). doi: 10.1007/b95112CrossRefzbMATHGoogle Scholar
  14. 14.
    Kahloul, L., Djouani, K., Chaoui, A.: Formal study of reconfigurable manufacturing systems: a high level Petri nets based approach. In: Mařík, V., Lastra, J.L.M., Skobelev, P. (eds.) HoloMAS 2013. LNCS, vol. 8062, pp. 106–117. Springer, Heidelberg (2013). doi: 10.1007/978-3-642-40090-2_10CrossRefGoogle Scholar
  15. 15.
    Köhler, M., Farwer, B.: Object nets for mobility. In: Kleijn, J., Yakovlev, A. (eds.) ICATPN 2007. LNCS, vol. 4546, pp. 244–262. Springer, Heidelberg (2007). doi: 10.1007/978-3-540-73094-1_16CrossRefzbMATHGoogle Scholar
  16. 16.
    Lautenbach, K.: Linear algebraic techniques for place/transition nets. In: Brauer, W., Reisig, W., Rozenberg, G. (eds.) Petri Nets: Central Models and Their Properties. LNCS, vol. 254, pp. 142–167. Springer, Heidelberg (1986). doi: 10.1007/978-3-540-47919-2_7CrossRefGoogle Scholar
  17. 17.
    Lomazova, I.A.: Modeling dynamic objects in distributed systems with nested Petri nets. Fundamenta Informaticae 51(1–2), 121–133 (2002)MathSciNetzbMATHGoogle Scholar
  18. 18.
    Lomazova, I.A.: Nested Petri nets - a formalism for specification and verification of multi-agent distributed systems. Fundamenta Informaticae 43(1), 195–214 (2000)MathSciNetzbMATHGoogle Scholar
  19. 19.
    Lomazova, I.A.: Nested Petri nets for adaptive process modeling. In: Avron, A., Dershowitz, N., Rabinovich, A. (eds.) Pillars of Computer Science. LNCS, vol. 4800, pp. 460–474. Springer, Heidelberg (2008). doi: 10.1007/978-3-540-78127-1_25CrossRefGoogle Scholar
  20. 20.
    Lomazova, I.A.: Nested Petri nets: multi-level and recursive systems. Fundamenta Informaticae 47(3–4), 283–293 (2001)MathSciNetzbMATHGoogle Scholar
  21. 21.
    Lomazova, I.A., Schnoebelen, P.: Some decidability results for nested Petri nets. In: Bjorner, D., Broy, M., Zamulin, A.V. (eds.) PSI 1999. LNCS, vol. 1755, p. 208. Springer, Heidelberg (2000). doi: 10.1007/3-540-46562-6_18CrossRefGoogle Scholar
  22. 22.
    Lopez-Mellado, E., Almeyda-Canepa, H.: A three-level net formalism for the modelling of multiple mobile robot systems. In: IEEE International Conference on Systems, Man and Cybernetics, vol. 3, pp. 2733–2738 (2003). doi: 10.1109/ICSMC.2003.1244298
  23. 23.
    Lopez-Mellado, E., Villanueva-Paredes, N., Almeyda-Canepa, H.: Modelling of batch production systems using Petri nets with dynamic tokens. Math. Comput. Simul. 67(6), 541–558 (2005). doi: 10.1016/j.matcom.2004.07.005MathSciNetCrossRefzbMATHGoogle Scholar
  24. 24.
    Schmidt, K.: On the computation of place invariants for algebraic Petri nets. In: Desel, J. (ed.) Structures in Concurrency Theory, pp. 310–325. Springer, Heidelberg (1995). doi: 10.1007/978-1-4471-3078-9_21CrossRefGoogle Scholar
  25. 25.
    Tărăbuţă, O.: Use of Petri nets system concept in modeling dynamics with increased complexity. In: 2011 15th International Conference on System Theory, Control, and Computing (ICSTCC), pp. 1–6, October 2011Google Scholar
  26. 26.
    Valk, R.: Object Petri nets using the nets-within-nets paradigm. In: Desel, J., Reisig, W., Rozenberg, G. (eds.) Lectures on Concurrency and Petri Nets. LNCS, vol. 3098, pp. 819–848. Springer, Heidelberg (2004). doi: 10.1007/978-3-540-27755-2_23CrossRefzbMATHGoogle Scholar
  27. 27.
    Venero, M.L.F., da Silva, F.S.C.: Model checking multi-level and recursive nets. Softw. Syst. Model., 1–28 (2016)Google Scholar
  28. 28.
    Zhang, L., Rodrigues, B.: Nested coloured timed Petri nets for production configuration of product families. Int. J. Prod. Res. 48(6), 1805–1833 (2010). doi: 10.1080/00207540802585329CrossRefGoogle Scholar

Copyright information

© Springer International Publishing Switzerland 2016

Open Access This chapter is licensed under the terms of the Creative Commons Attribution-NonCommercial 2.5 International License (, which permits any noncommercial use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons license and indicate if changes were made.

The images or other third party material in this chapter are included in the chapter's Creative Commons license, unless indicated otherwise in a credit line to the material. If material is not included in the chapter's Creative Commons license and your intended use is not permitted by statutory regulation or exceeds the permitted use, you will need to obtain permission directly from the copyright holder.

Authors and Affiliations

  1. 1.National Research University Higher School of EconomicsMoscowRussia

Personalised recommendations