Metric temporal equilibrium logic (\MEL) extends temporal equilibrium logic (\TEL) by incorporating quantitative timing constraints, enabling the specification and analysis of deadlines and durations. \MEL\ is particularly suited for domains where time-bound properties are crucial, such as embedded systems, cyber-physical systems, and real-time software. It facilitates the precise expression of timing behaviors, such as the requirement that an event must occur within 5 milliseconds of a trigger, which often elude traditional qualitative temporal logics. In this paper, we present a Tseitin-like translation that maps any metric temporal formula into a logic programming fragment restricted to past operators. This translation provides a formal bridge to leverage existing Answer Set Programming (ASP) solvers for reasoning about metric temporal constraints. By restricting the target fragment to past operators, we enable more effective evaluation and integration with current ASP-based toolchains for multi-shot solving.

翻译：摘要：度量时序均衡逻辑(\MEL)通过引入定量时序约束扩展了时序均衡逻辑(\TEL)，从而支持对截止期限和持续时间的规约与分析。\MEL\特别适用于时间约束至关重要的领域，例如嵌入式系统、信息物理系统和实时软件。它能够精确描述诸如"事件必须在触发后5毫秒内发生"等时序行为，而传统定性时序逻辑往往难以捕捉这类需求。本文提出一种类似Tseitin变换的翻译方法，可将任意度量时序公式转化为仅含过去算子的逻辑程序片段。该翻译为利用现有回答集编程(ASP)求解器处理度量时序约束建立了形式化桥梁。通过将目标片段限定为过去算子，我们能够实现更高效的评估，并促进与基于ASP的多轮求解工具链的集成。