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.

翻译：我们研究了具有多个属性的LTLf综合问题，其中同时满足所有属性可能无法实现。我们不是通过枚举属性子集，而是在一次不动点计算中计算产品博弈状态与从这些状态可实现的目标准则集合之间的关系，并综合实现最大可达成集合的策略。我们开发了一种完全符号化的算法，该算法引入布尔目标变量并利用单调性来紧凑地表示指数级数量的目标组合。我们的方法显著优于基于枚举的基线方法，加速比最高可达两个数量级。