en:users:kochdumper:index

A short overview over my education and research positions:

Postdoctoral Researcher, Research group of Prof. Eugene Asarin, IRIF/Université Paris Cité, France, 2024 - now

Postdoctoral Researcher, Research group of Prof. Stanley Bak, Stony Brook University, USA, 2021 - 2023

PhD in Computer Science, Research group of Prof. Matthias Althoff, Technical University of Munich, Germany, 2018 - 2021

Master Robotics, Cognition, Intelligence, Technical University of Munich, Germany, 2015 - 2017

Bachelor Mechanical Engineering, Technical University of Munich, Germany, 2012 - 2015

My research is centered around the following main topics:

Reachability Analysis: Since it is real-time capable, able to prove robust safety despite disturbances, measurement errors, as well as model uncertainties, and well-suited for handling dynamically changing environments, reachability analysis is considered to be one of the most promising techniques for the formal verification of dynamic systems, such as robots or autonomous vehicles. However, since the tightness of the computed reachable set often heavily depends on the correct tuning of algorithm parameters, one often requires an expert in reachability for the verification process to succeed. In addition to inventing new reachability algorithms for linear (HSCC 2023), nonlinear (CDC 2020), and hybrid systems (HSCC 2020), one of my main goals is therefore to develop fully automated verifiers that do not require any parameter tuning and can therefore also be applied by non-experts (TAC 2023, HSCC 2023, NAHS 2024).

Set-Based Computing: The efficiency of algorithms that compute with sets, such as reachability algorithms or algorithms for abstract interpretation, mainly depends on the efficiency of the set representation that is used. Therefore, a major focus of my research is to invent new set representations for which set operations such as intersection, union, and Minkowski sum can be computed very efficiently. Previously, I already introduced the two novel non-convex set representations sparse polynomial zonotopes (TAC 2020) and constrained polynomial zonotopes (Acta Informatica 2023), which are closed under all major set operations. However, since for these two set representations many operations significantly increase the representation size, the focus of our current research is to develop efficient algorithms for representation size reduction.

Safe-By-Construction Controllers: The common procedure to construct safe controllers is often to first design a controller for the nominal model, and afterward use reachability analysis to verify that the controller is robustly safe despite disturbances and model uncertainty. However, this procedure is actually quite likely to fail, since the disturbances and model uncertainties have not yet been taken into account during controller design. Therefore, I am researching the development of safe-by-construction controllers, which already take reachability analysis into account during controller synthesis and therefore yield a controller that is guaranteed to be robustly safe despite disturbances, model uncertainties, measurement errors, and input constraints (CDC 2018, TAC 2021, HSCC 2021, Automatica 2022).

Neural Network Verification: While artificial intelligence yields very impressive results for many applications, a major concern is the lack of safety guarantees. These concerns become even more severe due to the fact that it is often completely unclear to the human what exactly the neural network has learned. To address these issues, I developed approaches for open-loop verification where the neural network is considered standalone (NASA 2023), closed-loop verification where the neural network represents a controller for a dynamic system (NASA 2023), and safe reinforcement learning, where we apply a safety shield that prevents the reinforcement learning agent from applying unsafe actions to the system (Open Journal of Control Systems 2023). With these approaches one can obtain safety guarantees for systems with AI components, which facilitates the application of AI in safety-critical applications.

System Identification: Since modeling the dynamic behavior of a system by hand is often very time-consuming and cumbersome, there is a huge desire to avoid this modeling step and directly identify the dynamics from measurements of the real system. The process of directly learning a dynamic model from measurements is called system identification. I am mainly researching system identification via Koopman operator linearization (ATVA 2023), where the main idea is to transform the system to a higher-dimensional state space where the dynamics can be approximated well by a linear model. Since many tasks such as verification and control are much easier and faster for linear dynamic models compared to nonlinear ones, using Koopman models often results in significant advantages for many applications (CAV 2022, HSCC 2024).

Conformant Synthesis: No matter how accurately one models the dynamics of a system, the real system will always behave slightly different than the corresponding model. For formal verification this is a huge problem, because we actually want to verify the real system, and not just the model we have. The solution to this issue is to add uncertainty to the nominal model of the system to obtain an over-approximative/conformant model that explains all measurements of the real system. One research direction I am pursuing is therefore to develop algorithms for conformant synthesis, which automatically determine the amount of uncertainty one has to add to make the model conformant from measurements of the real system. So far, I developed conformant synthesis approaches for Koopman operator linearized systems (CDC 2022) and hybrid systems with linear continuous dynamics (ASP-DAC 2020).

Autonomous Driving: Due to the potentially fatal consequences of failures, safety is the most important aspect for autonomous vehicles, and the lack of safety guarantees is probably one of the main reasons why autonomous cars have not yet been released on a large scale. To improve safety, I am researching both, formally verifying existing motion planners for autonomous vehicles (ARCH 2021) as well as developing new motion planners that are safe-by-construction despite disturbances, model uncertainties, measurement errors, and the unknown behavior of other traffic participants. For the latter, I recently introduced a new reachability-based decision module (ICRA 2024), which results in significant speed-ups for motion planning with motion primitives, and therefore enables planning in real-time.