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.
Knor
Strix
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.
Strix
ltlsynt
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.
Strix
ltlsynt
Acacia bonsai
sdf
SPORE
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_sb
best
826
211030
86632
SPORE
ltl-real-recpar-bdd-seq
519
67800
67830
SPORE
ltl-real-recpar-fbdd-32-nodecomp-seq
715
71950
71960
SPORE
ltl-real-recpar-fbdd-32-seq
646
69159
69183
SPORE
ltl-real-recpar-fbdd-64-nodecomp-seq
715
72367
72309
SPORE
ltl-real-recpar-fbdd-64-seq
646
68257
68305
Strix
ltl_real_acd_bfs
892
43963
43974
Strix
ltl_real_zlk_bfs
893
39510
39518
Strix
ltl_real_zlk_pq
924
46340
46294
Otus
otus-ltl-realizability-parallel-sylvan
588
227382
57363
Otus
otus-ltl-realizability-sequential-jbdd
558
32009
32011
sdf
real
783
50466
40399
sdf
real_p
734
129252
72772
ltlsynt
segrealacd
831
67066
67064
ltlsynt
segrealds
800
55803
55810
ltlsynt
segreallar
828
57983
57956
LTL: synthesis
To summarize, the time-based ranking of the participating tools is as follows.
Strix
sdf
ltlsynt
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)
Strix
ltl_synth_acd_bfs
820
30218
30195
Strix
ltl_synth_zlk_bfs
818
23009
23012
Strix
ltl_synth_zlk_pq
845
29458
29380
Otus
otus-ltl-synthesis-parallel-sylvan
503
125103
31644
Otus
otus-ltl-synthesis-sequential-jbdd
490
27739
27705
ltlsynt
segsyntacdabc
709
50445
504463
ltlsynt
segsyntdsabc
689
46082
46196
ltlsynt
segsyntlarabc
703
49251
49337
sdf
synt
721
47772
37822
sdf
synt_p
666
112532
61328
For the quality ranking, ltlsynt and sdf swap places.
Strix
ltlsynt
sdf
Otus
More details regarding each solver
configuration is given in the table below.
Solver
Configuration
Synthesized controllers
Score
Strix
ltl_synth_acd_bfs
433
785
Strix
ltl_synth_zlk_bfs
432
780
Strix
ltl_synth_zlk_pq
430
772
Otus
otus-ltl-synthesis-parallel-sylvan
305
243
Otus
otus-ltl-synthesis-sequential-jbdd
298
238
ltlsynt
segsyntacdabc
375
500
ltlsynt
segsyntdsabc
377
540
ltlsynt
segsyntlarabc
371
487
sdf
synt
382
447
sdf
synt_p
354
400
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.
We are preparing for the annual reactive synthesis competition. This year SYNTCOMP will be part of the FLoC’22 olympic games. The competition will run in time for the results to be presented during CAV 2022 and SYNT 2022.
The competition will run on StarExec, as in 2020 and 2021. If you plan on submitting a benchmark or solver, please go to https://www.starexec.org/, create a user, and contact us (jacobs@cispa.saarland, guillermoalberto.perez@uantwerpen.be) to be added to the SYNTCOMP space. There are main tracks for – safety specifications in AIGER format, – LTL specifications in TLSF, and – parity games in Hanoi Omega-Automata (HOA) format, each separated into subtracks for realizability checking and synthesis. Tools will be evaluated with respect to the number of solved benchmarks, and with respect to the size of their solutions.
* Call for Benchmarks *
We are looking for new synthesis benchmarks to include into SYNTCOMP, in AIGER, TLSF, and HOA. New benchmarks can be included in this year’s SYNTCOMP if they are correctly uploaded (as an issue) to the SYNTCOMP benchmark repository into StarExec by July 1. Contact us (see above) if you have any questions regarding scope or format of benchmarks.
* Call for Solvers *
Solvers for all tracks of the competition will be accepted until July 1. Because of our move to StarExec, you will be allowed to update your solver as many times as needed. Your solver will be included in this year’s SYNTCOMP if it is correctly uploaded (i.e. passes a test run) into StarExec by July 1.
