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.

Symbol	Unicode	Name	Meaning
∘	U+2218	Composition	Place composition
⊗	U+2297	Tensor	Parallel
→	U+2192	Reaction	Rewrite
ν	U+03BD	Restriction	Fresh name

Metatheory. RPOs (relative pushouts) exist. Bisimulation congruences. Sorting disciplines. Faithfully encodes π, ambients.

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

Limitations. Complex formalism. Steep learning curve. Tool support developing. Practical applications few.