Title: Following the STARS: Dynamic ω-Regular Shielding of Learned Policies

Speaker: Ashwani Anand    (bio) (bio)

Ashwani Anand is a final-year PhD scholar at the Max Planck Institute for Software Systems (MPI-SWS), advised by Rupak Majumdar and Anne-Kathrin Schmuck. Prior to MPI-SWS, he earned a Master's in Computer Science and a Bachelor’s in Mathematics and Computer Science from the Chennai Mathematical Institute. His research focuses on the synthesis and verification of distributed systems, using two-player game models to construct systems that meet formal specifications—correct by construction, while remaining robust to change in practice. More recently, Ashwani's work has turned to providing formal guarantees for learned models to enable safer automated systems.

When: Tuesday, 10 February 2026 at 1900 hrs (IST)  

Meeting Details: Zoom link, ID: 891 6409 4870, Passcode: 082194

Abstract:
In this talk, I will present 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.

This talk is based on joint work with Satya Prakash Nayak, Ritam Raha and Anne-Kathrin Schmuck, which will appear at AAMAS 2026.