Bigraph

Aside from nodes and (hyper-)edges, a bigraph may have associated with it one or more regions which are roots in the place forest, and zero or more holes in the place graph, into which other bigraph regions may be inserted. Similarly, to nodes we may assign controls that define identities and an arity (the number of ports for a given node to which link-graph edges may connect). These controls are drawn from a bigraph signature. In the link graph we define inner and outer names, which define the connection points at which coincident names may be fused to form a single link.

A bigraph is a 5-tuple:

${\displaystyle (V,E,ctrl,prnt,link):\langle k,X\rangle \to \langle m,Y\rangle ,}$

where ${\displaystyle V}$ is a set of nodes, ${\displaystyle E}$ is a set of edges, ${\displaystyle ctrl}$ is the control map that assigns controls to nodes, ${\displaystyle prnt}$ is the parent map that defines the nesting of nodes, and ${\displaystyle link}$ is the link map that defines the link structure.

The notation ${\displaystyle \langle k,X\rangle \to \langle m,Y\rangle }$ indicates that the bigraph has ${\displaystyle k}$ holes (sites) and a set of inner names ${\displaystyle X}$ and ${\displaystyle m}$ regions, with a set of outer names ${\displaystyle Y}$. These are respectively known as the inner and outer interfaces of the bigraph.

Formally speaking, each bigraph is an arrow in a symmetric partial monoidal category (usually abbreviated spm-category) in which the objects are these interfaces.[5] As a result, the composition of bigraphs is definable in terms of the composition of arrows in the category.

• BigraphER is a modelling and reasoning environment for bigraphs consisting of an OCaml library and a command-line tool providing an efficient implementation of rewriting, simulation, and visualisation for both bigraphs and bigraphs with sharing.[14]
• jLibBig is a Java library providing efficient and extensible implementation of bigraphical reactive systems for both bigraphs and directed bigraphs.[15][16]

No longer actively developed:

• BigMC is model checker for bigraphs which includes a command line interface and visualisation.[17]
• Big Red is a graphical editor for bigraphs with easily extensible support for various file formats.[18]
• SBAM is a stochastic simulator for bigraphs, aimed at simulation of biological models.[19]
• DBAM is a distributed simulator for bigraphical reactive systems.[20]
• DBtk is a toolkit for directed bigraphs that provides calculation of IPOs, matching, and visualisation.[21]

• Bisimulation
• Combinatorial species

• Milner, Robin (2009). The Space and Motion of Communicating Agents. Cambridge University Press. ISBN 978-0521738330.
• Milner, Robin (2001). "Bigraphical reactive systems, (invited paper)". CONCUR 2001 – Concurrency Theory, Proc. 12th International Conference. Lecture Notes in Computer Science. Vol. 2154. Springer-Verlag. pp. 16–35. doi:10.1007/3-540-44685-0_2.
• Milner, Robin (2002). "Bigraphs as a Model for Mobile Interaction (invited paper)". ICGT 2002: First International Conference on Graph Transformation. Lecture Notes in Computer Science. Vol. 2505. Springer-Verlag. pp. 8–13. doi:10.1007/3-540-45832-8_3.
• Debois, Søren; Damgaard, Troels Christoffer (2005). "Bigraphs by Example". IT University Technical Report Series TR-2005-61. Denmark: IT University of Copenhagen. CiteSeerX 10.1.1.73.176. ISBN 978-87-7949-090-1.
• Sevegnani, Michele; Calder, Muffy (2015). "Bigraphs with sharing". Theoretical Computer Science. 577: 43–73. doi:10.1016/j.tcs.2015.02.011.

• Bibliography on Bigraphs