47 citations · 137 across the 13 of their papers we have counts for
15 papers
The Reactive Synthesis Competition (SYNTCOMP): 2018-2021
Swen Jacobs, Guillermo A. Perez, Remco Abraham +22
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. Th…
Live Synthesis
Bernd Finkbeiner, Felix Klein, Niklas Metzger
Synthesis automatically constructs an implementation that satisfies a given logical specification. In this paper, we study the live synthesis problem, where the synthesized impleme…
Syntroids: Synthesizing a Game for FPGAs using Temporal Logic Specifications
Gideon Geier, Philippe Heim, Felix Klein +1
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…
Synthesizing Functional Reactive Programs
Bernd Finkbeiner, Felix Klein, Ruzica Piskac +1
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 ab…
The 5th Reactive Synthesis Competition (SYNTCOMP 2018): Benchmarks, Participants & Results
Swen Jacobs, Roderick Bloem, Maximilien Colange +11
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 th…
Bounded Synthesis of Reactive Programs
Carsten Gerstacker, Felix Klein, Bernd Finkbeiner
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, unreadab…
Vehicle Platooning Simulations with Functional Reactive Programming
Bernd Finkbeiner, Felix Klein, Ruzica Piskac +1
Functional languages have provided major benefits to the verification community. Although features such as purity, a strong type system, and computational abstractions can help gui…
Reactive Synthesis: Towards Output-Sensitive Algorithms
Bernd Finkbeiner, Felix Klein
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 rea…
The 4th Reactive Synthesis Competition (SYNTCOMP 2017): Benchmarks, Participants & Results
Swen Jacobs, Nicolas Basset, Roderick Bloem +11
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 th…
The 3rd Reactive Synthesis Competition (SYNTCOMP 2016): Benchmarks, Participants & Results
Swen Jacobs, Roderick Bloem, Romain Brenguier +13
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 benchm…
Bounded Cycle Synthesis
Bernd Finkbeiner, Felix Klein
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 implem…
A High-Level LTL Synthesis Format: TLSF v1.1
Swen Jacobs, Felix Klein, Sebastian Schirmer
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…
What are Strategies in Delay Games? Borel Determinacy for Games with Lookahead
Felix Klein, Martin Zimmermann
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 opp…
Solving 3-Color Parity Games in Time
Felix Klein
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…
How Much Lookahead is Needed to Win Infinite Games?
Felix Klein, Martin Zimmermann
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. For -regular winning conditions it i…