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.

翻译：本文研究在特定输入变量不可靠的情况下，为实现LTLf目标规约而制定策略，同时确保至少满足LTLf备份规约的问题。我们形式化定义了该问题，并证明其最坏情况复杂度与标准LTLf综合问题相同，均为2EXPTIME完全。随后我们提出了三种不同的求解技术：第一种基于直接自动机操作（2EXPTIME复杂度）；第二种通过信念构造忽略不可靠输入变量（3EXPTIME复杂度）；第三种利用二阶量化LTLf（QLTLf）进行建模（2EXPTIME复杂度），该方法可直接编码为最坏情况下非初等复杂度的单调二阶逻辑。我们证明了这些技术的正确性，并通过实验对它们进行了比较评估。有趣的是，理论上的最坏情况复杂度界限并未直接反映在实际性能中：MSO技术表现最佳，信念构造次之，直接自动机操作最差。作为本研究的副产品，我们为任意QLTLf规约提供了一种通用的综合求解流程。