The First Reactive Synthesis Competition (SYNTCOMP 2014)

Abstract

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.

24 pages, published in STTT

References in corpus (6)

• A High-Level LTL Synthesis Format: TLSF v1.1
• The First Reactive Synthesis Competition (SYNTCOMP 2014)
• AbsSynthe: abstract synthesis from succinct safety specifications
• The Second Reactive Synthesis Competition (SYNTCOMP 2015)
• Extended AIGER Format for Synthesis
• Experimental Aspects of Synthesis

Cited by in corpus (8)

• A High-Level LTL Synthesis Format: TLSF v1.1
• The First Reactive Synthesis Competition (SYNTCOMP 2014)
• The 4th Reactive Synthesis Competition (SYNTCOMP 2017): Benchmarks, Participants & Results
• Solving QBF by Abstraction
• The 3rd Reactive Synthesis Competition (SYNTCOMP 2016): Benchmarks, Participants & Results
• The Reactive Synthesis Competition: SYNTCOMP 2016 and Beyond
• Using SyGuS to Synthesize Reactive Motion Plans
• Performance Heuristics for GR(1) Synthesis and Related Algorithms