Standard
SemML: Enhancing Automata-Theoretic LTL Synthesis with Machine Learning. / Křetínský, Jan
; Meggendorfer, Tobias; Prokop, Maximilian et al.
Tools and Algorithms for the Construction and Analysis of Systems - 31st International Conference, TACAS 2025, Held as Part of the International Joint Conferences on Theory and Practice of Software, ETAPS 2025, Proceedings. ed. / Arie Gurfinkel; Marijn Heule. Cham: Springer, 2025. p. 233-253 (Lecture Notes in Computer Science; Vol. 15696 LNCS).
Research output: Contribution in Book/Report/Proceedings - With ISBN/ISSN › Conference contribution/Paper › peer-review
Harvard
Křetínský, J
, Meggendorfer, T, Prokop, M & Zarkhah, A 2025,
SemML: Enhancing Automata-Theoretic LTL Synthesis with Machine Learning. in A Gurfinkel & M Heule (eds),
Tools and Algorithms for the Construction and Analysis of Systems - 31st International Conference, TACAS 2025, Held as Part of the International Joint Conferences on Theory and Practice of Software, ETAPS 2025, Proceedings. Lecture Notes in Computer Science, vol. 15696 LNCS, Springer, Cham, pp. 233-253, 31st International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2025, which was held as part of the International Joint Conferences on Theory and Practice of Software, ETAPS 2025, Hamilton, Canada,
3/05/25.
https://doi.org/10.1007/978-3-031-90643-5_12APA
Křetínský, J.
, Meggendorfer, T., Prokop, M., & Zarkhah, A. (2025).
SemML: Enhancing Automata-Theoretic LTL Synthesis with Machine Learning. In A. Gurfinkel, & M. Heule (Eds.),
Tools and Algorithms for the Construction and Analysis of Systems - 31st International Conference, TACAS 2025, Held as Part of the International Joint Conferences on Theory and Practice of Software, ETAPS 2025, Proceedings (pp. 233-253). (Lecture Notes in Computer Science; Vol. 15696 LNCS). Springer.
https://doi.org/10.1007/978-3-031-90643-5_12Vancouver
Křetínský J
, Meggendorfer T, Prokop M, Zarkhah A.
SemML: Enhancing Automata-Theoretic LTL Synthesis with Machine Learning. In Gurfinkel A, Heule M, editors, Tools and Algorithms for the Construction and Analysis of Systems - 31st International Conference, TACAS 2025, Held as Part of the International Joint Conferences on Theory and Practice of Software, ETAPS 2025, Proceedings. Cham: Springer. 2025. p. 233-253. (Lecture Notes in Computer Science). doi: 10.1007/978-3-031-90643-5_12
Author
Křetínský, Jan
; Meggendorfer, Tobias ; Prokop, Maximilian et al. /
SemML : Enhancing Automata-Theoretic LTL Synthesis with Machine Learning. Tools and Algorithms for the Construction and Analysis of Systems - 31st International Conference, TACAS 2025, Held as Part of the International Joint Conferences on Theory and Practice of Software, ETAPS 2025, Proceedings. editor / Arie Gurfinkel ; Marijn Heule. Cham : Springer, 2025. pp. 233-253 (Lecture Notes in Computer Science).
Bibtex
@inproceedings{8f98d2f8526044e0b6bea732a736f98b,
title = "SemML: Enhancing Automata-Theoretic LTL Synthesis with Machine Learning",
abstract = "Synthesizing a reactive system from specifications given in linear temporal logic (LTL) is a classical problem, finding its applications in safety-critical systems design. We present our tool SemML, which won this year{\textquoteright}s LTL realizability tracks of SYNTCOMP, after years of domination by Strix. While both tools are based on the automata-theoretic approach, ours relies heavily on (i) Semantic labelling, additional information of logical nature, coming from recent LTL-to-automata translations and decorating the resulting parity game, and (ii) Machine-Learning approaches turning this information into a guidance oracle for on-the-fly exploration of the parity game (whence the name SemML). Our tool fills the missing gaps of previous suggestions to use such an oracle and provides an efficient implementation with additional algorithmic improvements. We evaluate SemML both on the entire set of SYNTCOMP as well as a synthetic data set, compare it to Strix, and analyze the advantages and limitations. As SemML solves more instances on SYNTCOMP and does so significantly faster on larger instances, this demonstrates for the first time that machine-learning-aided approaches can out-perform state-of-the-art tools in real LTL synthesis.",
author = "Jan K{\v r}et{\'i}nsk{\'y} and Tobias Meggendorfer and Maximilian Prokop and Ashkan Zarkhah",
note = "Publisher Copyright: {\textcopyright} The Author(s) 2025.; 31st International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2025, which was held as part of the International Joint Conferences on Theory and Practice of Software, ETAPS 2025 ; Conference date: 03-05-2025 Through 08-05-2025",
year = "2025",
month = may,
day = "1",
doi = "10.1007/978-3-031-90643-5_12",
language = "English",
isbn = "9783031906428",
series = "Lecture Notes in Computer Science",
publisher = "Springer",
pages = "233--253",
editor = "Arie Gurfinkel and Marijn Heule",
booktitle = "Tools and Algorithms for the Construction and Analysis of Systems - 31st International Conference, TACAS 2025, Held as Part of the International Joint Conferences on Theory and Practice of Software, ETAPS 2025, Proceedings",
}
RIS
TY - GEN
T1 - SemML
T2 - 31st International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2025, which was held as part of the International Joint Conferences on Theory and Practice of Software, ETAPS 2025
AU - Křetínský, Jan
AU - Meggendorfer, Tobias
AU - Prokop, Maximilian
AU - Zarkhah, Ashkan
N1 - Publisher Copyright:
© The Author(s) 2025.
PY - 2025/5/1
Y1 - 2025/5/1
N2 - Synthesizing a reactive system from specifications given in linear temporal logic (LTL) is a classical problem, finding its applications in safety-critical systems design. We present our tool SemML, which won this year’s LTL realizability tracks of SYNTCOMP, after years of domination by Strix. While both tools are based on the automata-theoretic approach, ours relies heavily on (i) Semantic labelling, additional information of logical nature, coming from recent LTL-to-automata translations and decorating the resulting parity game, and (ii) Machine-Learning approaches turning this information into a guidance oracle for on-the-fly exploration of the parity game (whence the name SemML). Our tool fills the missing gaps of previous suggestions to use such an oracle and provides an efficient implementation with additional algorithmic improvements. We evaluate SemML both on the entire set of SYNTCOMP as well as a synthetic data set, compare it to Strix, and analyze the advantages and limitations. As SemML solves more instances on SYNTCOMP and does so significantly faster on larger instances, this demonstrates for the first time that machine-learning-aided approaches can out-perform state-of-the-art tools in real LTL synthesis.
AB - Synthesizing a reactive system from specifications given in linear temporal logic (LTL) is a classical problem, finding its applications in safety-critical systems design. We present our tool SemML, which won this year’s LTL realizability tracks of SYNTCOMP, after years of domination by Strix. While both tools are based on the automata-theoretic approach, ours relies heavily on (i) Semantic labelling, additional information of logical nature, coming from recent LTL-to-automata translations and decorating the resulting parity game, and (ii) Machine-Learning approaches turning this information into a guidance oracle for on-the-fly exploration of the parity game (whence the name SemML). Our tool fills the missing gaps of previous suggestions to use such an oracle and provides an efficient implementation with additional algorithmic improvements. We evaluate SemML both on the entire set of SYNTCOMP as well as a synthetic data set, compare it to Strix, and analyze the advantages and limitations. As SemML solves more instances on SYNTCOMP and does so significantly faster on larger instances, this demonstrates for the first time that machine-learning-aided approaches can out-perform state-of-the-art tools in real LTL synthesis.
U2 - 10.1007/978-3-031-90643-5_12
DO - 10.1007/978-3-031-90643-5_12
M3 - Conference contribution/Paper
AN - SCOPUS:105004789970
SN - 9783031906428
T3 - Lecture Notes in Computer Science
SP - 233
EP - 253
BT - Tools and Algorithms for the Construction and Analysis of Systems - 31st International Conference, TACAS 2025, Held as Part of the International Joint Conferences on Theory and Practice of Software, ETAPS 2025, Proceedings
A2 - Gurfinkel, Arie
A2 - Heule, Marijn
PB - Springer
CY - Cham
Y2 - 3 May 2025 through 8 May 2025
ER -
