Research

My research is about understanding complex systems and checking that they behave as intended. I am particularly interested in systems where space, connectivity and uncertainty matter, from communication networks and digital twins to autonomous agents. I develop mathematical models that describe how these systems are organised, how they change and what can go wrong. The models can be simulated and checked against requirements such as safety, security, reliability and privacy.

Much of my work builds on bigraphs, a modelling formalism introduced by Robin Milner. Bigraphs describe where things are and how they are connected. A model might show, for example, that a person is in a room and that their phone is connected to a display or a network. Rules describe changes such as the person leaving the room or the phone losing its connection. Bigraphs use a visual notation that makes models easier to inspect and discuss, together with a precise mathematical definition for rigorous analysis.

I have developed bigraphs with sharing, which can represent overlapping spaces, and worked on extensions for probabilistic, non-deterministic and conditional behaviour. Other parts of my work cover methods for ruling out invalid models with sorting schemes and algorithms for matching bigraphs efficiently (CAV 2016, CP 2021). These ideas are implemented in BigraphER, an open-source tool for constructing, visualising, running and analysing bigraph models. The Papers section contains a tutorial and further papers on the theory, implementation and applications of bigraphs.

A transition in the three-station CSMA/CA model. A and C (blue triangles) both want to send to B but cannot sense each other; their overlapping signals (S ovals) are represented using bigraphs with sharing. From FAC 2014.

One application is the modelling and verification of autonomous agents. In particular, I have worked on belief-desire-intention, or BDI, agents: systems whose behaviour is organised around what they believe, what they want to achieve and the plans available to them. We can analyse how an agent selects a plan, what happens when an action fails and how likely it is to reach its goal. This work includes the quantitative modelling and analysis of BDI agents and multi-objective strategy synthesis, where an agent must balance competing goals.

I also work on privacy, cybersecurity and responsible AI. Formal models can express privacy rules and check whether data-processing operations follow them, including when data are transferred between jurisdictions. My cybersecurity work covers communication protocols, Internet of Things systems and security games. The responsible AI strand examines probabilistic tools used in policing and criminal justice, particularly black-box systems and the effects of carrying uncertainty from one decision to the next.

Discussing with Lord Carloway how a mock trial can examine the role of AI in criminal justice, as part of PROBabLE Futures.

I also apply formal modelling to cyber-physical systems, where software and communication networks interact with physical infrastructure and people. This work covers railway networks, predictive maintenance, 5G and 6G protocols, autonomous vehicles, robotic fleets and mixed-reality systems, such as the Savannah game pictured below. Many of these systems change while they are operating, so analysing the initial design is not enough. Models can be updated at runtime to monitor current behaviour, examine possible future states and identify when the system needs to adapt.

A runtime model that is kept in step with the physical system it represents can act as a digital twin. My work studies how the twins of different parts of a system can be combined, for example to give a shared operational view of a transport network and support decarbonisation (LOCO 2024). I also evaluate runtime models with the people who use them. In a study of human-swarm interaction, runtime predictions improved team performance without increasing operator workload (THRI 2025).

Federating digital twins to support transport decarbonisation. From LOCO 2024.