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. In many applications, however, timing constraints are important like, for instance, when planning and scheduling go hand in hand. We address this by developing a metric extension of linear-time Dynamic Equilibrium Logic, in which dynamic operators are constrained by intervals over integers. The resulting Metric Dynamic Equilibrium Logic provides the foundation of an ASP-based approach for specifying qualitative and quantitative dynamic constraints. As such, it constitutes the most general among a whole spectrum of temporal extensions of Equilibrium Logic. In detail, we show that it encompasses Temporal, Dynamic, Metric, and regular Equilibrium Logic, as well as its classic counterparts once the law of the excluded middle is added.
翻译:在基于线性时间的回答集编程(ASP)时间扩展中,动态系统的行为通过状态序列进行刻画。尽管这种表示反映了状态的相对顺序,但并未体现与每个状态相关联的具体时间。然而在许多应用中,时间约束至关重要——例如当规划与调度需要协同进行时。为此,我们通过开发线性时间动态均衡逻辑的度量扩展来解决这一问题,其中动态算子受限于整数区间。所提出的度量动态均衡逻辑为基于ASP的定性与定量动态约束规范提供了基础,从而构成均衡逻辑时间扩展谱系中最通用的框架。具体而言,我们证明该框架涵盖了时间均衡逻辑、动态均衡逻辑、度量均衡逻辑、经典均衡逻辑,以及在加入排中律后对应的经典逻辑变体。