arXiv subjects

Felix Klein

Publications and source records attributed to Felix Klein.

At least 19 recordsLinked to original sources

arXiv2026

The Unified Evaluation App for DNA Data Storage Codecs

Background: Deoxyribonucleic acid (DNA) data storage is a paradigm with great potential for ultra-dense and durable information preservation. However, the rapid proliferation of coding schemes, or codecs, each with their own design constraints and reporting practices, has led to a fragmented landscape that lacks a standardized comparative assessment. Methods: We developed an open-source, modular benchmarking platform that systematically integrates and evaluates state-of-the-art DNA storage encoding and decoding methods (codecs). Our approach uses a curated, diverse set of baseline data and applies multidimensional assessment criteria that are aligned with the consensus standard of the DNA Data Storage Alliance. These criteria include encoding/decoding throughput, computational efficiency, error correction performance across substitutions, insertions, and deletions, and cost efficiency. Results: The developed platform integrates standardized wrapper functions for encoding and decoding, allows for the integration of new methods, and automates reproducible evaluations with comprehensive visual and tabular reporting. Benchmarking both contemporary and classical codecs using their default parameters and multiple metrics demonstrates that no single algorithm is optimal across all evaluated dimensions. The trade-offs between information density, success rate, runtime, and cost are quantified and shown to be critical factors in the design of future-proof formats. Conclusions: Our work establishes a rigorously standardized, open-source evaluation framework that enables reproducible benchmarking, supports evidence-based codec selection, and provides the necessary foundation for translating DNA data storage from experimental research into deployable archival systems.

cs.ET↗

arXiv2025

bittide: Control Time, Not Flows

This paper presents the first hardware implementation of bittide, a decentralized clock synchronization mechanism for achieving logical synchrony in distributed systems. We detail the design and implementation of an 8-node bittide network using off-the-shelf FPGA boards and adjustable clock sources. Through experiments with various network topologies, including fully connected, hourglass, and cube, we demonstrate the effectiveness of bittide in aligning node frequencies and bounding buffer excursions. We collect and analyze frequency, buffer occupancy, and logical latency data, validating the hardware's performance against theoretical predictions and simulations. Our results show that bittide achieves tight frequency alignment, robustly handles varying physical latencies, and establishes a consistent notion of logical time across the network, enabling predictable distributed computation at scale with zero in-band overhead.

cs.DC↗

arXiv2024

Double sine-Gordon class of universal coarsening dynamics in a spin-1 Bose gas

Far from equilibrium, universal dynamics prevails in many different situations, from pattern coarsening to turbulence. A central longstanding problem concerns the development of a theory of coarsening that rests on the microscopic properties of the system and allows identifying the interaction mechanisms underlying a possible overarching universality class of the associated scaling dynamics. In quantum systems, this is complicated by the existence of nonlinear and topological excitations due to the compact nature of phase degrees of freedom. We show that the double sine-Gordon model as a noncompact low-energy effective model of the spin-1 Bose gas accounts for subdiffusive coarsening dynamics, identifying field configurations spread over multiple wells of the sinusoidal potential as a precondition for the slow scaling. This is in contrast to diffusion-type scaling which the model is known to exhibit as well, where field configurations are seen to not extend over more than two wells. Experimental observations of a spinor BEC support these characteristics, thus constituting a platform for the investigation of sine-Gordon dynamics. Our results point to a path towards a classification of pattern coarsening in many-body systems on the basis of microscopic models.

cond-mat.quant-gas↗

arXiv2022

The Reactive Synthesis Competition (SYNTCOMP): 2018-2021

We report on the last four editions of the reactive synthesis competition (SYNTCOMP 2018-2021). We briefly describe the evaluation scheme and the experimental setup of SYNTCOMP. Then, we introduce new benchmark classes that have been added to the SYNTCOMP library and give an overview of the participants of SYNTCOMP. Finally, we present and analyze the results of our experimental evaluations, including a ranking of tools with respect to quantity and quality - that is, the total size in terms of logic and memory elements - of solutions.

cs.LO↗

arXiv2021

Live Synthesis

Synthesis automatically constructs an implementation that satisfies a given logical specification. In this paper, we study the live synthesis problem, where the synthesized implementation replaces an already running system. In addition to satisfying its own specification, the synthesized implementation must guarantee a sound transition from the previous implementation. This version of the synthesis problem is highly relevant in always-on applications, where updates happen while the system is running. To specify the correct handover between the old and new implementation, we introduce an extension of linear-time temporal logic (LTL) called LiveLTL. A LiveLTL specification defines separate requirements on the two implementations and ensures that the new implementation satisfies, in addition to its own requirements, any obligations left unfinished by the old implementation. For specifications in LiveLTL, we show that the live synthesis problem can be solved within the same complexity bound as standard reactive synthesis, i.e., in 2EXPTIME. Our experiments show the necessity of live synthesis for LiveLTL specifications created from benchmarks of SYNTCOMP and robot control.

