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

Abstract

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.

arXiv commentIn Proceedings SYNT 2016, arXiv:1611.07178

References in corpus (10)

• LTL to Büchi Automata Translation: Fast and More Deterministic
• The First Reactive Synthesis Competition (SYNTCOMP 2014)
• AbsSynthe: abstract synthesis from succinct safety specifications
• Parameterized Synthesis Case Study: AMBA AHB
• Parameterized Synthesis Case Study: AMBA AHB (extended version)
• The Second Reactive Synthesis Competition (SYNTCOMP 2015)
• Extended AIGER Format for Synthesis
• The Reactive Synthesis Competition: SYNTCOMP 2016 and Beyond
• Compositional Algorithms for Succinct Safety Games
• Specification Format for Reactive Synthesis Problems

Cited by in corpus (8)

• The 4th Reactive Synthesis Competition (SYNTCOMP 2017): Benchmarks, Participants & Results
• From LTL and Limit-Deterministic Büchi Automata to Deterministic Parity Automata
• Solving QBF by Abstraction
• The Reactive Synthesis Competition: SYNTCOMP 2016 and Beyond
• CTL* synthesis via LTL synthesis
• Performance Heuristics for GR(1) Synthesis and Related Algorithms
• Clausal Abstraction for DQBF (full version)
• BoSy: An Experimentation Framework for Bounded Synthesis