Bigraphs for Petri Nets

  • Robin Milner
Part of the Lecture Notes in Computer Science book series (LNCS, volume 3098)


A simple example is given of the use of bigraphical reactive systems (BRSs). It provides a behavioural semantics for condition-event Petri nets whose interfaces are named condition nodes, using a simple form of BRS equipped with a labelled transition system and its associated bisimilarity equivalence. Both of the latter are derived from the standard net firing rules by a uniform technique in bigraphs, which also ensures that the bisimilarity is a congruence. Furthermore, this bisimilarity is shown to coincide with one induced by a natural notion of experiment on condition-event nets, defined independently of bigraphs.

The paper is intended as a bridge between Petri net theory and bigraphs, as well as a pedagogical exercise in the latter.


Transition System Label Transition System Outer Face Semantic Function Open Link 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    Best, E., Devillers, R., Hall, J.G.: The box algebra: a model of nets and process expressions. In: Donatelli, S., Kleijn, J. (eds.) ICATPN 1999. LNCS, vol. 1639, pp. 344–363. Springer, Heidelberg (1999)CrossRefGoogle Scholar
  2. 2.
    Cardelli, L., Gordon, A.D.: Mobile ambients. In: Nivat, M. (ed.) FOSSACS 1998. LNCS, vol. 1378, pp. 140–155. Springer, Heidelberg (2000)CrossRefGoogle Scholar
  3. 3.
    Jensen, O.-H., Milner, R.: Bigraphs and transitions. In: Proc. 30th SIGPLAN-SIGACT Symposium on Principles of Programming Languages (2003)Google Scholar
  4. 4.
    Jensen, O.-H., Milner, R.: Bigraphs and mobile processes. Technical Report UCAMCL- TR-570, University of Cambridge Computer Laboratory (2003), Also available at, together with an index and slides
  5. 5.
    Leifer, J.J., Milner, R.: Deriving bisimulation congruences for reactive systems. In: Palamidessi, C. (ed.) CONCUR 2000. LNCS, vol. 1877, pp. 243–258. Springer, Heidelberg (2000)CrossRefGoogle Scholar
  6. 6.
    Milner, R.: Calculi for interaction. Acta Informatica 33, 707–737 (1996)MathSciNetGoogle Scholar
  7. 7.
    Milner, R., Parrow, J., Walker, D.: A calculus of mobile processes, Parts I and II. Journal of Information and Computation 100, 1–77 (1992)zbMATHCrossRefMathSciNetGoogle Scholar
  8. 8.
    Park, D.: Concurrency and automata on infinite sequences. In: Deussen, P. (ed.) GI-TCS 1981. LNCS, vol. 104, Springer, Heidelberg (1980)Google Scholar
  9. 9.
    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)Google Scholar
  10. 10.
    Pomello, L., Rozenberg, G., Simone, C.: A survey of equivalence notions for net-based systems. In: Rozenberg, G. (ed.) APN 1992. LNCS, vol. 609, pp. 410–472. Springer, Heidelberg (1992)Google Scholar
  11. 11.
    Priese, L., Wimmel, H.: A uniform approach to true-concurrency and interleaving semantics for Petri nets. Theoretical Computer Science 206, 206–219 (1998)CrossRefMathSciNetGoogle Scholar
  12. 12.
    Reisig, W.: Petri Nets: an Introduction. In: Rozenberg, G. (ed.) APN 1985. LNCS, vol. 222. Springer, Heidelberg (1985)Google Scholar
  13. 13.
    Sassone, V., Sobocinski, P.: Deriving bisimulation congruences: 2-categories vs. precategories. In: Gordon, A.D. (ed.) FOSSACS 2003. LNCS, vol. 2620, pp. 409–424. Springer, Heidelberg (2003)CrossRefGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2004

Authors and Affiliations

  • Robin Milner
    • 1
  1. 1.The Computer LaboratoryUniversity of CambridgeCambridgeUK

Personalised recommendations