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.