一次性解决多个无法全满足的逻辑约束，自动找出最优妥协方案。
Multi-Property Synthesis
- 用符号化方法统一计算所有属性组合的可实现性
- 一次固定点计算即可得出状态与可达成目标集的关系
- 适合需要权衡多个目标的自动化系统设计
我们研究在多个性质共存下的LTLf合成问题，当所有性质无法同时满足时，传统方法需枚举所有子集，效率低下。本文提出一种完全符号化的算法，引入布尔目标变量并利用单调性，以紧凑方式表示指数级多的目标组合。通过一次固定点计算，得到每个产品博弈状态能实现的目标集合，并合成达到最大可实现目标集的策略。该方法显著优于基于枚举的基线，速度提升最高达两个数量级。
原文摘要 · Abstract (English)
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.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。