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.
@article{arxiv.2601.10651,
title = {Multi-Property Synthesis},
author = {Christoph Weinhuber and Yannik Schnitzer and Alessandro Abate and David Parker and Giuseppe De Giacomo and Moshe Y. Vardi},
journal= {arXiv preprint arXiv:2601.10651},
year = {2026}
}