SemML 2.0: Synthesizing Controllers for LTL

TL;DR

SemML 2.0 is an advanced tool for synthesizing reactive systems from LTL specifications, outperforming existing solutions in efficiency and success rate through novel heuristics and machine learning guidance.

Contribution

The paper introduces SemML 2.0, which combines automata-theoretic methods, partial exploration, machine learning, and heuristics to improve LTL synthesis performance.

Findings

Solves more synthesis instances than competitors.

Operates significantly faster while maintaining solution quality.

Outperforms previous SemML and other state-of-the-art tools.

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. These systems are typically represented using either Mealy machines or AIGER circuits. We present the second version of SemML, which outperforms all state-of-the-art tools for finding either solution. Aside from implementing the classical automata-theoretic approach, our tool utilizes partial exploration and machine-learning guidance for obtaining solutions efficiently, and numerous heuristics and improvements of classic algorithms for extracting small representations of these solutions. We evaluate our tool against the existing state-of-the-art tools (in particular Strix, LtlSynt, and the previous version of SemML) on the dataset of the synthesis competition SYNTCOMP. We show that we solve significantly more instances and do so much faster than other tools, while maintaining state-of-the-art solution quality.