The data used comes from the TGCC jobs. All data, scripts, benchmarks, and (binaries of the) tools are archived and will be made available soon. Congratulations to the winners and thanks to all the participants!

The winners

Parity game realizability

• Realizability: Knor

LTL realizability

• Realizability: ltlsynt

LTL synthesis

• Synthesis time: ltlsynt
• Synthesis quality: semml

LTLf realizability

• Realizability: ltlfsynt

Parity game Realizability

LTL Realizability

LTL Synthesis

LTLf Realizability

Benchmarks and Solvers

The set of benchmarks used in 2025 can be fetched from the usual repository.

Below, you will find information regarding the participating solvers, their source code, license type, and links to their most recent reports or preferred publications to be cited in case you use the tool in your academic work.

This year, the competition will run with a new setup!

From 2025 onward, the competition will be run on the French Très Grand Centre de Calcul
du CEA (TGCC), https://www-hpc.cea.fr/tgcc-public/en/html/tgcc-public.html. To submit your solvers, things will be simplified to the creation of a docker image with your solver and you communicating to the organizers the repository address of the image.

In SYNTCOMP 2025, we will run the following tracks (based on the same rules and with the
same specification formats as in previous years):
– realizability and synthesis for LTL specifications in TLSF
– realizability for parity games in extended HOA and
– realizability for LTLf specifications in an extended version of the TLSF format.

Tools will be evaluated with respect to the number of solved benchmarks, and (for
synthesis) with respect to the size of their solutions.

Call for Benchmarks

We are looking for new synthesis benchmarks to include into SYNTCOMP, in any of the formats (TLSF, extended HOA). New benchmarks can be included in SYNTCOMP 2025 if they are correctly submitted to our benchmark repository https://github.com/SYNTCOMP/benchmarks by June 1, 2025. Please create a new issue, attach an archive with your new benchmarks with a sensible name, and make sure the archive should also contain a readme.md or readme.pdf describing the benchmarks, relevant papers, etc. We will check if everything is OK, and then add it to the repository. Alternatively, you can create a pull request with your benchmarks.

Call for Solvers

Solvers for all tracks of the competition will be accepted until June 1. Your solver will
be included in SYNTCOMP 2025 if:
– the address of a working docker extension is communicated to us by June 1, 2025, and
– a technical description of the solver is submitted with it. (A pdf of 1-2 pages in LNCS
format please.)

Please use this docker image as the basis for your submission and contact us as soon as possible so that we can start testing it in the cluster. This is especially important if you prefer that we compile your tool in the server!

If you are interested in submitting a solver, please have a look at the pages for Rules, Schedule, Submission, and FAQ on https://www.syntcomp.org/. If you have any further questions or comments, please write to jacobs@cispa.de, guillermo.perez@uantwerpen.be, and philipp.schlehuber-caissier@telecom-sudparis.eu.

The data used comes from the StarExec jobs. All data, scripts, benchmarks, and (binaries of the) tools are archived as a Zenodo artifact here. Congratulations to the winners and thanks to all the participants!

The winners

Parity game realizability

• Sequential realizability: Knor
• Parallel realizability: Knor

LTL realizability

• Sequential realizability: SemML
• Parallel realizability: SemML

LTLf realizability

• Sequential realizability: Nike
• Parallel realizability: Nike

Parity game Realizability

LTL Realizability

LTLf Realizability

Benchmarks and Solvers

The set of benchmarks used in 2024 can be fetched from the usual repository.

Below, you will find information regarding the participating solvers, their source code, license type, and links to their most recent reports or preferred publications to be cited in case you use the tool in your academic work.

New this year: The LTLf specification semantics have been updated so that the controller is expected to dictate the end of a trace. Please contact the organizers if this is not clear.

Each track is separated into subtracks for realizability checking and synthesis. Tools will be evaluated with respect to the number of solved benchmarks, and with respect to the size of their solutions.

* Call for Benchmarks *

