Reducing Arbitrary Metric Temporal Formulas into Logic Programs under Answer Set Semantics

问题
度量时序均衡逻辑（Metric Temporal Equilibrium Logic, MEL）通过引入定量时间约束，扩展了时序均衡逻辑（Temporal Equilibrium Logic, TEL），从而能够对嵌入式和信息物理系统等动态系统中的截止日期（deadlines）和持续时间（durations）进行规范。虽然 MEL 允许进行精确的表达，例如“一个事件必须在 5 毫秒内发生”，但现有的实现面临着挑战。以往将 MEL 归约为命题回答集程序（Answer Set Programming, ASP）的方法（例如 Becker 等人的方法）往往会导致逻辑程序中包含纯未来原子（pure future atoms）出现在规则头部，从而产生未来依赖（future dependencies）。这些依赖阻碍了增量式和多轮（multi-shot）求解器的效率，因为这类求解器在当前状态的推导仅依赖于先前计算出的状态信息，而非未计算的未来状态时表现最佳。此外，现有的翻译方法未能充分处理二元度量时序算子，如度量直到（metric until）或度量释放（metric release）。

方法论
作者提出了一种 Tseitin 式的翻译方法，将任意度量时序公式映射为特定片段的度量时序逻辑程序。其核心方法论包括：

1. 限制为严格轨迹（Strict Traces）： 该方法假设严格轨迹，即时间点严格递增（$\tau(i) < \tau(i+1)$）。这使得具有区间 $[0..n]$ 的二元度量算子可以通过等价关系进行递归展开，当区间为 $[0..0]$ 时，将算子折叠为其右侧参数或真值常数。
2. 闭包定义： 受动态逻辑中 Fisher-Ladner 闭包的启发，作者为公式 $\phi$ 定义了一个闭包集 $cl(\phi)$。该集合不仅包含子公式，还包括二元度量算子的递归展开（例如，$\phi U_{\le n} \psi$ 会生成 $\bigcirc^i(\phi U_{\le n-i} \psi)$）。
3. 三值语义： 为了证明翻译的正确性，论文利用了度量此处与那里（Metric Here-and-There, MHT）逻辑的三值特征化。这种语义与 MHT 等价，简化了归约所需的逻辑等价性的验证。
4. 翻译规则： 翻译为闭包中的每个公式引入了辅助原子（标签）。它生成的规则使得未来算子仅影响蕴含关系，而这些蕴含关系的体部（bodies）和头部（heads）仅包含过去和现在的引用。翻译区分了动态规则（涉及 next/previous 算子）以及初始/最终规则。
5. 良基序（Well-Founded Order）： 为了处理闭包的非结构性特征（即展开后的公式并非原有的真子公式），作者基于算子的展开定义了一个复杂度度量 $u(\phi)$，建立了一个良基严格偏序，以支持归纳证明。

核心贡献

• Tseitin 式归约： 将任意度量时序公式正式归约为受限于规则体中仅包含过去算子的度量时序逻辑程序。
• 处理二元算子： 该翻译显式处理了形式为 $[0..n]$ 区间的二元度量算子（$U_{\le n}, R_{\le n}, S_{\le n}, T_{\le n}$），这是以往命题 ASP 编码的一个局限。
• 消除未来依赖： 通过确保规则体仅依赖于过去和现在的信息，生成的逻辑程序能够兼容 telingo 等求解器中使用的增量式求解技术。
• 形式正确性： 论文证明了该翻译保留了度量均衡模型（相对于辅助原子的强等价性），并确立了生成的程序相对于输入公式大小和最大区间值 $n$ 的多项式规模界限。

结果
论文表明，对于任何度量时序公式 $\phi$，都存在一个度量时序逻辑程序 $\Gamma$，使得 $\phi$ 的度量均衡模型与 $\Gamma$ 的度量均衡模型在原始字母表上的投影完全对应。生成的程序大小由公式大小和最大区间值 $n$ 的多项式函数所界定。在严格轨迹和 $[0..n]$ 区间的假设下，该翻译被证明是正确的。

意义
论文声称提供了一种在回答集语义下解释度量时序理论的“标准型”。通过将度量时序公式与受限于过去算子的逻辑程序联系起来，这项工作使得利用现有的、高效的 ASP 求解器（特别是支持多轮和增量式求解的求解器）来推理度量时序约束成为可能。这促进了 MEL 在需要精确计时的领域（如实时软件和嵌入式系统）中的实际应用，而不会产生与未来依赖相关的低效问题。作者指出，虽然目前的工作局限于 $[0..n]$ 区间，但它为将这些归约扩展到任意区间并集成到 telingo 求解器中奠定了基础。