Papers

My publications are also listed on Google Scholar and DBLP. Alphabetical order of authors means equal contributions.

Recent works submitted for publication

• Mapping the Probabilistic AI Ecosystem in Criminal Justice in England and Wales
  Evdoxia Taka, Temitope Lawal, Muffy Calder, Michele Sevegnani, Kyriakos Kotsoglou, Elizabeth McClory-Tiarks, and Marion Oswald
  [preprint]
• Responsible AI in criminal justice: LLMs in policing and risks to case progression
  Muffy Calder, Marion Oswald, Elizabeth McClory-Tiarks, Michele Sevegnani, and Evdoxia Taka
  [preprint]
• NeuroFM: Toward Precision Neuroimaging with Foundation Models for Individualized Brain Health Estimation
  Austin Dibble, Connor Dalby, Michele Sevegnani, Alessio Fracasso, Donald M Lyall, Monika Harvey, and Michele Svanera
  [preprint]
• From Subsumption to Satisfiability: LLM-Assisted Active Learning for OWL Ontologies
  Haoruo Zhao, Wenshuo Tang, Duncan Guthrie, Michele Sevegnani, David Flynn, and Paul Harvey
  [preprint]
• Interactive 3D Debugging of Bigraph-Based Spatial CPS Models
  Dominik Grzelak, Michele Sevegnani, and Uwe Aßmann
• A Safeguarded Large Language Model Framework for Autonomous IoT Management
  Yao Ge, Yue Gu, Michele Sevegnani, Qammer Abbasi, Muhammad Imran, and Muffy Calder
• Verification of Graphical Interfaces Using a Formal Intermediate Language
  Nicolas Nalpon, Cyril Allignol, Blair Archibald, Celia Picard, and Michele Sevegnani

Published research

1. The Need for Assessment of the Cascade Effects from Sequencing AI Systems in Policing
   Evdoxia Taka, Temitope Lawal, and Michele Sevegnani
   extended abstract in Inclusive AI: Rethinking AI-based Multimodal Interaction for Diverse and Underrepresented Users (workshop at the 28th International Conference on Multimodal Interaction, ICMI Companion Publication), Naples, Italy, October 2026, pp 506--510
   [pdf] [doi] [bib]
2. Certified Intersection of Commutative Regular Expressions as Solutions of Systems of Linear Diophantine Equations
   Ricardo Almeida, Blair Archibald, Basile Pesin, and Michele Sevegnani
   in 17th International Conference on Interactive Theorem Proving (ITP), Lisbon, Portugal, July 2026, Leibniz International Proceedings in Informatics (LIPIcs), volume 382, pp 7:1--7:20, 2026
   [pdf] [doi] [bib] [CORE]
3. Reachability Specification Adaptation for Continuous Dynamical Systems
   Zhi Zhang, Dalal Alrajeh, Yue Gu, Roberto Metere, Michele Sevegnani, Kangfeng Ye, and Poonam Yadav
   in International Symposium DataMod, Toledo, Spain, November 2025, Lecture Notes in Computer Science, pp 54--66, Springer, 2026
   [pdf] [doi] [bib]
4. A nanopass approach to a modular RDF implementation
   Duncan Guthrie, Paul Harvey, and Michele Sevegnani
   in ACM SIGPLAN International Conference on Software Language Engineering (SLE), pp 22--33, 2026
   [pdf] [doi] [bib] [CORE]
5. The Domain Relationship Diagram: a Mapping Framework for Digital Twin Design in Complex Cyber-Physical Ecosystems
   Matt Tipuric, Daniel Mitchell, Blair Archibald, David Flynn, Paul Harvey, Michele Sevegnani, and David Wagg
   in Research in Engineering Design, volume 37, pp 25, 2026
   [pdf] [doi] [bib] [SJR]
6. Delineating In Vivo T1-Weighted Intensity Profiles Within the Human Insula Cortex Using 7-Tesla MRI
   Connor Dalby, Austin Dibble, J. Carvalheiro, F. Queirazza, Michele Sevegnani, M. Harvey, Michele Svanera, and Alessio Fracasso
   in Human Brain Mapping, volume 47, no. 4, pp e70486, 2026
   [pdf] [doi] [bib] [SJR]
