Personal Website of Astrid Horn Brorholt

You might know me by my old name, Asger Horn Brorholt. Photo of me in a yellow raincoat. I have long hair and glasses.

I am a PhD student at Department of Computer Science, Aalborg University. My supervisors are Kim Guldstrand Larsen and Chistian Schilling. I focus my research on shielded AI, where a shield compontent filters the actions of an AI-agent, such that the system as a whole is guaranteed to be safe, even when the AI-agent alone is not. My pronouns are they/them.

(I enjoy attending game jams. Check out the games I've made at itch.io.)

Contact: astrid [at] hornbrorholt [dot] dk · astridhb [at] cs.aau [dot] dk · +4540250274

My Thesis

Scalable Shielded Reinforcement Learning for Cyber-physical Systems

Astrid Horn Brorholt

Aalborg Universitet

Summary Advanced digital controllers can efficiently manage many kinds of physical processes, such as self-driving cars, water systems, industrial hydraulics and electrical power grids. Safety in these cyber-physical systems is often crucial, since mistakes can lead to costly damage of equipment, or even bodily harm. As such, it is important that the correctness of the policies controlling these systems can be verified. However, many of the most advanced and efficient policies are highly complex. They are represented as e.g. neural networks, for which verifying safe behaviour is known to be intricately hard. In particular, reinforcement learning has been shown to find policies which perform well in cases where direct search for an optimal policy is computationally infeasible. Shielding is a promising method for ensuring correctness without the need to verify the safety of policies (or of reinforcement learning agents) directly. Shields limit the possible behaviour to a set of actions that are safe for the given system state. In this way it acts as a guardrail that keeps the agent away from unsafe situations. Shields are often synthesized from an abstract representation of the system, one whose behaviour only covers the aspects which are relevant to safety. With these abstractions it is possible to describe the set of safe behaviour, even if the system as a whole is too complex to directly compute a safe an optimal policy. Current research describes shield synthesis methods for a variety of settings, but their applicability for cyber-physical systems has so far been limited. Cyber-physical systems pose unique challenges: They may exhibit hybrid behaviour (a combination of discrete switches and continuous dynamics), have unknown components, and may have several agents interacting. This thesis is a collection of papers, which each seek to address aspects of these challenges. A method for scalably synthesizing hybrid shields is presented, and made available as an extension of the modelling tool #uppaal. Moreover, an approach to scalable shielding in multi-agent settings is presented, which decomposes a global (complex) safety property into local (tractable) shields. A method is also given for learning the behaviour of unknown systems, while an adaptive shield ensures safe behaviour based on existing knowledge. These methods can be combined to achieve verifiably safe behaviour in cyber-physical systems. With the use of a shield, a reinforcement learning agent can be safely trained to find an optimized and verifiably correct policy.
preprint

Research Publications

Adaptive Probabilistic Shielding by Learning MDPs for Safe Reinforcement Learning

Astrid Horn Brorholt, Maris F. L. Galesloot, Nils Jansen, Kim Guldstrand Larsen and Christian Schilling

To appear in Runtime Verification, RV 2026

Abstract Probabilistic shielding is a technique for safe reinforcement learning (RL). Typically, a static observer—called the shield—constrains the learning agent's actions to those for which acting safely remains feasible. Traditionally, the shield is computed from the transition probabilities of the underlying Markov decision process (MDP). Thus, this technique is not applicable when the MDP model is not given a priori, which, unfortunately, is the case in typical RL applications. In this paper, we study the problem of computing a shield in the setting where the transition graph of the MDP is known, but the transition probabilities are unknown. Our approach integrates probabilistic shielding with online model learning: as the RL agent explores the environment, we estimate the transition probabilities. From this estimate, we compute a shield. While the shield may be conservative initially, it adapts as the model estimate becomes more precise. Thus, the shield improves in tandem with the RL agent. This paradigm of adaptive probabilistic shielding raises a number of challenges, such as when to recompute the shield and how to balance between exploration and safety during learning. We empirically evaluate multiple variants of this paradigm across several environments.
published version · arxiv · code

Uppaal Coshy: Automatic Synthesis of Compact Shields for Hybrid Systems

Asger Horn Brorholt, Andreas Holck Høeg-Petersen, Peter Gjøl Jensen, Kim Guldstrand Larsen, Marius Mikučionis, Christian Schilling, and Andrzej Wąsowski

Reachability Problems, RP 2025

Abstract We present Uppaal Coshy, a tool for automatic synthesis of a safety strategy—or shield —for Markov decision processes over continu- ous state spaces and complex hybrid dynamics. The general methodology is to partition the state space and then solve a two-player safety game, which entails a number of algorithmically hard problems such as reach- ability for hybrid systems. The general philosophy of Uppaal Coshy is to approximate hard-to-obtain solutions using simulations. Our imple- mentation is fully automatic and supports the expressive formalism of Uppaal models, which encompass stochastic hybrid automata. The precision of our partition-based approach benefits from using finer grids, which however are not efficient to store. We include an algorithm called Caap to efficiently compute a compact representation of a shield in the form of a decision tree, which yields significant reductions.
published version · arxiv · download the tool · documentation

Compositional Shielding and Reinforcement Learning
for Multi-Agent Systems

Asger Horn Brorholt, Kim Guldstrand Larsen, and Christian Schilling

Autonomous Agents and Multiagent Systems, AAMAS 2025

Abstract Deep reinforcement learning has emerged as a powerful tool for obtaining high-performance policies. However, the safety of these policies has been a long-standing issue. One promising paradigm to guarantee safety is a shield, which shields a policy from making unsafe actions. However, computing a shield scales exponentially in the number of state variables. This is a particular concern in multi-agent systems with many agents. In this work, we propose a novel approach for multi-agent shielding. We address scalability by computing individual shields for each agent. The challenge is that typical safety specifications are global properties, but the shields of individual agents only ensure local properties. Our key to overcome this challenge is to apply assume-guarantee reasoning. Specifically, we present a sound proof rule that decomposes a (global, complex) safety specification into (local, simple) obligations for the shields of the individual agents. Moreover, we show that applying the shields during reinforcement learning significantly improves the quality of the policies obtained for a given training budget. We demonstrate the effectiveness and scalability of our multi-agent shielding framework in two case studies, reducing the computation time from hours to seconds and achieving fast learning convergence.
published version · arxiv · short video · code

Efficient Shield Synthesis via State-Space Transformation

Asger Horn Brorholt, Andreas Holck Høeg-Petersen, Kim Guldstrand Larsen, and Christian Schilling

Bridging the Gap Between AI and Reality, AISoLA 2024

Abstract

We consider the problem of synthesizing safety strategies for control systems, also known as shields. Since the state space is infinite, shields are typically computed over a finite-state abstraction, with the most common abstraction being a rectangular grid. However, for many systems, such a grid does not align well with the safety property or the system dynamics. That is why a coarse grid is rarely sufficient, but a fine grid is typically computationally infeasible to obtain. In this paper, we show that appropriate state-space transformations can still allow to use a coarse grid at almost no computational overhead. We demonstrate in three case studies that our transformation-based synthesis outperforms a standard synthesis by several orders of magnitude. In the first two case studies, we use domain knowledge to select a suitable transformation. In the third case study, we instead report on results in engineering a transformation without domain knowledge.

published version · arxiv · code

Shielded Reinforcement Learning for Hybrid Systems

Asger Horn Brorholt, Peter Gjøl Jensen, Kim Guldstrand Larsen, Florian Lorber, Christian Schilling

Bridging the Gap Between AI and Reality, AISoLA 2023

Abstract

Safe and optimal controller synthesis for switched-controlled hybrid systems, which combine differential equations and discrete changes of the system’s state, is known to be intricately hard. Reinforcement learning has been leveraged to construct near-optimal controllers, but their behavior is not guaranteed to be safe, even when it is encouraged by reward engineering. One way of imposing safety to a learned controller is to use a shield, which is correct by design. However, obtaining a shield for non-linear and hybrid environments is itself intractable. In this paper, we propose the construction of a shield using the so-called barbaric method, where an approximate finite representation of an underlying partition-based two-player safety game is extracted via systematically picked samples of the true transition function. While hard safety guarantees are out of reach, we experimentally demonstrate strong statistical safety guarantees with a prototype implementation and Uppaal Stratego. Furthermore, we study the impact of the synthesized shield when applied as either a pre-shield (applied before learning a controller) or a post-shield (only applied after learning a controller). We experimentally demonstrate superiority of the pre-shielding approach. We apply our technique on a range of case studies, including two industrial examples, and further study post-optimization of the post-shielding approach.

published version · arxiv · code · julia package