Practical Bigraphs via Subgraph Isomorphism

Bigraphs simultaneously model the spatial and non-spatial relationships between entities, and have been used for systems modelling in areas including biology, networking, and sensors. Temporal evolution can be modelled through a rewriting system, driven by a matching algorithm that identifies instances of bigraphs to be rewritten. The previous state-of-the-art matching algorithm for bigraphs with sharing is based on Boolean satisfiability (SAT), and suffers from a large encoding that limits scalability and makes it hard to support extensions. This work instead adapts a subgraph isomorphism solver that is based upon constraint programming to solve the bigraph matching problem. This approach continues to support bigraphs with sharing, is more open to other extensions and side constraints, and improves performance by over two orders of magnitude on a range of problem instances drawn from real-world mixed-reality, protocol, and conference models.