在输入不可靠时，确保主目标与备用目标至少一个达成。
LTLf Synthesis Under Unreliable Input
- 用自动机直接处理不可靠输入变量，复杂度2EXPTIME。
- 通过信念构造忽略不可靠输入，复杂度3EXPTIME。
- 基于二阶LTLf的MSO编码表现最好，适合形式化验证者。
我们研究在某些输入变量不可靠的情况下，实现满足LTLf目标规范的策略，同时确保至少满足一个LTLf备份规范。本文形式化定义了该问题，并证明其最坏情况复杂度为2EXPTIME，与标准LTLf合成相同。提出了三种求解方法：基于直接自动机操作的方法（2EXPTIME）、通过信念构造忽略不可靠输入的方法（3EXPTIME），以及利用二阶量化LTLf（QLTLf）的方法（2EXPTIME），后者可直接编码为一阶二阶逻辑（MSO），但最坏情况为非初等。证明了三者的正确性，并进行了实证比较。有趣的是，理论复杂度未反映实际性能：MSO方法最优，其次为信念构造，最后是直接自动机方法。作为副产品，本文还提供了任意QLTLf规范的一般合成程序。
原文摘要 · Abstract (English)
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.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。