Structural Place Invariants for Analyzing the Behavioral Properties of Nested Petri Nets
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.
KeywordsNested Petri nets Place invariants Behavioral properties Structural analysis methods
- 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
- 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
- 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
- 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
- 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
Open Access This chapter is licensed under the terms of the Creative Commons Attribution-NonCommercial 2.5 International License (http://creativecommons.org/licenses/by-nc/2.5/), 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.