不可靠输入下的 LTLf 综合

我们研究在确保不可靠输入变量情况下，至少满足某个 LTLf 备份规范的目标 LTLf 规范实现策略的问题。我们形式化地定义了该问题并给出其最坏情况复杂度的特征，表明其为 2EXPTIME-complete，与标准 LTLf 综合相同。随后我们设计了三种不同的解决方案技术：一种基于直接自动机操作的技术，时间复杂度为 2EXPTIME；一种采用信念构造法忽略不可靠输入变量的技术，时间复杂度为 3EXPTIME；以及一种利用二阶量化 LTLf (QLTLf) 的技术，时间复杂度为 2EXPTIME，并且允许直接编码为一阶模态逻辑 (MSO)，后者的最坏情况复杂度为非可数。我们证明了这些方法的正确性，并对它们进行了彼此之间的实证评估。有趣的是，理论的最坏情况界限并不等同于观察到的实际性能；MSO 技术性能最佳，其次是信念构造和直接自动机操作。作为本研究的副产品，我们提供了一个通用的 QLTLf 规范综合程序，用于处理任意 QLTLf 规范。