BZPEERPapers, people, evidence and research paths
Menu

Discover

SearchFind papers, people, topics, institutions and opportunities from one place.GraphSee how papers, authors, topics and evidence connect.

Research tools

HomeContinue from the papers, people and topics that matter now.CollectionsTurn saved papers into reading lists, evidence maps and shareable context.ResearchReconstruct the path that led you from search to paper to question.CollaborationMove from a paper, topic or expert request into a focused thread.PublishCreate full-text research articles with metadata, formulas and versions.

Network

ExpertsFind specialists whose work and reviews explain why they can help.CommunitiesJoin research groups organized around papers, topics and shared evidence.

Opportunities

ListingsBrowse roles, calls and collaborations connected to real research context.

Account

Log inReturn to your saved papers, graph views and active threads.Create accountStart saving papers, building a research trail and joining teams.
Log inCreate account

Source author record

Rüdiger Ehlers

Rüdiger Ehlers appears in the imported research catalog. Authorship, coauthor and topic links are available while profile ownership is still unclaimed.

ResearcherUnclaimed source record
Logic in Computer ScienceFormal Languages and Automata TheorySoftware EngineeringArtificial IntelligenceMachine LearningProgramming LanguagesRoboticsSystems and Control

Catalog footprint

What is connected

11works
8topics
4close collaborators

Actions

Connect this record

Log in to claim
Open graphBrowse works

Research graph

See the researcher in context

Open full explorer

Inspect adjacent papers, topics, institutions and collaborators without losing the researcher page.

Building this map preview

BZPEER is loading the nearby papers, people, topics and institutions for this page.

Published work

11 published item(s)

preprint2022arXiv

Correct-by-Construction Runtime Enforcement in AI -- A Survey

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 interested in techniques for constructing runtime enforcers for the concrete application domain of enforcing safety in AI. We discuss how safety is traditionally handled in the field of AI and how more formal guarantees on the safety of a self-learning agent can be given by integrating a runtime enforcer. We survey a selection of work on such enforcers, where we distinguish between approaches for discrete and continuous action spaces. The purpose of this paper is to foster a better understanding of advantages and limitations of different enforcement techniques, focusing on the specific challenges that arise due to their application in AI. Finally, we present some open challenges and avenues for future work.

0 citations0 reviewsNo code linkedOpen access
preprint2021arXiv

Safe Multi-Agent Reinforcement Learning via Shielding

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 ever visited) during the learning process.Unfortunately, current MARL methods do not have safety guarantees. Therefore, we present two shielding approaches for safe MARL. In centralized shielding, we synthesize a single shield to monitor all agents' joint actions and correct any unsafe action if necessary. In factored shielding, we synthesize multiple shields based on a factorization of the joint state space observed by all agents; the set of shields monitors agents concurrently and each shield is only responsible for a subset of agents at each step.Experimental results show that both approaches can guarantee the safety of agents during learning without compromising the quality of learned policies; moreover, factored shielding is more scalable in the number of agents than centralized shielding.

0 citations0 reviewsNo code linkedOpen access
preprint2020arXiv

Playing Against Opponents With Limited Memory

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 are a natural formalization for reactive synthesis when the environment player is not genuinely adversarial to the system player. The environment player has goals of its own, but the exact goal of the environment player is unknown to the system player. We prove that the problem of determining the existence of a winning strategy for the system player is PSPACE-hard for reachability, safety, and parity objectives. Moreover, when the environment player is memoryless, the problem is PSPACE-complete. However, it is simpler to decide if the environment player has a winning strategy; it is only NP-complete. Additionally, we construct a game where the the partial-information player needs at least $\mathcal{O}(\sqrt{n})$ bits of memory to retain winning strategies in a game of size $\mathcal{O}(n)$.

0 citations0 reviewsNo code linkedOpen access
preprint2016arXiv

The First Reactive Synthesis Competition (SYNTCOMP 2014)

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 reactive systems. The first iteration of SYNTCOMP is based on the controller synthesis problem for finite-state systems and safety specifications. We provide an overview of this problem and existing approaches to solve it, and report on the design and results of the first SYNTCOMP. This includes the definition of the benchmark format, the collection of benchmarks, the rules of the competition, and the five synthesis tools that participated. We present and analyze the results of the competition and draw conclusions on the state of the art. Finally, we give an outlook on future directions of SYNTCOMP.

0 citations0 reviewsNo code linkedOpen access
preprint2015arXiv

