Multi-Property Synthesis
This addresses the challenge of efficient synthesis in formal verification for scenarios with conflicting properties, though it is incremental as it builds on existing synthesis frameworks.
The paper tackles the problem of LTLf synthesis with multiple properties when satisfying all is impossible, by computing realizable goal sets in a single fixed-point computation and synthesizing strategies for maximal sets. The result is a fully symbolic algorithm that achieves speedups of up to two orders of magnitude compared to enumeration-based methods.
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.