LTLf Synthesis Under Unreliable Input

We study the problem of realizing strategies for an ltl f goal specification while ensuring that at least an ltl f backup specification is satisfied in case of unreliability of certain input variables. We formally define the problem and characterize its worst-case complexity as 2EXPTIME-complete, like standard ltl f synthesis. Then we devise three different solution techniques: one based on direct automata manipulation, which is 2EXPTIME, one disregarding unreliable input variables by adopting a belief construction, which is 3EX-PTIME, and one leveraging second-order quantified ltl f (qltl f ), which is 2EXPTIME and allows for a direct encoding into monadic second-order logic, which in turn is worst-case nonelementary. We prove their correctness and evaluate them against each other empirically. Interestingly, theoretical worst-case bounds do not translate into observed performance; the MSO technique performs best, followed by belief construction and direct automata manipulation. As a byproduct of our study, we provide a general synthesis procedure for arbitrary qltl f specifications. Code - https://github.com/whitemech/ltlf-synth- unrel-input-aaai2025 * This is the extended preprint of the conference paper with the same title presented at AAAI 2025. It includes proof sketches of the main theorems in the text, with full proofs in Appendix A. Additionally, the examples used are described in more detail in Appendices B to D.