Monthly Archives: July 2022

SYNTCOMP 2022 Results

The results of the 2022 competition on Reactive Synthesis are in! As in previous years, the competition was run on StarExec. This year, the competition consisted of LTL tracks, with specifications in TLSF, and parity-game tracks, with specifications given in extended HOA. It is worth mentioning that we have removed the separation between so-called parallel and sequential tracks in favor of having two rankings based on total Wallclock time vs. total CPU time used by solvers. This year, though, the rankings happen to coincide. For more information on this and other updates to the competition, you can take a look at the most recent report about the competition.

Rankings

We present first the results for the parity-game tracks and then move to the LTL tracks.

Parity games: realizability

To summarize, the ranking of the participating tools is as follows.
  1. Knor
  2. Strix
  3. ltlsynt
More details regarding each solver configuration is given in the table below and the cactus plots that follow (where only the best configuration per tool is shown). The raw information can be fetched from the StarExec job.
Solver Configuration Solved benchmarks Total CPU time (s) Total Wallclock time (s)
Strix hoa_realizability_parallel 548 308532 124160
Strix hoa_realizability_sequential 515 89584 89232
ltlsynt pgreal 441 69416 69421
Knor real_ltl 587 1722 1039

Parity games: synthesis

To summarize, the time-based ranking of the participating tools is the same as for the realizability sub-track. More details regarding each solver configuration is given in the table below and the cactus plots that follow (where only the best configuration per tool is shown). The raw information can be fetched from the StarExec job.
Solver Configuration Solved benchmarks Total CPU time (s) Total Wallclock time (s)
Strix hoa_synthesis_parallel 470 159456 73077
Strix hoa_synthesis_sequential 451 48321 47884
ltlsynt pgsynt 334 69254 69250
ltlsynt pgsyntabc1 335 69386 69440
Knor synt_sym 278 4839 4839
Knor synt_sym_abc 278 5706 5401
Knor synt_tl 480 1695 994
The quality ranking is quite different.
  1. Strix
  2. ltlsynt
  3. Knor
More details regarding each solver configuration is given in the table below.
Solver Configuration Synthesized controllers Score
Strix hoa_synthesis_parallel 199 385
Strix hoa_synthesis_sequential 199 384
ltlsynt pgsynt 204 321
ltlsynt pgsyntabc1 205 358
Knor synt_sym 197 292
Knor synt_sym_abc 197 340
Knor synt_tl 201 268

LTL: realizability

To summarize, the ranking of the participating tools is as follows.
  1. Strix
  2. ltlsynt
  3. Acacia bonsai
  4. sdf
  5. SPORE
  6. Otus
More details regarding each solver configuration is given in the table below and the cactus plots that follow (where only the best configuration per tool is shown). The raw information can be fetched from the StarExec job.
Solver Configuration Solved benchmarks Total CPU time (s) Total Wallclock time (s)
_acab_sbbest826211030 86632
SPOREltl-real-recpar-bdd-seq51967800 67830
SPOREltl-real-recpar-fbdd-32-nodecomp-seq71571950 71960
SPOREltl-real-recpar-fbdd-32-seq64669159 69183
SPOREltl-real-recpar-fbdd-64-nodecomp-seq71572367 72309
SPOREltl-real-recpar-fbdd-64-seq64668257 68305
Strixltl_real_acd_bfs89243963 43974
Strixltl_real_zlk_bfs89339510 39518
Strixltl_real_zlk_pq92446340 46294
Otusotus-ltl-realizability-parallel-sylvan588227382 57363
Otusotus-ltl-realizability-sequential-jbdd55832009 32011
sdfreal78350466 40399
sdfreal_p734129252 72772
ltlsyntsegrealacd83167066 67064
ltlsyntsegrealds80055803 55810
ltlsyntsegreallar82857983 57956

LTL: synthesis

To summarize, the time-based ranking of the participating tools is as follows.
  1. Strix
  2. sdf
  3. ltlsynt
  4. Otus
More details regarding each solver configuration is given in the table below and the cactus plots that follow (where only the best configuration per tool is shown). The raw information can be fetched from the StarExec job.
Solver Configuration Solved benchmarks Total CPU time (s) Total Wallclock time (s)
Strixltl_synth_acd_bfs8203021830195
Strixltl_synth_zlk_bfs8182300923012
Strixltl_synth_zlk_pq8452945829380
Otusotus-ltl-synthesis-parallel-sylvan50312510331644
Otusotus-ltl-synthesis-sequential-jbdd4902773927705
ltlsyntsegsyntacdabc70950445504463
ltlsyntsegsyntdsabc6894608246196
ltlsyntsegsyntlarabc7034925149337
sdfsynt7214777237822
sdfsynt_p66611253261328
For the quality ranking, ltlsynt and sdf swap places.
  1. Strix
  2. ltlsynt
  3. sdf
  4. Otus
More details regarding each solver configuration is given in the table below.
Solver Configuration Synthesized controllers Score
Strixltl_synth_acd_bfs 433785
Strixltl_synth_zlk_bfs 432780
Strixltl_synth_zlk_pq 430772
Otusotus-ltl-synthesis-parallel-sylvan 305243
Otusotus-ltl-synthesis-sequential-jbdd 298238
ltlsyntsegsyntacdabc 375500
ltlsyntsegsyntdsabc 377540
ltlsyntsegsyntlarabc 371487
sdfsynt 382447
sdfsynt_p 354400

Benchmarks and Solvers

The set of benchmarks used in 2022 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.
Solver StarExec link Source repo License Report to cite
Acacia bonsai GitHub repo GPL-3.0 arXiv report
KnorGitHub repoGPL-3.0arXiv report
sdfGitHub repoMITarXiv report