Score: 0

Multi-Property Synthesis

Published: January 15, 2026 | arXiv ID: 2601.10651v1

By: Christoph Weinhuber , Yannik Schnitzer , Alessandro Abate and more

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.

Category
Computer Science:
Artificial Intelligence