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

TL;DR

This paper introduces STARs, a dynamic shielding framework that enforces both safety and liveness in learned policies, allowing flexible, runtime-adaptive control over correctness properties in cyber-physical systems.

Contribution

The paper proposes a novel dynamic post-shielding method using Strategy-Template-based Adaptive Runtime Shields (STARs) that enforce $oldsymbol{ ext{omega}}$-regular properties with tunable interference and adaptability.

Findings

STARs effectively enforce $oldsymbol{ ext{omega}}$-regular properties on learned policies.

The framework allows dynamic adjustment of enforcement aggressiveness.

Experimental results on a mobile robot benchmark demonstrate controllable interference.

Abstract

This paper presents a novel dynamic post-shielding framework that enforces the full class of $\omega$-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) $\omega$-regular correctness properties over learned probabilistic policies.