Publications (14)
The Habitable Exoplanet Observatory (HabEx) Mission Concept Study Final Report
B. Scott Gaudi, Sara Seager, Bertrand Mennesson +183
The Habitable Exoplanet Observatory, or HabEx, has been designed to be the Great Observatory of the 2030s. For the first time in human history, technologies have matured sufficient…
Formal Methods for Autonomous Systems
Tichakorn Wongpiromsarn, Mahsa Ghasemi, Murat Cubuktepe +6
Formal methods refer to rigorous, mathematical approaches to system development and have played a key role in establishing the correctness of safety-critical systems. The main buil…
Adaptive planning for risk-aware predictive digital twins
Marco Tezzele, Steven Carr, Ufuk Topcu +1
This work proposes a mathematical framework to increase the robustness to rare events of digital twins modelled with graphical models. We incorporate probabilistic model-checking a…
Affine Multiplexing Networks: System Analysis, Learning, and Computation
Ivan Papusha, Ufuk Topcu, Steven Carr +1
We introduce a novel architecture and computational framework for formal, automated analysis of systems with a broad set of nonlinearities in the feedback loop, such as neural netw…
Compositional shield synthesis for safe reinforcement learning in partial observability
Steven Carr, Georgios Bakirtzis, Ufuk Topcu
Agents controlled by the output of reinforcement learning (RL) algorithms often transition to unsafe states, particularly in uncertain and partially observable environments. Partia…
Human-in-the-Loop Synthesis for Partially Observable Markov Decision Processes
Steven Carr, Nils Jansen, Ralf Wimmer +2
We study planning problems where autonomous agents operate inside environments that are subject to uncertainties and not fully observable. Partially observable Markov decision proc…
Counterexample-Guided Strategy Improvement for POMDPs Using Recurrent Neural Networks
Steven Carr, Nils Jansen, Ralf Wimmer +3
We study strategy synthesis for partially observable Markov decision processes (POMDPs). The particular problem is to determine strategies that provably adhere to (probabilistic) t…
Byzantine-Resilient Distributed Hypothesis Testing With Time-Varying Network Topology
Bo Wu, Steven Carr, Suda Bharadwaj +2
We study the problem of distributed hypothesis testing over a network of mobile agents with limited communication and sensing ranges to infer the true hypothesis collaboratively. I…
Fine-Tuning Language Models Using Formal Methods Feedback
Yunhao Yang, Neel P. Bhatt, Tyler Ingebrand +4
Although pre-trained language models encode generic knowledge beneficial for planning and control, they may fail to generate appropriate control policies for domain-specific tasks.…
Safe Reinforcement Learning via Shielding under Partial Observability
Steven Carr, Nils Jansen, Sebastian Junges +1
Safe exploration is a common problem in reinforcement learning (RL) that aims to prevent agents from making disastrous decisions while exploring their environment. A family of appr…
Verifiable RNN-Based Policies for POMDPs Under Temporal Logic Constraints
Steven Carr, Nils Jansen, Ufuk Topcu
Recurrent neural networks (RNNs) have emerged as an effective representation of control policies in sequential decision-making problems. However, a major drawback in the applicatio…
Dynamic Certification for Autonomous Systems
Georgios Bakirtzis, Steven Carr, David Danks +1
Autonomous systems are often deployed in complex sociotechnical environments, such as public roads, where they must behave safely and securely. Unlike many traditionally engineered…
Quantifying homologous proteins and proteoforms
Dmitry Malioutov, Tianchi Chen, Jacob Jaffe +4
Many proteoforms - arising from alternative splicing, post-translational modifications (PTMs), or paralogous genes - have distinct biological functions, such as histone PTM proteof…
Pessimistic Iterative Planning with RNNs for Robust POMDPs
Maris F. L. Galesloot, Marnix Suilen, Thiago D. Simão +4
Robust POMDPs extend classical POMDPs to incorporate model uncertainty using so-called uncertainty sets on the transition and observation functions, effectively defining ranges of…