Bigraphs

Origin. Milner (2001-2009). Unifying framework for mobile processes. Two structures: place graph (locality) and link graph (connectivity). Foundation for ubiquitous computing models.

Models. Nodes with controls. Place graph: nesting hierarchy. Link graph: hyperedges (names). Composition and reaction rules. Subsumes π-calculus, ambient calculus.

Formalism.

Bigraph: B = (V, E, ctrl, prnt, link) V: nodes, E: edges (hyperedges) ctrl: V → K (node controls) prnt: V → V ∪ {root} (place hierarchy) link: ports ∪ names → E ∪ names (connectivity)

Place graph: Forest of nodes. Nesting: physical or logical containment. Regions: parallel roots. Sites: holes for composition.

Link graph: Hyperedges connect ports and names. Inner names: interface to inner. Outer names: interface to outer.

Composition: B₁ ∘ B₂: place sites of B₁ with regions of B₂. B₁ ⊗ B₂: tensor product (parallel).

Reaction rules: R = (redex, reactum, η) Pattern match redex, replace with reactum. η: instantiation map for sites.

Example (π-calculus encoding): Process P | Q: tensor in bigraph. Channel x: shared name. Restriction νx: inner name.

Sorting: Control signatures. Well-formedness conditions.

Symbols.

Metatheory. The framework rests on Leifer and Milner's theory of reactive systems (2000): if a category of contexts has relative pushouts, then taking minimal contexts as transition labels yields a labelled transition system whose strong bisimilarity is automatically a congruence. Milner proved that concrete bigraphs — those tracking node and edge identities — have relative pushouts, which is why the theory is developed concretely and abstract bigraphs are obtained afterwards by quotienting out support. Milner (2005) also gave a sound and complete equational axiomatization of bigraph equality, decomposing every bigraph into elementary place and link constituents; the place graph and link graph are orthogonal, so a bigraph factors as their pair over a shared node set. The encodings are checked, not asserted: CCS is encoded as a bigraphical reactive system whose derived congruence coincides with standard strong bisimilarity, and Jensen and Milner (2004) treated the π-calculus, with Petri nets and mobile ambients following. Sortings restrict to well-formed bigraphs, and a sorting must itself be shown to preserve relative pushouts.

Applies to. Mobile systems. Context-aware computing. Biological modeling. Network modeling. Distributed systems.

Limitations. Relative pushouts exist only in the concrete category, so the congruence theorem cannot be applied to abstract bigraphs directly; the derived equivalence must be built with identities tracked and then quotiented, and that detour is structural rather than bookkeeping. The derived labelled transition system is large, since every minimal context is a label, and the induced bisimilarity is often strictly finer than the equivalence one wants, requiring a restriction to engaged transitions to recover the intended notion. Sorting disciplines are not free: the main theorem must be re-established for each, because an arbitrary sorting can destroy the relative pushouts it depends on. Executing a bigraphical reactive system means locating a redex, an instance of subgraph matching and therefore intractable in general. The base theory has no time, rate or probability; stochastic behaviour is a separate extension with its own semantics.

© 2026 Lingenic LLC