7. A Challenge-Led Digital Twin Federation Architecture For Urban Passenger Transport Decarbonisation
   Jingjun Li, Heather Steele, Joseph Preece, David Kirkwood, Shiqi Sun, Wenhua Jiang, Alan Logan, Susmoy Das, Ricardo Almeida, Michele Sevegnani, John Easton, Clive Roberts, David Flynn, and Philip Greening
   in Procedia Computer Science, volume 280, pp 303--311, Elsevier, April 2026
   [pdf] [doi] [bib]
8. Introducing The Maximum Common Bigraph Problem
   Kyle Burns, Michele Sevegnani, Ciaran McCreesh, and James Trimble
   in International Workshop on Graph Computation Models (GCM), Koblenz, Germany, 2025
   [pdf] [doi] [bib]
9. Modelling Railway Networks with Bigraphs: Electrification, Failures, and Optimisation
   Ricardo Almeida, Susmoy Das, Blair Archibald, Muffy Calder, and Michele Sevegnani
   Modelling, Analysis, Verification, and Certification (RSSRail 2025), Pisa, Italy, Lecture Notes in Computer Science, vol 16236. Springer, 2026
   [pdf] [doi] [bib]
10. Federated Deep Reinforcement Learning for Privacy-Preserving Robotic-Assisted Surgery
    Sana Hafeez, Sundas Rafat Mulkana, Muhammad Ali Imran, and Michele Sevegnani
    in IEEE 45th International Conference on Distributed Computing Systems Workshops (ICDCSW), Glasgow, United Kingdom, pp 689--699, 2025
    [pdf] [doi] [bib]
11. Rational Verification in Repeated Security Games
    Surasak Phetmanee, Michele Sevegnani, and Oana Andrei
    in International Workshop on Safety-Security Interaction (SENSEI), Lecture Notes in Computer Science, volume 15955, pp 312--326, Springer, 2025.
    [pdf] [doi] [bib]
12. Formal Analysis of Resilience in Transport Systems with Bigraphs
    Susmoy Das, Ricardo Almeida, Blair Archibald, and Michele Sevegnani
    in International Workshop on Safety/Reliability/Trustworthiness of Intelligent Transportation Systems (SRToITS), Lecture Notes in Computer Science, volume 15955, pp 423--436, Springer, 2025
    [pdf] [doi] [bib]
13. Millimeter-Wave Contactless Vital Sign Monitoring Using Dynamic Metasurface Antenna
    Abdul Jabbar, Naila Azam, Prisila Ishabakaki, Masood Ur-Rehman, Muhammad Ali Imran, Michele Sevegnani, Hadi Larijani, Syed Aziz Shah, Qammer Abbasi, and Muhammad Usman
    in IEEE Antennas and Wireless Propagation Letters, August 2025
    [pdf] [doi] [bib] [SJR]
14. A Cyber Physical Architecture for Symbiotic Multi-robot Fleet Management Daniel Mitchell, Yue Gu, Jamie Blanche, Samuel Harper, Blair Archibald, Michele Sevegnani, and David Flynn
    in Virtual and Augmented Reality Technology-Enhanced Learning: Research and Applications, pp 379--421, Springer Nature Singapore, June 2025
    [pdf] [doi] [bib]
15. Formalising Privacy Regulations with Bigraphs
    Ebtihal Althubiti, Blair Archibald, and Michele Sevegnani
    in International Journal on Software and Systems Modeling (SoSyM), 2025
    [pdf] [doi] [bib] [SJR]
16. A User Study Evaluation of Predictive Formal Modelling at Runtime in Human-Swarm Interaction
    Ayodeji O. Abioye, William Hunt, Yue Gu, Eike Schneiders, Mohammad Naiseh, Blair Archibald, Michele Sevegnani, Sarvapali D. Ramchurn, Joel E. Fischer, and Mohammad D. Soorati
    in ACM Transactions on Human-Robot Interaction, 2025
    [pdf] [doi] [bib] [SJR]
17. Practical Modelling with Bigraphs
    Blair Archibald, Muffy Calder, and Michele Sevegnani
    in ACM Formal Aspects of Computing Journal, 2025
    [pdf] [doi] [bib] [SJR]
18. BiCoq : Bigraphs Formalisation with Coq
    Cecile Marcon, Cyril Allignol, Celia Picard, Blair Archibald, Michele Sevegnani, and Xavier Thirioux
    in ACM/SIGAPP Symposium On Applied Computing (Software Verification and Testing Track), pp 1982--1989, ACM, 2025
    [pdf] [doi] [bib] [CORE]
