Bigraphs for Petri Nets
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.
KeywordsTransition System Label Transition System Outer Face Semantic Function Open Link
Unable to display preview. Download preview PDF.
- 3.Jensen, O.-H., Milner, R.: Bigraphs and transitions. In: Proc. 30th SIGPLAN-SIGACT Symposium on Principles of Programming Languages (2003)Google Scholar
- 4.Jensen, O.-H., Milner, R.: Bigraphs and mobile processes. Technical Report UCAMCL- TR-570, University of Cambridge Computer Laboratory (2003), Also available at http://www.cl.cam.ac.uk/users/rm135, together with an index and slides
- 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.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.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
- 12.Reisig, W.: Petri Nets: an Introduction. In: Rozenberg, G. (ed.) APN 1985. LNCS, vol. 222. Springer, Heidelberg (1985)Google Scholar