Publications (65)
Expediting Reinforcement Learning by Incorporating Knowledge About Temporal Causality in the Environment
Jan Corazza, Hadi Partovi Aria, Daniel Neider +1
Reinforcement learning (RL) algorithms struggle with learning optimal policies for tasks where reward feedback is sparse and depends on a complex sequence of events in the environm…
An Automaton Learning Approach to Solving Safety Games over Infinite Graphs
Daniel Neider, Ufuk Topcu
We propose a method to construct finite-state reactive controllers for systems whose interactions with their adversarial environment are modeled by infinite-duration two-player gam…
Learning Interpretable Models in the Property Specification Language
Rajarshi Roy, Dana Fisman, Daniel Neider
We address the problem of learning human-interpretable descriptions of a complex system from a finite set of positive and negative examples of its behavior. In contrast to most of…
Formal verification for robo-advisors: Irrelevant for subjective end-user trust, yet decisive for investment behavior?
Alina Tausch, Magdalena Wischnewski, Mustafa Yalciner +1
This online-vignette study investigates the impact of certification and verification as measures for quality assurance of AI on trust and use of a robo-advisor. Confronting 520 par…
From LTL to rLTL Monitoring: Improved Monitorability through Robust Semantics
Corto Mascle, Daniel Neider, Maximilian Schwenger +3
Runtime monitoring is commonly used to detect the violation of desired properties in safety critical cyber-physical systems by observing its executions. Bauer et al. introduced an…
Scalable Anytime Algorithms for Learning Fragments of Linear Temporal Logic
Ritam Raha, Rajarshi Roy, Nathanaël Fijalkow +1
Linear temporal logic (LTL) is a specification language for finite sequences (called traces) widely used in program verification, motion planning in robotics, process mining, and m…
Probably Approximately Correct Explanations of Machine Learning Models via Syntax-Guided Synthesis
Daniel Neider, Bishwamittra Ghosh
We propose a novel approach to understanding the decision making of complex machine learning models (e.g., deep neural networks) using a combination of probably approximately corre…
Learning Universally Quantified Invariants of Linear Data Structures
Pranav Garg, Christof Loding, P. Madhusudan +1
We propose a new automaton model, called quantified data automata over words, that can model quantified invariants over linear data structures, and build poly-time active learning…
Resilient Abstraction-Based Controller Design
Stanly Samuel, Kaushik Mallik, Anne-Kathrin Schmuck +1
We consider the computation of resilient controllers for perturbed non-linear dynamical systems w.r.t. linear-time temporal logic specifications. We address this problem through th…
Robust Linear Temporal Logic
Paulo Tabuada, Daniel Neider
Although it is widely accepted that every system should be robust, in the sense that "small" violations of environment assumptions should lead to "small" violations of system guara…
Detecting Diffusion-Generated Time Series Under Generator Shift
Zhi Wen Soi, Aditya Shankar, Gert Lek +4
The boundary between real and diffusion-generated time series is becoming increasingly difficult to draw, yet detection in this domain remains underexplored, especially when the ge…
Learning DFAs from Positive Examples Only via Word Counting
Benjamin Bordais, Daniel Neider
Learning finite automata from positive examples has recently gained attention as a powerful approach for understanding, explaining, analyzing, and verifying black-box systems. The…
What is Formal Verification without Specifications? A Survey on mining LTL Specifications
Daniel Neider, Rajarshi Roy
Virtually all verification techniques using formal methods rely on the availability of a formal specification, which describes the design requirements precisely. However, formulati…
Robust, Expressive, and Quantitative Linear Temporal Logics: Pick any Two for Free (full version)
Daniel Neider, Alexander Weinert, Martin Zimmermann
Linear Temporal Logic (LTL) is the standard specification language for reactive systems and is successfully applied in industrial settings. However, many shortcomings of LTL have b…
Using Large Language Models to Automate and Expedite Reinforcement Learning with Reward Machine
Shayan Meshkat Alsadat, Jean-Raphael Gaglione, Daniel Neider +2
We present LARL-RM (Large language model-generated Automaton for Reinforcement Learning with Reward Machine) algorithm in order to encode high-level knowledge into reinforcement le…
Focused Chain-of-Thought: Efficient LLM Reasoning via Structured Input Information
Lukas Struppek, Dominik Hintersdorf, Hannah Struppek +2
Recent large language models achieve strong reasoning performance by generating detailed chain-of-thought traces, but this often leads to excessive token use and high inference lat…
Synthesizing Optimally Resilient Controllers
Daniel Neider, Alexander Weinert, Martin Zimmermann
Recently, Dallal, Neider, and Tabuada studied a generalization of the classical game-theoretic model used in program synthesis, which additionally accounts for unmodeled intermitte…
Decentralizing Multi-Agent Reinforcement Learning with Temporal Causal Information
Jan Corazza, Hadi Partovi Aria, Hyohun Kim +2
Reinforcement learning (RL) algorithms can find an optimal policy for a single agent to accomplish a particular task. However, many real-world problems require multiple agents to c…
Being correct is not enough: efficient verification using robust linear temporal logic
Tzanis Anevlavis, Matthew Philippe, Daniel Neider +1
While most approaches in formal methods address system correctness, ensuring robustness has remained a challenge. In this paper we present and study the logic rLTL which provides a…
Optimally Resilient Strategies in Pushdown Safety Games
Daniel Neider, Patrick Totzke, Martin Zimmermann
Infinite-duration games with disturbances extend the classical framework of infinite-duration games, which captures the reactive synthesis problem, with a discrete measure of resil…
On Uniformly Scaling Flows: A Density-Aligned Approach to Deep One-Class Classification
Faried Abu Zaid, Tim Katzke, Emmanuel Müller +1
Unsupervised anomaly detection is often framed around two widely studied paradigms. Deep one-class classification, exemplified by Deep SVDD, learns compact latent representations o…
Robustness-by-Construction Synthesis: Adapting to the Environment at Runtime
Satya Prakash Nayak, Daniel Neider, Martin Zimmermann
While most of the current synthesis algorithms only focus on correctness-by-construction, ensuring robustness has remained a challenge. Hence, in this paper, we address the robust-…
Learning Interpretable Temporal Properties from Positive Examples Only
Rajarshi Roy, Jean-Raphaël Gaglione, Nasim Baharisangari +3
We consider the problem of explaining the temporal behavior of black-box systems using human-interpretable models. To this end, based on recent research trends, we rely on the fund…
A framework for computing upper bounds in passive learning settings
Benjamin Bordais, Daniel Neider
The task of inferring logical formulas from examples has garnered significant attention as a means to assist engineers in creating formal specifications used in the design, synthes…
Learning Linear Temporal Properties from Noisy Data: A MaxSAT Approach
Jean-Raphaël Gaglione, Daniel Neider, Rajarshi Roy +2
We address the problem of inferring descriptions of system behavior using Linear Temporal Logic (LTL) from a finite set of positive and negative examples. Most of the existing appr…
Parameterized Synthesis with Safety Properties
Oliver Markgraf, Chih-Duo Hong, Anthony W. Lin +2
Parameterized synthesis offers a solution to the problem of constructing correct and verified controllers for parameterized systems. Such systems occur naturally in practice (e.g.,…
Deep Anomaly Detection on Tennessee Eastman Process Data
Fabian Hartung, Billy Joe Franks, Tobias Michels +15
This paper provides the first comprehensive evaluation and analysis of modern (deep-learning) unsupervised anomaly detection methods for chemical process data. We focus on the Tenn…
Reinforcement Learning with Temporal-Logic-Based Causal Diagrams
Yash Paliwal, Rajarshi Roy, Jean-Raphaël Gaglione +5
We study a class of reinforcement learning (RL) tasks where the objective of the agent is to accomplish temporally extended goals. In this setting, a common approach is to represen…
Learning-Based Synthesis of Safety Controllers
Daniel Neider, Oliver Markgraf
We propose a machine learning framework to synthesize reactive controllers for systems whose interactions with their adversarial environment are modeled by infinite-duration, two-p…
Learning Linear Temporal Properties
Daniel Neider, Ivan Gavran
We present two novel algorithms for learning formulas in Linear Temporal Logic (LTL) from examples. The first learning algorithm reduces the learning task to a series of satisfiabi…
Learning Tree Pattern Transformations
Daniel Neider, Leif Sabellek, Johannes Schmidt +2
Explaining why and how a tree structurally differs from another tree is a question that is encountered throughout computer science, including in understanding tree-st…
Making Embodied AI Reliable: A Community Agenda from Testing to Formal Verification
Xi Zheng, Dulanga Weerakoon, Yintong Huo +8
Embodied AI systems are increasingly deployed in open-world environments, yet ensuring their reliability remains a fundamental challenge. Drawing on discussions from the AAAI'26 Br…
Active Finite Reward Automaton Inference and Reinforcement Learning Using Queries and Counterexamples
Zhe Xu, Bo Wu, Aditya Ojha +2
Despite the fact that deep reinforcement learning (RL) has surpassed human-level performances in various tasks, it still has several fundamental challenges. First, most RL methods…
Learning to Break Deep Perceptual Hashing: The Use Case NeuralHash
Lukas Struppek, Dominik Hintersdorf, Daniel Neider +1
Apple recently revealed its deep perceptual hashing system NeuralHash to detect child sexual abuse material (CSAM) on user devices before files are uploaded to its iCloud service.…
A Formal Language Approach to Explaining RNNs
Bishwamittra Ghosh, Daniel Neider
This paper presents LEXR, a framework for explaining the decision making of recurrent neural networks (RNNs) using a formal description language called Linear Temporal Logic (LTL).…
Formally Exploring Time-Series Anomaly Detection Evaluation Metrics
Dennis Wagner, Arjun Nair, Billy Joe Franks +24
Undetected anomalies in time series can trigger catastrophic failures in safety-critical systems, such as chemical plant explosions or power grid outages. Although many detection m…
Accessible Smart Contracts Verification: Synthesizing Formal Models with Tamed LLMs
Jan Corazza, Ivan Gavran, Gabriela Moreira +1
When blockchain systems are said to be trustless, what this really means is that all the trust is put into software. Thus, there are strong incentives to ensure blockchain software…
Defending Our Privacy With Backdoors
Dominik Hintersdorf, Lukas Struppek, Daniel Neider +1
The proliferation of large AI models trained on uncurated, often sensitive web-scraped data has raised significant privacy concerns. One of the concerns is that adversaries can ext…
Neuro-Symbolic Verification of Deep Neural Networks
Xuan Xie, Kristian Kersting, Daniel Neider
Formal verification has emerged as a powerful approach to ensure the safety and reliability of deep neural networks. However, current verification tools are limited to only a handf…
Down the Borel Hierarchy: Solving Muller Games via Safety Games
Daniel Neider, Roman Rabinovich, Martin Zimmermann
We transform a Muller game with n vertices into a safety game with (n!)^3 vertices whose solution allows to determine the winning regions of the Muller game and to compute a finite…
Reinforcement Learning with Stochastic Reward Machines
Jan Corazza, Ivan Gavran, Daniel Neider
Reward machines are an established tool for dealing with reinforcement learning problems in which rewards are sparse and depend on complex sequences of actions. However, existing a…
Horn-ICE Learning for Synthesizing Invariants and Contracts
Deepak D'Souza, P. Ezudheen, Pranav Garg +2
We design learning algorithms for synthesizing invariants using Horn implication counterexamples (Horn-ICE), extending the ICE-learning model. In particular, we describe a decision…
Analyzing Robustness of Angluin's L Algorithm in Presence of Noise
Lina Ye, Igor Khmelnitsky, Serge Haddad +5
Angluin's L algorithm learns the minimal deterministic finite automaton (DFA) of a regular language using membership and equivalence queries. Its probabilistic approximatively…
Unsupervised Automata Learning via Discrete Optimization
Simon Lutz, Daniil Kaminskyi, Florian Wittbold +5
Automata learning is a successful tool for many application domains such as robotics and automatic verification. Typically, automata learning techniques operate in a supervised lea…
Evaluating Counterfactual Explanation Methods on Incomplete Inputs
Francesco Leofante, Daniel Neider, Mustafa Yalçıner
Existing algorithms for generating Counterfactual Explanations (CXs) for Machine Learning (ML) typically assume fully specified inputs. However, real-world data often contains miss…
The Complexity of Learning Temporal Properties
Benjamin Bordais, Daniel Neider, Rajarshi Roy
We consider the problem of learning temporal logic formulas from examples of system behavior. Learning temporal properties has crystallized as an effective mean to explain complex…
Specification sketching for Linear Temporal Logic
Simon Lutz, Daniel Neider, Rajarshi Roy
Virtually all verification and synthesis techniques assume that the formal specifications are readily available, functionally correct, and fully match the engineer's understanding…
Learning Branching-Time Properties in CTL and ATL via Constraint Solving
Benjamin Bordais, Daniel Neider, Rajarshi Roy
We address the problem of learning temporal properties from the branching-time behavior of systems. Existing research in this field has mostly focused on learning linear temporal p…
Robust Alternating-Time Temporal Logic
Aniello Murano, Daniel Neider, Martin Zimmermann
In multi-agent system design, a crucial aspect is to ensure robustness, meaning that for a coalition of agents A, small violations of adversarial assumptions only lead to small vio…
Robust Computation Tree Logic
Satya Prakash Nayak, Daniel Neider, Rajarshi Roy +1
It is widely accepted that every system should be robust in that ``small'' violations of environment assumptions should lead to ``small'' violations of system guarantees, but it is…
Learning Temporal Properties is NP-hard
Benjamin Bordais, Daniel Neider, Rajarshi Roy
We investigate the complexity of LTL learning, which consists in deciding given a finite set of positive ultimately periodic words, a finite set of negative ultimately periodic wor…
Invariant Synthesis for Incomplete Verification Engines
Daniel Neider, Pranav Garg, P. Madhusudan +2
We propose a framework for synthesizing inductive invariants for incomplete verification engines, which soundly reduce logical problems in undecidable theories to decidable theorie…
Joint Inference of Reward Machines and Policies for Reinforcement Learning
Zhe Xu, Ivan Gavran, Yousef Ahmad +4
Incorporating high-level knowledge is an effective way to expedite reinforcement learning (RL), especially for complex tasks with sparse rewards. We investigate an RL problem where…
Property-Directed Verification of Recurrent Neural Networks
Igor Khmelnitsky, Daniel Neider, Rajarshi Roy +6
This paper presents a property-directed approach to verifying recurrent neural networks (RNNs). To this end, we learn a deterministic finite automaton as a surrogate model from a g…
Synthesizing Efficiently Monitorable Formulas in Metric Temporal Logic
Ritam Raha, Rajarshi Roy, Nathanael Fijalkow +2
In runtime verification, manually formalizing a specification for monitoring system executions is a tedious and error-prone process. To address this issue, we consider the problem…
Uncertainty-Aware Signal Temporal Logic Inference
Nasim Baharisangari, Jean-Raphaël Gaglione, Daniel Neider +2
Temporal logic inference is the process of extracting formal descriptions of system behaviors from data in the form of temporal logic formulas. The existing temporal logic inferenc…
Robust, Expressive, and Quantitative Linear Temporal Logics: Pick any Two for Free
Daniel Neider, Alexander Weinert, Martin Zimmermann
Linear Temporal Logic (LTL) is the standard specification language for reactive systems and is successfully applied in industrial settings. However, many shortcomings of LTL have b…
A Cautionary Tale About "Neutrally" Informative AI Tools Ahead of the 2025 Federal Elections in Germany
Ina Dormuth, Sven Franke, Marlies Hafer +6
In this study, we examine the reliability of AI-based Voting Advice Applications (VAAs) and large language models (LLMs) in providing objective political information. Our analysis…
Analyzing Robustness of Angluin's L* Algorithm in Presence of Noise
Igor Khmelnitsky, Serge Haddad, Lina Ye +5
Angluin's L* algorithm learns the minimal (complete) deterministic finite automaton (DFA) of a regular language using membership and equivalence queries. Its probabilistic approxim…
VeriFlow: Modeling Distributions for Neural Network Verification
Faried Abu Zaid, Daniel Neider, Mustafa Yalçıner
Formal verification has emerged as a promising method to ensure the safety and reliability of neural networks. However, many relevant properties, such as fairness or global robustn…
Inferring Properties in Computation Tree Logic
Rajarshi Roy, Daniel Neider
We consider the problem of automatically inferring specifications in the branching-time logic, Computation Tree Logic (CTL), from a given system. Designing functional and usable sp…
Learning Temporal Logic Properties: an Overview of Two Recent Methods
Jean-Raphaël Gaglione, Rajarshi Roy, Nasim Baharisangari +3
Learning linear temporal logic (LTL) formulas from examples labeled as positive or negative has found applications in inferring descriptions of system behavior. We summarize two me…
Fine-Tuning Multilingual Language Models for Code Review: An Empirical Study on Industrial C# Projects
Igli Begolli, Meltem Aksoy, Daniel Neider
Code review is essential for maintaining software quality but often time-consuming and cognitively demanding, especially in industrial environments. Recent advancements in language…
Abstract Learning Frameworks for Synthesis
Christof Löding, P. Madhusudan, Daniel Neider
We develop abstract learning frameworks (ALFs) for synthesis that embody the principles of CEGIS (counter-example based inductive synthesis) strategies that have become widely appl…
Reinforcement Learning with Symbolic Reward Machines
Thomas Krug, Daniel Neider
Reward Machines (RMs) are an established mechanism in Reinforcement Learning (RL) to represent and learn sparse, temporally extended tasks with non-Markovian rewards. RMs rely on h…