# SemML 2.0: Synthesizing Controllers for LTL

arXiv: https://arxiv.org/abs/2604.24102 · HTML: https://mlsanity.com/paper/2604.24102/

## Key facts

- Cited by 1 papers in the map (data through 14 Oct 2026).
- Builds on 11 of its 36 references that are in the map.
- First posted on arXiv 27 Apr 2026.

## Builds on (most cited first, 11 of 11)

- [Boolean Abstractions for Realizability Modulo Theories (Extended version)](https://mlsanity.com/paper/2310.17292/) (2023)
- [The Reactive Synthesis Competition (SYNTCOMP): 2018-2021](https://mlsanity.com/paper/2206.00251/) (2022)
- [SemML: Enhancing Automata-Theoretic LTL Synthesis with Machine Learning](https://mlsanity.com/paper/2501.17496/) (2025)
- [Practical Synthesis of Reactive Systems from LTL Specifications via Parity Games](https://mlsanity.com/paper/1903.12576/) (2019)
- [Semantic Labelling and Learning for Parity Game Solving in LTL Synthesis](https://mlsanity.com/paper/1907.12157/) (2019)
- [A High-Level LTL Synthesis Format: TLSF v1.1](https://mlsanity.com/paper/1604.02284/) (2016)
- [From LTL and Limit-Deterministic B"uchi Automata to Deterministic Parity Automata](https://mlsanity.com/paper/1701.06103/) (2017)
- [An Efficient Normalisation Procedure for Linear Temporal Logic and Very Weak Alternating Automata](https://mlsanity.com/paper/2005.00472/) (2020)
- [Full LTL Synthesis over Infinite-state Arenas](https://mlsanity.com/paper/2307.09776/) (2023)
- [NeuroSynt: A Neuro-symbolic Portfolio Solver for Reactive Synthesis](https://mlsanity.com/paper/2401.12131/) (2024)
- [Symbolic Solution of Emerson-Lei Games for Reactive Synthesis](https://mlsanity.com/paper/2305.02793/) (2023)

## Built on by (most cited first, 1 of 1)

- [Infinite Trace Objectives with Finite Trace Techniques: Translating LTL to LTLf+](https://mlsanity.com/paper/2608.02454/) (2026)

## Abstract (arXiv)

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.