Practical Modelling with Bigraphs

TL;DR

Practical Modelling with Bigraphs presents a hands-on guide to using bigraphs for systems where placement and connectivity co-evolve. It surveys place graphs, link graphs, and Bigraphical Reactive Systems, introducing practical extensions such as parameterised, instantaneous, conditional, probabilistic, and stochastic rewriting implemented in BigraphER. The paper emphasizes diagrammatic notation, multi-perspective modelling, and techniques to handle fixed arity and ordering constraints, alongside tooling for simulation and model checking. It provides real-world examples and concrete modelling tips to help practitioners build executable, analysable bigraph models.

Abstract

Bigraphs are a versatile modelling formalism that allows easy expression of placement and connectivity relations in a graphical format. System evolution is user defined as a set of rewrite rules. This paper presents a practical, yet detailed guide to developing, executing, and reasoning about bigraph models, including recent extensions such as parameterised, instantaneous, prioritised and conditional rules, and probabilistic and stochastic rewriting.

Figures (25)

• Figure 1: Example bigraph with two regions: a physical containing a Wi-Fi-enabled , a , and their , and data consisting of a and an . (a) Diagrammatic representation: entities are black shapes and links are green lines. (b) The place graph. (c) The link graph. (d) Example reaction rule: a user leaves a room and takes the phone with them. (e) Application of the reaction rule from (d) to (a).
• Figure 2: Modelling buildings. (a) Diagrammatic place graph (b) Forest representation (c) BigraphER model. In (b), the red and blue dashed ovals, containing red and blue parallel and merge product operators resp., are superposed on the place graph. These are not part of bigraph notation, but serve to highlight the difference between and .
• Figure 3: Place graph with one region and three sites.
• Figure 4: Bigraphs with sharing: cameras with overlapping fields of vision that may capture a single . (a) Bigraph model. (b) Place graph. (c) BigraphER snippet.
• Figure 5: Link graph example: CCTV, phone calls, and remote network access. (a) Link graph. (b) BigraphER snippet.