Path-Based Program Repair

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 where the fault may be located. An iterative abstraction refinement loop is then used to repair the program: in each iteration, the faulty program part is re-synthesized considering a symbolic counterexample, where the control-flow is kept concrete but the data-flow is symbolic. The appeal of the idea is two-fold: 1) the approach lazily considers candidate repairs and 2) the repairs are directly derived from the logic specification. In contrast to prior work, our approach is complete for programs with finitely many control-flow paths, i.e., the program is repaired if and only if it can be repaired at the specified fault location. Initial results for small programs indicate that the approach is useful for debugging programs in practice.

0 citations0 reviewsNo code linkedOpen access
preprint2014arXiv

How to Handle Assumptions in Synthesis

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 to deal with assumptions on environment behavior. We present four goals that we think should be met and review several different possibilities that have been proposed. We argue that each of them falls short in at least one aspect.

0 citations0 reviewsNo code linkedOpen access
preprint2014arXiv

Low-Effort Specification Debugging and Analysis

Reactive synthesis deals with the automated construction of implementations of reactive systems from their specifications. To make the approach feasible in practice, systems engineers need effective and efficient means of debugging these specifications. In this paper, we provide techniques for report-based specification debugging, wherein salient properties of a specification are analyzed, and the result presented to the user in the form of a report. This provides a low-effort way to debug specifications, complementing high-effort techniques including the simulation of synthesized implementations. We demonstrate the usefulness of our report-based specification debugging toolkit by providing examples in the context of generalized reactivity(1) synthesis.

0 citations0 reviewsNo code linkedOpen access
preprint2014arXiv

Proceedings 3rd Workshop on Synthesis

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 engineering and reactive system design. While it is widely believed that, due to complexity/undecidability issues, synthesis cannot completely replace manual engineering, it can assist the process of designing the intricate pieces of code that most programmers find challenging, or help with orchestrating tasks in reactive environments. The SYNT workshop aims to bring together researchers interested in synthesis to discuss and present ongoing and mature work on all aspects of automated synthesis and its applications. The third iteration of the workshop took place in Vienna, Austria, and was co-located with the 26th International Conference on Computer Aided Verification, held in the context of the Vienna Summer of Logic in July 2014. The workshop included eight contributed talks and four invited talks. In addition, it featured a special session about the Syntax-Guided Synthesis Competition (SyGuS) and the SyntComp Synthesis competition.

0 citations0 reviewsNo code linkedOpen access
preprint2012arXiv

Sparse Positional Strategies for Safety Games

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 system with its environment explicit. Often, a winning strategy for one of the players is used as a certificate or as an artefact for further processing in the application. Small such certificates, i.e., strategies that can be written down very compactly, are typically preferred. For safety games, we only need to consider positional strategies. These map game positions of a player onto a move that is to be taken by the player whenever the play enters that position. For representing positional strategies compactly, a common goal is to minimize the number of positions for which a winning player's move needs to be defined such that the game is still won by the same player, without visiting a position with an undefined next move. We call winning strategies in which the next move is defined for few of the player's positions sparse. Unfortunately, even roughly approximating the density of the sparsest strategy for a safety game has been shown to be NP-hard. Thus, to obtain sparse strategies in practice, one either has to apply some heuristics, or use some exhaustive search technique, like ILP (integer linear programming) solving. In this paper, we perform a comparative study of currently available methods to obtain sparse winning strategies for the safety player in safety games. We consider techniques from common knowledge, such as using ILP or SAT (satisfiability) solving, and a novel technique based on iterative linear programming. The results of this paper tell us if current techniques are already scalable enough for practical use.

0 citations0 reviewsNo code linkedOpen access
preprint2011arXiv

Experimental Aspects of Synthesis

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 publicly available synthesis tools, and then draw conclusions by deriving useful schemes for future such evaluations. In particular, we explain why previous tools have incompatible scopes and semantics and provide a framework that reduces the impact of this problem for future experimental comparisons of such tools. Furthermore, we discuss which difficulties the complex workflows that begin to appear in modern synthesis tools induce on experimental evaluations and give answers to the question how convincing such evaluations can still be performed in such a setting.

0 citations0 reviewsNo code linkedOpen access
preprint2011arXiv

Reactive Safety

The distinction between safety and liveness properties is a fundamental classification with immediate implications on the feasibility and complexity of various monitoring, model checking, and synthesis problems. In this paper, we revisit the notion of safety for reactive systems, i.e., for systems whose behavior is characterized by the interplay of uncontrolled environment inputs and controlled system outputs. We show that reactive safety is a strictly larger class of properties than standard safety. We provide algorithms for checking if a property, given as a temporal formula or as a word or tree automaton, is a reactive safety property and for translating such properties into safety automata. Based on this construction, the standard verification and synthesis algorithms for safety properties immediately extend to the larger class of reactive safety.

0 citations0 reviewsNo code linkedOpen access