We are looking for new synthesis benchmarks to include into SYNTCOMP, in any of the formats (AIGER, TLSF, extended HOA). New benchmarks can be included in SYNTCOMP 2024 if they are correctly submitted to our benchmark repository by June 1, 2024. Please create a new issue, attach an archive with your new benchmarks with a sensible name, and make sure the archive should also contains a readme.md or readme.pdf describing the benchmarks, relevant papers, etc. We will check if everything is OK, and then add it to the repository. Alternatively, you can create a pull request with your benchmarks. Contact us (see above) if you have any questions regarding scope or format of benchmarks.

* Call for Solvers *

Solvers for all tracks of the competition will be accepted until June 1. Because of our move to StarExec, you will be allowed to update your solver as many times as needed. Your solver will be included in SYNTCOMP 2024 if it is correctly uploaded into StarExec by June 1, 2024.

* Communication *

If you are interested in submitting a solver, please have a look at the pages for Rules, Schedule, Submission, and FAQ. If you have any further questions or comments, please write to jacobs@cispa.saarland, guillermo.perez@uantwerpen.be, or philipp@lrde.epita.fr

All graphs and tables were obtained as described here. The data used comes from the StarExec jobs. All data, scripts, benchmarks, and (binaries of the) tools are archived as a Zenodo artifact here. Congratulations to the winners and thanks to all the participants!

The winners

Parity games

• Sequential realizability: Knor
• Parallel realizability: Knor
• Sequential synthesis: ltlsynt
• Parallel synthesis: Knor
• Sequential synthesis (quality): Strix
• Parallel synthesis (quality): Strix

LTL

• Sequential realizability: Strix
• Parallel realizability: Strix
• Sequential synthesis: Strix
• Parallel synthesis: Strix
• Sequential synthesis (quality): Strix
• Parallel synthesis (quality): Strix

LTLf

• Sequential realizability: Nike
• Parallel realizability: Nike

Parity game Realizability

Parity game Synthesis

LTL Realizability

LTL Synthesis

LTLf Realizability

Benchmarks and Solvers

The set of benchmarks used in 2023 can be fetched from the usual repository.

Below, you will find information regarding the participating solvers, their
source code, license type, and links to their most recent reports or preferred
publications to be cited in case you use the tool in your academic work.

New this year: LTLf specifications in an extended version of the TLSF format! If you are interested, please contact us for more details on the exact semantics and the format we will be using for this track.

Each track is separated into subtracks for realizability checking and synthesis. Tools will be evaluated with respect to the number of solved benchmarks, and with respect to the size of their solutions.

* Call for Benchmarks *

We are looking for new synthesis benchmarks to include into SYNTCOMP, in any of the formats (AIGER, TLSF, extended HOA). New benchmarks can be included in SYNTCOMP 2023 if they are correctly submitted to our benchmark repository by June 1, 2023. Please create a new issue, attach an archive with your new benchmarks with a sensible name, and make sure the archive should also contains a readme.md or readme.pdf describing the benchmarks, relevant papers, etc. We will check if everything is OK, and then add it to the repository. Alternatively, you can create a pull request with your benchmarks. Contact us (see above) if you have any questions regarding scope or format of benchmarks.

* Call for Solvers *

Solvers for all tracks of the competition will be accepted until June 1. Because of our move to StarExec, you will be allowed to update your solver as many times as needed. Your solver will be included in SYNTCOMP 2023 if it is correctly uploaded into StarExec by June 1, 2023.

* Communication *

If you are interested in submitting a solver, please have a look at the pages for Rules, Schedule, Submission, and FAQ. If you have any further questions or comments, please write to jacobs@cispa.saarland, guillermo.perez@uantwerpen.be, or philipp@lrde.epita.fr

Rankings

Parity games: realizability

1. Knor
2. Strix
3. ltlsynt

Parity games: synthesis

1. Strix
2. ltlsynt
3. Knor

LTL: realizability

1. Strix
2. ltlsynt
3. Acacia bonsai
4. sdf
5. SPORE
6. Otus

LTL: synthesis

