arXiv subjects

Rüdiger Ehlers

Publications and source records attributed to Rüdiger Ehlers.

At least 19 recordsLinked to original sources

arXiv2026

From LTL to COCOA without Detours

Chains of co-Büchi automata (COCOA) have recently been introduced as a new canonical representation of omega-regular languages. The co-Büchi automata in a chain assign each omega-word its natural color, which depends only on the language itself and not on the chosen automaton representation. Automata in such a chain can be minimized in polynomial time and are good-for-games, making this representation attractive for verification and reactive synthesis. However, in these applications, specifications are usually given in linear temporal logic (LTL). To make COCOA useful, an LTL specification must first be translated into the chain of automata. The only translation currently known proceeds via deterministic parity automata (LTL$\,{\to}\,$DPA$\,{\to}\,$COCOA), where the first step ignores natural colors and requires involved constructions due to Safra or Esparza et al. This raises the question of whether, by exploiting the definition of the natural color of words, one can avoid such constructions and obtain a direct translation from LTL to COCOA. In this paper, we present a simple yet optimal translation from LTL to COCOA, as well as a variant that translates LTL into DPA. The translation represents a new path from LTL to DPA and exploits the definition of natural colors. It relies on standard operations on weak alternating automata, the Miyano-Hayashi breakpoint construction, the subset construction, and simple graph algorithms. Starting from weak alternating automata, the procedure also applies to specifications in linear dynamic logic. The procedure runs in asymptotically optimal doubly exponential time and produces automata of asymptotically optimal size.

cs.FL↗

arXiv2026

How Concise are Chains of co-Büchi Automata?

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 time and are hence an attractive language representation for applications in which normally, deterministic omega-automata are used. While it is known how to build COCOA from deterministic parity automata, little is currently known about their relationship to automaton models introduced earlier than COCOA. In this paper, we analyze the conciseness of chains of co-Büchi automata. We provide three main results and give an overview of the implications of these results. First of all, we show that even in the case that all automata in the chain are deterministic, chains of co-Büchi automata can be exponentially more concise than deterministic parity automata. We then present two main results that together negatively answer the question if this conciseness is retained when performing Boolean operations (such as disjunction, conjunction, and complementation) over COCOA. For the binary operations, we show that there exist families of languages for which their application leads to an exponential growth of the sizes of the automata. The families have the property that when representing them using deterministic parity automata, taking the disjunction or conjunction of the family elements only requires a polynomial blow-up. We finally show that an exponential blow-up is also unavoidable when complementing a COCOA, as this operation can require redistributing with which colors words need to be recognized.

cs.LO↗

arXiv2025

How Concise are Chains of co-Büchi Automata?

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 time and are hence an attractive language representation for applications in which normally, deterministic omega-automata are used. While it is known how to build COCOA from deterministic parity automata, little is currently known about their relationship to automaton models introduced earlier than COCOA. In this paper, we analyze the conciseness of chains of co-Büchi automata. We show that even in the case that all automata in the chain are deterministic, chains of co-Büchi automata can be exponentially more concise than deterministic parity automata. We then answer the question if this conciseness is retained when performing Boolean operations (such as disjunction and conjunction) over COCOA by showing that there exist families of languages for which these operations lead to an exponential growth of the sizes of the automata. The families have the property that when representing them using deterministic parity automata, taking the disjunction or conjunction of them only requires a polynomial blow-up, which shows that Boolean operations over COCOA do not retain their conciseness in general.

cs.FL↗

arXiv2025

Characterizing the Polynomial-Time Minimizable $ω$-Automata

A central question in the theory of automata is which classes of automata can be minimized in polynomial time. We close the remaining gaps for deterministic and history-deterministic automata over infinite words by proving that deterministic co-Büchi automata with transition-based acceptance are NP-hard to minimize, as are history-deterministic Büchi automata with transition-based acceptance.

cs.FL↗

arXiv2025

Rerailing Automata

In this paper, we introduce rerailing automata for $ω$-regular languages. They generalize both deterministic parity (DPW) and minimized history-deterministic co-Büchi automata (with transition based acceptance, HdTbcBW) while combining their favorable properties. In particular, rerailing automata can represent arbitrary $ω$-regular languages while allowing for polynomial-time minimization, just as HdTbcBW do. Since DPW are a special case of rerailing automata, a minimized rerailing automaton is never larger than the smallest deterministic parity automaton for the same language. We also show that rerailing automata can be used as a replacement for deterministic parity automata for the realizability check of open systems. The price to be paid to obtain the useful properties of rerailing automata is that the acceptance condition in such automata refers to the dominating colors along all runs for a given word, where just as in parity automata, the dominating color along a run is the lowest one occurring infinitely often along it. A rerailing automaton accepts those words for which the greatest of the dominating colors along the runs is even. Additionally, rerailing automata guarantee that every prefix of a run for a word can be extended to eventually reach a point from which all runs for the word extending the prefix have the same dominating color, and it is even if and only if the word is in the language of the automaton. We show that these properties together allow characterizing the role of each state in such an automaton in a way that relates it to state combinations in a sequence of co-Büchi automata for the represented language. This characterization forms the basis of the polynomial-time minimization approach in this paper.

