Monthly Archives: June 2024

SYNTCOMP 2024 Results

The results of the 2024 edition of SYNTCOMP are in. First, we give a list of the winners for each one of the realizability tracks ran this year: Parity games, LTL, and finite-word LTL. Then, we give more details about running times and scores as well as some graphs (showing only the best configuration per tool, i.e. the one that solved the most benchmarks). Finally, we link to the participants of the competition.

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

SolverConfigurationSolved (seq/par)CPU time (s)Wallclock time (s)
Knorreal_rtl458/458421.28421.96
ltlsyntpgreal378/37810441.4810442.41

LTL Realizability

SolverConfigurationSolved (seq/par)CPU time (s)Wallclock time (s)
SemMLsemml_real972/96732740.5624985.99
Acacia bonsaireal768/78831902.3935682.57
A.bonsai (k-d trees)real734/75027733.0730132.75
ltlsyntsegrealacd944/93627596.3927286.30
ltlsyntsegrealds899/89127256.0326623.95
ltlsyntsegreallar941/93328680.5728347.82
sdfreal840/83830893.4631067.37
sdfreal_vg_hors_concours839/83829815.8131876.83

LTLf Realizability

SolverConfigurationSolved (seq/par)CPU time (s)Wallclock time (s)
LydiaSyftdefault.sh220/2206882.876887.78
LydiaSyftprint_strategy_in_file.sh220/2206888.986893.82
Nikebdd_ff230/2303972.703943.48
Nikebdd_random181/18118472.6918464.63
Nikebdd_tt225/2255319.705283.62
Nikedefault234/2345326.305326.69
Nikehash_random137/13712187.8312167.53
Nikehash_tt231/2316464.696462.08
lisaseqreal1.sh209/2095649.485645.42
lisaseqreal2.sh192/1928297.108295.19
lisaseqreal3.sh190/1907642.337646.71
ltlfsyntsegltlfrealbase77/7722988.6022990.84
ltlfsyntsegltlfrealopt77/7722951.0022952.93
ltlfsyntsegltlfsyntbase78/7824793.5624795.99
ltlfsyntsegltlfsyntopt77/7723028.2923030.55
topledefault131/1319375.099339.21

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.

SolverSource repoLicenseReport to cite
ltlsyntGitLab repoGPL-3.0+Paper
Acacia bonsaiGitHub repoGPL-3.0Paper
KnorGitHub repoGPL-3.0Paper
sdfGitHub repoMITarXiv report
NikeGitHub repoAGPL v3.0arXiv report
LydiaSyftGitHub repoAGPL v3.0report
LisaGitHub repoGPL v3.0arXiv report
topleCustom: all rights reservedContact authors
SemMLGitLab repoGPL v3.0Contact author