-
Conformal Safety Shielding for Imperfect-Perception Agents
Authors:
William Scarbro,
Calum Imrie,
Sinem Getir Yaman,
Kavan Fatehi,
Corina S. Pasareanu,
Radu Calinescu,
Ravi Mangal
Abstract:
We consider the problem of safe control in discrete autonomous agents that use learned components for imperfect perception (or more generally, state estimation) from high-dimensional observations. We propose a shield construction that provides run-time safety guarantees under perception errors by restricting the actions available to an agent, modeled as a Markov decision process, as a function of…
▽ More
We consider the problem of safe control in discrete autonomous agents that use learned components for imperfect perception (or more generally, state estimation) from high-dimensional observations. We propose a shield construction that provides run-time safety guarantees under perception errors by restricting the actions available to an agent, modeled as a Markov decision process, as a function of the state estimates. Our construction uses conformal prediction for the perception component, which guarantees that for each observation, the predicted set of estimates includes the actual state with a user-specified probability. The shield allows an action only if it is allowed for all the estimates in the predicted set, resulting in a local safety guarantee. We also articulate and prove a global safety property of existing shield constructions for perfect-perception agents bounding the probability of reaching unsafe states if the agent always chooses actions prescribed by the shield. We illustrate our approach with a case-study of an experimental autonomous system that guides airplanes on taxiways using high-dimensional perception DNNs.
△ Less
Submitted 12 June, 2025;
originally announced June 2025.
-
RESMETRIC: Analyzing Resilience to Enable Research on Antifragility
Authors:
Ferdinand Koenig,
Marc Carwehl,
Calum Imrie
Abstract:
A key feature in self-adaptive systems is resilience, which is an ongoing research topic. Recently, the community started to explore antifragility, which describes the improvement of resilience over time. While there are model-agnostic resilience metrics, there is currently no out-of-the-box tool for researchers and practitioners to determine to which degree their system is resilient. To facilitat…
▽ More
A key feature in self-adaptive systems is resilience, which is an ongoing research topic. Recently, the community started to explore antifragility, which describes the improvement of resilience over time. While there are model-agnostic resilience metrics, there is currently no out-of-the-box tool for researchers and practitioners to determine to which degree their system is resilient. To facilitate research on antifragility, we present ResMetric, a model-agnostic tool that calculates and visualizes various resilience metrics based on the quality of service over time. With ResMetric, researchers can evaluate their definition of resilience and antifragility. This paper highlights how ResMetric can be employed by demonstrating its use in a case study on gas detection.
△ Less
Submitted 30 January, 2025;
originally announced January 2025.
-
Safe Reinforcement Learning in Black-Box Environments via Adaptive Shielding
Authors:
Daniel Bethell,
Simos Gerasimou,
Radu Calinescu,
Calum Imrie
Abstract:
Empowering safe exploration of reinforcement learning (RL) agents during training is a critical challenge towards their deployment in many real-world scenarios. When prior knowledge of the domain or task is unavailable, training RL agents in unknown, \textit{black-box} environments presents an even greater safety risk. We introduce \mbox{ADVICE} (Adaptive Shielding with a Contrastive Autoencoder),…
▽ More
Empowering safe exploration of reinforcement learning (RL) agents during training is a critical challenge towards their deployment in many real-world scenarios. When prior knowledge of the domain or task is unavailable, training RL agents in unknown, \textit{black-box} environments presents an even greater safety risk. We introduce \mbox{ADVICE} (Adaptive Shielding with a Contrastive Autoencoder), a novel post-shielding technique that distinguishes safe and unsafe features of state-action pairs during training, and uses this knowledge to protect the RL agent from executing actions that yield likely hazardous outcomes. Our comprehensive experimental evaluation against state-of-the-art safe RL exploration techniques shows that ADVICE significantly reduces safety violations ($\approx\!\!50\%$) during training, with a competitive outcome reward compared to other techniques.
△ Less
Submitted 31 January, 2025; v1 submitted 28 May, 2024;
originally announced May 2024.
-
Formal Synthesis of Uncertainty Reduction Controllers
Authors:
Marc Carwehl,
Calum Imrie,
Thomas Vogel,
Genaína Rodrigues,
Radu Calinescu,
Lars Grunske
Abstract:
In its quest for approaches to taming uncertainty in self-adaptive systems (SAS), the research community has largely focused on solutions that adapt the SAS architecture or behaviour in response to uncertainty. By comparison, solutions that reduce the uncertainty affecting SAS (other than through the blanket monitoring of their components and environment) remain underexplored. Our paper proposes a…
▽ More
In its quest for approaches to taming uncertainty in self-adaptive systems (SAS), the research community has largely focused on solutions that adapt the SAS architecture or behaviour in response to uncertainty. By comparison, solutions that reduce the uncertainty affecting SAS (other than through the blanket monitoring of their components and environment) remain underexplored. Our paper proposes a more nuanced, adaptive approach to SAS uncertainty reduction. To that end, we introduce a SAS architecture comprising an uncertainty reduction controller that drives the adaptive acquisition of new information within the SAS adaptation loop, and a tool-supported method that uses probabilistic model checking to synthesise such controllers. The controllers generated by our method deliver optimal trade-offs between SAS uncertainty reduction benefits and new information acquisition costs. We illustrate the use and evaluate the effectiveness of our approach for mobile robot navigation and server infrastructure management SAS.
△ Less
Submitted 1 February, 2024; v1 submitted 30 January, 2024;
originally announced January 2024.
-
Analyzing and Debugging Normative Requirements via Satisfiability Checking
Authors:
Nick Feng,
Lina Marsso,
Sinem Getir Yaman,
Yesugen Baatartogtokh,
Reem Ayad,
Victória Oldemburgo de Mello,
Beverley Townsend,
Isobel Standen,
Ioannis Stefanakos,
Calum Imrie,
Genaína Nunes Rodrigues,
Ana Cavalcanti,
Radu Calinescu,
Marsha Chechik
Abstract:
As software systems increasingly interact with humans in application domains such as transportation and healthcare, they raise concerns related to the social, legal, ethical, empathetic, and cultural (SLEEC) norms and values of their stakeholders. Normative non-functional requirements (N-NFRs) are used to capture these concerns by setting SLEEC-relevant boundaries for system behavior. Since N-NFRs…
▽ More
As software systems increasingly interact with humans in application domains such as transportation and healthcare, they raise concerns related to the social, legal, ethical, empathetic, and cultural (SLEEC) norms and values of their stakeholders. Normative non-functional requirements (N-NFRs) are used to capture these concerns by setting SLEEC-relevant boundaries for system behavior. Since N-NFRs need to be specified by multiple stakeholders with widely different, non-technical expertise (ethicists, lawyers, regulators, end users, etc.), N-NFR elicitation is very challenging. To address this challenge, we introduce N-Check, a novel tool-supported formal approach to N-NFR analysis and debugging. N-Check employs satisfiability checking to identify a broad spectrum of N-NFR well-formedness issues (WFI), such as conflicts, redundancy, restrictiveness, insufficiency, yielding diagnostics which pinpoint their causes in a user-friendly way that enables non-technical stakeholders to understand and fix them. We show the effectiveness and usability of our approach through nine case studies in which teams of ethicists, lawyers, philosophers, psychologists, safety analysts, and engineers used N-Check to analyse and debug 233 N-NFRs comprising 62 issues for the software underpinning the operation of systems ranging from assistive-care robots and tree-disease detection drones to manufacturing collaborative robots.
△ Less
Submitted 11 January, 2024;
originally announced January 2024.
-
Bayesian Learning for the Robust Verification of Autonomous Robots
Authors:
Xingyu Zhao,
Simos Gerasimou,
Radu Calinescu,
Calum Imrie,
Valentin Robu,
David Flynn
Abstract:
Autonomous robots used in infrastructure inspection, space exploration and other critical missions operate in highly dynamic environments. As such, they must continually verify their ability to complete the tasks associated with these missions safely and effectively. Here we present a Bayesian learning framework that enables this runtime verification of autonomous robots. The framework uses prior…
▽ More
Autonomous robots used in infrastructure inspection, space exploration and other critical missions operate in highly dynamic environments. As such, they must continually verify their ability to complete the tasks associated with these missions safely and effectively. Here we present a Bayesian learning framework that enables this runtime verification of autonomous robots. The framework uses prior knowledge and observations of the verified robot to learn expected ranges for the occurrence rates of regular and singular (e.g., catastrophic failure) events. Interval continuous-time Markov models defined using these ranges are then analysed to obtain expected intervals of variation for system properties such as mission duration and success probability. We apply the framework to an autonomous robotic mission for underwater infrastructure inspection and repair. The formal proofs and experiments presented in the paper show that our framework produces results that reflect the uncertainty intrinsic to many real-world systems, enabling the robust verification of their quantitative properties under parametric uncertainty.
△ Less
Submitted 11 December, 2023; v1 submitted 15 March, 2023;
originally announced March 2023.
-
Closed-loop Analysis of Vision-based Autonomous Systems: A Case Study
Authors:
Corina S. Pasareanu,
Ravi Mangal,
Divya Gopinath,
Sinem Getir Yaman,
Calum Imrie,
Radu Calinescu,
Huafeng Yu
Abstract:
Deep neural networks (DNNs) are increasingly used in safety-critical autonomous systems as perception components processing high-dimensional image data. Formal analysis of these systems is particularly challenging due to the complexity of the perception DNNs, the sensors (cameras), and the environment conditions. We present a case study applying formal probabilistic analysis techniques to an exper…
▽ More
Deep neural networks (DNNs) are increasingly used in safety-critical autonomous systems as perception components processing high-dimensional image data. Formal analysis of these systems is particularly challenging due to the complexity of the perception DNNs, the sensors (cameras), and the environment conditions. We present a case study applying formal probabilistic analysis techniques to an experimental autonomous system that guides airplanes on taxiways using a perception DNN. We address the above challenges by replacing the camera and the network with a compact probabilistic abstraction built from the confusion matrices computed for the DNN on a representative image data set. We also show how to leverage local, DNN-specific analyses as run-time guards to increase the safety of the overall system. Our findings are applicable to other autonomous systems that use complex DNNs for perception.
△ Less
Submitted 6 February, 2023;
originally announced February 2023.
-
Discrete-Event Controller Synthesis for Autonomous Systems with Deep-Learning Perception Components
Authors:
Radu Calinescu,
Calum Imrie,
Ravi Mangal,
Genaína Nunes Rodrigues,
Corina Păsăreanu,
Misael Alpizar Santana,
Gricel Vázquez
Abstract:
We present DeepDECS, a new method for the synthesis of correct-by-construction discrete-event controllers for autonomous systems that use deep neural network (DNN) classifiers for the perception step of their decision-making processes. Despite major advances in deep learning in recent years, providing safety guarantees for these systems remains very challenging. Our controller synthesis method add…
▽ More
We present DeepDECS, a new method for the synthesis of correct-by-construction discrete-event controllers for autonomous systems that use deep neural network (DNN) classifiers for the perception step of their decision-making processes. Despite major advances in deep learning in recent years, providing safety guarantees for these systems remains very challenging. Our controller synthesis method addresses this challenge by integrating DNN verification with the synthesis of verified Markov models. The synthesised models correspond to discrete-event controllers guaranteed to satisfy the safety, dependability and performance requirements of the autonomous system, and to be Pareto optimal with respect to a set of optimisation objectives. We use the method in simulation to synthesise controllers for mobile-robot collision mitigation and for maintaining driver attentiveness in shared-control autonomous driving.
△ Less
Submitted 27 March, 2023; v1 submitted 7 February, 2022;
originally announced February 2022.
