Examples and Case Studies

This page presents ​examples that illustrate how bigraphical theory can be applied to model, simulate, and analyze complex dynamic systems.

What's built with and for BTS

Examples in Practice

Agent-based simulations with on-the-fly verification via bigraph rewriting on bi-grids. Simulator used: ds-crazyflies.

Real-time monitoring of spatial properties
for automated driving functions. Simulator used: CARLA.

Interactive term builder for bi-grids
(permutation-invariant, topology-optimized
formal data structures for spatial computing).

State space generated by bigraphical model checking using simulated annealing–based reachability analysis. Rendered with Gephi.

Geometrie und Algebra

A Common Language

Many algorithms for automated reasoning use first-order predicate calculus with equality or different flavors of category theory. BTS takes a different path. It employs a graphical and algebraic formalism grounded in graph rewriting and category theory that can also be interpreted geometrically in some cases. At the heart of this approach lie monoidal categories, which form the cornerstone of categorical algebra, connecting algebra, topology, and computer science. Bigraphical Reactive Systems bring this formal framework into practical application.         

Case Studies

Bigraphs have been applied in case studies across a range of application areas. The examples below show how BTS is used both as a "standalone tool," or integrated with commonly used third-party tools, with hands-on resources such as source code, tutorials, and papers provided where available.

Model Checking 
Swarms and Robots

  • Program Composition for Swarms: A formal approach to composing swarm behaviors. [Abstract] [Video] [Poster]
  • Self-Sorting Robots: Analysis of autonomous robot sorting behaviors. [Benchmark] [Paper] [Code] [Tutorial]
  • Drone Landing Coordination at Vertiports: Coordinating multiple drones using formal models. [Paper1] [​Paper2]
  • Simplified Proofs for Robotic Pick-and-Place Workflows: Techniques for reducing and structuring proofs to support the formal analysis. [Slides]
  • Multi-Agent Path Finding: Formal modeling and analysis of path-finding problems involving multiple agents operating in shared environments. [​Revised Preprint]

Software Verification

  • Concurrent Append Problem: Verifying thread-safe, parallel updates to a linked list by multiple processes.
    [Code] [Paper]
  • Vending Machine: Using a formal specification (BDSL) to guide the development of a correct RESTful web service. [Slides] [Code]