Abstract
We propose a framework for the specification of behaviour-preserving reconfigurations of systems modelled as Petri nets. The framework is based on open nets, a mild generalisation of ordinary Place/ Transition nets suited to model open systems which might interact with the surrounding environment and endowed with a colimit-based composition operation. We show that natural notions of (strong and weak) bisimilarity over open nets are congruences with respect to the composition operation. We also provide an up-to technique for facilitating bisimilarity proofs. The theory is used to identify suitable classes of reconfiguration rules (in the double-pushout approach to rewriting) whose application preserves the observational semantics of the net.
Research partially supported by the EU IST-2004-16004 SEnSOria, the MIUR Project ART, the DFG project SANDS and CRUI/DAAD Vigoni “Models based on Graph Transformation Systems: Analysis and Verification”.
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
Preview
Unable to display preview. Download preview PDF.
References
Badouel, E., Llorens, M., Oliver, J.: Modeling concurrent systems: Reconfigurable nets. In: Proc. of PDPTA 2003, vol. 4, pp. 1568–1574. CSREA Press (2003)
Baldan, P., Corradini, A., Ehrig, H., Heckel, R.: Compositional modeling of reactive systems using open nets. In: Larsen, K.G., Nielsen, M. (eds.) CONCUR 2001. LNCS, vol. 2154, pp. 502–518. Springer, Heidelberg (2001)
Baldan, P., Corradini, A., Ehrig, H., Heckel, R.: Compositional semantics for open Petri nets based on deterministic processes. Mathematical Structures in Computer Science 15(1), 1–35 (2004)
Baldan, P., Corradini, A., Ehrig, H., Heckel, R., König, B.: Bisimilarity and behaviour-preserving reconfigurations of open Petri nets. Technical Report CS-2006-9, Computer Science Department, University Ca’ Foscari of Venice (2006)
Bednarczyk, A.M., Borzyszkowski, M.A.: General morphisms of Petri nets. In: Wiedermann, J., van Emde Boas, P., Nielsen, M. (eds.) ICALP 1999. LNCS, vol. 1644, pp. 190–199. Springer, Heidelberg (1999)
Best, E., Devillers, R., Hall, J.G.: The Petri box calculus: a new causal algebra with multi-label communication. In: Rozenberg, G. (ed.) Advances in Petri Nets 1992. LNCS, vol. 609, pp. 21–69. Springer, Heidelberg (1992)
Bonchi, F., Brogi, A., Corfini, S., Gadducci, F.: A behavioural congruence for web services. In: Proc. of FSEN 2007. LNCS, Springer, Heidelberg (2007)
Buscemi, M.G., Sassone, V.: High-level Petri nets as type theories in the join calculus. In: Honsell, F., Miculan, M. (eds.) ETAPS 2001 and FOSSACS 2001. LNCS, vol. 2030, Springer, Heidelberg (2001)
Ehrig, H.: Tutorial introduction to the algebraic approach of graph-grammars. In: Ehrig, H., Nagl, M., Rosenfeld, A., Rozenberg, G. (eds.) Graph-Grammars and Their Application to Computer Science. LNCS, vol. 291, pp. 3–14. Springer, Heidelberg (1987)
Kindler, E.: A compositional partial order semantics for Petri net components. In: Azéma, P., Balbo, G. (eds.) ICATPN 1997. LNCS, vol. 1248, pp. 235–252. Springer, Heidelberg (1997)
Lack, S., Sobociński, P.: Adhesive and quasiadhesive categories. RAIRO – Theoretical Informatics and Applications 39(3) (2005)
Leifer, J., Milner, R.: Deriving bisimulation congruences for reactive systems. In: Palamidessi, C. (ed.) CONCUR 2000. LNCS, vol. 1877, pp. 243–258. Springer, Heidelberg (2000)
Llorens, M., Oliver, J.: Introducing structural dynamic changes in Petri nets: Marked-controlled reconfigurable nets. In: Wang, F. (ed.) ATVA 2004. LNCS, vol. 3299, pp. 310–323. Springer, Heidelberg (2004)
Milner, R.: Bigraphical reactive systems. In: Larsen, K.G., Nielsen, M. (eds.) CONCUR 2001. LNCS, vol. 2154, pp. 16–35. Springer, Heidelberg (2001)
Milner, R.: Bigraphs for Petri nets. In: Desel, J., Reisig, W., Rozenberg, G. (eds.) Lectures on Concurrency and Petri Nets. LNCS, vol. 3098, pp. 686–701. Springer, Heidelberg (2004)
Milner, R.: A Calculus of Communication Systems. LNCS, vol. 92. Springer, Heidelberg (1980)
Nielsen, M., Priese, L., Sassone, V.: Characterizing Behavioural Congruences for Petri Nets. In: Lee, I., Smolka, S.A. (eds.) CONCUR 1995. LNCS, vol. 962, pp. 175–189. Springer, Heidelberg (1995)
Padberg, J., Ehrig, H., Ribeiro, L.: High level replacement systems applied to algebraic high level net transformation systems. Mathematical Structures in Computer Science 5(2), 217–256 (1995)
Reisig, W.: Petri Nets: An Introduction. In: EATCS Monographs, Springer, Heidelberg (1985)
Sassone, V., Sobociński, P.: A congruence for Petri nets. In: Alternating Sequential-Parallel Processing. Electronic Notes in Computer Science, vol. 127(2), pp. 107–120. Elsevier, Amsterdam (1982)
Vogler, W.: Executions: A new partial-order semantics of Petri nets. Theoretical Computer Science 91(2), 205–238 (1991)
Winskel, G.: Event structures. In: Brauer, W., Reisig, W., Rozenberg, G. (eds.) Advances in Petri Nets 1986. Proceedings of an Advanced Course, Bad Honnef. LNCS, vol. 255, pp. 325–392. Springer, Heidelberg (1987)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2007 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Baldan, P., Corradini, A., Ehrig, H., Heckel, R., König, B. (2007). Bisimilarity and Behaviour-Preserving Reconfigurations of Open Petri Nets . In: Mossakowski, T., Montanari, U., Haveraaen, M. (eds) Algebra and Coalgebra in Computer Science. CALCO 2007. Lecture Notes in Computer Science, vol 4624. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-73859-6_9
Download citation
DOI: https://doi.org/10.1007/978-3-540-73859-6_9
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-73857-2
Online ISBN: 978-3-540-73859-6
eBook Packages: Computer ScienceComputer Science (R0)