48 citations · 172 across the 22 of their papers we have counts for
26 papers
How Concise are Chains of co-Büchi Automata?
Rüdiger Ehlers
Chains of co-Büchi automata (COCOA) have recently been introduced as a new canonical model for representing arbitrary omega-regular languages. They can be minimized in polynomial t…
How Concise are Chains of co-Büchi Automata?
Rüdiger Ehlers
Chains of co-Büchi automata (COCOA) have recently been introduced as a new canonical model for representing arbitrary omega-regular languages. They can be minimized in polynomial t…
Correct-by-Construction Runtime Enforcement in AI -- A Survey
Bettina Könighofer, Roderick Bloem, Rüdiger Ehlers +1
Runtime enforcement refers to the theories, techniques, and tools for enforcing correct behavior with respect to a formal specification of systems at runtime. In this paper, we are…
Adapting to the Behavior of Environments with Bounded Memory
Dhananjay Raju, Rüdiger Ehlers, Ufuk Topcu
We study the problem of synthesizing implementations from temporal logic specifications that need to work correctly in all environments that can be represented as transducers with…
Safe Multi-Agent Reinforcement Learning via Shielding
Ingy Elsayed-Aly, Suda Bharadwaj, Christopher Amato +3
Multi-agent reinforcement learning (MARL) has been increasingly used in a wide range of safety-critical applications, which require guaranteed safety (e.g., no unsafe states are ev…
Playing Against Opponents With Limited Memory
Dhananjay Raju, Rüdiger Ehlers, Ufuk Topcu
We study \emph{partial-information} two-player turn-based games on graphs with omega-regular objectives, when the partial-information player has \emph{limited memory}. Such games a…
Exact Synthesis of ESOP Forms
Heinz Riener, Rüdiger Ehlers, Bruno Schmitt +1
We present an exact synthesis approach for computing Exclusive-or Sum-of-Products (ESOP) forms with a minimum number of product terms using Boolean satisfiability. Our approach fin…
Revisiting Decision Diagrams for SAT
Tom van Dijk, Rüdiger Ehlers, Armin Biere
Symbolic variants of clause distribution using decision diagrams to eliminate variables in SAT were shown to perform well on hard combinatorial instances. In this paper we revisit…
Symmetric Synthesis
Ruediger Ehlers, Bernd Finkbeiner
We study the problem of determining whether a given temporal specification can be implemented by a symmetric system, i.e., a system composed from identical components. Symmetry is…
Safe Reinforcement Learning via Shielding
Mohammed Alshiekh, Roderick Bloem, Ruediger Ehlers +3
Reinforcement learning algorithms discover policies that maximize reward, but do not necessarily guarantee safety during learning or execution phases. We introduce a new approach t…
Formal Verification of Piece-Wise Linear Feed-Forward Neural Networks
Ruediger Ehlers
We present an approach for the verification of feed-forward neural networks in which all nodes have a piece-wise linear activation function. Such networks are often used in deep le…
Risk-Averse -regular Markov Decision Process Control
Ruediger Ehlers, Salar Moarref, Ufuk Topcu
Many control problems in environments that can be modeled as Markov decision processes (MDPs) concern infinite-time horizon specifications. The classical aim in this context is to…
Computing the Complete Pareto Front
Ruediger Ehlers
We give an efficient algorithm to enumerate all elements of a Pareto front in a multi-objective optimization problem in which the space of values is finite for all objectives. Our…
Cooperative Reactive Synthesis
Roderick Bloem, Ruediger Ehlers, Robert Koenighofer
A modern approach to engineering correct-by-construction systems is to synthesize them automatically from formal specifications. Oftentimes, a system can only satisfy its guarantee…
The First Reactive Synthesis Competition (SYNTCOMP 2014)
Swen Jacobs, Roderick Bloem, Romain Brenguier +10
We introduce the reactive synthesis competition (SYNTCOMP), a long-term effort intended to stimulate and guide advances in the design and application of synthesis procedures for re…
Path-Based Program Repair
Heinz Riener, Rüdiger Ehlers, Görschwin Fey
We propose a path-based approach to program repair for imperative programs. Our repair framework takes as input a faulty program, a logic specification that is refuted, and a hint…
Correct-by-synthesis reinforcement learning with temporal logic constraints
Min Wen, Ruediger Ehlers, Ufuk Topcu
We consider a problem on the synthesis of reactive controllers that optimize some a priori unknown performance criterion while interacting with an uncontrolled environment such tha…
Dynamics-Based Reactive Synthesis and Automated Revisions for High-Level Robot Control
Jonathan A. DeCastro, Ruediger Ehlers, Matthias Rungger +3
The aim of this work is to address issues where formal specifications cannot be realized on a given dynamical system subjected to a changing environment. Such failures occur whenev…
Low-Effort Specification Debugging and Analysis
Rüdiger Ehlers, Vasumathi Raman
Reactive synthesis deals with the automated construction of implementations of reactive systems from their specifications. To make the approach feasible in practice, systems engine…
How to Handle Assumptions in Synthesis
Roderick Bloem, Rüdiger Ehlers, Swen Jacobs +1
The increased interest in reactive synthesis over the last decade has led to many improved solutions but also to many new questions. In this paper, we discuss the question of how t…
Proceedings 3rd Workshop on Synthesis
Krishnendu Chatterjee, Rüdiger Ehlers, Susmit Jha
The idea of synthesis, i.e., the process of automatically computing implementations from their specifications, has recently gained a lot of momentum in the contexts of software eng…
Sparse Positional Strategies for Safety Games
Rüdiger Ehlers, Daniela Moldovan
We consider the problem of obtaining sparse positional strategies for safety games. Such games are a commonly used model in many formal methods, as they make the interaction of a s…
Small witnesses, accepting lassos and winning strategies in omega-automata and games
Ruediger Ehlers
Obtaining accepting lassos, witnesses and winning strategies in omega-automata and games with omega-regular winning conditions is an integral part of many formal methods commonly f…
Reactive Safety
Rüdiger Ehlers, Bernd Finkbeiner
The distinction between safety and liveness properties is a fundamental classification with immediate implications on the feasibility and complexity of various monitoring, model ch…