arXiv subjects

Felix Klein

Publications and source records attributed to Felix Klein.

23 records · Page 2Linked to original sources

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.0

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. We also 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↗

arXiv2015

What are Strategies in Delay Games? Borel Determinacy for Games with Lookahead

We investigate determinacy of delay games with Borel winning conditions, infinite-duration two-player games in which one player may delay her moves to obtain a lookahead on her opponent's moves. First, we prove determinacy of such games with respect to a fixed evolution of the lookahead. However, strategies in such games may depend on information about the evolution. Thus, we introduce different notions of universal strategies for both players, which are evolution-independent, and determine the exact amount of information a universal strategy needs about the history of a play and the evolution of the lookahead to be winning. In particular, we show that delay games with Borel winning conditions are determined with respect to universal strategies. Finally, we consider decidability problems, e.g., "Does a player have a universal winning strategy for delay games with a given winning condition?", for omega-regular and omega-context-free winning conditions.

cs.LO↗

arXiv2014

Solving 3-Color Parity Games in $ O(n^2) $ Time

Parity games are an expressive framework to consider realizability questions for omega-regular languages. However, it is open whether they can be solved in polynomial time, making them unamenable for practical usage. To overcome this restriction, we consider 3-color parity games, which can be solved in polynomial time. They still cover an expressive fragment of specifications, as they include the classical Büchi and co-Büchi winning conditions as well as their union and intersection. This already suffices to express many useful combinations of safety and liveness properties, as for example the family of GR(1). The best known algorithm for 3-color parity games solves a game with n vertices in $ O(n^{2}\sqrt{n}) $ time. We improve on this result by presenting a new algorithm, based on simple attractor constructions, which only needs time $ O(n^2) $. As a result, we match the best known running times for solving (co)-Büchi games, showing that 3-color parity games are not harder to solve in general.

cs.LO↗

arXiv2008

SDSS J120923.7+264047: A new massive galaxy cluster with a bright giant arc

Highly magnified lensed galaxies allow us to probe the morphological and spectroscopic properties of high-redshift stellar systems in great detail. However, such objects are rare, and there are only a handful of lensed galaxies which are bright enough for a high-resolution spectroscopic study with current instrumentation. We report the discovery of a new massive lensing cluster, SDSS J120923.7+264047, at z=0.558. Present around the cluster core, at angular distances of up to ~40'', are many arcs and arc candidates, presumably due to lensing of background galaxies by the cluster gravitational potential. One of the arcs, 21'' long, has an r-band magnitude of 20, making it one of the brightest known lensed galaxies. We obtained a low-resolution spectrum of this galaxy, using the Keck-I telescope, and found it is at redshift of z=1.018.

astro-ph↗