Abstract
In this paper we consider a calculus of connectors that allows for the most general combination of synchronisation, non-determinism and buffering. According to previous results, this calculus is tightly related to a flavour of Petri nets with interfaces for composition, called Petri nets with boundaries. The calculus and the net version are equipped with equivalent bisimilarity semantics. Also the buffers (the net places) can be one-place (C/E nets) or with unlimited capacity (P/T nets). In the paper we investigate the idea of finding normal form representations for terms of this calculus, in the sense that equivalent (bisimilar) terms should have the same (isomorphic) normal form. We show that this is possible for finite state terms. The result is obtained by computing the minimal marking graph (when finite) for the net with boundaries corresponding to the given term, and reconstructing from it a canonical net and a canonical term.
This research was supported by the EU project IP 257414 (ASCENS), EU 7th FP under grant agreement no. 295261 (MEALS), by the Italian MIUR Project CINA (PRIN 2010/11), and by the UBACyT Project 20020130200092BA.
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.
- 2.
Formally, a net is bounded if \(\exists k\in \mathbb {N}\) such that in any reachable marking the number of tokens in any place is less than or equal to k, i.e., k is a bound for the capacity of places. Note that the marking graph of a net is finite iff the net is bounded.
- 3.
In the context of C/E nets some authors call places conditions and transitions events.
References
Arbab, F.: Reo: a channel-based coordination model for component composition. Math. Struct. Comp. Sci. 14(3), 329–366 (2004)
Arbab, F., Bruni, R., Clarke, D., Lanese, I., Montanari, U.: Tiles for Reo. In: Corradini, A., Montanari, U. (eds.) WADT 2008. LNCS, vol. 5486, pp. 37–55. Springer, Heidelberg (2009)
Baldan, P., Corradini, A., Ehrig, H., Heckel, R.: Compositional semantics for open Petri nets based on deterministic processes. Math. Struct. Comp. Sci. 15(1), 1–35 (2005)
Basu, A., Bozga, M., Sifakis, J.: Modeling heterogeneous real-time components in BIP. In: SEFM 2006, pp. 3–12. IEEE Computer Society (2006)
Bliudze, S., Sifakis, J.: The algebra of connectors - structuring interaction in BIP. IEEE Trans. Comput. 57(10), 1315–1330 (2008)
Bonchi, F., Sobociński, P., Zanasi, F.: A categorical semantics of signal flow graphs. In: Baldan, P., Gorla, D. (eds.) CONCUR 2014. LNCS, vol. 8704, pp. 435–450. Springer, Heidelberg (2014)
Bonchi, F., Sobocinski, P., Zanasi, F.: Full abstraction for signal flow graphs. In: POPL 2015, pp. 515–526. ACM (2015)
Bruni, R., Lanese, I., Montanari, U.: A basic algebra of stateless connectors. Theor. Comput. Sci. 366(1–2), 98–120 (2006)
Bruni, R., Melgratti, H., Montanari, U.: A connector algebra for P/T nets interactions. In: Katoen, J.-P., König, B. (eds.) CONCUR 2011. LNCS, vol. 6901, pp. 312–326. Springer, Heidelberg (2011)
Bruni, R., Melgratti, H., Montanari, U.: Connector algebras, Petri nets, and BIP. In: Clarke, E., Virbitskaite, I., Voronkov, A. (eds.) PSI 2011. LNCS, vol. 7162, pp. 19–38. Springer, Heidelberg (2012)
Bruni, R., Melgratti, H., Montanari, U.: Behaviour, interaction and dynamics. In: Iida, S., Meseguer, J., Ogata, K. (eds.) Specification, Algebra, and Software. LNCS, vol. 8373, pp. 382–401. Springer, Heidelberg (2014)
Bruni, R., Melgratti, H.C., Montanari, U., Sobocinski, P.: Connector algebras for C/E and P/T nets’ interactions. Log. Methods Comput. Sci. 9(3), 1–65 (2013)
Bruni, R., Meseguer, J., Montanari, U., Sassone, V.: Functorial models for Petri nets. Inf. Comput. 170(2), 207–236 (2001)
Degano, P., Meseguer, J., Montanari, U.: Axiomatizing the algebra of net computations and processes. Acta Inf. 33(7), 641–667 (1996)
Gadducci, F., Montanari, U.: The tile model. In: Proof, Language, and Interaction, pp. 133–166. The MIT Press (2000)
Hackney, P., Robertson, M.: On the category of props (2012). arXiv:1207.2773
Jongmans, S.S.T., Arbab, F.: Overview of thirty semantic formalisms for Reo. Sci. Ann. Comput. Sci. 22(1), 201–251 (2012)
Kanellakis, P.C., Smolka, S.A.: CCS expressions, finite state processes, and three problems of equivalence. In: PODC 1983, pp. 228–240. ACM (1983)
Katis, P., Sabadini, N., Walters, R.F.C.: Representing place/transition nets in Span(Graph). In: Johnson, M. (ed.) AMAST 1997. LNCS, vol. 1349. Springer, Heidelberg (1997)
Katis, P., Sabadini, N., Walters, R.F.C.: Representing place/transition nets in Span(Graph). In: Johnson, M. (ed.) AMAST 1997. LNCS, vol. 1349, pp. 322–336. Springer, Heidelberg (1997)
MacLane, S.: Categorical algebra. Bull. AMS 71(1), 40–106 (1965)
Meseguer, J., Montanari, U.: Petri nets are monoids. Inf. Comp. 88(2), 105–155 (1990)
Meseguer, J., Montanari, U., Sassone, V.: On the semantics of place/transition Petri nets. Math. Struct. Comp. Sci. 7(4), 359–397 (1997)
Paige, R., Tarjan, R.E.: Three partition refinement algorithms. SIAM J. Comput. 16(6), 973–989 (1987)
Perry, D.E., Wolf, E.L.: Foundations for the study of software architecture. ACM SIGSOFT Soft. Eng. Notes 17, 40–52 (1992)
Petri, C.: Kommunikation mit Automaten. Ph.D. thesis, Institut für Instrumentelle Mathematik, Bonn (1962)
Sobocinski, P.: A non-interleaving process calculus for multi-party synchronisation. In: ICE 2009, EPTCS, vol. 12, pp. 87–98 (2009)
Sobociński, P.: Representations of Petri net interactions. In: Gastin, P., Laroussinie, F. (eds.) CONCUR 2010. LNCS, vol. 6269, pp. 554–568. Springer, Heidelberg (2010)
Acknowledgements
We thank the anonymous reviewers for their careful reading and helpful suggestions for improving the presentation. We would like to express infinite gratitude to José, for his guidance, support and friendship during our long-standing collaboration.
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2015 Springer International Publishing Switzerland
About this chapter
Cite this chapter
Bruni, R., Melgratti, H., Montanari, U. (2015). A Normal Form for Stateful Connectors. In: Martí-Oliet, N., Ölveczky, P., Talcott, C. (eds) Logic, Rewriting, and Concurrency. Lecture Notes in Computer Science(), vol 9200. Springer, Cham. https://doi.org/10.1007/978-3-319-23165-5_9
Download citation
DOI: https://doi.org/10.1007/978-3-319-23165-5_9
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-23164-8
Online ISBN: 978-3-319-23165-5
eBook Packages: Computer ScienceComputer Science (R0)