Abstract
The nested Petri nets are a nets-within-nets formalism convenient for modelling systems that consist of distributed mobile agents with individual behaviour. The formalism is supported by developed verification methods based on structural analysis and model checking techniques. Time constraints are crucial for many safety critical and everyday IoT systems. Recently, the non Turing-complete time semantics for Time Petri nets based on restricted urgency was suggested; and, it was shown that some behavioural analysis problems are decidable under the semantics. In the paper, the semantics is extended to the nested Petri nets formalism and it was demonstrated that some behavioural analysis problems are still decidable. The semantics is illustrated by an example of a health monitoring system.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
References
A Fleet of Self-Driving Trucks Just Completed a 1,000-Mile Trip Across Europe, 7 April 2016. http://www.popularmechanics.com
Akshay, S., Genest, B., Hélouët, L.: Timed-arc petri nets with (restricted) urgency. In: Proceedings of Application and Theory of Petri Nets and Concurrency - 37th International Conference, PETRI NETS, Torun, Poland, 19–24 June 2016. Springer, Berlin Heidelberg (2016)
Baeten, J.C.M., Middelburg, C.A.: Process Algebra with Timing. Springer, Heidelberg (2013)
Bérard, B., Cassez, F., Haddad, S., Lime, D., Roux, O.H.: Comparison of different semantics for time petri nets. In: Peled, D.A., Tsay, Y.-K. (eds.) ATVA 2005. LNCS, vol. 3707, pp. 293–307. Springer, Heidelberg (2005)
Brown, C., Gurr, D.: Timing petri nets categorically. In: Kuich, W. (ed.) ICALP 1992. LNCS, vol. 623, pp. 571–582. Springer, Heidelberg (1992)
Chang, L., et al.: Applying a nested petri net modeling paradigm to coordination of sensor networks with mobile agents. In: Proceedings of PNDS 2008, Xian, China, pp. 132–45 (2008)
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)
Dworzanski, L.W., Lomazova, I.A.: Structural place invariants for analyzing the behavioral properties of nested petri nets. In: Kordon, F., Moldt, D. (eds.) PETRI NETS 2016. LNCS, vol. 9698, pp. 325–344. Springer, Heidelberg (2016). doi:10.1007/978-3-319-39086-4_19
Dworzański, L.W., Lomazova, I.A.: CPN tools-assisted simulation and verification of nested petri nets. Autom. Control Comput. Sci. 47(7), 393–402 (2013)
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)
Dworzanski, L., Frumin, D.: NPNtool: modelling and analysis toolset for nested petri nets. In: Proceedings of SYRCoSE 2013, pp. 9–14 (2013)
Finkel, A., Schnoebelen, P.: Well-structured transition systems everywhere!. Theor. Comput. Sci. 256(1–2), 63–92 (2001)
van Hee, K.M., et al.: Checking properties of adaptive workflow nets. Fundamenta Informaticae 79(3–4), 347–362 (2007)
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)
Jensen, K., Kristensen, L.M.: Coloured Petri Nets - Modelling and Validation of Concurrent Systems. Springer, Heidelberg (2009)
Jones, N.D., Landweber, L.H., Lien, Y.E.: Complexity of some problems in petri nets. Theor. Comput. Sci. 4(3), 277–299 (1977)
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)
Lomazova, I.A.: Nested petri nets - a formalism for specification and verification of multi-agent distributed systems. Fundamenta Informaticae 43(1), 195–214 (2000)
Lomazova, I.A.: Nested petri nets: multi-level and recursive systems. Fundamenta Informaticae 47(3–4), 283–293 (2001)
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, October 2003
Nicollin, X., Sifakis, J.: An overview and synthesis on timed process algebras. In: de Bakker, J.W., Huizing, C., de Roever, W.P., Rozenberg, G. (eds.) REX 1991. LNCS, vol. 600, pp. 526–548. Springer, Heidelberg (1991)
Popova-Zeugmann, L.: Time and Petri Nets. Springer, Heidelberg (2013)
Ramchandani, C.: Analysis of asynchronous concurrent systems by timed petri nets. Technical report, Cambridge (1974)
Valk, R.: Object petri nets. In: Desel, J., Reisig, W., Rozenberg, G. (eds.) Lectures on Concurrency and Petri Nets. LNCS, vol. 3098, pp. 819–848. Springer, Heidelberg (2004)
Valk, R.: Petri nets as token objects: an introduction to elementary object nets. In: Desel, J., Silva, M. (eds.) ICATPN 1998. LNCS, vol. 1420, pp. 1–25. Springer, Heidelberg (1998)
Venero, M.L.F., da Silva, F.S.C.: Model checking multi-level and recursive nets. Softw. Syst. Model. 15, 1–28 (2016)
Acknowledgments
This work is supported by Russian Foundation for Basic Research, project No. 16-37-00482 mol_a.
The authors would like to thank three anonymous referees for the very helpful and insightful comments.
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2016 Springer International Publishing Switzerland
About this paper
Cite this paper
Dworzanski, L.W. (2016). Consistent Timed Semantics for Nested Petri Nets with Restricted Urgency. In: Fränzle, M., Markey, N. (eds) Formal Modeling and Analysis of Timed Systems. FORMATS 2016. Lecture Notes in Computer Science(), vol 9884. Springer, Cham. https://doi.org/10.1007/978-3-319-44878-7_1
Download citation
DOI: https://doi.org/10.1007/978-3-319-44878-7_1
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-44877-0
Online ISBN: 978-3-319-44878-7
eBook Packages: Computer ScienceComputer Science (R0)