Skip to main content

Overview

In bigraphs, the dynamic behavior of a system is represented by means of reaction rules written reaction-relation-between-agents, where reaction-relation-between-agents are called agents (in bigraph-jargon) before and after a reaction, and R is a reaction rule. Generally, an agent is a bigraphical state of the system; a snapshot of the system at a specific point in time.

Given a signature, a set of reaction rules and an initial agent (all defined over the same signature), one can create a so-called bigraphical reactive system. It acts like a container including all these components. A BRS can be regarded as the specification of a system, process or model under consideration.

BRSs introduce a temporal notion to bigraphs and allows to perform and track changes of the system over time.

This page explains how to create BRSs. Moreover, the structure of reaction rules and their different kinds are introduced.

BRS Model Checking

Refer to Verification to get to know more about how to use a BRS specification for model checking.

Example

Refer to the Usage Example, which describes a complete procedure on how to practically use bigraph matching and rewriting in Bigraph Framework. It introduces the basic functionality regarding matching and rewriting.

An overview of the most important classes is also listed on this page in section Changing Bigraphs over Time: Overview.

Bigraphical Reactive System (BRS)​

A BRS is a model of a system or system specification containing an agent (i.e., the host graph, the initial state) and a collection of reaction rules.

Mathematical Definition

In category theory, BRSs are defined as syntactical categories endowed with a set of reaction rules. Specifically, a concrete BRS is a s-category reaction-relation-between-agents containing a signature and a set of rules.

All reactive system implementations extend the interface org.bigraphs.framework.core.reactivesystem.ReactiveSystem<B extends Bigraph<? extends Signature<?>>> of the Core Module in Bigraph Framework.

Creating a BRS by Instantiation​

A reactive system for pure bigraphs can be created by calling its constructor as follows:

PureReactiveSystem reactiveSystem = new PureReactiveSystem();

Then, an agent and reaction rules can be added like this:

// Set the initial agent
PureBigraph agent = ...;
reactiveSystem.setAgent(agent);
// Add a reaction rule
ReactionRule<PureBigraph> rr = ...;
reactiveSystem.addReactionRule(rr);
Format of the Agent

In the bigraph theory, an agent is any ground bigraph, i.e., a bigraph that has no sites and inner names. It must also be prime, i.e., it must have only one root.

Exceptions

An exception will be thrown if the rules or agent are not in the correct format.

Some further remarks
  • Predicates as used in model checking for reachability checking can be added using the method PureReactiveSystem#addPredicate(ReactiveSystemPredicates<B> predicate).
  • See also here on how to create predicates.

Creating a BRS by Inheritance​

Inheriting a reactive system implementation allows for an object-oriented approach to better organize and manage domain-specific BRSs in an application.

The following examples defines a BRS that can compute the sum of two integers, which are represented in bigraphs in unary form. In this form the symbol S is used to denote successor, and Z to mean zero. For example, the number 2 would be writing as S.S.Z.

public class AddExpr extends PureReactiveSystem {

    public AddExpr(int a, int b) throws Exception {
        setAgent(createAgent(a, b));
        addReactionRule(createReactionRule_1());
        addReactionRule(createReactionRule_2());
    }

    // Custom extended method of this reactive system specification that allows execution
    public PureBigraph execute() throws Exception {
        // Instantiate a matcher
        AbstractBigraphMatcher<PureBigraph> matcher = AbstractBigraphMatcher.create(PureBigraph.class);
        // Get the current state
        PureBigraph agentTmp = getAgent();

        // ...
        // apply rules according to some strategy or randomly
        // ...

        // Return the final state
        return agentTmp;
    }
}

The concrete methods AddExpr#createAgent(), AddExpr#createReactionRule_1() and AddExpr#createReactionRule_2() are omitted in this example for clarity.

Anatomy of Reaction Rules​

BRS introduce a time-varying notion to bigraphs through reaction rules. That is, reaction rules allow some kind of simulation, which internally is enabled by means of graph rewriting. The bigraph rewriting formalism allows to synthesize a (potentially infinite) labelled transition system (LTS). Each node of the LTS is a bigraph state. States are connected by edges called transition relations labeled with the reaction rule that led to this state. The LTS can have cycles.

To generate an LTS, reaction rules must be applied. A reaction rule comprises a redex and reactum. That is, a rule consists of a left-hand side, and a right-hand side. The meaning of a rule is as follows: The redex specifies the pre-conditions and the reactum the post-conditions. If the redex could be found in some agent (i.e., host graph), the matched part of the agent is replaced by the reactum. This is also called graph rewriting, which solves the subgraph matching problem.

bigraph-reaction-rule-example Example of a bigraphical reaction rule comprising a redex (left-hand side) and reactum (right-hand side), which both are bigraphs. The rule describes the movement of the smaller circle from one place to another place (larger circles).

Simulating a BRS works as follows: Beginning with an agent (i.e., the initial bigraph state of the BRS), a set of reaction rules is applied as long as a match can be found, or until some stopping criteria eventuates (such as time, number of states explored, any convergence criteria, etc.). Note that the agent and the reaction rules need to be defined over the same signature.

Non-Deterministic Rules

Sometimes a rule can have multiple occurrences in a host graph. Thus, rules are often non-deterministic.

Reaction Rules

Refer to section Reaction Rules, which explains bigraphical reaction rules in more detail.

Rule Strategies

Bigraphical reaction rules enable a form of the more general rule-based programming paradigm. Therefore, you can use advanced rule strategies to control the execution order of rules.

Changing Bigraphs over Time: Overview​

Having explained the essentials of BRSs until here, the matching and rewriting functionality from the following classes can be used to conveniently execute BRSs in arbitrary ways:

Matching

  • org.bigraphs.framework.simulation.matching.AbstractBigraphMatcher
    • This abstract class defines a matcher and needs a host graph and rule to perform bigraph matching.
    • A bigraph matcher consists of a bigraph matching engine w.r.t. to the bigraph type.
    • The correct one is automatically created using the factory method #create(Class) by supplying the bigraph class type.
    • Matches are returned via an iterator (the instances of the matches are of type BigraphMatch).

Rewriting