Sorted Bigraphs

Building upon work of Milner, Leifer, Jensen and ourselves, we develop a theory of sorted bigraphical reactive systems. Concretely, we show how to automatically get a sorting on bigraphs sustaining the behavioural theory of pure bigraphical reactive systems by lifting a safe sorting on the underlying reactive system of abstract bigraphs. We back this result by a general construction of a safe sorting, the Closure sorting. This sorting restricts a reactive system, and thus by the main result any bigraphical reactive system, to the contexts satisfying any given decomposable predicate. We demonstrate the applicability of the Closure sorting by proving that Milner’s Local Bigraphs arise as a closure sorting of pure bigraphs, using part of the usual scoping condition as predicate