Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

The Reactive Synthesis Competition (SYNTCOMP): 2018-2021

Swen Jacobs, Guillermo A. Perez, Remco Abraham, Veronique Bruyere, Michael Cadilhac, Maximilien Colange, Charly Delfosse, Tom van Dijk, Alexandre Duret-Lutz, Peter Faymonville, Bernd Finkbeiner, Ayrat Khalimov, Felix Klein, Michael Luttenberger, Klara Meyer, Thibaud Michaud, Adrien Pommellet, Florian Renkin, Philipp Schlehuber-Caissier, Mouhammad Sakr, Salomon Sickert, Gaetan Staquet, Clement Tamines, Leander Tentrup, Adam Walker

TL;DR

The paper documents SYNTCOMP 2018–2021, detailing the evaluation framework, benchmark evolution, participating tools, and experimental results across safety, parity, and LTL tracks. It highlights advances in LTL and parity-synthesis, including the rise of Owl-Pig approaches (Strix, Ltlsynt) and symbolic parity-game solving (Knor-BDD), and notes the ongoing importance of TLSF-encoded, parameterized benchmarks for scalability assessment. The authors analyze tool performance, discuss lessons learned for LTL synthesis and parity games, and propose rule changes to enhance comparability and industrial relevance in future editions. Overall, SYNTCOMP demonstrates measurable progress in synthesis tool quality and benchmark diversity, reinforcing its role as a benchmark platform to drive practical, scalable reactive synthesis research.

Abstract

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.

The Reactive Synthesis Competition (SYNTCOMP): 2018-2021

TL;DR

The paper documents SYNTCOMP 2018–2021, detailing the evaluation framework, benchmark evolution, participating tools, and experimental results across safety, parity, and LTL tracks. It highlights advances in LTL and parity-synthesis, including the rise of Owl-Pig approaches (Strix, Ltlsynt) and symbolic parity-game solving (Knor-BDD), and notes the ongoing importance of TLSF-encoded, parameterized benchmarks for scalability assessment. The authors analyze tool performance, discuss lessons learned for LTL synthesis and parity games, and propose rule changes to enhance comparability and industrial relevance in future editions. Overall, SYNTCOMP demonstrates measurable progress in synthesis tool quality and benchmark diversity, reinforcing its role as a benchmark platform to drive practical, scalable reactive synthesis research.

Abstract

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.
Paper Structure (44 sections, 1 equation, 7 figures, 9 tables)

This paper contains 44 sections, 1 equation, 7 figures, 9 tables.

Table of Contents

  1. Introduction
  2. Setup, Rules, and Execution
  3. Synthesis and realizability
  4. Synthesis games and strategies
  5. Finite-memory strategies
  6. Safety, parity, and linear-temporal specifications
  7. LTL-defined payoff sets
  8. Specification formats
  9. Output format
  10. Rules
  11. Disqualification
  12. Extraordinary comparisons
  13. Ranking schemes
  14. Selection of benchmarks
  15. Execution
  16. ...and 29 more sections

Figures (7)

  • Figure 1: Bump plot of the rankings for the LTL realizability tracks for all editions of SYNTCOMP 2017--2021 (2017 is included for reference since some tools are no longer maintained and being updated)
  • Figure 2: Cactus (a.k.a. survival) plots for the participants of the LTL realizability track of SYNTCOMP 2021; Note that the y-axis is displayed using logarithmic scale
  • Figure 3: Cactus (a.k.a. survival) plots for the participants of the LTL synthesis track of SYNTCOMP 2018 (left) and 2021 (right); Again, the y-axis is displayed using logarithmic scale
  • Figure 4: Cactus plots for the participants of the LTL synthesis track of SYNTCOMP 2018 (left) and 2021 (right) --- this time, showing total output size instead of time (counting AND-gates only); Note that the y-axis is displayed using logarithmic scale
  • Figure 5: Cactus plots for all the participants of the LTL synthesis track of SYNTCOMP 2021, restricted to the mux (left) and shift (right) benchmark families
  • ...and 2 more figures

Theorems & Definitions (4)

  • Definition 1: Infinite-word automata
  • Definition 2: Games
  • Definition 3: Strategies
  • Definition 4: Realizability and Synthesis