# Multi-Property Synthesis

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

## Key facts

- No citing papers in the map yet (data through 14 Oct 2026).
- Builds on 3 of its 30 references that are in the map.
- First posted on arXiv 15 Jan 2026.

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

- [Symbolic LTLf Synthesis](https://mlsanity.com/paper/1705.08426/) (2017)
- [Maximum Realizability for Linear Temporal Logic Specifications](https://mlsanity.com/paper/1804.00415/) (2018)
- [Good-for-MDP State Reduction for Stochastic LTL Planning](https://mlsanity.com/paper/2511.09073/) (2025)

## Abstract (arXiv)

We study LTLf synthesis with multiple properties, where satisfying all properties may be impossible. Instead of enumerating subsets of properties, we compute in one fixed-point computation the relation between product-game states and the goal sets that are realizable from them, and we synthesize strategies achieving maximal realizable sets. We develop a fully symbolic algorithm that introduces Boolean goal variables and exploits monotonicity to represent exponentially many goal combinations compactly. Our approach substantially outperforms enumeration-based baselines, with speedups of up to two orders of magnitude.