LTLf synthesis under partial observability requires reasoning about unobservable environment variables, which is typically handled by constructing a belief-state DFA via subset construction that universally quantifies these variables. Existing approaches perform this construction as a separate step prior to game solving, often generating belief states that are unnecessary in practice. We propose an on-the-fly approach to LTLf synthesis under partial observability based on observable progression. Our method incrementally builds the belief-state DFA by progressing the specification with respect to observable variables only, universally quantifying unobservable variables on the fly. We prove the correctness of the construction and show that it naturally enables on-the-fly game solving, leading to a fully on-the-fly synthesis framework. Our implementation leverages DFAs represented using Multi-Terminal Binary Decision Diagrams: a compact representation that has proven highly effective for LTLf synthesis under full observability. Experimental results demonstrate that our approach significantly outperforms existing methods and further highlight the practical benefits of integrating on-the-fly game solving with belief-state construction.

翻译：部分可观测条件下的LTLf综合需要推理不可观测的环境变量，通常通过子集构造构建信念状态确定有限自动机（DFA）并对这些变量进行全称量化来处理。现有方法将这一构造作为博弈求解前的独立步骤执行，常会生成实际中不必要的信念状态。我们提出一种基于可观测演进的在线方法，用于求解部分可观测条件下的LTLf综合。该方法仅依据可观测变量对规范进行演进，在线对不可观测变量进行全称量化，从而增量式构建信念状态DFA。我们证明了构造的正确性，并表明其能自然实现在线博弈求解，进而形成完整的在线综合框架。我们的实现采用多终端二元决策图表示的DFA：该紧凑表示已在完全可观测条件下的LTLf综合中展现出高效性。实验结果表明，我们的方法显著优于现有方案，并进一步凸显了将在线博弈求解与信念状态构建相结合的实际优势。