Multi-Property Synthesis
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.
Similar Papers
LTLf Adaptive Synthesis for Multi-Tier Goals in Nondeterministic Domains
Artificial Intelligence
Helps robots achieve harder goals by adapting.
A Compositional Framework for On-the-Fly LTLf Synthesis
Artificial Intelligence
Makes computer programs follow complex rules better.
A Compositional Framework for On-the-Fly LTLf Synthesis
Artificial Intelligence
Helps computers make better decisions from rules.