Skip to main content
SpringerLink
Log in

A Normal Form for Stateful Connectors

  • Chapter
  • First Online:
Book cover Logic, Rewriting, and Concurrency

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 9200))

  • 798 Accesses

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

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Notes

  1. 1.

    http://www.ascens-ist.eu/.

  2. 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. 3.

    In the context of C/E nets some authors call places conditions and transitions events.

References

  1. Arbab, F.: Reo: a channel-based coordination model for component composition. Math. Struct. Comp. Sci. 14(3), 329–366 (2004)

    Article  MathSciNet  MATH  Google Scholar 

  2. 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)

    Chapter  Google Scholar 

  3. 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)

    Article  MathSciNet  MATH  Google Scholar 

  4. Basu, A., Bozga, M., Sifakis, J.: Modeling heterogeneous real-time components in BIP. In: SEFM 2006, pp. 3–12. IEEE Computer Society (2006)

    Google Scholar 

  5. Bliudze, S., Sifakis, J.: The algebra of connectors - structuring interaction in BIP. IEEE Trans. Comput. 57(10), 1315–1330 (2008)

    Article  MathSciNet  MATH  Google Scholar 

  6. 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)

    Google Scholar 

  7. Bonchi, F., Sobocinski, P., Zanasi, F.: Full abstraction for signal flow graphs. In: POPL 2015, pp. 515–526. ACM (2015)

    Google Scholar 

  8. Bruni, R., Lanese, I., Montanari, U.: A basic algebra of stateless connectors. Theor. Comput. Sci. 366(1–2), 98–120 (2006)

    Article  MathSciNet  MATH  Google Scholar 

  9. 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)

    Chapter  Google Scholar 

  10. 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)

    Chapter  Google Scholar 

  11. 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)

    Chapter  Google Scholar 

  12. 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)

    Article  MathSciNet  MATH  Google Scholar 

  13. Bruni, R., Meseguer, J., Montanari, U., Sassone, V.: Functorial models for Petri nets. Inf. Comput. 170(2), 207–236 (2001)

    Article  MathSciNet  MATH  Google Scholar 

  14. Degano, P., Meseguer, J., Montanari, U.: Axiomatizing the algebra of net computations and processes. Acta Inf. 33(7), 641–667 (1996)

    Article  MathSciNet  MATH  Google Scholar 

  15. Gadducci, F., Montanari, U.: The tile model. In: Proof, Language, and Interaction, pp. 133–166. The MIT Press (2000)

    Google Scholar 

  16. Hackney, P., Robertson, M.: On the category of props (2012). arXiv:1207.2773

  17. Jongmans, S.S.T., Arbab, F.: Overview of thirty semantic formalisms for Reo. Sci. Ann. Comput. Sci. 22(1), 201–251 (2012)

    MathSciNet  Google Scholar 

  18. Kanellakis, P.C., Smolka, S.A.: CCS expressions, finite state processes, and three problems of equivalence. In: PODC 1983, pp. 228–240. ACM (1983)

    Google Scholar 

  19. 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)

    Google Scholar 

  20. 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)

    Chapter  Google Scholar 

  21. MacLane, S.: Categorical algebra. Bull. AMS 71(1), 40–106 (1965)

    Article  MathSciNet  MATH  Google Scholar 

  22. Meseguer, J., Montanari, U.: Petri nets are monoids. Inf. Comp. 88(2), 105–155 (1990)

    Article  MathSciNet  MATH  Google Scholar 

  23. Meseguer, J., Montanari, U., Sassone, V.: On the semantics of place/transition Petri nets. Math. Struct. Comp. Sci. 7(4), 359–397 (1997)

    Article  MathSciNet  MATH  Google Scholar 

  24. Paige, R., Tarjan, R.E.: Three partition refinement algorithms. SIAM J. Comput. 16(6), 973–989 (1987)

    Article  MathSciNet  MATH  Google Scholar 

  25. Perry, D.E., Wolf, E.L.: Foundations for the study of software architecture. ACM SIGSOFT Soft. Eng. Notes 17, 40–52 (1992)

    Article  Google Scholar 

  26. Petri, C.: Kommunikation mit Automaten. Ph.D. thesis, Institut für Instrumentelle Mathematik, Bonn (1962)

    Google Scholar 

  27. Sobocinski, P.: A non-interleaving process calculus for multi-party synchronisation. In: ICE 2009, EPTCS, vol. 12, pp. 87–98 (2009)

    Google Scholar 

  28. 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)

    Chapter  Google Scholar 

Download references

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

  1. Department of Computer Science, University of Pisa, Pisa, Italy

    Roberto Bruni & Ugo Montanari

  2. Departamento de Computación, FCEyN, Universidad de Buenos Aires - Conicet, Buenos Aires, Argentina

    Hernán Melgratti

Authors
  1. Roberto Bruni
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Hernán Melgratti
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Ugo Montanari
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Roberto Bruni .

Editor information

Editors and Affiliations

  1. Universidad Complutense de Madrid, Madrid, Spain

    Narciso Martí-Oliet

  2. University of Oslo, Oslo, Norway

    Peter Csaba Ölveczky

  3. SRI International, Menlo Park, California, USA

    Carolyn Talcott

Rights and permissions

Reprints 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)

Publish with us

Policies and ethics

Search

Navigation