In temporal extensions of Answer Set Programming (ASP) based on linear-time, the behavior of dynamic systems is captured by sequences of states. While this representation reflects their relative order, it abstracts away the specific times associated with each state. However, timing constraints are important in many applications like, for instance, when planning and scheduling go hand in hand. We address this by developing a metric extension of linear-time temporal equilibrium logic, in which temporal operators are constrained by intervals over natural numbers. The resulting Metric Equilibrium Logic provides the foundation of an ASP-based approach for specifying qualitative and quantitative dynamic constraints. To this end, we define a translation of metric formulas into monadic first-order formulas and give a correspondence between their models in Metric Equilibrium Logic and Monadic Quantified Equilibrium Logic, respectively. Interestingly, our translation provides a blue print for implementation in terms of ASP modulo difference constraints.

翻译：在基于线性时间的回答集编程（ASP）时间扩展中，动态系统的行为通过状态序列来刻画。虽然这种表示反映了状态间的相对次序，但抽象掉了每个状态对应的具体时间。然而在许多应用中，例如当规划与调度需协同展开时，时序约束至关重要。为此，我们开发了线性时间均衡逻辑的度量扩展，其中时间算子受自然数区间的约束。由此产生的度量均衡逻辑为基于ASP的定性与定量动态约束规范提供了理论基础。我们定义了将度量公式转换为单子一阶公式的翻译方法，并分别建立了其在度量均衡逻辑与单子量化均衡逻辑中模型间的对应关系。值得注意的是，该翻译方案为基于差分约束的ASP实现提供了蓝图。