The results of the 2025 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 (realizability & synthesis), and finite-word LTL. Then, we give more details about running times and scores as well as some graphs. Finally, we link to the participants of the competition.

The data used comes from the TGCC jobs. All data, scripts, benchmarks, and (binaries of the) tools are archived and will be made available soon. Congratulations to the winners and thanks to all the participants!

The winners

Parity game realizability

• Realizability: Knor

LTL realizability

• Realizability: ltlsynt

LTL synthesis

• Synthesis time: ltlsynt
• Synthesis quality: semml

LTLf realizability

• Realizability: ltlfsynt

Parity game Realizability

Solver	SOLVED	WALLCLOCK TIME	CPU time	MEMORY
knor_npp	429	6126	6063	63642
knor_tl	429	505	466	65872
knor_tlq (DISQUALIFIED)	429	6362	6298	67459
ltlsynt	359	55625	55375	12733

LTL Realizability

SOLVER	SOLVED	WALLCLOCK TIME	CPU TIME	MEMORY
sdf	897	54965.88	77963.8	130538
semml_real	1318	130507.16	169790.13	4196118
ltlsynt-real-acd	1328	71128.38	70476.148	551247
ltlsynt-real-lar	1330	96028.58	95261.66	731324
ltlsynt-real-ds	1225	148534	147510.032	796639
acacia (DISQUALIFIED)	1156	143432.74	405899.895	924200

LTL Synthesis

SOLVER	SOLVED	WALLCLOCK TIME	CPU TIME	MEMORY	MEAN QUALITY SCORE
ltlsynt-acd	1297	99166.52	98194.135	570252	1.46065726224849
ltlsynt-lar	1296	122680.21	121552.643	659468	1.44114796838032
ltlsynt-ds	1187	151797.75	150610.886	667925	1.58878496479921
semml_small	1293	153231.04	204678.48	4410877	1.91733469356956
semml_fast	1295	162855.38	217312.52	4252316	1.43764597172091
sdf	877	68625.23	94958.965	140973	1.33605459519285
sdf-abc	873	62592.85	90679.445	147208	1.58398914443439

LTLf Realizability

SOLVER	SOLVED	WALLCLOCK TIME	CPU TIME	MEMORY
ltlfsynt-bfs-os	402	21777.78	21630.707	121595
ltlfsynt-bfs	392	21677.56	21528.201	124140
ltlfsynt-dfs-os	401	18443.58	18312.239	105114
Cosy-m1 (DISQUALIFIED)	357	20287.27	20166.786	264615
Cosy-m2 (DISQUALIFIED)	356	11322.28	11181.704	156241
LydiaSynt	308	23019.55	22842.952	83175

Benchmarks and Solvers

The set of benchmarks used in 2025 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(S) to cite
ltl(f)synt	GitLab repo	GPL-3.0+	Paper on ltlsynt, CIAA paper for ltlfsynt
Acacia bonsai	GitHub repo	GPL-3.0	Paper
Knor	GitHub repo	GPL-3.0	Paper
sdf	GitHub repo	MIT	arXiv report
LydiaSyft	GitHub repo	AGPL v3.0	Paper
SemML	GitLab repo	GPL v3.0	Paper
Cosy	TBA	TBA	Contact author