Modelling Real-time Systems with Bigraphs

TL;DR

This paper extends Bigraphical Reactive Systems to support real-time systems by incorporating digital clocks and Markov Decision Processes, enabling modeling of systems with temporal constraints.

Contribution

It introduces a novel approach combining multiple perspectives for digital clocks within BRSs and implements it using the BigraphER toolkit.

Findings

Successfully models real-time behaviors in BRSs

Demonstrates applicability with cloud system request examples

Enables analysis of timing decisions in system transitions

Abstract

Bigraphical Reactive Systems (BRSs) are a graph-rewriting formalism describing systems evolving in two dimensions: spatially, e.g. a person in a room, and non-spatially, e.g. mobile phones communicating regardless of location. Despite use in domains including communication protocols, agent programming, biology, and security, there is no support for real-time systems. We extend BRSs to support real-time systems with a modelling approach that uses multiple perspectives to represent digital clocks. We use Action BRSs, a recent extension of BRSs, where the resulting transition system is a Markov Decision Process (MDP). This allows a natural representation of the choices in each system state: to either allow time to pass or perform a specific action. We implement our proposed approach using the BigraphER toolkit, and demonstrate the effectiveness through multiple examples including modelling cloud system requests.