The results of the 2023 edition of SYNTCOMP are in. First, we give a list of the winners for each one of the 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.
All graphs and tables were obtained as described here. 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 games
- Sequential realizability: Knor
- Parallel realizability: Knor
- Sequential synthesis: ltlsynt
- Parallel synthesis: Knor
- Sequential synthesis (quality): Strix
- Parallel synthesis (quality): Strix
LTL
- Sequential realizability: Strix
- Parallel realizability: Strix
- Sequential synthesis: Strix
- Parallel synthesis: Strix
- Sequential synthesis (quality): Strix
- Parallel synthesis (quality): Strix
LTLf
- Sequential realizability: Nike
- Parallel realizability: Nike
Parity game Realizability
| Solver | Configuration | Solved (seq/par) | CPU time (s) | Wallclock time (s) |
|---|---|---|---|---|
| Knor repair | real_tl | 876/876 | 1035.45 | 648.11 |
| Strix PGAME | hoa_realizability_parallel | 800/835 | 61377.20 | 65541.26 |
| Strix PGAME | hoa_realizability_sequential | 802/802 | 50668.25 | 49536.76 |
| ltlsynt | pgreal | 733/733 | 39810.50 | 39811.10 |
Parity game Synthesis
| Solver | Config | Solved (seq/par) | CPU time (s) | Wallclock (s) | Score (seq/par) |
|---|---|---|---|---|---|
| Knor repair | synt_sym | 282/282 | 3257.02 | 3257.45 | 439.37/439.37 |
| Knor repair | synt_sym_abc | 283/283 | 3846.52 | 3568.78 | 489.49/489.49 |
| Knor repair | synt_tl | 272/272 | 9.66 | 9.25 | 289.48/289.48 |
| Strix PGAME | hoa_synthesis_parallel | 285/285 | 4596.27 | 4359.80 | 554.48/554.48 |
| Strix PGAME | hoa_synthesis_sequential | 284/284 | 4562.27 | 4350.23 | 552.65/552.65 |
| ltlsynt | pgsynt | 292/292 | 1687.63 | 1672.48 | 464.30/464.30 |
| ltlsynt | pgsyntabc1 | 294/294 | 1718.05 | 1720.58 | 504.33/504.33 |
LTL Realizability
| Solver | Configuration | Solved (seq/par) | CPU time (s) | Wallclock time (s) |
|---|---|---|---|---|
| SPORE | ltl-real-recpar-bdd-seq | 479/479 | 30222.87 | 30201.10 |
| SPORE | ltl-real-recpar-fbdd-32-nodecomp-seq | 666/666 | 35025.32 | 34928.26 |
| SPORE | ltl-real-recpar-fbdd-32-seq | 588/588 | 31316.82 | 31223.80 |
| SPORE | ltl-real-recpar-fbdd-64-nodecomp-seq | 660/660 | 30986.12 | 30956.60 |
| SPORE | ltl-real-recpar-fbdd-64-seq | 600/600 | 33176.62 | 33168.87 |
| Strix | ltl_real_acd_bfs | 914/914 | 31507.38 | 31516.81 |
| Strix | ltl_real_zlk_bfs | 921/921 | 34268.65 | 34271.52 |
| Strix | ltl_real_zlk_pq | 948/948 | 35447.26 | 35409.72 |
| abonsai | real | 703/716 | 26947.08 | 26005.19 |
| ltlsynt23 | segrealacd | 845/845 | 39379.60 | 39370.62 |
| ltlsynt23 | segrealds | 809/809 | 32401.23 | 32353.34 |
| ltlsynt23 | segreallar | 845/845 | 35477.35 | 35460.15 |
| sdf | real | 782/786 | 23287.54 | 24888.38 |
| sdf | real_p | 709/723 | 36894.35 | 39242.12 |
LTL Synthesis
| Solver | Config | Solved (seq/par) | CPU time (s) | Wallclock (s) | Score (seq/par) |
|---|---|---|---|---|---|
| Otus | otus-ltl-synthesis-parallel-sylvan | 330/332 | 7791.82 | 3340.19 | 264.98/266.96 |
| Otus | otus-ltl-synthesis-sequential-jbdd | 327/327 | 2248.72 | 2235.18 | 265.37/265.37 |
| Strix | ltl_synth_acd_bfs | 472/472 | 11715.48 | 11701.96 | 863.33/863.33 |
| Strix | ltl_synth_zlk_bfs | 490/490 | 15849.71 | 15805.41 | 895.74/895.74 |
| Strix | ltl_synth_zlk_pq | 488/488 | 12977.18 | 12917.15 | 888.37/888.37 |
| abonsai | synt | 382/385 | 11886.38 | 7609.35 | 573.52/578.05 |
| ltlsynt23 | segsyntacdabc | 416/416 | 9392.32 | 9395.10 | 573.13/573.13 |
| ltlsynt23 | segsyntdsabc | 412/412 | 5319.05 | 5313.80 | 614.11/614.11 |
| ltlsynt23 | segsyntlarabc | 413/413 | 9472.05 | 9456.58 | 559.24/559.24 |
| sdf | synt | 415/417 | 4007.84 | 5611.84 | 493.06/496.44 |
| sdf | synt_p | 381/383 | 12838.66 | 11905.57 | 431.96/435.34 |
LTLf Realizability
| Solver | Configuration | Solved (seq/par) | CPU time (s) | Wallclock time (s) |
|---|---|---|---|---|
| LydiaSyft | default.sh | 255/255 | 3885.47 | 3890.82 |
| LydiaSyft | print_strategy_in_file.sh | 255/255 | 3964.93 | 3969.52 |
| Nike | bdd_ff | 264/264 | 4621.82 | 4617.48 |
| Nike | bdd_random | 235/235 | 40752.96 | 40766.24 |
| Nike | bdd_tt | 260/260 | 5832.94 | 5820.82 |
| Nike | default | 269/269 | 6383.23 | 6364.09 |
| Nike | hash_random | 177/177 | 30639.28 | 30647.51 |
| Nike | hash_tt | 266/266 | 9680.75 | 9678.20 |
| lisa-syntcomp | seqreal1.sh | 225/225 | 7078.87 | 7081.29 |
| lisa-syntcomp | seqreal2.sh | 206/206 | 9674.94 | 9664.04 |
| lisa-syntcomp | seqreal3.sh | 205/205 | 9147.83 | 9152.23 |
| ltlfsynt23prebuild | segltlfrealbase | 85/85 | 18451.05 | 18453.08 |
| ltlfsynt23prebuild | segltlfrealopt | 85/85 | 18422.37 | 18415.12 |
| ltlfsynt23prebuild | segltlfsyntbase | 85/85 | 18555.46 | 18540.76 |
| ltlfsynt23prebuild | segltlfsyntopt | 85/85 | 18503.75 | 18505.74 |
| tople | default | 147/147 | 15514.12 | 15523.45 |
Benchmarks and Solvers
The set of benchmarks used in 2023 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 | Source repo | License | Report to cite |
|---|---|---|---|
| ltlsynt | GitLab repo | GPL-3.0+ | |
| Acacia bonsai | GitHub repo | GPL-3.0 | Paper |
| Knor | GitHub repo | GPL-3.0 | arXiv report |
| sdf | GitHub repo | MIT | arXiv report |
| Nike | GitHub repo | AGPL v3.0 | arXiv report |
| LydiaSyft | GitHub repo | AGPL v3.0 | report |
| Lisa | GitHub repo | GPL v3.0 | arXiv report |
| tople | Custom: all rights reserved | Contact authors |