Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Follow the STARs: Dynamic $ω$-Regular Shielding of Learned Policies

Ashwani Anand, Satya Prakash Nayak, Ritam Raha, Anne-Kathrin Schmuck

TL;DR

This work addresses the challenge of enforcing both safety and liveness properties for learned policies in autonomous systems by introducing Dynamic $\omega$-Regular Shielding with STARs. STARs blend a nominal policy with a parity-objective strategy template, enabling runtime enforcement of $\omega$-regular properties through controllable interference governed by a parameter $\gamma$ and a threshold $\theta$. The framework ensures correctness via winning strategy templates, proves minimal interference under suitable settings, and supports dynamic adaptations and composition of multiple specifications. Empirically, STARs improve liveness (frequency of visiting target regions) while maintaining near-optimal rewards, and scale to large, realistic benchmarks like FactoryBot, Overcooked-AI, and LunarLander, all without retraining the underlying policies.

Abstract

This paper presents a novel dynamic post-shielding framework that enforces the full class of $ω$-regular correctness properties over pre-computed probabilistic policies. This constitutes a paradigm shift from the predominant setting of safety-shielding -- i.e., ensuring that nothing bad ever happens -- to a shielding process that additionally enforces liveness -- i.e., ensures that something good eventually happens. At the core, our method uses Strategy-Template-based Adaptive Runtime Shields (STARs), which leverage permissive strategy templates to enable post-shielding with minimal interference. As its main feature, STARs introduce a mechanism to dynamically control interference, allowing a tunable enforcement parameter to balance formal obligations and task-specific behavior at runtime. This allows to trigger more aggressive enforcement when needed, while allowing for optimized policy choices otherwise. In addition, STARs support runtime adaptation to changing specifications or actuator failures, making them especially suited for cyber-physical applications. We evaluate STARs on a mobile robot benchmark to demonstrate their controllable interference when enforcing (incrementally updated) $ω$-regular correctness properties over learned probabilistic policies.

Follow the STARs: Dynamic $ω$-Regular Shielding of Learned Policies

TL;DR

This work addresses the challenge of enforcing both safety and liveness properties for learned policies in autonomous systems by introducing Dynamic -Regular Shielding with STARs. STARs blend a nominal policy with a parity-objective strategy template, enabling runtime enforcement of -regular properties through controllable interference governed by a parameter and a threshold . The framework ensures correctness via winning strategy templates, proves minimal interference under suitable settings, and supports dynamic adaptations and composition of multiple specifications. Empirically, STARs improve liveness (frequency of visiting target regions) while maintaining near-optimal rewards, and scale to large, realistic benchmarks like FactoryBot, Overcooked-AI, and LunarLander, all without retraining the underlying policies.

Abstract

This paper presents a novel dynamic post-shielding framework that enforces the full class of -regular correctness properties over pre-computed probabilistic policies. This constitutes a paradigm shift from the predominant setting of safety-shielding -- i.e., ensuring that nothing bad ever happens -- to a shielding process that additionally enforces liveness -- i.e., ensures that something good eventually happens. At the core, our method uses Strategy-Template-based Adaptive Runtime Shields (STARs), which leverage permissive strategy templates to enable post-shielding with minimal interference. As its main feature, STARs introduce a mechanism to dynamically control interference, allowing a tunable enforcement parameter to balance formal obligations and task-specific behavior at runtime. This allows to trigger more aggressive enforcement when needed, while allowing for optimized policy choices otherwise. In addition, STARs support runtime adaptation to changing specifications or actuator failures, making them especially suited for cyber-physical applications. We evaluate STARs on a mobile robot benchmark to demonstrate their controllable interference when enforcing (incrementally updated) -regular correctness properties over learned probabilistic policies.

Paper Structure

This paper contains 27 sections, 13 theorems, 5 equations, 12 figures.

Table of Contents

  1. Introduction
  2. Applications
  3. Related Work
  4. Preliminaries
  5. Dynamic $\omega$-Regular Shielding
  6. Dynamical Interference via STARs
  7. Correctness of STARs
  8. Minimal Interference of STARs
  9. Dynamic Adaptations of STARs
  10. Optimality of STARs in Rewardful MDPs
  11. Experiments
  12. FactoryBot Benchmarks
  13. Overcooked-AI Benchmarks
  14. LunarLander Benchmarks
  15. Additional Related Work
  16. ...and 12 more sections

Key Result

Theorem 5

Given the premises of def:shieldedPolicy it holds that $\sigma|^{\Gamma_\star,{\theta}}_{\gamma}$ follows $\Gamma_\star$. Moreover, if $\Gamma_\star:=\textsc{ParityTemplate}_\star(M,\Phi)$, then, every $\sigma|^{\Gamma_\star,{\theta}}_{\gamma}$-run from the winning region of $\Phi$ satisfies $\Phi$

Figures (12)

  • Figure 1: Applying STARs on different benchmarks. For FactoryBot : The agent must visit $\mathcal{B}$ (green), while maximizing the average reward (small numbers in cells). Images show the agent's heatmap without a shield (a), with our shield (b). For LunarLander: The agent must land on the helipad (between the flags) while avoiding crashing. Images show the lander's trajectory without a shield (c), with our shield (d).
  • Figure 2: Overview of STARs synthesis (left) and runtime-application of STARs (right). The detailed operation of STARs is illustrated in \ref{['fig:stesh']}. Cyan components are taken from the literature. Purple components illustrate dynamic adaptability.
  • Figure 3: Illustration of dynamic interference via STARs. Length of arrows indicate the relative probability of the corresponding action in $\mu\in\mathcal{D}(A(q))$. The strategy template $\Gamma=(S,D,H_\ell)$ is illustrated via colors red ($S$), orange ($D$) and green ($H_\ell$). Blending applies \ref{['eq:shieldpolicy:gamma']} in \ref{['def:stesh']}, bounding applies \ref{['eq:shieldpolicy:eps']} in \ref{['def:stesh']} and normalizing applies standard normalization, respectively.
  • Figure 4: Evaluation summary. (a) Effect of $\gamma$ on the üchi Büchi frequency and average reward for ApplySTARs in FactoryBot (b) üchi Büchi frequency vs. average reward for ApplySTARs and ApplyNaive (c) Scalability of ApplySTARs on Overcooked-AI.
  • Figure 5: (a) Rate of different landing outcomes in LunarLander (b) Average steps to successfully land in LunarLander.
  • ...and 7 more figures

Theorems & Definitions (23)

  • Definition 1
  • Definition 2: STARs
  • Remark 3
  • Definition 4
  • Theorem 5
  • Theorem 6
  • Theorem 7
  • Remark 8
  • Theorem 9
  • Remark 10
  • ...and 13 more