Introduction to Bigraphs¶

Bigraphs were invented by Robin Milner as an extension/generalization of previous process calculi (some of which he invented as well). A process calculus is a way to formally model concurrent and distributed systems, including communication/interactions/synchronizations, along with a set of algebraic laws to reason about them.

bigraph

space¶

The structure of a bigraph is defined as two superimposed graphs over a single set of nodes

  • place graph (forest) which is modeled as a tree
  • link graph (hypergraph) which is a set of hyperedges

bare bigraph

place graph¶

The place graph represents the relative location of each node (in terms of containment).

forest

link graph¶

The link graph represents communication across place boundaries, ie common signals that all linked nodes share.

hypergraph

anatomy

motion¶

The "motion" of a bigraph is accomplished by reaction rules, which specify a redex showing a bigraph to match and reactum that shows the bigraph to replace it by.

Here is an example bigraph (showing the system in a "locked" state): locked

redex¶

When we take that bigraph and match it with this redex

redex

reactum¶

and substitute with this reactum

reactum

transition¶

we end up with this result (the key has been "unlocked"):

unlocked

full reaction¶

Here is the full reaction from locked to unlocked state:

reaction

operations¶

You can build complex bigraphs out of simpler bigraphs using the basic operations:

  • A.B - nest (nesting B inside A)
  • A | B - merge (side by side, but in the same region)
  • A || B - parallel (side by side, different regions)
  • A{b} - link (A is linked to edge b)
  • A(b) - parameterize (A has parameter b)

python API¶

You can parse bigraphs from strings into python objects, and you can also build up bigraphs programmatically using the python API. The basic operations are available:

nest¶

In [2]:
A = bigraph('A')
B = bigraph('B')
A.nest(B)
Out[2]:
A.B
In [3]:
visualize(A)
0.svg r0 0 v0 A r0->v0 v1 B v0->v1
Out[3]:
A.B

merge¶

In [4]:
A = bigraph('A')
B = bigraph('B')
merge = Merge([A, B])
merge
Out[4]:
A | B
In [5]:
visualize(merge)
0.svg r0 0 v0 A r0->v0 v1 B r0->v1
Out[5]:
A | B

link¶

In [7]:
A = bigraph('A')
b = Edge('b')
A.link(b)
Out[7]:
A{b}
In [8]:
visualize(A)
0.svg r0 0 v0 A r0->v0 ob b v0->ob
Out[8]:
A{b}

parsing¶

The notation we have been using for bigraphs is Milner's original formalized into a language named .big, as implemented by the Glasgow Bigraph Team. We are using their engine to run simulations, but we have our own parser for .big files implemented as a Parsing Expression Grammar that converts strings into python bigraph objects.

To access the .big parser, use the bigraph function:

In [9]:
parsed = bigraph('A.(B | C{m, n})')
parsed
Out[9]:
A.(B | C{m,n})

The python bigraph objects are rendered by default, which mirrors the original form we parsed.

We can also build this bigraph programmatically.

In [10]:
A = bigraph('A')
B = bigraph('B')
C = bigraph('C')
A, B, C
Out[10]:
(A, B, C)
In [11]:
C.link('m')
C.link('n')
C
Out[11]:
C{m,n}
In [12]:
merge = B.merge(C)
merge
Out[12]:
B | C{m,n}
In [13]:
A.nest(merge)
A
Out[13]:
A.(B | C{m,n})

Let's visualize this bigraph:

In [14]:
print(A)
visualize(A)
A.(B | C{m,n})
0.svg r0 0 v0 A r0->v0 om m on n v1 B v0->v1 v2 C v0->v2 v2->om v2->on
Out[14]:
A.(B | C{m,n})

controls¶

Controls are a way to label nodes, giving it a kind of "type" which declares:

  • symbol - the label given by this control
  • arity - how many ports it has (where edges can connect)
  • fun - any parameters nodes of this control may have
  • atomic - whether it can have subnodes or not

Here is an example of a control with an arity of 2:

In [15]:
D1 = bigraph('ctrl D = 2')
D1.symbol, D1.arity
Out[15]:
('D', 2)

Here is another control with named parameters:

In [16]:
C = bigraph('fun ctrl Compartment(volume, state) = 1')
C.symbol, C.arity, C.fun
Out[16]:
('Compartment', 1, ('volume', 'state'))

nodes and controls¶

Controls give us a more principled way to create nodes, and provide a way to structure our systems and guide reactions to target specific elements.

In [17]:
C1 = Node(control=C, params=(0.3, "stable"), ports=('atp',))
C2 = Node(control=C, params=(11.1111, "active"), ports=('chromosome',))
C1, C2
Out[17]:
(Compartment(0.3,stable){atp}, Compartment(11.1111,active){chromosome})

We can even assign parameters this way

In [18]:
C1.assign('volume', 0.4)
Out[18]:
Compartment(0.4,stable){atp}

general representation¶

The nested notation we've been using so far is succinct, but sometimes we want to represent the bigraphs in a more general way, specifically not directly nesting the nodes but instead tracking the four components of a bigraph separately:

  • controls
  • nodes
  • places
  • links

We can do this by using the unfold() method of the Bigraph class to generate an instance of Bigraph:

