Intelligent cyber-physical systems must operate in dynamic environments under uncertainty in real time while adhering to multi-level safety and performance requirements. Machine learning (ML) excels at solving complex tasks, but purely ML-based controllers typically lack interpretability, fail to provide behavioral guarantees, and require large, high-quality training datasets and extensive high-fidelity simulation. In contrast, model-based control methods provide guarantees and explainability, but existing approaches suffer from the curse of dimensionality and rely heavily on domain expertise, resulting in low transferability.
My research unlocks the potential of ML-based techniques by leveraging scalable formal methods to achieve data-efficient, reliable, and interpretable physical intelligence. To this end, I design specification guards that enable cyber-physical systems to learn, reason, and act in challenging domains while adhering to complex behavioral requirements. The foundational insight is that reconciling the tension between model-based approaches and machine learning creates a synergy that simultaneously improves learning efficiency and enforces rigorous guarantees, both of which are indispensable for real-world systems. I currently focus on scalable neuro-symbolic physical intelligence that pushes the boundaries in terms of system dimensionality, the complexity of behavioral guarantees, and cross-domain transferability. I demonstrate these neuro-symbolic algorithms across diverse domains, including autonomous driving, maritime and aerial navigation, robotic manipulation, and biomolecular systems.
Selected Publications
Any-Body Guard: Universal Safeguarding for Manipulation Policies via Action Masking
Alex Beaudin*, Hanna Krasowski*, Kartik Nagpal*, Sanjit A. Seshia, Murat Arcak, and Negar Mehr
Ensuring safety of learning-enabled robotic manipulation across diverse embodiments and tasks still requires significant manual engineering. Existing approaches typically rely on heuristically designed fallback controllers or complex forward invariance assessments. These methods are often too conservative for task success, too computationally expensive for real-time execution, too heuristic to provide useful safety guarantees, or too engineering-heavy to transfer between setups. In this paper, we propose a universal safeguarding approach, X-Safe, which reasons directly in the robot’s configuration space to provide formal probabilistic guarantees for collision avoidance. By operating in the configuration space, our method transfers across embodiments while relying solely on an object-based, quasi-static scene representation and a forward kinematics model of the robotic manipulator. Thus, X-Safe provides useful formal safety guarantees without requiring additional data, or engineering effort for different embodiments or scenes. We demonstrate X-Safe for diverse embodiments and policies, both in simulation and on hardware. We observe less degradation in task performance compared to state-of-the-art safeguarding, no collisions on hardware experiments, and empirically corroborate our formal guarantees.
pacSTL: PAC-Bounded Signal Temporal Logic from Data-Driven Reachability Analysis
Hanna Krasowski*, Elizabeth Dietrich*, Emir Cem Gezer, Roger Skjetne, Asgeir Johan Sørensen, and Murat Arcak
Signal Temporal Logic (STL) is an expressive language for specifying behaviors of dynamical systems from continuous signals. However, a limitation of standard STL is its inherently deterministic semantics, which prevents it from accommodating uncertainty. Existing approaches to overcome this limitation are computationally costly and limit real-time capability, requiring repeated trajectory sampling or the redesign of probability distributions over atomic propositions whenever the atomic propositions or specifications change. We introduce pacSTL, a framework that combines Probably Approximately Correct (PAC)-bounded reachable set predictions with an interval extension of STL. pacSTL computes lower and upper bounds on atomic robustness values by solving optimization problems over PAC-bounded reachable sets and propagates the bounds through the temporal logic operators. The resulting evaluation yields a PAC-bounded robustness interval at the specification level. We demonstrate the efficiency and relevance of pacSTL by verifying a quadrotor flight scenario and runtime monitoring a maritime navigation specification.
Provable Traffic Rule Compliance in Safe Reinforcement Learning on the Open Sea
For safe operation, autonomous vehicles have to obey traffic rules that are set forth in legal documents formulated in natural language. Temporal logic is a suitable concept to formalize such traffic rules. Still, temporal logic rules often result in constraints that are hard to solve using optimization-based motion planners. Reinforcement learning (RL) is a promising method to find motion plans for autonomous vehicles. However, vanilla RL algorithms are based on random exploration and do not automatically comply with traffic rules. Our approach accomplishes guaranteed rule-compliance by integrating temporal logic specifications into RL. Specifically, we consider the application of vessels on the open sea, which must adhere to the Convention on the International Regulations for Preventing Collisions at Sea (COLREGS). To efficiently synthesize rule-compliant actions, we combine predicates based on set-based prediction with a statechart representing our formalized rules and their priorities. Action masking then restricts the RL agent to this set of verified rule-compliant actions. In numerical evaluations on critical maritime traffic situations, our agent always complies with the formalized legal rules and never collides while achieving a high goal-reaching rate during training and deployment. In contrast, vanilla and traffic rule-informed RL agents frequently violate traffic rules and collide even after training.
@article{Krasowski2024.safeRLautonomousVessels,title={Provable Traffic Rule Compliance in Safe Reinforcement Learning on the Open Sea},author={Krasowski*, Hanna and Althoff, Matthias},year={2024},journal={IEEE Transactions on Intelligent Vehicles},volume={9},number={12},pages={7617--7634},doi={10.1109/TIV.2024.3400597},issn={2379-8904},}
Excluding the Irrelevant: Focusing Reinforcement Learning through Continuous Action Masking
Roland Stolz*, Hanna Krasowski*, Jakob Thumm, Michael Eichelbeck, Philipp Gassert, and Matthias Althoff
In Proc. of the Thirty-eighth Annual Conference on Neural Information Processing Systems (NeurIPS), 2024
Continuous action spaces in reinforcement learning (RL) are commonly defined as interval sets. While intervals usually reflect the action boundaries for tasks well, they can be challenging for learning because the typically large global action space leads to frequent exploration of irrelevant actions. Yet, little task knowledge can be sufficient to identify significantly smaller state-specific sets of relevant actions. Focusing learning on these relevant actions can significantly improve training efficiency and effectiveness. In this paper, we propose to focus learning on the set of relevant actions and introduce three continuous action masking methods for exactly mapping the action space to the state-dependent set of relevant actions. Thus, our methods ensure that only relevant actions are executed, enhancing the predictability of the RL agent and enabling its use in safety-critical applications. We further derive the implications of the proposed methods on the policy gradient. Using Proximal Policy Optimization (PPO), we evaluate our methods on three control tasks, where the relevant action set is computed based on the system dynamics and a relevant state set. Our experiments show that the three action masking methods achieve higher final rewards and converge faster than the baseline without action masking.
@inproceedings{Stolz2024,title={Excluding the Irrelevant: Focusing Reinforcement Learning through Continuous Action Masking},author={Stolz*, Roland and Krasowski*, Hanna and Thumm, Jakob and Eichelbeck, Michael and Gassert, Philipp and Althoff, Matthias},year={2024},booktitle={Proc. of the Thirty-eighth Annual Conference on Neural Information Processing Systems (NeurIPS)},}
Provably Safe Reinforcement Learning via Action Projection Using Reachability Analysis and Polynomial Zonotopes
Niklas Kochdumper*, Hanna Krasowski*, Xiao Wang*, Stanley Bak, and Matthias Althoff
While reinforcement learning produces very promising results for many applications, its main disadvantage is the lack of safety guarantees, which prevents its use in safety-critical systems. In this work, we address this issue by a safety shield for nonlinear continuous systems that solve reach-avoid tasks. Our safety shield prevents applying potentially unsafe actions from a reinforcement learning agent by projecting the proposed action to the closest safe action. This approach is called action projection and is implemented via mixed-integer optimization. The safety constraints for action projection are obtained by applying parameterized reachability analysis using polynomial zonotopes, which enables to accurately capture the nonlinear effects of the actions on the system. In contrast to other state-of-the-art approaches for action projection, our safety shield can efficiently handle input constraints and dynamic obstacles, eases incorporation of the spatial robot dimensions into the safety constraints, guarantees robust safety despite process noise and measurement errors, and is well suited for high-dimensional systems, as we demonstrate on several challenging benchmark systems.
@article{Kochdumper2023.safeRLReachabilityAnalysis,author={Kochdumper*, Niklas and Krasowski*, Hanna and Wang*, Xiao and Bak, Stanley and Althoff, Matthias},journal={IEEE Open Journal of Control Systems},title={Provably Safe Reinforcement Learning via Action Projection Using Reachability Analysis and Polynomial Zonotopes},year={2023},volume={2},pages={79-92},doi={10.1109/OJCSYS.2023.3256305},}
