Abstract
Petri Nets (PN) are a central model for concurrent or distributed systems, but not expressive enough to represent dynamically reconfigurable systems. On the other side, Rewriting Logic has proved to be a natural framework for several formal models of distributed systems. We propose an efficient Maude formalization of dynamically reconfigurable PT nets (with inhibitor arcs), using as a running example a fault-tolerant manufacturing system. We discuss the advantages of such a hybrid approach, as well as some concerns that are raised.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Similar content being viewed by others
Notes
- 1.
A kind is an implicit equivalence class gathering all sorts connected by the subsort relation; terms having a kind but not a sort may be considered as undefined or errors.
- 2.
R rules don’t apply to frozen arguments; in the paper we do not use frozen arguments.
- 3.
Maude uses views to instantiate the type-parameters (theories) of a generic module to concrete modules. In this context, theories and views are very intuitive.
- 4.
S and \(S'\) are isomorphic iff there are a two bijections \(\phi _p: P \rightarrow P'\), \(\phi _t: T \rightarrow T'\), preserving the edges and the initial markings.
- 5.
\(\sigma \) nay be empty is u is a ground term; if r is a conditional rule \(\sigma \) may involve free variables introduced by matching equations used in the rule’s condition.
- 6.
Using the LTL modules we can even check that the initial marking is a home-state.
- 7.
Computed with the GreatSPN tool (github.com/greatspn/SOURCES).
References
Barbosa, P., et al.: SysVeritas: a framework for verifying IOPT nets and execution semantics within embedded systems design. In: Camarinha-Matos, L.M. (ed.) DoCEIS 2011. IAICT, vol. 349, pp. 256–265. Springer, Heidelberg (2011). https://doi.org/10.1007/978-3-642-19170-1_28
Bouhoula, A., Jouannaud, J.P., Meseguer, J.: Specification and proof in membership equational logic. Theor. Comput. Sci. 236(1), 35–132 (2000). https://doi.org/10.1016/S0304-3975(99)00206-6
Bruni, R., Meseguer, J.: Generalized rewrite theories. In: Baeten, J.C.M., Lenstra, J.K., Parrow, J., Woeginger, G.J. (eds.) ICALP 2003. LNCS, vol. 2719, pp. 252–266. Springer, Heidelberg (2003). https://doi.org/10.1007/3-540-45061-0_22
Burstall, R.M., Goguen, J.A.: Algebras, theories and freeness: an introduction for computer scientists. In: Broy, M., Schmidt, G. (eds.) Theoretical Foundations of Programming Methodology: Lecture Notes of an International Summer School, directed by F. L. Bauer, E. W. Dijkstra and C. A. R. Hoare, pp. 329–349. Springer, Dordrecht (1982). https://doi.org/10.1007/978-94-009-7893-5_11
Camilli, M., Capra, L.: Formal specification and verification of decentralized self-adaptive systems using symmetric nets. Discrete Event Dyn. Syst. 31(4), 609–657 (2021). https://doi.org/10.1007/s10626-021-00343-3
Clavel, M., et al.: All About Maude - A High-Performance Logical Framework: How to Specify, Program and Verify Systems in Rewriting Logic. LNCS, vol. 4350. Springer, Heidelberg (2007). https://doi.org/10.1007/978-3-540-71999-1
Ehrig, H., Hoffmann, K., Padberg, J., Prange, U., Ermel, C.: Independence of net transformations and token firing in reconfigurable place/transition systems. In: Kleijn, J., Yakovlev, A. (eds.) ICATPN 2007. LNCS, vol. 4546, pp. 104–123. Springer, Heidelberg (2007). https://doi.org/10.1007/978-3-540-73094-1_9
Ehrig, H., Padberg, J.: Graph grammars and petri net transformations. In: Desel, J., Reisig, W., Rozenberg, G. (eds.) ACPN 2003. LNCS, vol. 3098, pp. 496–536. Springer, Heidelberg (2004). https://doi.org/10.1007/978-3-540-27755-2_14
Kahloul, L., Chaoui, A., Djouani, K.: Modeling and analysis of reconfigurable systems using flexible petri nets. In: Zavoral, F., Yaghob, J., Pichappan, P., El-Qawasmeh, E. (eds.) Networked Digital Technologies, pp. 343–357. Springer, Heidelberg (2010). https://doi.org/10.1109/TASE.2010.28
Köhler-Bußmeier, M.: Hornets: nets within nets combined with net algebra. In: Franceschinis, G., Wolf, K. (eds.) PETRI NETS 2009. LNCS, vol. 5606, pp. 243–262. Springer, Heidelberg (2009). https://doi.org/10.1007/978-3-642-02424-5_15
Llorens, M., Oliver, J.: Structural and dynamic changes in concurrent systems: reconfigurable petri nets. IEEE Trans. Comput. 53(9), 1147–1158 (2004). https://doi.org/10.1109/TC.2004.66
Meseguer, J.: Membership algebra as a logical framework for equational specification. In: Presicce, F.P. (ed.) WADT 1997. LNCS, vol. 1376, pp. 18–61. Springer, Heidelberg (1998). https://doi.org/10.1007/3-540-64299-4_26
Meseguer, J.: Conditional rewriting logic as a unified model of concurrency. Theor. Comput. Sci. 96(1), 73–155 (1992). https://doi.org/10.1016/0304-3975(92)90182-F
Padberg, J., Kahloul, L.: Overview of reconfigurable petri nets. In: Heckel, R., Taentzer, G. (eds.) Graph Transformation, Specifications, and Nets. LNCS, vol. 10800, pp. 201–222. Springer, Cham (2018). https://doi.org/10.1007/978-3-319-75396-6_11
Padberg, J., Schulz, A.: Model checking reconfigurable petri nets with Maude. In: Echahed, R., Minas, M. (eds.) ICGT 2016. LNCS, vol. 9761, pp. 54–70. Springer, Cham (2016). https://doi.org/10.1007/978-3-319-40530-8_4
Prange, U., Ehrig, H., Hoffmann, K., Padberg, J.: Transformations in reconfigurable place/transition systems. In: Degano, P., De Nicola, R., Meseguer, J. (eds.) Concurrency, Graphs and Models: Essays Dedicated to Ugo Montanari on the Occasion of His 65th Birthday. LNCS, vol. 5065, pp. 96–113. Springer, Heidelberg (2008). https://doi.org/10.1007/978-3-540-68679-8_7
Reisig, W.: Petri Nets: An Introduction. Springer-Verlag, New York Inc., New York (1985). https://doi.org/10.1007/978-3-642-69968-9
Stehr, M.-O., Meseguer, J., Ölveczky, P.C.: Rewriting logic as a unifying framework for petri nets. In: Ehrig, H., Padberg, J., Juhás, G., Rozenberg, G. (eds.) Unifying Petri Nets. LNCS, vol. 2128, pp. 250–303. Springer, Heidelberg (2001). https://doi.org/10.1007/3-540-45541-8_9
Valk, R.: Object petri nets. In: Desel, J., Reisig, W., Rozenberg, G. (eds.) ACPN 2003. LNCS, vol. 3098, pp. 819–848. Springer, Heidelberg (2004). https://doi.org/10.1007/978-3-540-27755-2_23
Viola, E.: E-unifiability via narrowing. In: ICTCS 2001. LNCS, vol. 2202, pp. 426–438. Springer, Heidelberg (2001). https://doi.org/10.1007/3-540-45446-2_27
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2022 Springer Nature Switzerland AG
About this paper
Cite this paper
Capra, L. (2022). Rewriting Logic and Petri Nets: A Natural Model for Reconfigurable Distributed Systems. In: Bapi, R., Kulkarni, S., Mohalik, S., Peri, S. (eds) Distributed Computing and Intelligent Technology. ICDCIT 2022. Lecture Notes in Computer Science(), vol 13145. Springer, Cham. https://doi.org/10.1007/978-3-030-94876-4_9
Download citation
DOI: https://doi.org/10.1007/978-3-030-94876-4_9
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-030-94875-7
Online ISBN: 978-3-030-94876-4
eBook Packages: Computer ScienceComputer Science (R0)