Modelling Real-time Systems with Bigraphs

TL;DR

This paper extends Bigraphical Reactive Systems (BRSs) to real-time domains by using Action Bigraphs to yield a Markov Decision Process ($MDP$) semantics and introduces a digital clocks approximation. Clocks are modelled as dedicated bigraph entities, with a global wall-clock and local clocks per timed entity, enabling simultaneous clock advancement via a single $clock\_advance$ rule and non-deterministic choices between time progression and discrete actions. The authors implement the approach in BigraphER and demonstrate it with two case studies—the probabilistic timed automaton (PTA) and a cloud-system with timed requests—and show how to verify properties using $PRISM$ and $PCTL$. This work provides a practical, executable framework for real-time ABRSs, offering scalable clock management and formal verification, while outlining limitations such as the absence of diagonal clocks and strict inequalities, and plans for future syntactic and semantic extensions.

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.

Figures (10)

• Figure 1: (a) Example network topology with three sensors; (b) corresponding bigraph with data to be transmitted by sensor A and the status of each sensor (e.g. Active).
• Figure 2: Reaction rule $\mathtt{send\_Data}$ applies when the receiver is active.
• Figure 3: Example Action Bigraphical Reactive System: probabilistic reaction rules using weights.
• Figure 4: Example from \ref{['exampleB']} extended with clocks perspective.
• Figure 5: Reaction rule $\mathtt{clock\_advance}(n_1, n_2, n_3, n)$ for a system with three timed entities.