# LTLf Synthesis Under Unreliable Input

arXiv: https://arxiv.org/abs/2412.14728 · HTML: https://mlsanity.com/paper/2412.14728/

## Key facts

- No citing papers in the map yet (data through 14 Oct 2026).
- Builds on 8 of its 42 references that are in the map.
- First posted on arXiv 19 Dec 2024.

## Builds on (most cited first, 8 of 8)

- [Partially Observable Markov Decision Processes in Robotics: A Survey](https://mlsanity.com/paper/2209.10342/) (2022)
- [Symbolic LTLf Synthesis](https://mlsanity.com/paper/1705.08426/) (2017)
- [Probabilistic Motion Planning under Temporal Tasks and Soft Constraints](https://mlsanity.com/paper/1706.05209/) (2017)
- [What to Do When You Can't Do It All: Temporal Logic Planning with Soft Temporal Logic Constraints](https://mlsanity.com/paper/2008.01926/) (2020)
- [First-Order vs. Second-Order Encodings for LTLf-to-Automata Translation](https://mlsanity.com/paper/1901.06108/) (2019)
- [Unpredictable Planning Under Partial Observability](https://mlsanity.com/paper/1903.07665/) (2019)
- [LTLf Synthesis under Partial Observability: From Theory to Practice](https://mlsanity.com/paper/2009.10875/) (2020)
- [The Trembling-Hand Problem for LTLf Planning](https://mlsanity.com/paper/2404.16163/) (2024)

## Abstract (arXiv)

We study the problem of realizing strategies for an LTLf goal specification while ensuring that at least an LTLf 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 LTLf 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 3EXPTIME, and one leveraging second-order quantified LTLf (QLTLf), 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 QLTLf specifications.