SemML: Enhancing Automata-Theoretic LTL Synthesis with Machine Learning
The result's identifiers
Result code in IS VaVaI
<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F00216224%3A14330%2F25%3A00142460" target="_blank" >RIV/00216224:14330/25:00142460 - isvavai.cz</a>
Result on the web
<a href="http://dx.doi.org/10.1007/978-3-031-90643-5_12" target="_blank" >http://dx.doi.org/10.1007/978-3-031-90643-5_12</a>
DOI - Digital Object Identifier
<a href="http://dx.doi.org/10.1007/978-3-031-90643-5_12" target="_blank" >10.1007/978-3-031-90643-5_12</a>
Alternative languages
Result language
angličtina
Original language name
SemML: Enhancing Automata-Theoretic LTL Synthesis with Machine Learning
Original language description
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.
Czech name
—
Czech description
—
Classification
Type
D - Article in proceedings
CEP classification
—
OECD FORD branch
10201 - Computer sciences, information science, bioinformathics (hardware development to be 2.2, social aspect to be 5.8)
Result continuities
Project
—
Continuities
S - Specificky vyzkum na vysokych skolach
Others
Publication year
2025
Confidentiality
S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů
Data specific for result type
Article name in the collection
Tools and Algorithms for the Construction and Analysis of Systems. TACAS 2025.
ISBN
9783031906428
ISSN
0302-9743
e-ISSN
—
Number of pages
21
Pages from-to
233-253
Publisher name
Springer
Place of publication
Cham
Event location
Hamilton, Canada
Event date
May 3, 2025
Type of event by nationality
WRD - Celosvětová akce
UT code for WoS article
—