Bigraphs with sharing

Bigraphical Reactive Systems (BRS) were designed by Milner as a universal formalism for modelling systems that evolve in time, locality, co-locality and connectivity. But the underlying model of location (the place graph) is a forest, which means there is no straightforward representation of locations that can overlap or intersect. This occurs in many domains, for example in wireless signalling, social interactions and audio communications. Here, we define bigraphs with sharing, which solves this problem by an extension of the basic formalism: we define the place graph as a directed acyclic graph, thus allowing a natural representation of overlapping or intersecting locations. We give a complete presentation of the theory of bigraphs with sharing, including a categorical semantics, algebraic properties, and several essential procedures for computation: bigraph with sharing matching, a SAT encoding of matching, and checking a fragment of the logic BiLog. We show that matching is an instance of the NP-complete sub-graph isomorphism problem and our approach based on a SAT encoding is also efficient for standard bigraphs. We give an overview of BigraphER (Bigraph Evaluator & Rewriting), an efficient implementation of bigraphs with sharing that provides manipulation, simulation and visualisation. The matching engine is based on the SAT encoding of the matching algorithm. Examples from the 802.11 CSMA/CA RTS/CTS protocol and a network management support system illustrate the applicability of the new theory.