SemML: Enhancing Automata-Theoretic LTL Synthesis with Machine
Learning

D 2025

SemML: Enhancing Automata-Theoretic LTL Synthesis with Machine Learning

KŘETÍNSKÝ, Jan; Tobias MEGGENDORFER; Maximilian PROKOP a Ashkan ZARKAH

Základní údaje

Originální název

SemML: Enhancing Automata-Theoretic LTL Synthesis with Machine Learning

Autoři

KŘETÍNSKÝ, Jan; Tobias MEGGENDORFER; Maximilian PROKOP a Ashkan ZARKAH

Vydání

Cham, Tools and Algorithms for the Construction and Analysis of Systems. TACAS 2025. od s. 233-253, 21 s. 2025

Nakladatel

Springer

Další údaje

Jazyk

angličtina

Typ výsledku

Stať ve sborníku

Obor

10201 Computer sciences, information science, bioinformatics

Utajení

není předmětem státního či obchodního tajemství

Forma vydání

tištěná verze "print"

Odkazy

URL

Impakt faktor

Impact factor: 0.402 v roce 2005

Označené pro přenos do RIV

Ano

Kód RIV

RIV/00216224:14330/25:00142478

Organizační jednotka

Fakulta informatiky

ISBN

978-3-031-90642-8

ISSN

DOI

https://doi.org/10.1007/978-3-031-90643-5_12

EID Scopus

2-s2.0-105004789970

Klíčová slova anglicky

LTL; synthesis; formal methods; artificial intelligence

Štítky

core_A, firank_A

Změněno: 9. 4. 2026 07:37, RNDr. Pavel Šmerk, Ph.D.

Anotace

V originále

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) Sem antic labelling, additional information of logical nature, coming from recent LTL-to-automata translations and decorating the resulting parity game, and (ii) M achine-L earning 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.

Návaznosti

MUNI/A/1600/2024, interní kód MU

Název: Modelování, analýza a verifikace (2025)

Investor: Masarykova univerzita, Modelování, analýza a verifikace (2025)

MUNI/I/1757/2021, interní kód MU

Název: MUNI Award in Science and Humanities (Akronym: Křetínský)

Investor: Masarykova univerzita, MUNI Award in Science and Humanities, MASH - MUNI Award in Science and Humanities

Citovat

KŘETÍNSKÝ, Jan; Tobias MEGGENDORFER; Maximilian PROKOP a Ashkan ZARKAH. SemML: Enhancing Automata-Theoretic LTL Synthesis with Machine Learning. In Tools and Algorithms for the Construction and Analysis of Systems. TACAS 2025. Cham: Springer, 2025, s. 233-253. ISBN 978-3-031-90642-8. Dostupné z: https://doi.org/10.1007/978-3-031-90643-5_12.

@inproceedings{2530802,
   author = {Křetínský, Jan and Meggendorfer, Tobias and Prokop, Maximilian and Zarkah, Ashkan},
   address = {Cham},
   booktitle = {Tools and Algorithms for the Construction and Analysis of Systems. TACAS 2025.},
   doi = {https://doi.org/10.1007/978-3-031-90643-5_12},
   keywords = {LTL; synthesis; formal methods; artificial intelligence},
   howpublished = {tištěná verze "print"},
   language = {eng},
   location = {Cham},
   isbn = {978-3-031-90642-8},
   pages = {233-253},
   publisher = {Springer},
   title = {SemML: Enhancing Automata-Theoretic LTL Synthesis with Machine Learning},
   url = {https://link.springer.com/chapter/10.1007/978-3-031-90643-5_12},
   year = {2025}
}

TY  - CONF
ID  - 2530802
AU  - Křetínský, Jan - Meggendorfer, Tobias - Prokop, Maximilian - Zarkah, Ashkan
PY  - 2025
TI  - SemML: Enhancing Automata-Theoretic LTL Synthesis with Machine Learning
PB  - Springer
CY  - Cham
SN  - 9783031906428
KW  - LTL
KW  - synthesis
KW  - formal methods
KW  - artificial intelligence
UR  - https://link.springer.com/chapter/10.1007/978-3-031-90643-5_12
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) Sem antic labelling, additional information of logical nature, coming from recent LTL-to-automata translations and decorating the resulting parity game, and (ii) M achine-L earning 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.
ER  -

KŘETÍNSKÝ, Jan; Tobias MEGGENDORFER; Maximilian PROKOP a Ashkan ZARKAH. SemML: Enhancing Automata-Theoretic LTL Synthesis with Machine Learning. In \textit{Tools and Algorithms for the Construction and Analysis of Systems. TACAS 2025.}. Cham: Springer, 2025, s.~233-253. ISBN~978-3-031-90642-8. Dostupné z: https://doi.org/10.1007/978-3-031-90643-5\_{}12.

Přehled o publikaci