On-the-fly LTLf Synthesis under Partial Observability

TL;DR

This paper introduces an on-the-fly method for LTLf synthesis under partial observability that incrementally constructs belief-state automata, improving efficiency and enabling practical on-the-fly game solving.

Contribution

It presents a novel incremental belief-state construction approach based on observable progression, enhancing existing synthesis methods under partial observability.

Findings

Significantly outperforms existing methods in experiments.

Enables fully on-the-fly synthesis with belief-state automata.

Leverages Multi-Terminal Binary Decision Diagrams for compactness.

Abstract

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.