1. Strix
2. sdf
3. ltlsynt
4. Otus

1. Strix
2. ltlsynt
3. sdf
4. Otus

Benchmarks and Solvers

The competition will run on StarExec, as in 2020 and 2021. If you plan on submitting a benchmark or solver, please go to https://www.starexec.org/, create a user,
and contact us (jacobs@cispa.saarland, guillermoalberto.perez@uantwerpen.be) to be added to the SYNTCOMP space. There are main tracks for
– safety specifications in AIGER format,
– LTL specifications in TLSF, and
– parity games in Hanoi Omega-Automata (HOA) format,
each separated into subtracks for realizability checking and synthesis. Tools will be evaluated with respect to the number of solved benchmarks, and with respect to the size of their solutions.

* Call for Benchmarks *

We are looking for new synthesis benchmarks to include into SYNTCOMP, in AIGER, TLSF, and HOA. New benchmarks can be included in this year’s SYNTCOMP if they are correctly uploaded (as an issue) to the SYNTCOMP benchmark repository into StarExec by July 1. Contact us (see above) if you have any questions regarding scope or format of benchmarks.

* Call for Solvers *

Solvers for all tracks of the competition will be accepted until July 1. Because of our move to StarExec, you will be allowed to update your solver as many times as needed. Your solver will be included in this year’s SYNTCOMP if it is correctly uploaded (i.e. passes a test run) into StarExec by July 1.

* Communication *

If you are interested in submitting a solver, please have a look at the pages for Rules, Schedule, Submission, and FAQ. If you have any further questions or comments, please write to jacobs@cispa.saarland and guillermoalberto.perez@uantwerpen.be

This year, the competition consisted of LTL tracks, with specifications in TLSF, and parity-game tracks, with specifications in extended HOA. Since we had an increase in participants, this year we had sequential and parallel versions of the realizability and synthesis sub-tracks! Also worth mentioning is the reorganization of our benchmark library.

Winners

Knor won the parity-game synthesis track, solving 276/303 benchmarks. It also won the hard-parity-game realizability track by solving 216/217 benchmarks.

Strix placed first in the quality ranking for parity-game synthesis. In its LTL/TLSF version, Strix won the LTL sequential realizability track by solving 827/924 benchmarks; and placed first in the quality ranking for LTL sequential synthesis.

sdf won the LTL parallel realizability track, solving 730/942 benchmarks, and the LTL parallel synthesis track.

Congratulations to the winners, and many thanks to all contributors of benchmarks and all participants!

The competition will run on StarExec, as in 2020. If you plan on submitting a benchmark or solver, please go to https://www.starexec.org/, create a user,
and contact us (jacobs@cispa.saarland, guillermoalberto.perez@uantwerpen.be) to be added to the SYNTCOMP space. There are main tracks for
– safety specifications in AIGER format,
– LTL specifications in TLSF, and
– parity games in Hanoi Omega-Automata (HOA) format,
each separated into subtracks for realizability checking and synthesis, and
into sequential and parallel execution modes. Tools will be evaluated with respect to the number of solved benchmarks, and with respect to the size of their solutions.

* Call for Benchmarks *

We are looking for new synthesis benchmarks to include into SYNTCOMP, in AIGER, TLSF, and HOA. New benchmarks can be included in SYNTCOMP 2021 if they are correctly uploaded (as an issue) to the SYNTCOMP benchmark repository into StarExec by June 1, 2021. Contact us (see above) if you have any questions regarding scope or format of benchmarks.

* Call for Solvers *

Solvers for all tracks of the competition will be accepted until June 1. Because of our move to StarExec, you will be allowed to update your solver as many times as needed. Your solver will be included in SYNTCOMP 2021 if it is correctly uploaded (i.e. passes a test run) into StarExec by June 1, 2021.

* Communication *

If you are interested in submitting a solver, please have a look at the pages for Rules, Schedule, Submission, and FAQ. If you have any further questions or comments, please write to jacobs@cispa.saarland and guillermoalberto.perez@uantwerpen.be