Note: alphabetical order of authors means equal contributions.
Bigraphs, introduced by Robin Milner, provide a universal
categorical framework for modelling systems that combine
spatial structure and connectivity. Formally, bigraphs
consist of a pair of graph structures organised within a
symmetric monoidal category, with rewriting defined via
subgraph isomorphism. This categorical foundation supports
algebraic reasoning about mobility, locality, and dynamic
reconfiguration.
This talk introduces the core ideas of bigraph theory,
including its diagrammatic notation and algebraic
structure, and highlights recent theoretical developments
such as bigraphs with sharing, probabilistic semantics,
and sorting. We then present BigraphER, a tool suite for
simulation and verification, and illustrate its role in
bridging theory and practice. Recent applications include
a bigraph-based semantics and implementation for rational
agents supporting advanced features such as probabilistic
failure recovery and declarative goals, and digital
twinning for transport systems, where bigraph-based twins
enable runtime verification and predictive “what-if”
analytics.
Finally, we outline future directions: formalisation in
Rocq, approaches for scalability, and the integration of
expressive spatial logics within quantitative
verification.
As Open Radio Access Networks (O-RAN) adoption continues
to expand, AI/ML-driven applications (xApps) are
increasingly being deployed to enhance and simplify
network management. One of the main drivers for utilising
AI is its effectiveness in dealing with the complexity and
the rapidly evolving nature of real-world network
environments. While these approaches show promising
results in many scenarios, AI-based management
applications can introduce new critical challenges that
traditional models did not face. One example is the risk
of misconfiguration by introducing logical inconsistencies
when trying to balance between availability, QoS, and
power efficiency.
An emerging trend in this area is the application of
formal verification to address these challenges by
providing mathematical guarantees on the behaviour of
deployed systems. An established technique used in the
past primarily for the development of high-assurance
software, its more recent evolution to support stochastic
analysis has enabled its application to whole system
analysis in domains such as reliability of cyber-physical
systems and verification of wireless protocols.
In this talk, we present ongoing work of applying formal
verification to two O-RAN scenarios: safeguarding resource
allocation optimisation xApps generated by Large Language
Models (LLMs) and computing optimal thresholds between
energy efficiency and service availability using the PRISM
model checker.
This work is part
of CHEDDAR, the
flagship UK hub dedicated to advancing future
communications.
Bigraphs are an expressive graphical modelling formalism to represent systems that have both spatial aspects, e.g. a Person in a Room, and non-local aspects, e.g. communication between Person entities in (possibly) different Rooms. In fact, they are sometimes too expressive: allowing nonsense models to be created, for example where a Room is nested inside a Person! This talk explores "sorting schemes" for bigraphs which filter badly formed models in a similar way to how type systems filter badly formed programs. We show a language for specifying sorts, rules for verifying the well-sortedness of models, and many sorts of applications.
Bigraphs are an expressive modelling formalism, first introduced by Robin Milner, to model systems with strong notions of space and mobility. This talk informally introduces bigraphs---including their diagrammatic notation and gives some context around their development. We then give a high-level overview of some high-level overview of some of applications we have used them for before, some of the research and development undertaken at Glasgow including the state of the art BigraphER tool, and give some hints for where we might take bigraphs in the future.
When an asset fails in a critical air navigation service,
how urgent is a repair? If we repair within 1 hour, 2
hours, or n hours, how does this affect the
likelihood of service failure? Can a formal model support
assessing the impact, prioritisation, and scheduling of
repairs in the event of component failures, and
forecasting of maintenance costs? These are some of the
questions posed to us by a large organisation and here we
report on our experience of developing a stochastic
framework to answer them. We define and explore logic
properties concerning the likelihood of service failure
within certain time bounds, forecasting maintenance costs,
and we introduce a new concept of envelopes of
behaviour that quantify the effect of the status of
lower level components on service availability. The
resulting model is highly parameterised and user
interaction for experimentation is supported by a
lightweight, web-based interface.
Reference: Michele Sevegnani, and Muffy
Calder. Stochastic model checking for predicting
component failures and service availability IEEE
Transactions on Dependable and Secure Computing (2017).
This seminar will be divided in two parts. In the first, I will present a novel algorithm for the target counting problem based on Constraint Satisfaction Problem. In the second, I will introduce a systematic approach based on bigraphs for ensuring the requirements of resource-competing applications are satisfied by a Wireless Sensor Network both before deployment and at runtime.
While HCI has a long tradition of formally modelling task-based interactions with graphical user interfaces, there has been less progress in modelling emerging ubiquitous computing systems due in large part to their highly contextual nature and dependence on unreliable sensing systems. We present an exploration of modelling an example ubiquitous system, the Savannah game, using the mathematical formalism of bigraphs, which are based on a universal process algebra that encapsulates both dynamic and spatial behaviour of autonomous agents that interact and move among each other, or within each other. We establish a modelling approach based on four perspectives on ubiquitous systems - Computational, Physical, Human, and Technology - and explore how these interact with one another. We show how our model explains observed inconsistencies in user trials of Savannah, and then, how formal analysis reveals an incompleteness in design and guides extensions of the model and/or possible system re-design to resolve this.
Bigraphs were introduced by Robin Milner as a universal mathematical model for representing the spatial configuration of physical or virtual objects, their interaction capabilities and their temporal evolution. In my previous work, I have extended the theory to "bigraphs with sharing" to allow overlapping or intersecting spaces. In the first part of the talk, I will showcase four example applications of bigraphs with sharing: a wireless communication protocol, a management framework for domestic wireless networks, a strategic location-based pervasive mixed-reality game, and BigraphER, a set of tools providing an efficient implementation of computation, simulation, and visualisation for bigraphs. The second part of the talk will focus on current research: Formal analysis of multi-purpose sensor networks, Languages for programming IoT systems, Reachability and coverability in bigraphical reactive systems.
In this talk, I will argue that some deficiencies of current software engineering practice for IoT can be addressed by new frameworks and software tools based on the theory of bigraphs. Bigraphs were introduced by Robin Milner as a universal mathematical model for representing the spatial configuration of physical or virtual objects, their interaction capabilities and their temporal evolution. In my previous work, I have extended the theory to allow overlapping, or intersecting spaces. In the first part of the talk I will showcase three example applications of bigraphs: a wireless communication protocol, a run-time verification system for home-networks and a mixed-reality game. The second part of the talk will focus on current research: Service interoperability and compositionality, Automatic deployment and dynamic contextual reconfiguration, and Languages for programming IoT systems.
Bigraphical Reactive Systems (BRS) are a universal model of computation for the representation of interacting systems that evolve in both time and space. Bigraphs have been shown forming a category called symmetric partial monoidal category and their dynamic theory is defined in terms of rewriting and transition systems, which can be explained in a categorical setting by the notions of relative push-outs (RPOs) and idem push-outs (IPOs). A limitation of bigraphs is that the underlying model of location is a forest, which means there is no straightforward representation of locations that can overlap or intersect. In this talk, I will introduce bigraphs with sharing, an extension of bigraphs which solves this problem by defining the model of location as a directed acyclic graph, thus allowing a natural representation of overlapping or intersecting locations. I will give a complete presentation of the extended theory, including a categorical semantics, algebraic properties, a normal form and several essential procedures for computation.