Please accept that the overall spirit of this competition is friendly, honest and well-spirited. The goal is to foster research and to motivate the implementation and optimization of new synthesis tools. However as it is still a competition, the following rules shall apply:

Categories

There will be 8 competitive categories in SYNTCOMP:

• Safety Realizability (AIGER)
• Safety Synthesis (AIGER)
• LTL Realizability (TLSF)
• LTL Synthesis (TLSF)
• LTLf Realizability (TLSF)
• LTLf Synthesis (TLSF)
• Parity game Realizability (HOA)
• Parity game Synthesis (HOA)

In each category, tools can run either in sequential (single-thread) or in parallel (multi-thread) mode.

General Rules for All Categories

Organizational:

• The competition will be managed and run on the StarExec platform. Tools have to be uploaded to the SYNTCOMP space at https://www.starexec.org. Click here for additional details on the preparation of your submission.

• Submitted tools must be accompanied by a 2-4 page description (EPTCS format) of the synthesis approach and important aspects of implementation and optimizations. This should include a list of all authors and their present institutional affiliations. We encourage tool authors to submit a paper describing their tool to the synthesis workshop SYNT. If a (submitted or already published) tool paper that describes the current status of the tool exists, it can be included in the tool submission to SYNTCOMP instead of the description mentioned above. 

• Not more than 6 configurations per author in a category (parallel and sequential configurations are now bundled together). Two tools or configurations are different as soon as their sources differ or as soon as the compilation options or command line arguments are different.

• Competition organizers can compete, but have to make the MD5 of their code available until the deadline for submitting first versions of tools.

Technical:

• Tools must not include pre-calculated results to any of the benchmarks and there must not be any intentional sabotage of the evaluation system.

• Tools write the solution to stdout. If the tool concludes that the specification is unrealizable, it should write “UNREALIZABLE”. If the specification is found to be realizable, the output should be “REALIZABLE”. In the synthesis categories, a “REALIZABLE” output should be followed by the solution (as an AIGER circuit, see below). No other output should be written to stdout.

Ranking:

In all categories, tools will be ranked according to the number of problems that can be solved within the time limit, with total computation time as a tie-breaker. For the synthesis tracks, we additionally require that produced solutions can be model-checked within a separate time limit. From 2022 onward, sequential and parallel configurations are bundled together in the submission phase. After the experiments for the competition are run, two rankings will be prepared: one where the user CPU time is bounded by the time limit and one where the wall-clock time is used instead.

Additionally, for the synthesis categories we will have a separate quality ranking: the size of solutions (in number of synthesized AND gates + latches) is compared to the size of reference solutions; if a tool produces a solution of size n, and the reference solution is of size r, then for this benchmark the tool receives 2 – log_10(n + 1/r + 1) points. That is, a solution of the same size as the reference solution receives 2 points, a solution that is smaller by factor 10 receives ~3 points, a solution that is bigger by factor 10 receives ~1 point (with a minimum of 0 points for 100 times or more of the size of the reference solution).

The exact choice of reference solutions is to be determined. However, in several previous editions we have used the minimal solution from the current run as reference.

Benchmark Selection:

Benchmarks that are added this year will not be made available publicly before the competition. A subset of all available benchmarks will be selected for the competition. Randomization and consultation with our advisory committee will ensure a fair selection. The exact benchmark selection scheme is to be determined.

Rules in AIGER Categories

Technical:

• All solvers must conform to the Extended AIGER Format for Synthesis for inputs.

• In the synthesis category, solutions must also be in extended AIGER format, and will be model checked with the best-performing model checkers from the single-safety track of the Hardware Model Checking Competition. Additionally, tools may output, after their solution, a winning region of the system as a witness for correctness. The winning region should be output after the solution, separated by a line containing “WINNING_REGION”. It should be given as a boolean function in AIGER format, with one input for every latch of the solution circuit (in the same order as the latches in the solution), no latches, and a single output. If a winning region is given, then we check the correctness of the winning region for the given solution, and fall back to model checking if that is not possible.

Rules in LTL Categories

Technical:

• Specifications are given in TLSF format (and its LTLf extension). For tools that don’t support TLSF directly, the organizers supply a number of translators to different existing formats in the SyFCo tool. You can download a StarExec-ready SyFCo binary from here if you wish to use it in your toolchain (it will not be installed on the competition machine so include it as part of your tool).

• Realizability is defined with respect to the semantics specified in the benchmark file. (Tools that only support the other semantics can use a translation of the specification, and then translate their solution into the right target.)

• In the synthesis categories, tools must produce outputs in AIGER format (if the specification is realizable). As a syntactical restriction, the sets of inputs and outputs of the TLSF file must be identical to the sets of inputs and outputs of the AIGER solution. Additionally, solutions are model checked with existing LTL model checkers (the precise model checker is to be determined).

Rules in HOA Categories

Technical:

• Specifications are given in extended HOA format. For tools that don’t support the format directly, you can make use of our translator into PGSolver format (it will not be installed on the competition machine so include it as part of your tool).
• In the synthesis categories, tools must produce outputs in AIGER format. The sets of inputs and outputs of the HOA file must be identical to the sets of inputs and outputs of the AIGER solution. Solutions will be model checked using a verification pipeline akin to the one used for the TLSF categories.