Reducing Arbitrary Metric Temporal Formulas into Logic Programs under Answer Set Semantics
Fuente:
arXiv
Salvato in:
| Autori principali: | , , , |
|---|---|
| Natura: | Preprint |
| Pubblicazione: |
2026
|
| Soggetti: | |
| Accesso online: | |
| Tags: |
Aggiungi Tag
Nessun Tag, puoi essere il primo ad aggiungerne!!
|
| _version_ | 1866918531051814912 |
|---|---|
| author | Diéguez, Martín Hahn, Susana Schaub, Torsten Stéphan, Igor |
| author_facet | Diéguez, Martín Hahn, Susana Schaub, Torsten Stéphan, Igor |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2605_30618 |
| institution | arXiv |
| publishDate | 2026 |
| record_format | arxiv |
| spellingShingle | Reducing Arbitrary Metric Temporal Formulas into Logic Programs under Answer Set Semantics Diéguez, Martín Hahn, Susana Schaub, Torsten Stéphan, Igor Logic in Computer Science 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. |
| title | Reducing Arbitrary Metric Temporal Formulas into Logic Programs under Answer Set Semantics |
| topic | Logic in Computer Science |
| url | https://arxiv.org/abs/2605.30618 |