Spacecraft Control

Spacecraft proximity operations involve maneuvers in which two or more spacecraft operate in close proximity, as encountered in applications such as on-orbit servicing, active debris removal, automated docking, and on-orbit assembly. We develop automated control algorithms for these scenarios, with a particular emphasis on safe reinforcement learning through shielding techniques. Furthermore, as the number of deployed spacecraft continues to grow rapidly, future systems will require a significantly higher degree of autonomy, as human operators will no longer be able to directly control all assets. To address this challenge, we develop tools that ensure the safety of autonomous decision-making, for example by correcting unsafe actions or by restricting the system to choose only from a predefined set of safe alternatives.

Formal Verification via Reachability Analysis

Because it is real-time capable, can rigorously guarantee robustness in the presence of disturbances, measurement errors, and model uncertainties, and naturally accommodates dynamically changing environments, reachability analysis is widely regarded as one of the most promising techniques for the formal verification of dynamical systems such as robots, spacecrafts and autonomous vehicles. However, the quality of the computed reachable sets often depends critically on careful hyper-parameter tuning, which typically requires expert knowledge for the verification process to succeed. In addition to developing new reachability algorithms for linear (HSCC 2023), nonlinear (CDC 2020), neural-network-controlled (NASA 2023), and hybrid systems (HSCC 2020), one of our primary research goals is therefore to design fully automated verification algorithms that eliminate the need for hyper-parameter tuning altogether and can be reliably applied by non-experts (TAC 2023, HSCC 2023, NAHS 2024).

Safe-By-Construction Controller Synthesis

A common approach to control with formal safety guarantees is to first synthesize a controller for a nominal model and subsequently use reachability analysis to verify its robustness against disturbances and model uncertainties. However, this sequential procedure often fails to verify the system, as the uncertainties are not explicitly considered during the controller design phase. To address this limitation, our research focuses on the development of safe-by-construction controllers. These methods integrate reachability analysis directly into the design process, resulting in controllers that are guaranteed to ensure robust safety in the presence of disturbances, model uncertainties, measurement errors, and input constraints (CDC 2018, TAC 2021, HSCC 2021, Automatica 2022).

Safe Reinforcement Learning and Neural Network Verification

While artificial intelligence has achieved remarkable success across a wide range of applications, a key challenge remains the lack of rigorous safety guarantees. This concern is further amplified by the limited interpretability of neural networks, which often makes it difficult to understand what exactly has been learned. To address these issues, we develop methods for open-loop verification, where the neural network is analyzed in isolation (NASA 2023), as well as closed-loop verification, where the network acts as a controller for a dynamical system (NASA 2023). In addition, we work on safe reinforcement learning approaches that incorporate a safety shield to prevent the agent from executing unsafe actions (Open Journal of Control Systems 2023). Together, these approaches enable the provision of formal safety guarantees for systems that include AI components, thereby supporting the reliable deployment of AI in safety-critical applications.

Conformant System Identification

Modeling the dynamic behavior of a system manually is often time-consuming and labor-intensive, which has led to a strong interest in bypassing this step by directly learning system dynamics from measurement data. This process is known as system identification. Our research primarily focuses on learning hybrid automata from noisy data (HSCC 2025) and on system identification via Koopman operator linearization (ATVA 2023). The key idea for the Koopman approach is to lift the system into a higher-dimensional state space in which the dynamics can be well approximated by a linear model. Since many tasks, such as verification and control, are significantly more efficient for linear systems than for nonlinear ones, Koopman-based models often provide substantial advantages across a wide range of applications (CAV 2022, HSCC 2024). Moreover, for formal verification, the approximate models obtained through system identification are insufficient. What is required are over-approximative models that encompass all possible behaviors of the real system. Such models can be constructed via conformant synthesis, for which we have developed specialized algorithms tailored to Koopman-linearized (CDC 2022) and hybrid systems (ASP-DAC 2020).

Set-Based Computing

The efficiency of algorithms that operate on sets, such as reachability analysis and abstract interpretation, largely depends on the underlying set representation. Consequently, a central focus of our research is the development of novel set representations that enable highly efficient computation of fundamental operations, including unions, intersection checks, and Minkowski sums. In previous work, we introduced two non-convex set representations, sparse polynomial zonotopes (TAC 2020) and constrained polynomial zonotopes (Acta Informatica 2023), which are closed under all major set operations. Moreover, since many operations on sets can lead to a significant increase in representation size, our current research also focuses on designing efficient methods for reducing this growth and maintaining computational tractability (Control Systems Letters 2025).