Talks

• Designing for Federation: When Connected Twins Need to Agree
  Gemini Call (Digital Twin Hub), online, 27 October 2026
  
  abstract

  This talk introduces why federation matters to the work of TransiT, the UK research hub exploring digital twinning for transport decarbonisation, and why simply connecting different digital twins does not automatically create a trustworthy system-of-systems.
  Drawing on examples around freight electrification, charging infrastructure and energy networks, it explores some of the deeper questions that emerge when independently developed models begin working together.

• Responsible AI in Policing and Criminal Justice
  Digital Justice & Policing 2026, University of Strathclyde, Technology & Innovation Centre, Glasgow, UK, 22 October 2026
• LLMs in policing and risks to case progression
  Data for Policy 2026, Universitat Pompeu Fabra, Barcelona, Spain, 8-10 September 2026
  [post]
• PROBabLE Futures Mapping Launch
  PROBabLE Futures Mapping Launch, online, 24 June 2026
  [post] [post] [tool] [report]
• Bigraphs: From Category Theory to Digital Twins
  Bigraph Workshop: Mobility and Swarms in Cyber-Physical-Spaces at TUD, Dresden, Germany, October 2025
  [slides]
  abstract

  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.

• Probabilistic AI Systems in Law Enforcement
  2nd Michele Taruffo Evidence Week, Girona, Spain, 6 June 2025
• Mapping AI Tools in Criminal Justice
  PROBabLE Futures and CETaS (Centre for Emerging Technology and Security) workshop: AI-transforming Crime and the Response to Crime, The Turing Institute, London, UK, 12 March 2025
  [post]
• A Digital Twinning Approach to Decarbonisation: Research Challenges
  International Workshop on Low Carbon Computing (LOCO 2024), University of Glasgow, Scotland, UK, December 2024
  [abstract]
• Formal Verification of 5G Advanced Protocols to Inform a Verifiable 6G
  IRC for Communication Systems and Sensing (IRC-CSS) at KFUPM, Dhahran, Saudi Arabia, October 2024
  [post]
  abstract

  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.

• Sorting out Bigraphs
  École nationale de l'aviation civile (ENAC) (National School of Civil Aviation), Toulouse, France, May 2024
  
  abstract

  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.

• Systems Modelling with Bigraphs
  École nationale de l'aviation civile (ENAC) (National School of Civil Aviation), Toulouse, France, June 2022
  
  abstract

  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 of the 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.

• Problems of uncertainty in Sensor System Software
  London Interdisciplinary Biosciences Consortium (LIDo) Teaching Week, London, February 2020
• Digital twinning for predicting component failures and service availability
  NATS Research Collaboration Conference, Southampton, September 2019
• Bigraphs with sharing and their algebra
  MSP101 Seminar Series, Mathematically Structured Programming Group, University of Strathclyde, Glasgow, May 2019
• Reliability analysis and forecasting for assets management and Computational models for autonomous navigation and mixed-reality systems
  China Aerodynamics Research and Development Center (CARDC), Mianyang (China), October 2018
• Air navigation services assets management with stochastic model checking
  EU-China Workshop on Aviation, Air Traffic Management, Safety and Security, University of Glasgow, June 2018
  
  abstract

  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).

• Formal models for target counting and Multi-Tenancy Wireless Sensor Networks
  National Chiao Tung University, Computer Science, Hsinchu (Taiwan), February 2018
  
  abstract

  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.

• Formal modelling and analysis of IoT systems with bigraphs
  Network Plus: Industrial Systems in the Digital Age Conference 2017 – Looking Beyond Industry 4.0, Glasgow, June 2017 (Poster presentation)
  [pdf]
• On Lions, Impala, and Bigraphs: Modelling Interactions in Physical/Virtual Spaces
  ACM CHI 2017, Denver (USA), May 2017
  
  abstract

  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 with sharing and their algebra
  Algebra Seminar series, School of Mathematics and Statistics, University of Glasgow, May 2016
  
  abstract

  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.

• An overview on Bigraphs with sharing and their applications
  ARM Research, Cambridge, April 2016
• IoT research at the Glasgow Computing S4 group
  NXP Smarter World Tour, East Kilbride, March 2016
• Life out on the Savannah...Formal Models meet Mixed-Reality Systems
  Electronics and Computer Science (ECS) Research Seminars, University of Southampton, February 2016
• An Overview on Bigraphs, their applications, and future research directions
  Computer Laboratory Systems Research Group Seminar series, University of Cambridge, January 2016
• What makes IoT insecure and how can bigraphs help?
  Workshop on "Systems Research Challenges in the Internet of Things", Newcastle, January 2016
• An introduction to bigraphs with sharing, with applications to comms and mixed-reality systems
  DEIB Seminar, Politecnico Milano (Italy), July 2015
• Life out on the Savannah...Formal Models meet Mixed-Reality Systems
  Computer Laboratory Systems Research Group Seminar series, University of Cambridge, June 2015
• Life out on the Savannah...Formal Models meet Mixed-Reality Systems
  Visiting Lecture Series hosted by the Mixed Reality Lab, University of Nottingham, January 2015
• Do I need to fix a failed component now, or can I wait until tomorrow?
  DACS group seminar, University of Twente (Netherlands), November 2014
• Formal models & analysis for UAVs
  Greener Aeronautics Symposium, University of Glasgow, November 2014
• Bigraphs with sharing: applications with runtime verification
  Robotics group webinar, UC Berkeley/University of Salzburg, May 2013
• Runtime verification of domestic wireless management with bigraphs with sharing
  SICSA Workshop on Cyber Physical Systems, University of Edinburgh, May 2013
• Applications of bigraphs with sharing
  3rd International Workshop on Bigraphs (Bigraph 2013), IT University of Copenhagen (Denmark), February 2013
  [abstract]
• Real-time verification with bigraphs with sharing
  Computer Laboratory Systems Research Group Seminar series, University of Cambridge, March 2012
  
• Modelling the 802.11 CSMA/CA protocol with bigraphs with sharing
  Seminar on developments in bigraphs, University of Edinburgh, October 2009
  [notes (pages 19-24)]