Multi-Property Synthesis

TL;DR

This paper introduces a symbolic fixed-point algorithm for multi-property LTLf synthesis that efficiently computes strategies to achieve maximal realizable goal sets, significantly outperforming enumeration methods.

Contribution

The paper presents a novel symbolic approach using Boolean goal variables for multi-property LTLf synthesis, enabling scalable synthesis of strategies for multiple properties.

Findings

Achieves up to 100x speedup over baseline methods

Handles exponentially many goal combinations efficiently

Outperforms enumeration-based approaches significantly

Abstract

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.