Advertisement

Place Bisimulation and Liveness for Open Petri Nets

  • Xiaoju DongEmail author
  • Yuxi Fu
  • Daniele Varacca
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 9984)

Abstract

Petri nets are a kind of concurrent models for distributed and asynchronous systems. However they can only model closed systems, but not open ones. We extend Petri nets to model open systems. In Open Petri Nets, the way of interaction is achieved by composing nets. Some places with labels, called open or external, are considered as an interface with environment. Every external places are both input and output ones. Two such open Petri nets can be composed by joining the external places with the same label. In addition, we focus on the operational semantics of open nets and study observational properties, especially bisimulation properties. We define place bisimulations on nets with external places. It turns out that the largest bisimulation, i.e. the bisimilarity, is a congruence. A further result is that liveness is preserved by bisimilarity.

Keywords

Open Petri net Interaction Bisimulation Liveness 

Notes

Acknowledgments

The work is supported by the National Nature Science Foundation of China(61472239, 61100053). The authors would like to thank the unknown reviewers for the comments.

References

  1. 1.
    van der Aalst, W.M.P.: Pi calculus versus petri nets: let us eat humble pie rather than further inflate the pi hype (2003)Google Scholar
  2. 2.
    Baldan, P., Bonchi, F., Gadducci, F.: Encoding asynchronous interactions using open petri nets. In: Bravetti, M., Zavattaro, G. (eds.) CONCUR 2009. LNCS, vol. 5710, pp. 99–114. Springer, Heidelberg (2009). doi: 10.1007/978-3-642-04081-8_8 CrossRefGoogle Scholar
  3. 3.
    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). doi: 10.1007/3-540-44685-0_34 CrossRefGoogle Scholar
  4. 4.
    Baldan, P., Corradini, A., Ehrig, H., Heckel, R.: Compositional semantics for open petri nets based on deterministic processes. Math. Struct. Comput. Sci. 15(1), 1–35 (2005)MathSciNetCrossRefzbMATHGoogle Scholar
  5. 5.
    Baldan, P., Corradini, A., Ehrig, H., Heckel, R., König, B.: Bisimilarity and behaviour-preserving reconfigurations of open petri nets. In: Mossakowski, T., Montanari, U., Haveraaen, M. (eds.) CALCO 2007. LNCS, vol. 4624, pp. 126–142. Springer, Heidelberg (2007). doi: 10.1007/978-3-540-73859-6_9 CrossRefGoogle Scholar
  6. 6.
    Baldan, P., Corradini, A., Ehrig, H., König, B.: Open petri nets: non-deterministic processes and compositionality. In: Ehrig, H., Heckel, R., Rozenberg, G., Taentzer, G. (eds.) ICGT 2008. LNCS, vol. 5214, pp. 257–273. Springer, Heidelberg (2008). doi: 10.1007/978-3-540-87405-8_18 CrossRefGoogle Scholar
  7. 7.
    Best, E., Devillers, R., Hall, J.G.: The 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). doi: 10.1007/3-540-55610-9_167 CrossRefGoogle Scholar
  8. 8.
    Best, E., Devillers, R., Koutny, M.: A unified model for nets and process algebras. In: Bergstra, J., Ponse, A., Smolka, S. (eds.) Handbook of Process Algebra, pp. 875–944. Elsevier Science, Amsterdam (2001)Google Scholar
  9. 9.
    Busi, N., Gorrieri, R.: A Petri net semantics for pi-calculus. In: Lee, I., Smolka, S.A. (eds.) CONCUR 1995. LNCS, vol. 962, pp. 145–159. Springer, Heidelberg (1995). doi: 10.1007/3-540-60218-6_11 CrossRefGoogle Scholar
  10. 10.
    Busi, N., Gorrieri, R.: Distributed semantics for the -calculus based on Petri nets with inhibitor arcs. J. Logic Algebraic Programm. 78(3), 138–162 (2009)MathSciNetCrossRefzbMATHGoogle Scholar
  11. 11.
    Bergstra, J.A., Klop, J.W.: The algebra of recursively defined processes and the algebra of regular processes. In: Paredaens, J. (ed.) ICALP 1984. LNCS, vol. 172, pp. 82–94. Springer, Heidelberg (1984). doi: 10.1007/3-540-13345-3_7 CrossRefGoogle Scholar
  12. 12.
    Cao, M., Wu, Z., Yang, G.: Pi net - a new modular higher petri net. J. Shanghai Jiaotong Univ. 38(1), 52–58 (2004). in ChineseMathSciNetGoogle Scholar
  13. 13.
    Devillers, R., Klaudel, H., Koutny, M.: Petri net semantics of the finite pi-calculus. In: Frutos-Escrig, D., Núñez, M. (eds.) FORTE 2004. LNCS, vol. 3235, pp. 309–325. Springer, Heidelberg (2004). doi: 10.1007/978-3-540-30232-2_20 CrossRefGoogle Scholar
  14. 14.
    Degano, P., Nicola, R.D., Montanari, U.: A distributed operational semantics for CCS based on C/E systems. Acta Informatica 26(1–2), 59–91 (1988)MathSciNetCrossRefzbMATHGoogle Scholar
  15. 15.
    Fu, Y., Lv, H.: On the expressiveness of interaction. Theoret. Comput. Sci. 411, 1387–1451 (2010)MathSciNetCrossRefzbMATHGoogle Scholar
  16. 16.
    Fu, Y.: Theory of interaction. Theoret. Comput. Sci. 611, 1–49 (2016)MathSciNetCrossRefzbMATHGoogle Scholar
  17. 17.
    Guo, X., Hao, K., Hou, H., Ding, J.: The representation of petri nets with prohibition arcs by Pi+ calculus. J. Syst. Simul. S2, 9–12 (2002)Google Scholar
  18. 18.
    Goltz, U.: CCS and petri nets. In: Guessarian, I. (ed.) LITP 1990. LNCS, vol. 469, pp. 334–357. Springer, Heidelberg (1990). doi: 10.1007/3-540-53479-2_14 CrossRefGoogle Scholar
  19. 19.
    Hao, K.: Open nets - a model for interative concurrent systems. J. Northwest Univ. (Nat. Sci. Ed.) 27(6), 461–466 (1997)Google Scholar
  20. 20.
    Hoare, C.A.R.: Communicating Sequential Processes. Commun. ACM 21(8), 666–677 (1978)CrossRefzbMATHGoogle Scholar
  21. 21.
    Koutny, M., Best, E.: Operational and denotational semantics for the box algebra. Theoret. Comput. Sci. 211(1–2), 1–83 (1999)MathSciNetCrossRefzbMATHGoogle Scholar
  22. 22.
    Koutny, M., Esparza, J., Best, E.: Operational semantics for the petri box calculus. In: Jonsson, B., Parrow, J. (eds.) CONCUR 1994. LNCS, vol. 836, pp. 210–225. Springer, Heidelberg (1994). doi: 10.1007/978-3-540-48654-1_19 CrossRefGoogle Scholar
  23. 23.
    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). doi: 10.1007/3-540-63139-9_39 CrossRefGoogle Scholar
  24. 24.
    Liu, G., Jiang, C., Zhou, M.: Interactive petri nets. IEEE Trans. Syst. Man Cybern. Syst. 43(2), 291–302 (2013)CrossRefGoogle Scholar
  25. 25.
    Milner, R.: A Calculus of Communicating systems. LNCS. Springer, Berlin (1980)CrossRefzbMATHGoogle Scholar
  26. 26.
    Meseguer, J., Montanari, U.: Petri nets are monoids. Inf. Comput. 88, 105–155 (1990)MathSciNetCrossRefzbMATHGoogle Scholar
  27. 27.
    Milner, R., Parrow, J., Walker, D.: A calculus of mobile processes. Inf. Comput. 100, 1–40(Part I), 41–77 (Part II) (1992)Google Scholar
  28. 28.
    Nielsen, M.: CCS — and its relationship to net theory. In: Brauer, W., Reisig, W., Rozenberg, G. (eds.) ACPN 1986. LNCS, vol. 255, pp. 393–415. Springer, Heidelberg (1987). doi: 10.1007/3-540-17906-2_32 CrossRefGoogle Scholar
  29. 29.
    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). doi: 10.1007/3-540-60218-6_13 CrossRefGoogle Scholar
  30. 30.
    Peterson, J.L.: Petri Net Theory and the Modelling of Systems. Prentice Hall, Englewood Cliffs (1981)zbMATHGoogle Scholar
  31. 31.
    Priese, L., Wimmel, H.: A uniform approach to true-concurrency and interleaving semantics for Petri nets. Theoret. Comput. Sci. 206(1–2), 219–256 (1998)MathSciNetCrossRefzbMATHGoogle Scholar
  32. 32.
    Winskel, G.: Event structures. In: Brauer, W., Reisig, W., Rozenberg, G. (eds.) ACPN 1986. LNCS, vol. 255, pp. 325–392. Springer, Heidelberg (1987). doi: 10.1007/3-540-17906-2_31 CrossRefGoogle Scholar
  33. 33.
    Yu, Z., Cai, Y., Xu, H.: Petri net semantics for Pi Calculus. Control Decis. 22(8), 864–868 (2007). in ChineseMathSciNetGoogle Scholar

Copyright information

© Springer International Publishing AG 2016

Authors and Affiliations

  1. 1.BASICS, Department of Computer ScienceShanghai Jiao Tong UniversityShanghaiChina
  2. 2.PPS - CNRS and Université Paris DiderotParisFrance

Personalised recommendations