probablytom
commented
6 years ago Bigraphs and composability
Bigraphs are all about composability. This is one of the benefits they take from category theory; it's really easy to do composition in bigraphs, as well as subsystem isolation.
Bigraphs and Behaviour
Bigraphs use two notions to represent behaviour: "controls" and "reaction rules". The changes that a system can undergo are referred to as reaction rules. They're either drawn graphically or written in the Bigraph algebra (there's a one-to-one mapping between the two). However, behaviour doesn't make much sense outside of context (we need to effectively "type" the nodes on the bigraph so we don't apply the wrong rules to nodes representing things that shouldn't undergo the transformation), so we contextualise the graph through the control, which is really just fancy labelling or simple typing for bigraph nodes.
Bigraphs and Obashi
After a little frustration it became clear that, while a little messy, we can absolutely represent Obashi in bigraphs! Clean decompositions exist.
What we can learn
A few things.
First off, Obashi has no notion of state change in a model: it's like changing a text file on a computer, not richly simulating possible future states. Bigraphs represent this via their reaction rules. If we decomposed Obashi to a bigraph, we could simulate some of the possible future states for the model.
This is actually pretty useful, in that tools like BigraphER (Muffy and Michele's OCaml tool) export a Bigraph model to prism code, so you can do probabilistic model checking on your system!
This is really neat. We don't want to actually design or model a system in bigraphs directly, because Obashi is more readable and pleasant (and comes with a proven methodology for B&IT systems), but decomposing to Bigraphs gives us motion rather than just structure, and acts as an adapter to probabilistic model checking. We might say, "is there a >5% chance that our network infrastructure will break in the next 12 months" and we can calculate this kind of risk (or impact) analysis on a very large model, without losing data.
One possible issue here would be that the bigraph and subsequent prism code produced by the export of an entire Obashi diagram would be massive; we'd want to export subsystems and provide nice semantics for the "environment" of the subsystem.
Combined with the rigorous analysis of system composition and decomposition, and a superset of possible system models compared to what Obashi is capable of, there are lots of things Bigraphs give us that we don't get in Obashi.
(What we lose is simplicity, though, which is easily Obashi's greatest strength. An adapter from something simple to something rigorous would be wonderful, though it's not obvious the two have to be mutually exclusive / sit on some spectrum.)
So presumably, bigraphs are useful for composing systems How does Bigraph represent behaviour Can bigraphs be used to represent Obashi models and if so, what can we learn about an Obashi model from the bigraph?