48 citations · 172 across the 22 of their papers we have counts for
15 papers · 1 filter
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…
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…
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…
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…
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…
Experimental Aspects of Synthesis
Rüdiger Ehlers
We discuss the problem of experimentally evaluating linear-time temporal logic (LTL) synthesis tools for reactive systems. We first survey previous such work for the currently publ…
Generalised Rabin(1) synthesis
Ruediger Ehlers
We present a novel method for the synthesis of finite state systems that is a generalisation of the generalised reactivity(1) synthesis approach by Piterman, Pnueli and Sa'ar. In p…