Adaptive Shielding via Parametric Safety Proofs

TL;DR

This paper introduces a programming framework for designing adaptive safety shields for learning-enabled cyber-physical systems, enabling flexible, knowledge-based safety guarantees that improve as the system learns from the environment.

Contribution

It presents a novel language-based approach for specifying and inferring adaptive safety shields with formal probabilistic guarantees, addressing limitations of existing model-checking methods.

Findings

Enables static specification of adaptive shields with knowledge-dependent safety models.

Provides a domain-specific language for runtime knowledge inference.

Offers rigorous probabilistic safety guarantees through theorem proving.

Abstract

A major challenge to deploying cyber-physical systems with learning-enabled controllers is to ensure their safety, especially in the face of changing environments that necessitate runtime knowledge acquisition. Model-checking and automated reasoning have been successfully used for shielding, i.e., to monitor untrusted controllers and override potentially unsafe decisions, but only at the cost of hard tradeoffs in terms of expressivity, safety, adaptivity, precision and runtime efficiency. We propose a programming-language framework that allows experts to statically specify adaptive shields for learning-enabled agents, which enforce a safe control envelope that gets more permissive as knowledge is gathered at runtime. A shield specification provides a safety model that is parametric in the current agent's knowledge. In addition, a nondeterministic inference strategy can be specified using a dedicated domain-specific language, enforcing that such knowledge parameters are inferred at runtime in a statistically-sound way. By leveraging language design and theorem proving, our proposed framework empowers experts to design adaptive shields with an unprecedented level of modeling flexibility, while providing rigorous, end-to-end probabilistic safety guarantees.