Home > Research > Publications & Outputs > SemML

Links

Text available via DOI:

View graph of relations

SemML: Enhancing Automata-Theoretic LTL Synthesis with Machine Learning

Research output: Contribution in Book/Report/Proceedings - With ISBN/ISSNConference contribution/Paperpeer-review

Published
Close
Publication date1/05/2025
Host publicationTools 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
EditorsArie Gurfinkel, Marijn Heule
Place of PublicationCham
PublisherSpringer
Pages233-253
Number of pages21
ISBN (electronic)9783031906435
ISBN (print)9783031906428
<mark>Original language</mark>English
Event31st 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
Duration: 3/05/20258/05/2025

Conference

Conference31st 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
Country/TerritoryCanada
CityHamilton
Period3/05/258/05/25

Publication series

NameLecture Notes in Computer Science
Volume15696 LNCS
ISSN (Print)0302-9743
ISSN (electronic)1611-3349

Conference

Conference31st 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
Country/TerritoryCanada
CityHamilton
Period3/05/258/05/25

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’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.

Bibliographic note

Publisher Copyright: © The Author(s) 2025.