Knor, a synthesis tool for parity automata developed at the FMT group, has won the parity-game synthesis track of SYNTCOMP 2021. Knor was the fastest solver, solving most benchmarks (276 of 303) within the time limit. Knor also won the "hard-parity-game" track by solving 216 out of 217 benchmarks within the time limit. This is due to effective use of binary decision diagrams and of symbolic parity game algorithms that have been developed at the UT by Tom van Dijk in collaboration with Oebele Lijzenga and Bob Rubbens.
Ongoing research focuses on improving the size of the generated controllers, a category that was won by the competitor Strix. Smaller controllers are considered better, so we are looking at various methods to improve here, such as clever BDD variable orderings, different methods to translate from a BDD to an And-Inverter-Graph, and methods to reduce the number of states and the state encoding.
Tom van Dijk is supported by the European Union’s Horizon 2020 research and innovation programme under the Marie Sklodowska-Curie grant agreement No 893732.
