SemML: Enhancing Automata-Theoretic LTL Synthesis with Machine Learning

TL;DR

SemML tackles LTL synthesis by embedding semantic labelling into an ML-guided, on-the-fly parity-game exploration pipeline. By ranking frontier moves with a pairwise edge classifier and leveraging synthetic training data, it overcomes limitations of previous approaches and achieves faster performance and higher solvability on SYNTCOMP, including large instances. The work demonstrates that machine-learning-guided exploration can outperform the leading automata-based tool Strix in real LTL synthesis, with practical implications for safety-critical system design. The approach combines algorithmic engineering, a Java-based implementation, and accessible data to advance scalable, real-time LTL synthesis literature.

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

Figures (6)

• Figure 1: An example of a part of an automaton with semantic labelling
• Figure 2: High level architecture of SemML.
• Figure 3: Illustration of the exploration process together with an example for each step.
• Figure 4: A simple game to illustrate two challenges for the ground truth. For simplicity, all states are controlled by one player. Clearly, all states are winning.
• Figure 5: Scatter plots of the runtimes of SemML, Strix, and SemML on SYNTCOMP. A point $(x, y)$ denotes that tool X and tool Y needed $x$ and $y$ seconds, respectively. If a point is above/below the diagonal, tool X is faster/slower. Plots are on logarithmic scale, dashed diagonals indicate that one tool is twice as fast. Timeouts are pushed to the orthogonal dashed line. The axes start at 1 second.

Theorems & Definitions (2)

• remark thmcounterremark
• remark thmcounterremark