# Guessing Winning Policies in LTL Synthesis by Semantic Learning

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

## Key facts

- Cited by 4 papers in the map (data through 14 Oct 2026).
- Builds on 12 of its 51 references that are in the map.
- First posted on arXiv 24 May 2023.

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

- [Neural Circuit Synthesis from Specification Patterns](https://mlsanity.com/paper/2107.11864/) (2021)
- [Iterative Circuit Repair Against Formal Specifications](https://mlsanity.com/paper/2303.01158/) (2023)
- [The Reactive Synthesis Competition (SYNTCOMP): 2018-2021](https://mlsanity.com/paper/2206.00251/) (2022)
- [The Unary Fragments of Metric Interval Temporal Logic: Bounded versus Lower bound Constraints (Full Version)](https://mlsanity.com/paper/1305.3204/) (2013)
- [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)
- [From LTL and Limit-Deterministic B"uchi Automata to Deterministic Parity Automata](https://mlsanity.com/paper/1701.06103/) (2017)
- [Oink: an Implementation and Evaluation of Modern Parity Game Solvers](https://mlsanity.com/paper/1801.03859/) (2018)
- [Efficient Parallel Strategy Improvement for Parity Games](https://mlsanity.com/paper/1705.02313/) (2017)
- [One Theorem to Rule Them All: A Unified Translation of LTL into ω-Automata](https://mlsanity.com/paper/1805.00748/) (2018)
- [An Ordered Approach to Solving Parity Games in Quasi Polynomial Time and Quasi Linear Space](https://mlsanity.com/paper/1703.01296/) (2017)
- [A Recursive Approach to Solving Parity Games in Quasipolynomial Time](https://mlsanity.com/paper/2104.09717/) (2021)

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

- [SemML: Enhancing Automata-Theoretic LTL Synthesis with Machine Learning](https://mlsanity.com/paper/2501.17496/) (2025)
- [NeuroSynt: A Neuro-symbolic Portfolio Solver for Reactive Synthesis](https://mlsanity.com/paper/2401.12131/) (2024)
- [Semantically Labelled Automata for Multi-Task Reinforcement Learning with LTL Instructions](https://mlsanity.com/paper/2602.06746/) (2026)
- [dtControl2+varepsilon: Trading Optimality for Explainability in MDPs via Decision Trees](https://mlsanity.com/paper/2607.25925/) (2026)

## Abstract (arXiv)

We provide a learning-based technique for guessing a winning strategy in a parity game originating from an LTL synthesis problem. A cheaply obtained guess can be useful in several applications. Not only can the guessed strategy be applied as best-effort in cases where the game's huge size prohibits rigorous approaches, but it can also increase the scalability of rigorous LTL synthesis in several ways. Firstly, checking whether a guessed strategy is winning is easier than constructing one. Secondly, even if the guess is wrong in some places, it can be fixed by strategy iteration faster than constructing one from scratch. Thirdly, the guess can be used in on-the-fly approaches to prioritize exploration in the most fruitful directions. In contrast to previous works, we (i)~reflect the highly structured logical information in game's states, the so-called semantic labelling, coming from the recent LTL-to-automata translations, and (ii)~learn to reflect it properly by learning from previously solved games, bringing the solving process closer to human-like reasoning.