On-the-fly LTLf Synthesis under Partial Observability
For researchers in formal methods and reactive synthesis, this work provides a more efficient algorithm for LTLf synthesis under partial observability, reducing unnecessary state space exploration.
The paper tackles LTLf synthesis under partial observability, proposing an on-the-fly approach that incrementally builds belief-state DFAs via observable progression. Experimental results show significant performance improvements over existing methods.
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.