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综合非常高效的紧凑表示。实验结果表明，我们的方法显著优于现有方法，并进一步凸显了将在线博弈求解与信念状态构造相结合的实际优势。