cs.FL↗

arXiv2024

Fully Generalized Reactivity(1) Synthesis

Generalized Reactivity(1) (GR(1)) synthesis is a reactive synthesis approach in which the specification is split into two parts: a symbolic game graph, describing the safe transitions of a system, a liveness specification in a subset of Linear Temporal Logic (LTL) on top of it. Many specifications can naturally be written in this restricted form, and the restriction gives rise to a scalable synthesis procedure -- the reasons for the high popularity of the approach. For specifications even slightly beyond GR(1), however, the approach is inapplicable. This necessitates a transition to synthesizers for full LTL specifications, introducing a huge efficiency drop. This paper proposes a synthesis approach that smoothly bridges the efficiency gap from GR(1) to LTL by unifying synthesis for both classes of specifications. The approach leverages a recently introduced canonical representation of omega-regular languages based on a chain of good-for-games co-Büchi automata (COCOA). By constructing COCOA for the liveness part of a specification, we can then build a fixpoint formula that can be efficiently evaluated on the symbolic game graph. The COCOA-based synthesis approach outperforms standard approaches and retains the efficiency of GR(1) synthesis for specifications in GR(1) form and those with few non-GR(1) specification parts.

cs.FL↗

arXiv2022

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.

cs.AI↗

arXiv2022

Natural Colors of Infinite Words

While finite automata have minimal DFAs as a simple and natural normal form, deterministic omega-automata do not currently have anything similar. One reason for this is that a normal form for omega-regular languages has to speak about more than acceptance - for example, to have a normal form for a parity language, it should relate every infinite word to some natural color for this language. This raises the question of whether or not a concept such as a natural color of an infinite word (for a given language) exists, and, if it does, how it relates back to automata. We define the natural color of a word purely based on an omega-regular language, and show how this natural color can be traced back from any deterministic parity automaton after two cheap and simple automaton transformations. The resulting streamlined automaton does not necessarily accept every word with its natural color, but it has a 'co-run', which is like a run, but can once move to a language equivalent state, whose color is the natural color, and no co-run with a higher color exists. The streamlined automaton defines, for every color c, a good-for-games co-Büchi automaton that recognizes the words whose natural colors w.r.t. the represented language are at least c. This provides a canonical representation for every $ω$-regular language, because good-for-games co-Büchi automata have a canonical minimal (and cheap to obtain) representation for every co-Büchi language.

cs.FL↗

arXiv2021

Adapting to the Behavior of Environments with Bounded Memory

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 a limited number of states. This problem was originally defined and studied by Kupferman, Lustig, Vardi, and Yannakakis. They provide NP and 2-EXPTIME lower and upper bounds (respectively) for the complexity of this problem, in the size of the transducer. We tighten the gap by providing a PSPACE lower bound, thereby showing that algorithms for solving this problem are unlikely to scale to large environment sizes. This result is somewhat unfortunate as solving this problem enables tackling some high-level control problems in which an agent has to infer the environment behavior from observations. To address this observation, we study a modified synthesis problem in which the synthesized controller must gather information about the environment's behavior safely. We show that the problem of determining whether the behavior of such an environment can be safely learned is only co-NP-complete. Furthermore, in such scenarios, the behavior of the environment can be learned using a Turing machine that requires at most polynomial space in the size of the environment's transducer.

cs.FL↗

arXiv2021

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.

cs.LG↗

arXiv2020

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)$.

cs.FL↗

arXiv2018

Exact Synthesis of ESOP Forms

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 finds one or more ESOP forms for a given Boolean function. The approach can deal with incompletely-specified Boolean functions defined over many Boolean variables and is particularly fast if the Boolean function can be expressed with only a few product terms. We describe the formalization of the ESOP synthesis problem with a fixed number of terms as a decision problem and present search procedures for determining ESOP forms of minimum size. We further discuss how the search procedures can be relaxed to find ESOP forms of small sizes in reasonable time. We experimentally evaluate the performance of the SAT-based synthesis procedures on completely- and incompletely-specified Boolean functions.

cs.LO↗

arXiv2018

Revisiting Decision Diagrams for SAT

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 both existing ZDD and BDD variants of this approach. We further investigate different heuristics for selecting the next variable to eliminate. Our implementation makes further use of parallel features of the open source BDD library Sylvan.

cs.LO↗

arXiv2016

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.

cs.LO↗

arXiv2015

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.

cs.PL↗

arXiv2014

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.

cs.SE↗

arXiv2014

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.

cs.LO↗

arXiv2014

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.

cs.LO↗