Reducing Arbitrary Metric Temporal Formulas into Logic Programs under Answer Set Semantics
This work provides a formal bridge for researchers and practitioners in embedded systems and cyber-physical systems to leverage existing ASP solvers for precise reasoning about time-bound properties, addressing a limitation of traditional qualitative temporal logics.
This paper introduces a Tseitin-like translation to convert arbitrary metric temporal formulas into a logic programming fragment using only past operators. This allows the use of existing Answer Set Programming (ASP) solvers to reason about quantitative timing constraints, which are crucial for domains like embedded and cyber-physical systems.
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.