Adaptive Shielding via Parametric Safety Proofs

TL;DR

This work tackles safety for learning-enabled cyber-physical systems by introducing Adaptive Shielding via Parametric Safety Proofs, a programming-language framework in which experts specify parametric safety shields that adapt online as runtime knowledge improves. Shields are extracted from verified nondeterministic controllers using differential dynamic logic and are augmented with an inference-strategy language that sounds bound-parameter updates with probabilistic guarantees. The framework supports local bounds for functional unknowns, symbolic inference assignments, and compatible-environment wrappers that together yield end-to-end probabilistic safety guarantees while enabling learning-driven performance gains. Experimental case studies across train robotics, river crossing, and ACASX illustrate safety preservation, adaptability, and the ability to learn inference policies that optimize safety budgets and information gathering. The work shows how to push most safety analysis offline, enabling practical runtime overhead and offering a path toward scalable, rigorous, learnable shielding for complex hybrid systems.

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.

Figures (23)

• Figure 1: A Simple $\mathop{}\!\mathrm{d} \text{L}$ Model of a Train Braking-Control System DBLP:conf/hybrid/PlatzerQ08
• Figure 2: An adaptive shield for a train control system, where the relationship between the commanded and actual train acceleration is governed by an unknown linear function.
• Figure 3: An adaptive shield for a train control system where the railway tracks are assumed to follow an unkown, space-varying slope function. We write $\textsf{Bdist}_{v}(b) \equiv v^2/2b$. For simplicity, the train faces a binary choice between acceleration and braking (as in Figure \ref{['fig:overview-etcs']} and unlike in Figure \ref{['fig:overview-train-global']}).
• Figure 4: Adaptive Shielding Overview Diagram
• Figure 5: Syntax and semantics of $\mathop{}\!\mathrm{d} \text{L}$. $\mathcal{P}(\cdot)$ denotes the powerset operator.

Theorems & Definitions (9)

• lemma 1: Existence of a controller monitor and fallback policy
• definition 1: Sound inference assignment
• definition 2: Compatible environments
• definition 3: Shielded environment
• theorem 1: Safety of shielded environments
• theorem 2: Soundness of the inference strategy language
• definition 4: Consistent history
• definition 5: Consistent shielded state
• lemma 2: Consistency Preservation