4. Concrete bigraphs, relative pushouts and bisimulation
Concrete bigraphs, whose nodes and edges are drawn from one supply so that
composition is partial, and the derivation from reaction rules of a labelled
transition system whose bisimilarity is a congruence. The sources are Jensen
and Milner (Bigraphs and mobile processes (revised), TR-580, 2004), Leifer and
Milner (Deriving bisimulation congruences for reactive systems, 2000), Milner
(The Space and Motion of Communicating Agents, 2009) and Jensen (Mobile
Processes in Bigraphs, 2006). Milner's book is cited from the author's draft
of 1 December 2008, with the draft's numbering; the printed book has not been
checked. Symbols are those of the Notation chapter; a
transition also carries a location \lambda. Every other result is in
Bigraph/Concrete/: supports and translation (Support.lean), the RPO
constructions and the characterisation of IPOs (Place*.lean, Link*.lean),
transfer to a quotient (Transfer*.lean), hard bigraphs and the tensor
(Hard.lean, Tensor.lean), the scope rule (Binding*.lean,
ScopeRuleCounter.lean), Example 6 of TR-580 (Example6*.lean) and the cases
of the adequacy proof (Relative*.lean, DisjointIPO*.lean, Adequacy*.lean).