19. Towards Achieving Energy Efficiency and Service Availability in O-RAN via Formal Verification
    Roberto Metere, Kangfeng Ye, Yue Gu, Zhi Zhang, Dalal Alrajeh, Michele Sevegnani, and Poonam Yadav
    in International Symposium DataMod, Aveiro, Portugal, November 2024
    [pdf] [doi] [bib]
20. StEVe: A Rational Verification Tool for Stackelberg Security Games
    Surasak Phetmanee, Oana Andrei, and Michele Sevegnani
    in International Conference on integrated Formal Methods (iFM), Manchester, UK, November 2024
    [pdf] [doi] [bib] [CORE]
21. Modelling and Analysing Routing Protocols Diagrammatically with Bigraphs
    Maram Albalwe, Blair Archibald, and Michele Sevegnani
    in ACM Formal Aspects of Computing Journal, volume 36, issue 3, pp 1--25, September 2024
    [pdf] [doi] [slides] [post] [bib] [SJR]
22. Modelling Real-time Systems with Bigraphs
    Maram Albalwe, Blair Archibald, and Michele Sevegnani
    in International Workshop on Graph Computation Models (GCM), Enschede, Netherlands, July 2024
    [pdf] [doi] [bib]
23. Modelling Privacy Compliance in Cross-border Data Transfers with Bigraphs
    Ebtihal Althubiti, Blair Archibald, and Michele Sevegnani
    in International Workshop on Graph Computation Models (GCM), Enschede, Netherlands, July 2024
    [pdf] [doi] [bib]
24. A Bigraphs Paper of Sorts
    Blair Archibald and Michele Sevegnani
    in International Conference on Graph Transformation (ICGT), Lecture Notes in Computer Science, 14774, pp 21--38, Springer, July 2024
    [pdf] [doi] [bib] [CORE]
25. The Effect of Predictive Formal Modelling at Runtime on Performance in Human-Swarm Interaction
    Ayodeji O. Abioye, William Hunt, Yue Gu, Eike Schneiders, Mohammad Naiseh, Joel E. Fischer, Sarvapali D. Ramchurn, Mohammad D. Soorati, Blair Archibald, and Michele Sevegnani
    in ACM/IEEE International Conference on Human Robot Interaction (HRI), Boulder, Colorado, USA, March 2024
    [pdf] [doi] [bib] [CORE]
    video
26. CAN-verify: A Verification Tool for BDI Agents
    Mengwei Xu, Thibault Rivoalen, Blair Archibald, and Michele Sevegnani
    in International Conference on integrated Formal Methods (iFM), Leiden, the Netherlands, November 2023
    [pdf] [doi] [bib] [CORE]
27. Quantitative Modelling and Analysis of BDI Agents
    Blair Archibald, Muffy Calder, Michele Sevegnani, and Mengwei Xu
    in International Journal on Software and Systems Modeling (SoSyM), volume 23, pp 343--367, August 2023
    [pdf] [doi] [bib] [SJR]
28. Successful Swarms: Operator Situational Awareness with Modelling and Verification at Runtime
    Yue Gu, William Hunt, Blair Archibald, Mengwei Xu, Michele Sevegnani, and Mohammad D. Soorati
    in IEEE International Conference on Robot and Human Interactive Communication (RO-MAN 2023), Busan, Korea, 28-31 August 2023
    [pdf] [doi] [bib]
    video
29. Quantitative Verification and Strategy Synthesis for BDI Agents
    Mengwei Xu, Blair Archibald, Muffy Calder, and Michele Sevegnani
    in NASA Formal Methods Symposium (NFM 2023), Houston, TX, USA, 2023
    [pdf] [doi] [slides] [bib]
30. Adaptive Model Verification for Modularised Industry 4.0 Applications
    Xin Xin, Sye Loong Keoh, Michele Sevegnani, Martin Saerbeck, and Teck Ping Khoo
    in IEEE Access, volume 10, pp 125353--125364, 2022
    [pdf] [doi] [bib] [SJR]
31. Run-Time Probabilistic Model Checking for Failure Prediction: A Smart Lift Case Study
    Xin Xin, Sye Loong Keoh, Michele Sevegnani, and Martin Saerbeck
    in IEEE 8th World Forum on Internet of Things (WF-IoT2022), Yokohama, Japan, 31 October - 4 November, 2022
    [pdf] [doi] [bib]
32. Probabilistic Bigraphs
    Blair Archibald, Muffy Calder, and Michele Sevegnani
    in ACM Formal Aspects of Computing Journal, volume 34, issue 2, June 2022
    [pdf] [doi] [bib] [SJR]
33. Verifying BDI Agents in Dynamic Environments
    Mengwei Xu, Blair Archibald, Muffy Calder, and Michele Sevegnani
    in proceedings of 34th International Conference on Software Engineering & Knowledge Engineering (SEKE 2022), Pittsburgh, USA, July 2022
    [pdf] [doi] [bib] [CORE]
34. Fine-grained RNN with Transfer Learning for Energy Consumption Estimation on EVs
    Yining Hua, Michele Sevegnani, Dewei Yi, Andrew Birnie, and Steve McAslan
    in IEEE Transactions on Industrial Informatics, volume 18, issue 11, pp 8182--8190, November 2022
    [pdf] [doi] [bib] [SJR]
35. Modelling and Verifying BDI Agents with Bigraphs
    Blair Archibald, Muffy Calder, Michele Sevegnani, and Mengwei Xu
    in Science of Computer Programming, volume 215, pp 288--310, Elsevier, March 2022
    [pdf] [doi] [bib] [SJR]
36. Probabilistic BDI Agents: Actions, Plans, and Intentions
    Blair Archibald, Muffy Calder, Michele Sevegnani, and Mengwei Xu
    in proceedings of 19th International Conference on Software Engineering and Formal Methods (SEFM 2021)
    [pdf] [doi] [bib] [CORE]
37. Practical Bigraphs via Subgraph Isomorphism
    Blair Archibald, Kyle Burns, Ciaran McCreesh, and Michele Sevegnani
    in proceedings of 27th International Conference on Principles and Practice of Constraint Programming (CP 2021)
    [pdf] [doi] [video] [bib] [CORE]
38. Observable and Attention-Directing BDI Agents for Human-Autonomy Teaming
    Blair Archibald, Muffy Calder, Michele Sevegnani, and Mengwei Xu
    in proceedings of Third Workshop on Formal Methods for Autonomous Systems (FMAS 2021), Electronic Proceedings in Theoretical Computer Science, volume 348, pp 167--175, Virtual, October 2021
    [pdf] [doi] [bib]
39. A Tale of Two Graph Models: A Case Study in Wireless Sensor Networks
    Blair Archibald, Géza Kulcsár, and Michele Sevegnani
    in ACM Formal Aspects of Computing Journal, volume 33, issue 6, December 2021
    [pdf] [doi] [bib] [SJR]
40. Finite Models for a Spatial Logic with Discrete and Topological Path Operators
    Sven Linker, Fabio Papacchini, and Michele Sevegnani
    in proceedings of 46th International Symposium on Mathematical Foundations of Computer Science (MFCS 2021), Leibniz International Proceedings in Informatics (LIPIcs), volume 202, pp 72:1--72:16, Tallin, Estonia, August 2021
    [pdf] [doi] [bib] [CORE]
41. Analysing Spatial Properties on Neighbourhood Spaces
    Sven Linker, Fabio Papacchini, and Michele Sevegnani
    in proceedings of 45th International Symposium on Mathematical Foundations of Computer Science (MFCS 2020), Leibniz International Proceedings in Informatics (LIPIcs), volume 170, pp 66:1--66:14, Prague, Czech Republic, August 2020
    [pdf] [doi] [video] [bib] [CORE]
42. Dynamic Probabilistic Model Checking for Sensor Validation in Industry 4.0 Applications
    Xin Xin, Sye Loong Keoh, Michele Sevegnani, and Martin Saerbeck
    in proceedings of 2020 IEEE International Conference on Smart Internet of Things (IEEE SmartIoT 2020), volume 1, pp 43--50, Beijing, China, August 2020
    [pdf] [doi] [bib]
43. Conditional Bigraphs
    Blair Archibald, Muffy Calder, and Michele Sevegnani
    in proceedings of International Conference on Graph Transformation (ICGT 2020), Lecture Notes in Computer Science, volume 12150, pp 3--19, Bergen, Norway, June 2020
    [pdf] [doi] [video] [bib] [CORE]
44. BigraphTalk: Verified Design of IoT Applications
    Blair Archibald, Min-Zheng Shieh, Yu-Hsuan Hu, Michele Sevegnani, and Yi-Bing Lin
    in IEEE Internet of Things Journal, volume 7, issue 4, pp 2955--2967, April 2020
    [pdf] [doi] [bib] [SJR]
45. Target counting with Presburger constraints and its application in sensor networks
    Sven Linker and Michele Sevegnani
    in Proceedings of the Royal Society A, volume 475, issue 2231, November 2019
    [pdf] [doi] [bib] [SJR]
46. Stochastic model checking for predicting component failures and service availability
    Muffy Calder and Michele Sevegnani
    in IEEE Transactions on Dependable and Secure Computing (TDSC), volume 16, issue 1, pp 174--187, January 2019
    [pdf] [doi] [bib] [SJR]
47. Modelling and Verification of Large-Scale Sensor Network Infrastructures
    Michele Sevegnani, Milan Kabac, Muffy Calder, and Julie A. McCann
    in proceedings of International Conference on Engineering of Complex Computer Systems (ICECCS 2018), pp 71--81, IEEE, Melbourne, Australia, December 2018
    [pdf] [doi] [bib] [CORE]
48. Formalising Sensor Topologies for Target Counting
    Sven Linker and Michele Sevegnani
    in proceedings of 1st Workshop on Architectures, Languages and Paradigms for IoT (ALP4IoT 2017), Turin, Italy, September 2017
    [pdf] [doi] [bib]
49. BigraphER: rewriting and analysis engine for bigraphs
    Michele Sevegnani and Muffy Calder
    in proceedings of Computer Aided Verification (CAV 2016), Lecture Notes in Computer Science, volume 9780 Part II, pp 494--501, Springer, Toronto, Canada, July 2016
    [pdf] [doi] [bib] [CORE]
50. On lions, impala, and bigraphs: modelling interactions in physical/virtual spaces
    Steve Benford, Muffy Calder, Tom Rodden, and Michele Sevegnani
    in Transactions on Computer-Human Interaction (TOCHI), Issue 23:2, pp 9:1--9:56, ACM, May 2016
    [pdf] [doi] [bib] [supplementary material] [SJR]
51. Bigraphs with sharing
    Michele Sevegnani and Muffy Calder
    in Theoretical Computer Science, volume 577, pp 43--73, Elsevier, April 2015
    [pdf] [doi] [bib] [SJR]
52. Towards a Bigraphical Encoding of Actors
    Michele Sevegnani and Eloi Pereira
    in proceedings of 1st Workshop on Meta Models for Process Languages (MeMo'14), Berlin, Germany, June 2014
    [pdf] [bib]
53. Do I need to fix a failed component now, or can I wait until tomorrow?
    Muffy Calder and Michele Sevegnani
    in proceedings of European Dependable Computing Conference (EDCC'14), pp 70--81, IEEE, Newcastle, UK, May 2014
    [pdf] [doi] [bib]
54. Modelling IEEE 802.11 CSMA/CA RTS/CTS with stochastic bigraphs with sharing
    Muffy Calder and Michele Sevegnani
    in Formal Aspects of Computing, volume 26, issue 3, pp 537--561, Springer, May 2014
    [pdf] [doi] [bib] [SJR]
55. Real-time verification of wireless home networks using bigraphs with sharing
    Muffy Calder, Alexandros Koliousis, Michele Sevegnani, and Joseph Sventek
    in Science of Computer Programming, volume 80, part B, pp 288--310, Elsevier, February 2014
    [pdf] [doi] [bib] [SJR]
56. Process Algebra for Event-Driven Runtime Verification: A Case Study of Wireless Network Management
    Muffy Calder and Michele Sevegnani
    in proceedings of Integrated Formal Methods (IFM'12), Lecture Notes in Computer Science, volume 7321, pp 21--23, Springer, Pisa, Italy, June 2012
    [pdf] [doi] [bib] [CORE]
57. Bigraphs with sharing and applications in wireless networks
    Michele Sevegnani
    Ph.D. thesis, School of Computing Science, University of Glasgow, September 2012
    Nominated for the BCS Distinguished Dissertation Award '13
    [pdf] [bib]

Talks

• 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)]