-
Modelling Real-time Systems with Bigraphs
Authors:
Maram Albalwe,
Blair Archibald,
Michele Sevegnani
Abstract:
Bigraphical Reactive Systems (BRSs) are a graph-rewriting formalism describing systems evolving in two dimensions: spatially, e.g. a person in a room, and non-spatially, e.g. mobile phones communicating regardless of location. Despite use in domains including communication protocols, agent programming, biology, and security, there is no support for real-time systems. We extend BRSs to support real…
▽ More
Bigraphical Reactive Systems (BRSs) are a graph-rewriting formalism describing systems evolving in two dimensions: spatially, e.g. a person in a room, and non-spatially, e.g. mobile phones communicating regardless of location. Despite use in domains including communication protocols, agent programming, biology, and security, there is no support for real-time systems. We extend BRSs to support real-time systems with a modelling approach that uses multiple perspectives to represent digital clocks. We use Action BRSs, a recent extension of BRSs, where the resulting transition system is a Markov Decision Process (MDP). This allows a natural representation of the choices in each system state: to either allow time to pass or perform a specific action. We implement our proposed approach using the BigraphER toolkit, and demonstrate the effectiveness through multiple examples including modelling cloud system requests.
△ Less
Submitted 26 March, 2025;
originally announced May 2025.
-
Federated Deep Reinforcement Learning for Privacy-Preserving Robotic-Assisted Surgery
Authors:
Sana Hafeez,
Sundas Rafat Mulkana,
Muhammad Ali Imran,
Michele Sevegnani
Abstract:
The integration of Reinforcement Learning (RL) into robotic-assisted surgery (RAS) holds significant promise for advancing surgical precision, adaptability, and autonomous decision-making. However, the development of robust RL models in clinical settings is hindered by key challenges, including stringent patient data privacy regulations, limited access to diverse surgical datasets, and high proced…
▽ More
The integration of Reinforcement Learning (RL) into robotic-assisted surgery (RAS) holds significant promise for advancing surgical precision, adaptability, and autonomous decision-making. However, the development of robust RL models in clinical settings is hindered by key challenges, including stringent patient data privacy regulations, limited access to diverse surgical datasets, and high procedural variability. To address these limitations, this paper presents a Federated Deep Reinforcement Learning (FDRL) framework that enables decentralized training of RL models across multiple healthcare institutions without exposing sensitive patient information. A central innovation of the proposed framework is its dynamic policy adaptation mechanism, which allows surgical robots to select and tailor patient-specific policies in real-time, thereby ensuring personalized and Optimised interventions. To uphold rigorous privacy standards while facilitating collaborative learning, the FDRL framework incorporates secure aggregation, differential privacy, and homomorphic encryption techniques. Experimental results demonstrate a 60\% reduction in privacy leakage compared to conventional methods, with surgical precision maintained within a 1.5\% margin of a centralized baseline. This work establishes a foundational approach for adaptive, secure, and patient-centric AI-driven surgical robotics, offering a pathway toward clinical translation and scalable deployment across diverse healthcare environments.
△ Less
Submitted 17 May, 2025;
originally announced May 2025.
-
Modelling Privacy Compliance in Cross-border Data Transfers with Bigraphs
Authors:
Ebtihal Althubiti,
Michele Sevegnani
Abstract:
Advancements in information technology have led to the sharing of users' data across borders, raising privacy concerns, particularly when destination countries lack adequate protection measures. Regulations like the European General Data Protection Regulation (GDPR) govern international data transfers, imposing significant fines on companies failing to comply. To achieve compliance, we propose a p…
▽ More
Advancements in information technology have led to the sharing of users' data across borders, raising privacy concerns, particularly when destination countries lack adequate protection measures. Regulations like the European General Data Protection Regulation (GDPR) govern international data transfers, imposing significant fines on companies failing to comply. To achieve compliance, we propose a privacy framework based on Milner's Bigraphical Reactive Systems (BRSs), a formalism modelling spatial and non-spatial relationships between entities. BRSs evolve over time via user-specified rewriting rules, defined algebraically and diagrammatically. In this paper, we rely on diagrammatic notations, enabling adoption by end-users and privacy experts without formal modelling backgrounds. The framework comprises predefined privacy reaction rules modelling GDPR requirements for international data transfers, properties expressed in Computation Tree Logic (CTL) to automatically verify these requirements with a model checker and sorting schemes to statically ensure models are well-formed. We demonstrate the framework's applicability by modelling WhatsApp's privacy policies.
△ Less
Submitted 26 March, 2025;
originally announced March 2025.
-
Towards Achieving Energy Efficiency and Service Availability in O-RAN via Formal Verification
Authors:
Roberto Metere,
Kangfeng Ye,
Yue Gu,
Zhi Zhang,
Dalal Alrajeh,
Michele Sevegnani,
Poonam Yadav
Abstract:
As Open Radio Access Networks (O-RAN) continue to expand, AI-driven applications (xApps) are increasingly being deployed enhance network management. However, developing xApps without formal verification risks introducing logical inconsistencies, particularly in balancing energy efficiency and service availability. In this paper, we argue that prior to their development, the formal analysis of xApp…
▽ More
As Open Radio Access Networks (O-RAN) continue to expand, AI-driven applications (xApps) are increasingly being deployed enhance network management. However, developing xApps without formal verification risks introducing logical inconsistencies, particularly in balancing energy efficiency and service availability. In this paper, we argue that prior to their development, the formal analysis of xApp models should be a critical early step in the O-RAN design process. Using the PRISM model checker, we demonstrate how our results provide realistic insights into the thresholds between energy efficiency and service availability. While our models are simplified, the findings highlight how AI-informed decisions can enable more effective cell-switching policies. We position formal verification as an essential practice for future xApp development, avoiding fallacies in real-world applications and ensuring networks operate efficiently.
△ Less
Submitted 6 November, 2024;
originally announced November 2024.
-
Practical Modelling with Bigraphs
Authors:
Blair Archibald,
Muffy Calder,
Michele Sevegnani
Abstract:
Bigraphs are a versatile modelling formalism that allows easy expression of placement and connectivity relations in a graphical format. System evolution is user defined as a set of rewrite rules. This paper presents a practical, yet detailed guide to developing, executing, and reasoning about bigraph models, including recent extensions such as parameterised, instantaneous, prioritised and conditio…
▽ More
Bigraphs are a versatile modelling formalism that allows easy expression of placement and connectivity relations in a graphical format. System evolution is user defined as a set of rewrite rules. This paper presents a practical, yet detailed guide to developing, executing, and reasoning about bigraph models, including recent extensions such as parameterised, instantaneous, prioritised and conditional rules, and probabilistic and stochastic rewriting.
△ Less
Submitted 31 May, 2024;
originally announced May 2024.
-
The Effect of Predictive Formal Modelling at Runtime on Performance in Human-Swarm Interaction
Authors:
Ayodeji O. Abioye,
William Hunt,
Yue Gu,
Eike Schneiders,
Mohammad Naiseh,
Joel E. Fischer,
Sarvapali D. Ramchurn,
Mohammad D. Soorati,
Blair Archibald,
Michele Sevegnani
Abstract:
Formal Modelling is often used as part of the design and testing process of software development to ensure that components operate within suitable bounds even in unexpected circumstances. In this paper, we use predictive formal modelling (PFM) at runtime in a human-swarm mission and show that this integration can be used to improve the performance of human-swarm teams. We recruited 60 participants…
▽ More
Formal Modelling is often used as part of the design and testing process of software development to ensure that components operate within suitable bounds even in unexpected circumstances. In this paper, we use predictive formal modelling (PFM) at runtime in a human-swarm mission and show that this integration can be used to improve the performance of human-swarm teams. We recruited 60 participants to operate a simulated aerial swarm to deliver parcels to target locations. In the PFM condition, operators were informed of the estimated completion times given the number of drones deployed, whereas in the No-PFM condition, operators did not have this information. The operators could control the mission by adding or removing drones from the mission and thereby, increasing or decreasing the overall mission cost. The evaluation of human-swarm performance relied on four key metrics: the time taken to complete tasks, the number of agents involved, the total number of tasks accomplished, and the overall cost associated with the human-swarm task. Our results show that PFM modelling at runtime improves mission performance without significantly affecting the operator's workload or the system's usability.
△ Less
Submitted 22 January, 2024;
originally announced January 2024.
-
Observable and Attention-Directing BDI Agents for Human-Autonomy Teaming
Authors:
Blair Archibald,
Muffy Calder,
Michele Sevegnani,
Mengwei Xu
Abstract:
Human-autonomy teaming (HAT) scenarios feature humans and autonomous agents collaborating to meet a shared goal. For effective collaboration, the agents must be transparent and able to share important information about their operation with human teammates. We address the challenge of transparency for Belief-Desire-Intention agents defined in the Conceptual Agent Notation (CAN) language. We extend…
▽ More
Human-autonomy teaming (HAT) scenarios feature humans and autonomous agents collaborating to meet a shared goal. For effective collaboration, the agents must be transparent and able to share important information about their operation with human teammates. We address the challenge of transparency for Belief-Desire-Intention agents defined in the Conceptual Agent Notation (CAN) language. We extend the semantics to model agents that are observable (i.e. the internal state of tasks is available), and attention-directing (i.e. specific states can be flagged to users), and provide an executable semantics via an encoding in Milner's bigraphs. Using an example of unmanned aerial vehicles, the BigraphER tool, and PRISM, we show and verify how the extensions work in practice.
△ Less
Submitted 24 October, 2021;
originally announced October 2021.
-
Modelling and Verifying BDI Agents with Bigraphs
Authors:
Blair Archibald,
Muffy Calder,
Michele Sevegnani,
Mengwei Xu
Abstract:
The Belief-Desire-Intention (BDI) architecture is a popular framework for rational agents; most verification approaches are based on reasoning about implementations of BDI programming languages. We investigate an alternative approach based on reasoning about BDI agent semantics, through a model of the execution of an agent program. We employ Milner's bigraphs as the modelling framework and present…
▽ More
The Belief-Desire-Intention (BDI) architecture is a popular framework for rational agents; most verification approaches are based on reasoning about implementations of BDI programming languages. We investigate an alternative approach based on reasoning about BDI agent semantics, through a model of the execution of an agent program. We employ Milner's bigraphs as the modelling framework and present an encoding for the Conceptual Agent Notation (CAN) language - a superset of AgentSpeak featuring declarative goals, concurrency, and failure recovery.
We provide an encoding of the syntax and semantics of CAN agents, and give a rigorous proof that the encoding is faithful. Verification is based on the use of mainstream software tools including BigraphER, and a small case study verifying several properties of Unmanned Aerial Vehicles (UAVs) illustrates the framework in action. The executable framework is a foundational step that will enable more advanced reasoning such as plan preference, intention priorities and trade-offs, and interactions with an environment under uncertainty.
△ Less
Submitted 6 May, 2021;
originally announced May 2021.
-
Probablistic Bigraphs
Authors:
Blair Archibald,
Muffy Calder,
Michele Sevegnani
Abstract:
Bigraphs are a universal computational modelling formalism for the spatial and temporal evolution of a system in which entities can be added and removed. We extend bigraphs to probablistic bigraphs, and then again to action bigraphs, which include non-determinism and rewards. The extensions are implemented in the BigraphER toolkit and illustrated through examples of virus spread in computer networ…
▽ More
Bigraphs are a universal computational modelling formalism for the spatial and temporal evolution of a system in which entities can be added and removed. We extend bigraphs to probablistic bigraphs, and then again to action bigraphs, which include non-determinism and rewards. The extensions are implemented in the BigraphER toolkit and illustrated through examples of virus spread in computer networks and data harvesting in wireless sensor systems. BigraphER also supports the existing stochastic bigraphs extension of Krivine et al., and using BigraphER we give, for the first time, a direct implementation of the membrane budding model used to motivate stochastic bigraphs.
△ Less
Submitted 6 May, 2021;
originally announced May 2021.
-
Analysing Spatial Properties on Neighbourhood Spaces
Authors:
Sven Linker,
Fabio Papacchini,
Michele Sevegnani
Abstract:
We present a bisimulation relation for neighbourhood spaces, a generalisation of topological spaces. We show that this notion, path preserving bisimulation, preserves formulas of the spatial logic SLCS. We then use this preservation result to show that SLCS cannot express standard topological properties such as separation and connectedness. Furthermore, we compare the bisimulation relation with st…
▽ More
We present a bisimulation relation for neighbourhood spaces, a generalisation of topological spaces. We show that this notion, path preserving bisimulation, preserves formulas of the spatial logic SLCS. We then use this preservation result to show that SLCS cannot express standard topological properties such as separation and connectedness. Furthermore, we compare the bisimulation relation with standard modal bisimulation and modal bisimulation with converse on graphs and prove it coincides with the latter.
△ Less
Submitted 2 July, 2020;
originally announced July 2020.
-
Formalising Sensor Topologies for Target Counting
Authors:
Sven Linker,
Michele Sevegnani
Abstract:
We present a formal model developed to reason about topologies created by sensor ranges. This model is used to formalise the topological aspects of an existing counting algorithm to estimate the number of targets in the area covered by the sensors. To that end, we present a first-order logic tailored to specify relations between parts of the space with respect to sensor coverage. The logic serves…
▽ More
We present a formal model developed to reason about topologies created by sensor ranges. This model is used to formalise the topological aspects of an existing counting algorithm to estimate the number of targets in the area covered by the sensors. To that end, we present a first-order logic tailored to specify relations between parts of the space with respect to sensor coverage. The logic serves as a specification language for Hoare-style proofs of correctness of the topological computations of the algorithm, which uncovers ambiguities in their results. Subsequently, we extend the formal model as a step towards improving the estimation of the algorithm. Finally, we sketch how the model can be extended to take mobile sensors and temporal aspects into account.
△ Less
Submitted 5 February, 2018;
originally announced February 2018.