cs.LO↗

arXiv2021

Syntroids: Synthesizing a Game for FPGAs using Temporal Logic Specifications

We present Syntroids, a case study for the automatic synthesis of hardware from a temporal logic specification. Syntroids is a space shooter arcade game realized on an FPGA, where the control flow architecture has been completely specified in Temporal Stream Logic (TSL) and implemented using reactive synthesis. TSL is a recently introduced temporal logic that separates control and data. This leads to scalable synthesis, because the cost of the synthesis process is independent of the complexity of the handled data. In this case study, we report on our experience with the TSL-based development of the Syntroids game and on the implementation quality obtained with synthesis in comparison to manual programming. We also discuss solved and open challenges with respect to currently available synthesis tools.

cs.LO↗

arXiv2020

A cavity optomechanical locking scheme based on the optical spring effect

We present a novel locking scheme for active length-stabilization and frequency detuning of a cavity optomechanical device based on the optical spring effect. The scheme can be used as an alternative to the Pound-Drever-Hall locking technique but in contrast doesn't require signal processing on time-scales of the cavity decay rate. It is therefore particularly suited for stabilizing micro cavities, where this time-scale can be extremely fast. The error signal is generated through the optical spring effect, i.e. the detuning-dependent frequency-shift of a nanomechanical oscillator that is dispersively coupled to the intra-cavity light field. We explain the functional principle of the lock and characterize its performance in terms of bandwidth and gain profile. The optical spring locking scheme can be implemented without larger efforts in a wide variety of optomechanical systems in the unresolved sideband regime.

physics.ins-det↗

arXiv2019

Synthesizing Functional Reactive Programs

Functional Reactive Programming (FRP) is a paradigm that has simplified the construction of reactive programs. There are many libraries that implement incarnations of FRP, using abstractions such as Applicative, Monads, and Arrows. However, finding a good control flow, that correctly manages state and switches behaviors at the right times, still poses a major challenge to developers. An attractive alternative is specifying the behavior instead of programming it, as made possible by the recently developed logic: Temporal Stream Logic (TSL). However, it has not been explored so far how Control Flow Models (CFMs), as synthesized from TSL specifications, can be turned into executable code that is compatible with libraries building on FRP. We bridge this gap, by showing that CFMs are indeed a suitable formalism to be turned into Applicative, Monadic, and Arrowized FRP. We demonstrate the effectiveness of our translations on a real-world kitchen timer application, which we translate to a desktop application using the Arrowized FRP library Yampa, a web application using the Monadic threepenny-gui library, and to hardware using the Applicative hardware description language ClaSH.

cs.PL↗

arXiv2019

The 5th Reactive Synthesis Competition (SYNTCOMP 2018): Benchmarks, Participants & Results

We report on the fifth reactive synthesis competition (SYNTCOMP 2018). We introduce four new benchmark classes that have been added to the SYNTCOMP library, and briefly describe the evaluation scheme and the experimental setup of SYNTCOMP 2018. We give an overview of the participants of SYNTCOMP 2018 and highlight changes compared to previous years. Finally, we present and analyze the results of our experimental evaluation, including a ranking of tools with respect to quantity and quality of solutions.

cs.LO↗

arXiv2018

Bounded Synthesis of Reactive Programs

Most algorithms for the synthesis of reactive systems focus on the construction of finite-state machines rather than actual programs. This often leads to badly structured, unreadable code. In this paper, we present a bounded synthesis approach that automatically constructs, from a given specification in linear-time temporal logic (LTL), a program in Madhusudan's simple imperative language for reactive programs. We develop and compare two principal approaches for the reduction of the synthesis problem to a Boolean constraint satisfaction problem. The first reduction is based on a generalization of bounded synthesis to two-way alternating automata, the second reduction is based on a direct encoding of the program syntax in the constraint system. We report on preliminary experience with a prototype implementation, which indicates that the direct encoding outperforms the automata approach.

cs.FL↗

arXiv2018

Vehicle Platooning Simulations with Functional Reactive Programming

Functional languages have provided major benefits to the verification community. Although features such as purity, a strong type system, and computational abstractions can help guide programmers away from costly errors, these can present challenges when used in a reactive system. Functional Reactive Programming is a paradigm that allows users the benefits of functional languages and an easy interface to a reactive environment. We present a tool for building autonomous vehicle controllers in FRP using Haskell.

cs.PL↗

arXiv2018

Reactive Synthesis: Towards Output-Sensitive Algorithms

Reactive synthesis is a technology for the automatic construction of reactive systems from logical specifications. In these lecture notes, we study different algorithms for the reactive synthesis problem of linear-time temporal logic (LTL). The classic game-based synthesis algorithm is input-sensitive in the sense that its performance is asymptotically optimal in the size of the specification, but it produces implementations that may be larger than necessary. We contrast this algorithm with output-sensitive algorithms for reactive synthesis, i.e., algorithms that are optimized towards the size or structural complexity of the synthesized system. We study the bounded synthesis algorithm, which produces an implementation with a minimal number of states, and the bounded cycle synthesis algorithm, which additionally guarantees that the number of cycles of the implementation is minimal.