In [19]:
ABC = bigraph('A.(B | C{m,n})')
open_form = Bigraph.unfold(ABC)
open_form.get_spec()
Out[19]:
{'controls': {'B': {'symbol': 'B', 'arity': 0, 'atomic': False, 'fun': []},
  'C': {'symbol': 'C', 'arity': 2, 'atomic': False, 'fun': []},
  'A': {'symbol': 'A', 'arity': 0, 'atomic': False, 'fun': []}},
 'nodes': {1: {'control': 'B', 'params': []},
  2: {'control': 'C', 'params': []},
  0: {'control': 'A', 'params': []}},
 'places': {0: (1, 2)},
 'links': {'m': (2,), 'n': (2,)}}

This means that if you have a dictionary with the four keys controls, nodes, places, links you can make a nested bigraph out of it (going in reverse)

In [20]:
spec = {'controls': {'B': {'symbol': 'B', 'arity': 0, 'atomic': False, 'fun': []},
  'C': {'symbol': 'C', 'arity': 2, 'atomic': False, 'fun': []},
  'A': {'symbol': 'A', 'arity': 0, 'atomic': False, 'fun': []}},
  'nodes': {1: {'control': 'B', 'params': []},
  2: {'control': 'C', 'params': []},
  0: {'control': 'A', 'params': []}},
  'places': {0: (1, 2)},
  'links': {'m': (2,), 'n': (2,)}}
from_spec = Bigraph(**spec)
from_spec.fold()
Out[20]:
A.(B | C{m,n})

reactions¶

We have been talking a lot about the structure of bigraphs, but the real point is to operate dynamically, in this case through reactions. A reaction is composed of two separate bigraphs, the redex which matches some existing structure, and the reactum that signifies what to modify in that structure.

reaction

declaring a reaction¶

To create a new reaction, we need to specify the redex bigraph and the reactum bigraph. Here is a simple reaction which takes any node with a Hello control and nests a World node inside it:

In [21]:
add_world = bigraph("""
react add_world =
    Hello
    -->
    Hello.World
""")
add_world
Out[21]:
react add_world = 
Hello
-->
Hello.World

applying a reaction¶

Now let's apply our reaction. We need an initial bigraph, in this case the lone node with control Hello. Then we can call react with the add_world reaction on it:

In [22]:
hello = bigraph("Hello")
result = react(add_world, hello)

visualize(hello)
visualize(result)
result
0.svg r0 0 v0 Hello r0->v0
0.svg r0 0 v0 Hello r0->v0 v1 World v0->v1
Out[22]:
Hello.World

reactive systems¶

Beyond applying a single reaction to a single bigraph, we can also run whole systems of reactions in a series of transitions starting from an initial bigraph. In order to do this, we need to define the system.

declaring a reactive system¶

We can declare the system using .big notation:

In [23]:
system = bigraph("""
begin brs
    init hello;
    rules = [
        {add_world}
    ];
end
""")
system
Out[23]:
begin brs
    init hello;
    rules = [
        {add_world}
    ];
end

There are a few components to this:

  • begin brs declares which type of reactive system we are creating. Other options are pbrs and sbrs for probabilistic and stochastic reactive systems respectively.
  • init hello declares the bigraph we'll use as the initial state for the system. Reactions will match against this initial state at first, and then each subsequent state as transitions are applied.
  • rules = [....] is the collection of rules, organized into "rule groups", each group enclosed by squirrely braces.

rule groups¶

Rule groups are a way to specify groups of alternative reactions to apply to the current bigraph state. Each group will be checked one by one in order, and if any of the rules in that group match, one of the matching rules will be selected (non-deterministically) to apply a transition to the current state, then we go back to the top of the rules section.

rules = [
    {add_world, grow_world},
    {perturb_world},
    {remove_world, duplicate_world, invert_world}
]

In this case, we check first whether the redex of either add_world or grow_world matches the current state. If one of them does, it is applied, otherwise we check the next group. If both of them match, then one is selected at randomly.

Once a rule is applied, we go back to the top and iterate through the rule groups again. If none of the rules match, the simulation ends.

execution¶

Now that we have all the pieces, let's put them together into a whole system and run it!

In [24]:
hello_world = bigraph("""
ctrl Hello = 0;
ctrl World = 0;

react add_world = 
    Hello
    -->
    Hello.World;

big initial = Hello.1;

begin brs
    init initial;
    rules = [
        {add_world}
    ];
end
""")

Here is our system:

In [25]:
hello_world
Out[25]:
ctrl Hello = 0;
ctrl World = 0;

react add_world = 
    Hello
    -->
    Hello.World;


big initial = Hello.1;

begin brs
    init initial;
    rules = [
        {add_world}
    ];
end

Let's simulate this system now:

In [26]:
# a path to write the simulation results
path = "out/bigraph/hello"
In [27]:
# we must set a number of steps to simulate
# as this system would otherwise run forever!
steps = 5
In [28]:
# simulate the system
results = hello_world.simulate(path=path, steps=steps)
In [29]:
for transition in results:
    print(transition)
Hello
Hello.World
Hello.World.World
Hello.World.World.World
Hello.World.World.World.World
Hello.World.World.World.World.World
Hello.World.World.World.World.World.World

Let's visualize all these transitions!

In [30]:
hello_world.display_transitions(path=path)
In [ ]: