Author Archives: Guillermo Perez

SYNTCOMP 2020 Results

The results of SYNTCOMP 2020 have been presented at the SYNT workshop, part of CAV 2020. The slides used for the SYNT presentation can be found here. The experiments can now be browsed on StarExec here (see the subspaces corresponding to each track).

This year, the competition was split into a safety track, based on specifications in AIGER format an LTL track, with specifications in TLSF, and a parity-game track, with specifications in an extended HOA format. Just like last year, for the safety track we have only considered the realizability-checking task. Furthermore, we have only ran the sequential mode of the resulting three categories. For the LTL track and the synthesis task we have an additional ranking based on not only the quantity, but also the quality of solutions.

Here are the tools that had the best results in these categories:

simpleBDDSolver (solved 186 out of 274 problems in the AIGER/safety Realizability Track)

Strix (solved 424 out of 434 problems in the TLSF/LTL Realizability track and won the quality ranking in the TLSF/LTL Synthesis Track)

Strix (solved all problems in the EHOA/parity game Realizability track and was the only participant in the synthesis track)

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

New Track for SYNTCOMP 2020

Dear synthesis enthusiasts, for the next edition of the Reactive Synthesis competition (SYNTCOMP 2020) we will have a new track which is meant to further distinguish the strengths of LTL/TLSF synthesis tools. The new track will have as input deterministic parity automata, an intermediate representation for most LTL-synthesis pipelines.

The new input format is an extension of the Hanoi Omega-Automata (HOA) format. There exist Java and C++ parsers (see the website) for the original format and the extension is such that those parsers should work for it. Furthermore, for PGSolver-format fanatics we provide a translator from the new format to PGSolver format. The output format will remain AIGER, as explained in the arXiv document describing the input/output formats.

We encourage you to start preparing benchmarks and tools for this new track as soon as possible and to try them out in our StarExec community. If you have questions or comments regarding the input/output formats, do not hesitate to contact us.

SYNTCOMP 2019 Results

The results of SYNTCOMP 2019 have been presented at the SYNT workshop and at CAV 2019. The slides used for the SYNT presentation can be found here. The experiments can now be browsed on StarExec here (see the subspaces corresponding to each track).

Like in the previous years, the competition was split into a safety track, based on specifications in AIGER format, and an LTL track, with specifications in TLSF. This year exceptionally, for the safety track we have only considered the realizability-checking task. Furthermore, we have only ran the sequential mode of the resulting three categories. For the LTL track and the synthesis task we have an additional ranking based on not only the quantity, but also the quality of solutions.

Here are the tools that had the best results in these categories:

AbsSynthe (solved 192 out of 274 problems in the AIGER/safety Realizability Track, sequential mode)

Strix (solved the most problems in all TLSF/LTL tracks and modes, and won the quality ranking in the TLSF/LTL Synthesis Track, with 717 points in sequential mode)

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