cs.LO↗

arXiv2017

Temporal Stream Logic: Synthesis beyond the Bools

Reactive systems that operate in environments with complex data, such as mobile apps or embedded controllers with many sensors, are difficult to synthesize. Synthesis tools usually fail for such systems because the state space resulting from the discretization of the data is too large. We introduce TSL, a new temporal logic that separates control and data. We provide a CEGAR-based synthesis approach for the construction of implementations that are guaranteed to satisfy a TSL specification for all possible instantiations of the data processing functions. TSL provides an attractive trade-off for synthesis. On the one hand, synthesis from TSL, unlike synthesis from standard temporal logics, is undecidable in general. On the other hand, however, synthesis from TSL is scalable, because it is independent of the complexity of the handled data. Among other benchmarks, we have successfully synthesized a music player Android app and a controller for an autonomous vehicle in the Open Race Car Simulator (TORCS.)

cs.LO↗

arXiv2017

The 4th Reactive Synthesis Competition (SYNTCOMP 2017): Benchmarks, Participants & Results

We report on the fourth reactive synthesis competition (SYNTCOMP 2017). We introduce two new benchmark classes that have been added to the SYNTCOMP library, and briefly describe the benchmark selection, evaluation scheme and the experimental setup of SYNTCOMP 2017. We present the participants of SYNTCOMP 2017, with a focus on changes with respect to the previous years and on the two completely new tools that have entered the competition. Finally, we present and analyze the results of our experimental evaluation, including a ranking of tools with respect to quantity and quality of solutions.

cs.LO↗

arXiv2016

The 3rd Reactive Synthesis Competition (SYNTCOMP 2016): Benchmarks, Participants & Results

We report on the benchmarks, participants and results of the third reactive synthesis competition(SYNTCOMP 2016). The benchmark library of SYNTCOMP 2016 has been extended to benchmarks in the new LTL-based temporal logic synthesis format (TLSF), and 2 new sets of benchmarks for the existing AIGER-based format for safety specifications. The participants of SYNTCOMP 2016 can be separated according to these two classes of specifications, and we give an overview of the 6 tools that entered the competition in the AIGER-based track, and the 3 participants that entered the TLSF-based track. We briefly describe the benchmark selection, evaluation scheme and the experimental setup of SYNTCOMP 2016. Finally, we present and analyze the results of our experimental evaluation, including a comparison to participants of previous competitions and a legacy tool.

cs.LO↗

arXiv2016

Bounded Cycle Synthesis

We introduce a new approach for the synthesis of Mealy machines from specifications in linear-time temporal logic (LTL), where the number of cycles in the state graph of the implementation is limited by a given bound. Bounding the number of cycles leads to implementations that are structurally simpler and easier to understand. We solve the synthesis problem via an extension of SAT-based bounded synthesis, where we additionally construct a witness structure that limits the number of cycles. We also establish a triple-exponential upper and lower bound for the potential blow-up between the length of the LTL formula and the number of cycles in the state graph.

cs.LO↗

arXiv2016

A High-Level LTL Synthesis Format: TLSF v1.1

We present the Temporal Logic Synthesis Format (TLSF), a high-level format to describe synthesis problems via Linear Temporal Logic (LTL). The format builds upon standard LTL, but additionally allows to use high-level constructs, such as sets and functions, to provide a compact and human-readable representation. Furthermore, the format allows to identify parameters of a specification such that a single description can be used to define a family of problems. Additionally, we present a tool to automatically translate the format into plain LTL, which then can be used for synthesis by a solver. The tool also allows to adjust parameters of the specification and to apply standard transformations on the resulting formula.

cs.LO↗

arXiv2016

Prompt Delay

Delay games are two-player games of infinite duration in which one player may delay her moves to obtain a lookahead on her opponent's moves. Recently, such games with quantitative winning conditions in weak MSO with the unbounding quantifier were studied, but their properties turned out to be unsatisfactory. In particular, unbounded lookahead is in general necessary. Here, we study delay games with winning conditions given by Prompt-LTL, Linear Temporal Logic equipped with a parameterized eventually operator whose scope is bounded. Our main result shows that solving Prompt-LTL delay games is complete for triply-exponential time. Furthermore, we give tight triply-exponential bounds on the necessary lookahead and on the scope of the parameterized eventually operator. Thus, we identify Prompt-LTL as the first known class of well-behaved quantitative winning conditions for delay games. Finally, we show that applying our techniques to delay games with \omega-regular winning conditions answers open questions in the cases where the winning conditions are given by non-deterministic, universal, or alternating automata.

cs.GT↗