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

Abstract Metric temporal equilibrium logic (MEL MEL MEL) extends temporal equilibrium logic (TEL TEL TEL) by incorporating quantitative timing constraints, enabling the specification and analysis of deadlines and durations. MEL MEL 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.