Metric Temporal Equilibrium Logic over Timed Traces

Abstract

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 (MEL) 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 MEL and Monadic Quantified Equilibrium Logic, respectively. Interestingly, our translation provides a blue print for implementation in terms of ASP modulo difference constraints.

1 Introduction

Reasoning about actions and change, or more generally about dynamic systems, is not only central to knowledge representation and reasoning but at the heart of Computer Science (Fisher et al. 2005). In practice, this kind of reasoning often requires both qualitative as well as quantitative dynamic constraints. For instance, when planning and scheduling at once, actions may have durations and their effects may need to meet deadlines. On the other hand, any flexible formalism for actions and change must incorporate some form of non-monotonic reasoning to deal with inertia and other types of defaults.

Over the last years, we addressed qualitative dynamic constraints by combining traditional approaches, like Dynamic and Linear Temporal Logic (DL (Harel et al. 2000) and LTL (Pnueli 1977)), with the base logic of answer set programming (ASP (Lifschitz 1999)), namely, the logic of Here-and-There (HT (Heyting 1930)) and its non-monotonic extension, called Equilibrium Logic (Pearce 1997). This resulted in non-monotonic linear dynamic and temporal equilibrium logics (DEL (Bosser et al. 2018; Cabalar et al. 2019) and ${\mathrm{TEL}}$ (Aguado et al. 2013; Cabalar et al. 2018; Aguado et al. 2023)) that gave rise to the temporal ASP system telingo (Cabalar et al 2020). 2019; extending the ASP system clingo (Gebser et al. 2016).

A commonality of such dynamic and temporal logics is that they abstract from specific time points when capturing temporal relationships. For instance, in temporal logic, we can use the formula ${{\square}} ( \mathit{use} \to {{\Diamond}} \mathit{clean})$ to express that a machine has to be eventually cleaned after being used. Nothing can be said about the delay between using and cleaning the machine.

A key design decision was to base both aforementioned logics, ${\mathrm{TEL}}$ and DEL, on the same linear-time semantics. We continued to maintain the same linear-time semantics, embodied by sequences of states, when elaborating upon a first “light-weight” metric temporal extension of HT (Cabalar et al. 2020). The “light-weightiness” is due to treating time as a state counter by identifying the next time with the next state. For instance, this allows us to refine our example by stating that, if the machine is used, it has to be cleaned within the next 3 states, viz. $(use \to { \Diamond _{[1..3]}}clean)$ . Although this permits the restriction of temporal operators to subsequences of states, no fine-grained timing constraints are expressible. In other words, it is as if state transitions were identified with time clicks, and the two things could not be dissociated.

In this paper, we overcome this limitation by dealing with timed traces where each state has an associated time, as done in Metric Temporal Logic ( ${{\mathrm{MTL}}}$ (Koymans 1990)). This allows us to measure time differences between events. For instance, in our example, we may thus express that whenever the machine is used, it has to be cleaned within 60 to 120 time units, by writing:

\begin{align*} \square (use \to {\rm{ }}{ \Diamond _{[60..120]}}clean).\end{align*}

Unlike the non-metric version, this stipulates that once $\mathit{use}$ is true in a state, $\mathit{clean}$ must be true in some future state whose associated time is at least 60 and at most 120 time units after the time of $\mathit{use}$ . The choice of time domain is crucial and might even lead to undecidability in the continuous case. We rather adapt a discrete approach that offers a sequence of snapshots of a dynamic system.

The definition of the new variant of Metric (Temporal) Equilibrium Logic ( ${{\mathrm{MEL}}}$ for short) is done in two steps. We start with the definition of a monotonic logic called Metric (Temporal) logic of Here-and-There ( ${\mathrm{MHT}}$ ), a temporal extension of the intermediate logic of Here-and-There, mentioned above. We then select some models from ${\mathrm{MHT}}$ that are said to be in equilibrium, obtaining in this way a non-monotonic entailment relation.

The rest of the paper is organized as follows. In the next section, we start describing the monotonic basis, ${\mathrm{MHT}}$ , that generalizes (Cabalar et al. 2020) by adding timed traces, and provide some basic properties and useful equivalences in this logic. In Section 3, we study the non-monotonic formalism, ${{\mathrm{MEL}}}$ , providing the definition of metric equilibrium models as a kind of minimal ${\mathrm{MHT}}$ models. We also illustrate this definition with an example and discuss the property of strong equivalence for metric theories, proving that it coincides with equivalence in the monotonic logic, ${\mathrm{MHT}}$ . Section 4 provides a translation of ${\mathrm{MHT}}$ into a fragment of first-order HT, called Quantified Here-and-There with Difference Constraints, following a similar spirit to the well-known translation of Kamp (1968) from Linear Temporal Logic ( ${\mathrm{LTL}}$ ) to first-order logic. Finally, Section 6 contains a discussion and concludes the paper. Appendix A includes all the proofs of the results in the paper.

2 Metric logic of here-and-there

In this section, we start describing the metric extension of HT, called ${\mathrm{MHT}}$ , that is used as monotonic basis for defining Metric Equilibrium Logic (MEL) later on. We begin introducing some notation. Given $m \in \mathbb{N}$ and $n \in \mathbb{N} \cup \{\omega\}$ , we let ${{[m..n]}}$ stand for the set $\{i \in \mathbb{N} \mid m \leq i \leq n\}$ , ${{[m..n)}}$ for $\{i \in \mathbb{N} \mid m \leq i < n\}$ , and ${{(m..n]}}$ stand for $\{i \in \mathbb{N} \mid m < i \leq n\}$ . We use letters I, J to denote intervals and, since they stand for sets, we assume standard set relations like inclusion $I \subseteq J$ or membership $n \in I$ .

Given a set ${{\mathcal{A}}}$ of propositional variables (called alphabet), a metric formula $\varphi$ is defined by the grammar:

where ${{p}} \in{{\mathcal{A}}}$ is an atom and $\otimes$ is any binary Boolean connective $\otimes \in \{\to,\wedge,\vee\}$ . The last six cases above correspond to temporal operators, each of them indexed by some interval I of the form ${{[m..n)}}$ with $m\in\mathbb{N}$ and $n\in\mathbb{N}\cup\{\omega\}$ . In words, ${ \bullet _I}$ , ${{{{\mathbin{\boldsymbol{\mathsf{S}}}}}_{I}}}$ , and ${{{{\mathbin{\boldsymbol{\mathsf{T}}}}}_{I}}}$ are past operators called previous, since, and trigger, respectively; their future counterparts ${ \circ _I}$ ,

, and are called next, until, and release. Strictly speaking, we should differentiate between the syntactic representation of an interval, and its semantic counterpart, the associated set of time points it represents. For simplicity, we just use the same representation for both concepts but, as said above, we restrict the form of intervals that can be used as modal subindices to the case ${{[m..n)}}$ where n is possibly $\omega$ . Yet, some syntactic abbreviations are allowed in the temporal subindices. For instance, we let subindex ${{[m..n]}}$ stand for ${{[m..n{+}1)}}$ , provided $n\neq\omega$ . Also, we sometimes use the subindices ‘ ${\leq}n$ ’, ‘ ${\geq} m$ ’, and ‘m’ as abbreviations of intervals ${{[0..n]}}$ , ${{[m..\omega)}}$ and ${{[m..m]}}$ , respectively. Also, whenever $I={{[0..\omega)}}$ , we simply omit subindex I.

We also define several common derived operators like the Boolean connectives $\top \stackrel{\mathit{def}}{=} \neg \bot$ , $\neg \varphi \stackrel{\mathit{def}}{=} \varphi \to \bot$ , $\varphi \leftrightarrow \psi \stackrel{\mathit{def}}{=} (\varphi \to \psi) \wedge (\psi \to \varphi)$ , and the following temporal operators:

Note that initial and final are not indexed by any interval; they only depend on the state of the trace, not on the actual time associated with this state. On the other hand, the weak version of next can no longer be defined in terms of final, as done in (Cabalar et al. 2018) with non-metric . For the metric case ${\widehat{\rm{O}}_I}\varphi$ , the implication $${{\rm{O}}_I} \top \to {\rm{ }}{{\rm{O}}_I}\varphi$$ (or equivalently the disjunction ${\rm{ }}{{\rm{O}}_I}\varphi \vee \neg {\rm{ }}{{\rm{O}}_I} \top$ ) must be used instead, in order to keep the usual dualities among operators (the same applies to weak previous).

A metric theory is a (possibly infinite) set of metric formulas. As an example of a metric theory, we may consider the following scenario for modeling the behavior of traffic lights. While the light is red by default, it changes to green within less than 15 time units (say, seconds) whenever the button is pushed; and it stays green for another 30 seconds at least. This can be represented as follows.

(1) \begin{align}{\square} ( \mathit{red} \wedge \mathit{green} \to \bot), \end{align}

(2) \begin{align}{{\square}} ( \neg\mathit{green} \to \mathit{red} ), \end{align}

(3) $$\square (push \to { \Diamond _{[1..15)}}({\square _{ \le 30}}green)).$$

Note that this example combines a default rule (2) with a metric rule (3), describing the initiation and duration period of events. This nicely illustrates the interest in non-monotonic metric representation and reasoning methods.

A Here-and-There trace (for short HT-trace) of length $\lambda \in \mathbb{N} \cup \{\omega\}$ over alphabet ${{\mathcal{A}}}$ is a sequence of pairs $(\langle H_i,T_i \rangle)_{{{i \in {{[0..\lambda)}}}}}$ with $H_i\subseteq T_i\subseteq{{\mathcal{A}}}$ for any ${{i \in {{[0..\lambda)}}}}$ . For convenience, we usually represent an HT-trace as the pair $\langle {\mathbf{H}},\mathbf{T} \rangle$ of sequences ${\mathbf{H}} = (H_i)_{{{i \in {{[0..\lambda)}}}}}$ and $\mathbf{T} = (T_i)_{{{i \in {{[0..\lambda)}}}}}$ . Notice that, when $\lambda=\omega$ , this covers traces of infinite length. We say that $\langle {\mathbf{H}},\mathbf{T} \rangle$ is total whenever $\mathbf{H}=\mathbf{T}$ , that is, $H_i=T_i$ for all ${{i \in {{[0..\lambda)}}}}$ .

Definition 1

A timed HT-trace $(\langle \mathbf{H},\mathbf{T} \rangle,{{\tau}})$ of length $\lambda$ over $(\mathbb{N},<)$ and alphabet $\mathcal{A}$ is a pair consisting of

an HT-trace $\langle \mathbf{H},\mathbf{T} \rangle $ of length $\lambda$ over $\mathcal{A}$ and

a function ${{\tau}}: {{[0..\lambda)}} \to \mathbb{N}$ such that ${{\tau}}(i)\leq {{\tau}}(i{+}1)$ .

A timed HT-trace of length $\lambda > 1$ is called strict if ${{\tau}}(i)<{{\tau}}(i{+}1)$ for all $i{+}1 \in {{(0..\lambda)}}$ such that $i+1 < \lambda$ and non-strict otherwise. We assume w.l.o.g. that ${{\tau}}(0)=0$ .

Function ${{\tau}}$ assigns to each state index $i \in {{[0..\lambda)}}$ a time point ${{\tau}}(i) \in \mathbb{N}$ representing the number of time units (seconds, milliseconds, etc, depending on the chosen granularity) elapsed since time point ${{\tau}}(0)=0$ , chosen as the beginning of the trace. The difference to the variant of ${\mathrm{MHT}}$ presented in (Cabalar et al. 2020) boils down to the choice of function ${{\tau}}$ . Essentially, the latter corresponds now to the case where ${{\tau}}$ is the identity function on the interval ${{[0..\lambda)}}$ .

Given any timed HT-trace, satisfaction of formulas is defined as follows.

Definition 2 ( ${\mathrm{MHT}}$ -satisfaction)

A timed HT-trace $\mathbf{M}=(\langle \mathbf{H},\mathbf{T} \rangle, {{\tau}})$ of length $\lambda$ over alphabet ${{\mathcal{A}}}$ satisfies a metric formula $\varphi$ at step ${{k \in {{[0..\lambda)}}}}$ , written $\mathbf{M},k \models \varphi$ , if the following conditions hold:

1. $\mathbf{M},k \not\models \bot$

2. $\mathbf{M},k \models {{p}}$ if ${{p}} \in H_k$ for any atom ${{p}} \in {{\mathcal{A}}}$

3. $\mathbf{M}, k \models \varphi \wedge \psi$ iff $\mathbf{M}, k \models \varphi$ and $\mathbf{M}, k \models \psi$

4. $\mathbf{M}, k \models \varphi \vee \psi$ iff $\mathbf{M}, k \models \varphi$ or $\mathbf{M}, k \models \psi$

5. $\mathbf{M}, k \models \varphi \to \psi$ iff $\mathbf{M}', k \not \models \varphi$ or $\mathbf{M}', k \models \psi$ , for both $\mathbf{M}'=\mathbf{M}$ and $\mathbf{M}'=(\langle \mathbf{T},\mathbf{T} \rangle, {{\tau}})$

6. ${\bf{M}},k| = { \bullet _I}{\mkern 1mu} \varphi$ iff $k>0$ and $\mathbf{M}, k{-}1 \models \varphi$ and ${{\tau}}(k)-{{\tau}}(k{-}1) \in I$

7. $\mathbf{M}, k \models \varphi {{{{\mathbin{\boldsymbol{\mathsf{S}}}}}_{I}}} \psi$ iff for some ${{j \in {{[0..k]}}}}$ with ${{\tau}}(k)-{{\tau}}(j) \in I$ , we have $\mathbf{M}, j \models \psi$ and $\mathbf{M}, i \models \varphi$ for all ${{i \in {{(j..k]}}}}$

8. $\mathbf{M}, k \models \varphi {{{{\mathbin{\boldsymbol{\mathsf{T}}}}}_{I}}} \psi$ iff for all ${{j \in {{[0..k]}}}}$ with ${{\tau}}(k)-{{\tau}}(j) \in I$ , we have $\mathbf{M}, j \models \psi$ or $\mathbf{M}, i \models \varphi$ for some ${{i \in {{(j..k]}}}}$

9. ${\bf{M}},k{\rm{| = }}{{\rm{O}}_I}{\mkern 1mu} \varphi$ iff $k+1<\lambda$ and $\mathbf{M}, k{+}1 \models \varphi$ and ${{\tau}}(k{+}1)-{{\tau}}(k) \in I$

10.

iff for some ${{j \in {{[k..\lambda)}}}}$ with ${{\tau}}(j)-{{\tau}}(k) \in I$ , we have $\mathbf{M}, j \models \psi$ and $\mathbf{M}, i \models \varphi$ for all ${{i \in {{[k..j)}}}}$

11. iff for all ${{j \in {{[k..\lambda)}}}}$ with ${{\tau}}(j)-{{\tau}}(k) \in I$ , we have $\mathbf{M}, j \models \psi$ or $\mathbf{M}, i \models \varphi$ for some ${{i \in {{[k..j)}}}}$

Satisfaction of derived operators can be easily deduced:

Proposition 1

Let $\mathbf{M}=(\langle \mathbf{H},\mathbf{T} \rangle,{{\tau}})$ be a timed HT-trace of length $\lambda$ over ${{\mathcal{A}}}$ . Given the respective definitions of derived operators, we get the following satisfaction conditions:

12. $\mathbf{M}, k \models {{\boldsymbol{\mathsf{I}}}}$ iff $k =0$

13. ${\bf{M}},k| = {\widehat \bullet _I}{\mkern 1mu} \varphi$ iff $k =0$ or $\mathbf{M}, k{-}1 \models \varphi$ or ${{\tau}}(k)-{{\tau}}(k{-}1) \not\in I$

14. $\mathbf{M}, k \models {{{{\blacklozenge}}_{I}}}\, \varphi$ iff $\mathbf{M}, i \models \varphi$ for some ${{i \in {{[0..k]}}}}$ with ${{\tau}}(k)-{{\tau}}(i) \in I$

15. $\mathbf{M}, k \models {{{{\blacksquare}}_{I}}}\, \varphi$ iff $\mathbf{M}, i \models \varphi$ for all ${{i \in {{[0..k]}}}}$ with ${{\tau}}(k)-{{\tau}}(i) \in I$

16. iff $k+1 = \lambda$

17. ${\bf{M}},k| = {\widehat{\rm{O}}_I}{\mkern 1mu} \varphi$ iff $k+1 = \lambda$ or $\mathbf{M}, k{+}1 \models \varphi$ or ${{\tau}}(k{+}1)-{{\tau}}(k) \not\in I$

18. $\mathbf{M}, k \models {{{{\Diamond}}_{I}}}\, \varphi$ iff $\mathbf{M}, i \models \varphi$ for some ${{i \in {{[k..\lambda)}}}}$ with ${{\tau}}(i)-{{\tau}}(k) \in I$

19. $\mathbf{M}, k \models {{{{\square}}_{I}}}\, \varphi$ iff $\mathbf{M}, i \models \varphi$ for all ${{i \in {{[k..\lambda)}}}}$ with ${{\tau}}(i)-{{\tau}}(k) \in I$

A formula $\varphi$ is a tautology (or is valid), written $\models \varphi$ , iff $\mathbf{M},k \models \varphi$ for any timed HT-trace $\mathbf{M}$ and any $k \in {{[0..\lambda)}}$ . ${\mathrm{MHT}}$ is the logic induced by the set of all such tautologies. For two formulas $\varphi, \psi$ we write $\varphi \equiv \psi$ , iff $\models \varphi \leftrightarrow \psi$ , that is, $\mathbf{M},k \models \varphi \leftrightarrow \psi$ for any timed HT-trace $\mathbf{M}$ of length $\lambda$ and any $k \in {{[0..\lambda)}}$ . A timed HT-trace $\mathbf{M}$ is an ${\mathrm{MHT}}$ model of a metric theory $\Gamma$ if $\mathbf{M},0 \models \varphi$ for all $\varphi \in \Gamma$ . The set of ${\mathrm{MHT}}$ models of $\Gamma$ having length $\lambda$ is denoted as ${\mathrm{MHT}}(\Gamma,\lambda)$ , whereas ${{\mathrm{MHT}}}(\Gamma) \stackrel{\mathit{def}}{=} \bigcup_{\lambda=0}^\omega {{\mathrm{MHT}}}(\Gamma,\lambda)$ is the set of all ${\mathrm{MHT}}$ models of $\Gamma$ of any length. We may obtain fragments of any metric logic by imposing restrictions on the timed traces used for defining tautologies and models. That is, ${{\mathrm{MHT}_{\!f}}}$ stands for the restriction of ${\mathrm{MHT}}$ to traces of any finite length $\lambda \in \mathbb{N}$ and ${{\mathrm{MHT}_{\!\omega}}}$ corresponds to the restriction to traces of infinite length $\lambda=\omega$ .

We say that a metric theory is temporal if all its modal operators are subindex-free. Temporal formulas share the same syntax as ${\mathrm{LTL}}$ , although the absence of an interval in ${\mathrm{MHT}}$ is understood as an abbreviation for the fixed interval ${{[0..\omega)}}$ . The following result shows that, for temporal theories, ${\mathrm{MHT}}$ satisfaction collapses into Temporal Here-and-There ( ${{\mathrm{THT}}}$ ) satisfaction (Aguado et al. 2023). Hence, we can use non-timed traces and ignore function ${{\tau}}$ in this case.

Proposition 2

Let $\Gamma$ be a temporal theory. Then $(\langle \mathbf{H}, \mathbf{T} \rangle, {{\tau}}) \models \Gamma$ in ${\mathrm{MHT}}$ iff $\langle \mathbf{H}, \mathbf{T} \rangle \models \Gamma$ in ${{\mathrm{THT}}}$ .

An interesting subset of ${\mathrm{MHT}}$ is the one formed by total timed traces like $(\langle \mathbf{T}, \mathbf{T} \rangle, {{\tau}})$ . In the non-metric version of temporal HT, the restriction to total models corresponds to ${\mathrm{LTL}}$ (Pnueli 1977). In our case, the restriction to total traces defines a metric version of ${\mathrm{LTL}}$ , which we call Metric Temporal Logic (or ${{\mathrm{MTL}}}$ for short). We present next several properties about total traces and the relation between ${\mathrm{MHT}}$ and ${{\mathrm{MTL}}}$ .

Proposition 3 (Persistence)

Let $(\langle \mathbf{H},\mathbf{T} \rangle,{{\tau}})$ be a timed HT-trace of length $\lambda$ over ${{\mathcal{A}}}$ and let $\varphi$ be a metric formula over ${{\mathcal{A}}}$ . Then, for any ${{k \in {{[0..\lambda)}}}}$ , if $(\langle \mathbf{H},\mathbf{T} \rangle, {{\tau}}), k \models \varphi$ then $(\langle \mathbf{T},\mathbf{T} \rangle, {{\tau}}), k \models \varphi$ .

Thanks to Proposition 3 and a decidability result in (Ouaknine and Worrell 2007), we get:

Corollary 1 (Decidability of ${{\mathrm{MHT}_{\!f}}}$ )

The logic of ${{\mathrm{MHT}_{\!f}}}$ is decidable.

The next result shows that the satisfaction of negated formulas as classical ones also extends from HT to ${\mathrm{MHT}}$ :

Proposition 4

Let $(\langle \mathbf{H},\mathbf{T} \rangle,{{\tau}})$ be a timed HT-trace of length $\lambda$ over ${{\mathcal{A}}}$ and let $\varphi$ be a metric formula over ${{\mathcal{A}}}$ . Then, $(\langle \mathbf{H},\mathbf{T} \rangle, {{\tau}}), k \models \neg \varphi$ iff $(\langle \mathbf{T},\mathbf{T} \rangle, {{\tau}}), k \not\models \varphi$ .

In the non-metric case, ${\mathrm{LTL}}$ models can be obtained from ${{\mathrm{THT}}}$ by adding a particular axiom schema, we call the temporal excluded middle axiom.

Definition 3 (Temporal Excluded Middle)

Given a set of propositional variables ${{\mathcal{A}}}$ , we define the theory ${{\mathrm{EM}({{\mathcal{A}}})}}$ as

\begin{align*} {{\mathrm{EM}({{\mathcal{A}}})}}& \stackrel{\mathit{def}}{=} \lbrace {{\square}}(p \vee \neg p) \mid p \in {{\mathcal{A}}} \rbrace.\end{align*}

This same axiom schema can also be used to reduce ${\mathrm{MHT}}$ to $ {{\mathrm{MTL}}}$ , assuming that, in our current context, operator ${{\square}}$ stands for ${{\square}}_{{{[0..\omega)}}}$ as detailed above.

Proposition 5

Let ${{\mathcal{A}}}$ be a set of atoms. For all ${\mathrm{MHT}}$ interpretation $(\langle \mathbf{H},\mathbf{T} \rangle,{{\tau}})$ over ${{\mathcal{A}}}$ , we have that $(\langle \mathbf{H},\mathbf{T} \rangle,{{\tau}}), 0 \models {{\mathrm{EM}({{\mathcal{A}}})}}$ iff $\mathbf{H}=\mathbf{T}$ .

Corollary 2

Let $\Gamma$ be a metric theory over alphabet ${{\mathcal{A}}}$ . The ${{\mathrm{MTL}}}$ models of $\Gamma$ coincide with the ${\mathrm{MHT}}$ models of $\Gamma \cup {{\mathrm{EM}({{\mathcal{A}}})}}$ .

Interestingly, if an equivalence does not involve implication (or negation), we can just check it by only considering total models:

Proposition 6

Let $\varphi$ and $\psi$ be metric formulas without implication (and so, without negation either). Then, $\varphi \equiv \psi$ in ${{\mathrm{MTL}}}$ iff $\varphi \equiv \psi$ in ${\mathrm{MHT}}$ .

Many tautologies in ${\mathrm{MHT}}$ or its fragments have a dual version depending on the nature of the operators involved. This can be formally exploited to save proof effort. We define all pairs of dual connectives as follows: $\top/\bot$ , $\wedge/\vee$ ,

, ${{\rm{O}}_I}/{\widehat{\rm{O}}_I}$ , ${{{{\square}}_{I}}}/{{{{\Diamond}}_{I}}}$ , ${{{{\mathbin{\boldsymbol{\mathsf{S}}}}}_{I}}}/{{{{\mathbin{\boldsymbol{\mathsf{T}}}}}_{I}}}$ , ${ \bullet _I}/{\widehat \bullet _I}$ , ${{{{\blacksquare}}_{I}}}/{{{{\blacklozenge}}_{I}}}$ . For any formula $\varphi$ without implications, we define $\delta(\varphi)$ as the result of replacing each connective by its dual operator.

Then, we get the following corollary of Proposition 6.

Corollary 3 (Boolean Duality)

Let $\varphi$ and $\psi$ be metric formulas without implication. Then, we have in ${\mathrm{MHT}}$ that $\varphi\; {{\mathrel{\equiv}}}\; \psi$ iff $\delta(\varphi) \; {{\mathrel{\equiv}}}\; \delta(\psi)$ .

Let

, , ${{\rm{O}}_I}/{ \bullet _I}$ , ${\widehat{\rm{O}}_I}/{\widehat \bullet _I}$ , ${{{{\square}}_{I}}}/{{{{\blacksquare}}_{I}}}$ , and ${{{{\Diamond}}_{I}}}/{{{{\blacklozenge}}_{I}}}$ be all pairs of swapped-time connectives and $\sigma(\varphi)$ be the replacement in $\varphi$ of each connective by its swapped-time version. Then, we have the following result for finite traces.

Lemma 1

Let $\mathbf{M}$ be a finite timed HT-trace of length $\lambda \in \mathbb{N}$ . There exists a mapping $\varrho$ from $\mathbf{M}$ to another HT-trace $\varrho(\mathbf{M})$ of the same length such that for any ${{k \in {{[0..\lambda)}}}}$ , $\mathbf{M},k \models \varphi$ iff $\varrho(\mathbf{M}),\lambda\!-\!1\!-\!k \models \sigma(\varphi)$ .

Theorem 1 (Temporal Duality Theorem)

A metric formula $\varphi$ is a ${{\mathrm{MHT}_{\!f}}}$ -tautology iff $\sigma(\varphi)$ is a $ {{\mathrm{MHT}_{\!f}}}$ -tautology.

The next properties capture some distributivity laws for temporal operators with respect to conjunction and disjunction.

Proposition 7

For all metric formulas $\varphi$ , $\psi$ , and $\chi$ , the following equivalences hold in ${\mathrm{MHT}}$ :

We can also prove a kind of De Morgan duality between until and release, and analogously, between since and trigger:

Proposition 8

For all metric formulas $\varphi$ and $\psi$ , the following equivalences hold in ${\mathrm{MHT}}$ :

Another interesting result has to do with the effect of extending or stretching the interval in these operators.

Proposition 9

Let I and J be two intervals satisfying $I \subseteq J$ . For all metric formulas $\varphi$ and $\psi$ , the following expressions are valid in ${\mathrm{MHT}}$ :

We observe next the effect of the semantics of always and eventually on truth constants. If $m, n \in \mathbb{N}$ , then ${{{\square}}}_{{{[m..n)}}} \bot$ means that there is no state in interval ${{[m..n)}}$ and ${{{\Diamond}}}_{{{[m..n)}}} \top$ means that there is at least one state in this interval. The formula ${{{\square}}}_{{{[m..n)}}} \top$ is a tautology, whereas ${{{\Diamond}}}_{{{[m..n)}}} \bot$ is unsatisfiable. The same applies to past operators ${{{\blacklozenge}}}_{{{[m..n)}}}$ and ${{{\blacksquare}}}_{{{[m..n)}}}$ .

Strict traces

In the rest of this section, we consider a group of results that hold under the assumption of strict traces, namely, that ${{\tau}}(i) < {{\tau}}(i+1)$ for any pair of consecutive time points. We can enforce metric models to be traces with a strict timing function ${{\tau}}$ . This can be achieved with the simple addition of the axiom ${{\square}} \neg {{\rm{o}}_0} \top$ . In the following, we assume that this axiom is included and consider, in this way, strict timing.

The following equivalences state that interval ${{[0..0]}}$ makes all binary metric operators collapse into their right hand argument formula, whereas unary operators collapse to a truth constant. For metric formulas $\psi$ and $\varphi$ and for strict traces, we have

(4)

(5)

(6)

The last two lines are precisely an effect of dealing with strict traces. For instance, ${{\rm{O}}_0}{\mkern 1mu} \varphi \equiv \bot$ tells us that it is always impossible to have a successor state with the same time (the time difference is 0) as the current one, regardless of the formula $\varphi$ at hand.

The next lemma allows us to unfold metric operators for single-point time intervals ${{[n..n]}}$ with $n>0$ . Moreover, this lemma shows that for a single-point time interval ${{\rm{O}}_n}\varphi$ is definable.

Lemma 2

For metric formulas $\psi$ and $\varphi$ and for $n>0$ , we have

(7)

(8)

(9)

(10)

(11)

(12)

The same applies for the dual past operators.

Going one step further, we can also unfold until and release for intervals of the form ${{[0..n]}}$ with the application of the following result.

Lemma 3

For metric formulas $\psi$ and $\varphi$ and for $n > 0$ , we have:

(13)

(14)

The same applies for the dual past operators.

We can also prove that for any interval of the form ${{[m..n)}}$ , where $n\not=\omega$ , the metric versions of next and weak next (resp. previous and weak previous) can be defined in terms of the other metric connectives.

Proposition 10

For all $m , n \in \mathbb{N}$ , the following equivalences hold

(15) ${{\rm{O}}_{[m..n)}}\varphi \equiv \vee _{i = m}^{n - 1}{{\rm{O}}_i}\varphi ,$

(16) ${\widehat{\rm{O}}_{[m..n)}}\varphi \equiv \wedge _{i = m}^{n - 1}{\widehat{\rm{O}}_i}\varphi .$

The same applies for the dual past operators.

Finally, the next theorem contains a pair of equivalences that, when dealing with finite intervals, can be used to recursively unfold until and release into combinations of next with Boolean operators (an analogous result applies for since, trigger and previous due to temporal duality).

Theorem 2 (Next-unfolding)

For metric formulas $\psi$ and $\varphi$ and for $m, n \in \mathbb{N}$ such that $0 < m < n-1$ , we have:

(17)

(18)

The same applies for the dual past operators.

As an example, consider the metric formula .

Another useful result that can be applied to unfold metric operators is the following range splitting theorem.

Theorem 3 (Range splitting)

For metric formulas $\psi$ and $\varphi$ ,

(19)

(20)

The same applies for the dual past operators.

A metric formula $\varphi$ is said to be in unary normal form, if intervals only affect unary temporal operators, while binary operators , , ${{\mathbin{\boldsymbol{\mathsf{S}}}}}$ , ${{\mathbin{\boldsymbol{\mathsf{T}}}}}$ are only used in their temporal form, without any attached intervals. The following proposition, inspired by (D’Souza and Tabareau 2004), allows us to translate any arbitrary metric formula into unary normal form.

Proposition 11

For metric formulas $\varphi$ and $\psi$ and for m and n such that $m > 0$ , the following equivalences hold in ${\mathrm{MHT}}$ :

Corollary 4

Any metric formula can be translated into unary normal form (assuming strict traces).

3 Metric equilibrium logic

As in traditional Equilibrium Logic (Pearce 1997), non-monotonicity is achieved in ${{\mathrm{MEL}}}$ by a selection among the ${\mathrm{MHT}}$ models of a theory. In what follows, we keep assuming the use of strict traces.

Definition 4 (Metric Equilibrium/Stable Model) Let $\mathfrak{S}$ be some set of timed HT-traces. A total timed HT-trace $(\langle \mathbf{T}, \mathbf{T} \rangle, \tau) \in\mathfrak{S}$ is a metric equilibrium model of $\mathfrak{S}$ iff there is no other $\mathbf{H}$ different from $\mathbf{T}$ such that $(\langle \mathbf{H}, \mathbf{T} \rangle, \tau) \in \mathfrak{S}$ .

We talk about metric equilibrium (or metric stable) models of a theory $\Gamma$ when $\mathfrak{S} = {\mathrm{MHT}}(\Gamma)$ , and we write ${{\mathrm{MEL}}}(\Gamma, \lambda)$ and ${{\mathrm{MEL}}}(\Gamma)$ to stand for the metric equilibrium models of ${{\mathrm{MHT}}}(\Gamma, \lambda)$ and ${{\mathrm{MHT}}}(\Gamma)$ , respectively. MEL is the non-monotonic logic induced by the metric equilibrium models of metric theories. As before, variants ${{{{{\mathrm{MEL}}}}_{\!f}}}$ and ${{{{{\mathrm{MEL}}}}_{\omega}}}$ refer to ${{\mathrm{MEL}}}$ when restricted to traces of finite and infinite length, respectively.

Observation 1

The set of metric equilibrium models of $\Gamma$ can be partitioned on the trace lengths, namely, $\bigcup_{\lambda=0}^{\omega} {{\mathrm{MEL}}}(\Gamma,\lambda) = {{\mathrm{MEL}}}(\Gamma)$ .

Back to our example, suppose we have the theory $\Gamma$ consisting of formulas (1)-(3), viz.

In the example, we abbreviate subsets of the set of atoms $\{\mathit{green},\mathit{push},\mathit{red}\}$ as strings formed by their initials: For instance, pr stands for $\{\mathit{push},\mathit{red}\}$ . For the sake of readability, we represent sequences $(T_0, T_1, T_2)$ as $T_0 \cdot T_1 \cdot T_2$ . Consider first the total models of $\Gamma$ : the first two rules force one of the two atoms $\mathit{green}$ or $\mathit{red}$ to hold at every state. Besides, we can choose adding $\mathit{push}$ or not, but if we do so, $\mathit{green}$ should hold later on according to (3). Now, for any total model $(\langle \mathbf{T},\mathbf{T} \rangle,\tau),0 \models \Gamma$ where $\mathit{green}$ or $\mathit{push}$ hold at some states, we can always form $\mathbf{H}$ in which we remove those atoms from all the states and it is not difficult to see that $(\langle \mathbf{H},\mathbf{T} \rangle,\tau),0 \models \Gamma$ , so $(\langle \mathbf{T},\mathbf{T} \rangle,\tau)$ is not in equilibrium. As a consequence, metric equilibrium models of $\Gamma$ have the form $(\langle \mathbf{T},\mathbf{T} \rangle,\tau)$ being $\mathbf{T}=\langle T_i \rangle _{i \in {{[0..\lambda)}}}$ with $T_i = \{\mathit{red}\}$ for all ${i \in {{[0..\lambda)}}}$ and any arbitrary strict timing function $\tau$ . To illustrate non-monotonicity, suppose now that we have $\Gamma ' = \Gamma \cup \{ {\rm{ }}{{\rm{O}}_5}\;push\}$ and, for simplicity, consider length $\lambda=3$ and traces of the form $T_0 \cdot T_1 \cdot T_2$ . Again, it is not hard to see that total models with $\mathit{green}$ or $\mathit{push}$ in state $T_0$ are not in equilibrium, leaving the only option $T_0=\{\mathit{red}\}$ . The same happens for $\mathit{green}$ at $T_1$ , so we get $T_1=\{\mathit{push},\mathit{red}\}$ as only candidate for equilibrium model. However, since $\mathit{push} \in T_1$ , the only possibility to satisfy the consequent of (3) is having $\mathit{green} \in T_2$ . Again, we can also see that adding $\mathit{push}$ at that state would not be in equilibrium so that the only trace in equilibrium is the total trace formed with $T_0=\{\mathit{red}\}$ , $T_1=\{\mathit{push},\mathit{red}\}$ and $T_2=\{\mathit{green}\}$ . As for the timing, $\tau(0)=0$ is fixed, and satisfaction of formula $({{\rm{O}}_5}\;push)$ fixes $\tau(1)=5$ . Then, from (3) we conclude that $\mathit{green}$ must hold at any moment starting at t between $5+1$ and $5+14$ and is kept true in all states between t and $t+30$ time units, but as $\lambda=2$ , this means just t. To sum up, we get 14 metric equilibrium models with $\tau(0)=0$ and $\tau(1)=5$ fixed, but varying $\tau(2)$ between 6 and 19.

We close this section by considering strong equivalence. Two metric theories $\Gamma_1$ and $\Gamma_2$ are strongly equivalent when ${{\mathrm{MEL}}}(\Gamma_1 \cup \Delta)={{\mathrm{MEL}}}(\Gamma_2 \cup \Delta)$ for any metric theory $\Delta$ . This means that we can safely replace $\Gamma_1$ by $\Gamma_2$ in any common context $\Delta$ and still get the same set of metric equilibrium models. The following result shows that checking strong equivalence for ${{\mathrm{MEL}}}$ collapses to regular equivalence in the monotonic logic of ${\mathrm{MHT}}$ .

Theorem 4

Let $\Gamma_1$ and $\Gamma_2$ be two metric temporal theories built over a finite alphabet ${{\mathcal{A}}}$ . Then, $\Gamma_1$ and $\Gamma_2$ are strongly equivalent iff $\Gamma_1$ and $\Gamma_2$ are ${\mathrm{MHT}}$ -equivalent.

4 Translation into monadic quantified here-and-there with difference constraints

In a similar spirit as the well-known translation of Kamp (1968) from ${\mathrm{LTL}}$ to first-order logic, we consider a translation from ${\mathrm{MHT}}$ into a first-order version of HT, more precisely, a function-free fragment of the logic of Quantified Here-and-There with static domains ( ${{\mathit{QHT}^s}}$ in (Pearce and Valverde 2008)). The word static means that the first-order domain D is fixed for both worlds, here and there. We refer to our fragment of ${{\mathit{QHT}^s}}$ as monadic QHT with difference constraints (or ${{\mathit{QHT}[\preccurlyeq_{\delta}]}}$ for short). In this logic, the static domain is a subset $D \subseteq \mathbb{N}$ of the natural numbers containing at least the element $0 \in D$ . Intuitively, D corresponds to the set of relevant time points (i.e. those associated with states) considered in each model. Note that the first state is always associated with time $0 \in D$ .

The syntax of ${{\mathit{QHT}[\preccurlyeq_{\delta}]}}$ is the same as for first-order logic with several restrictions: First, there are no functions other than the 0-ary function (or constant) ‘0’ always interpreted as the domain element 0 (when there is no ambiguity, we drop quotes around constant names). Second, all predicates are monadic except for a family of binary predicates of the form $\preccurlyeq_{\delta}$ with $\delta \in \mathbb{Z}\cup \lbrace\omega \rbrace$ where $\delta$ is understood as part of the predicate name. For simplicity, we write $x \preccurlyeq_{\delta} y$ instead of ${\preccurlyeq_{\delta}}(x,y)$ and $x \preccurlyeq_{\delta} y \preccurlyeq_{\delta'} z$ to stand for $x \preccurlyeq_{\delta} y \wedge y \preccurlyeq_{\delta'} z$ . Unlike monadic predicates, the interpretation of $x \preccurlyeq_{\delta} y$ is static (it does not vary in worlds here and there) and intuitively means that the difference $x-y$ in time points is smaller or equal than $\delta$ . A first-order formula $\varphi$ satisfying all these restrictions is called a first-order metric formula or FOM-formula for short. A formula is a sentence if it contains no free variables. For instance, we will see that the metric formula (3) can be equivalently translated into the FOM-sentence:

(21) \begin{align}\forall x \, (0 \preccurlyeq_{0} x \wedge \mathit{push}(x) \to\exists y\, (x \preccurlyeq_{-1} y \preccurlyeq_{14} x \wedge \forall z \, (y \preccurlyeq_{0} z \preccurlyeq_{30} y \to \mathit{green}(z) ) ) ), \end{align}

We sometimes handle partially grounded FOM sentences where some variables in predicate arguments have been directly replaced by elements from D. For instance, if we represent (21) as $\forall x \ \varphi(x)$ , the expression $\varphi(4)$ stands for:

\begin{align*}0 \preccurlyeq_{0} 4 \wedge \mathit{push}(4) \to\exists y\, (4 \preccurlyeq_{-1} y \preccurlyeq_{14} 4 \wedge \forall z \, (y \preccurlyeq_{0} z \preccurlyeq_{30} y \to \mathit{green}(z) ) ), \end{align*}

and corresponds to a partially grounded FOM-sentence where the domain element 4 is used as predicate argument in atoms $0 \preccurlyeq_{0} 4$ and $\mathit{push}(4)$ .

A ${{\mathit{QHT}[\preccurlyeq_{\delta}]}}$ -signature is simply a set of monadic predicates $\mathcal{P}$ . Given D as above, ${{\mathit{Atoms}(D,\mathcal{P})}}$ denotes the set of all ground atoms p(n) for every monadic predicate $p \in \mathcal{P}$ and every $n \in D$ . A ${{\mathit{QHT}[\preccurlyeq_{\delta}]}}$ -interpretation for signature $\mathcal{P}$ has the form $\langle D,H,T \rangle$ where $D \subseteq \mathbb{N}$ , $0 \in D$ , and $H \subseteq T \subseteq {{\mathit{Atoms}(D,\mathcal{P})}}$ .

Definition 5 ( ${{\mathit{QHT}[\preccurlyeq_{\delta}]}}$ -satisfaction; ( Pearce and Valverde 2008 ))

A ${{\mathit{QHT}[\preccurlyeq_{\delta}]}}$ -interpretation $\mathcal{M}=\langle D,H,T \rangle$ satisfies a (partially grounded) FOM-sentence $\varphi$ , written $\mathcal{M}\models \varphi$ , if the following conditions hold:

1. $\mathcal{M} \models \top$ and $\mathcal{M} \not \models \bot$

2. $\mathcal{M} \models p(t)$ iff $p(t) \in H$

3. $\mathcal{M} \models t_1 \preccurlyeq_{\delta} t_2$ iff $t_1-t_2 \le \delta$ with $t_1, t_2 \in D$

4. $\mathcal{M} \models \varphi \wedge \psi$ iff $\mathcal{M} \models\varphi$ and $\mathcal{M} \models\psi$

5. $\mathcal{M} \models \varphi \vee \psi$ iff $\mathcal{M} \models\varphi$ or $\mathcal{M} \models\psi$

6. $\mathcal{M} \models \varphi \rightarrow \psi$ iff $\langle D, X, T \rangle \not \models \varphi$ or $\langle D, X, T \rangle\models\psi$ for $X \in \{H,T\}$

7. $\mathcal{M} \models \forall\, x\ \varphi(x)$ iff $\mathcal{M} \models \varphi(t)$ for all $t \in D$

8. $\mathcal{M} \models \exists\, x\ \varphi(x)$ iff $\mathcal{M} \models \varphi(t)$ for some $t \in D$

We can read the expression $x \preccurlyeq_{\delta} y$ as just another way of writing the difference constraint $x-y \leq \delta$ . When $\delta$ is an integer, we may see it as a lower bound $x-\delta \leq y$ for y or as an upper bound $x \leq y+\delta$ for x. For $\delta=\omega$ , $x \preccurlyeq_{\omega} y$ is equivalent to $\top$ since it amounts to the comparison $x-y \leq \omega$ . An important observation is that this difference predicate $\preccurlyeq_{\delta}$ satisfies the excluded middle axiom, that is, the following formula is a ${{\mathit{QHT}[\preccurlyeq_{\delta}]}}$ -tautology:

$$\forall x \, \forall y\, (\ x \preccurlyeq_{\delta} y \vee \neg (x \preccurlyeq_{\delta} y) \ ),$$

for every $\delta \in \mathbb{Z} \cup \{\omega\}$ . We provide next several useful abbreviations:

$$\begin{array}{rcl@{\hspace{30pt}}rcl}x \prec_{\delta} y & \stackrel{\mathit{def}}{=} & \neg (y \preccurlyeq_{-\delta} x) \\[2pt]x \leq y & \stackrel{\mathit{def}}{=} & x \preccurlyeq_{0} y &x \neq y & \stackrel{\mathit{def}}{=} & \neg (x = y) \\[2pt]x = y &\stackrel{\mathit{def}}{=} & \left(x \leq y\right) \wedge \left(y \leq x\right) &x < y & \stackrel{\mathit{def}}{=} & (x \le y)\wedge (x \not = y). \\[2pt]\end{array}$$

For any pair $\odot$ , $\oplus$ of comparison symbols, we extend the abbreviation $x \odot y \oplus z$ to stand for the conjunction $x \odot y \wedge y \oplus z$ . Note that the above derived order relation $x \le y$ captures the one used in Kamp’s original translation (Kamp 1968) for ${\mathrm{LTL}}$ .

Equilibrium models for first-order theories are defined as in (Pearce and Valverde 2008).

Definition 6 (Quantified Equilibrium Model; ( Pearce and Valverde 2008 ))

Let $\varphi$ be a first-order formula. A total ${{\mathit{QHT}[\preccurlyeq_{\delta}]}}$ -interpretation $\langle D,T,T \rangle$ is a first-order equilibrium model of $\varphi$ if $\langle D,T,T \rangle \models \varphi$ and there is no $H \subset T$ satisfying $\langle D,H,T \rangle \models \varphi$ .

Before presenting our translation, we need to remark that we consider non-empty intervals of the form ${{[m..n)}}$ with $m < n$ .

Definition 7 (First-order encoding) Let $\varphi$ be a metric formula over ${{\mathcal{A}}}$ . We define the translation $[\varphi]_x$ of $\varphi$ for some time point $x\in\mathbb{N}$ as follows:

Each quantification introduces a new variable. For instance, consider the translation of (3) at point $x=0$ . Let us denote (3) as ${{\square}} ( \mathit{push} \to \alpha )$ where $\alpha$ is the formula ${ \Diamond _{[1..15)}}({\square_{ \le 30}}\;green)$ . Then, if we translate the outermost operator ${{\square}}$ , we get:

where we renamed the quantified variable for convenience. If we proceed further, with $\alpha$ as ${{{\Diamond}}}_{{{[1..15)}}}\beta$ and letting $\beta$ be $({\square_{ \le 30}}\;green)$ , we obtain:

Finally, the translation of $\beta$ at y amounts to:

so that, when joining all steps together, we get the formula (21) given above.

The following model correspondence between ${{\mathrm{MHT}_{\!f}}}$ and ${{\mathit{QHT}[\preccurlyeq_{\delta}]}}$ interpretations can be established. Given a timed trace $(\langle \mathbf{H},\mathbf{T} \rangle, \tau)$ of length $\lambda > 0$ for signature ${{\mathcal{A}}}$ , we define the first-order signature $\mathcal{P} = \{ {{p}}/1 \mid {{p}} \in {{\mathcal{A}}} \}$ containing unary predicates and a corresponding ${{\mathit{QHT}[\preccurlyeq_{\delta}]}}$ interpretation $\langle D,H,T \rangle$ where $D=\{\tau(i) \mid i \in {{[0..\lambda)}}\}$ , $H = \lbrace {{p}}(\tau(i)) \mid i \in {{[0..\lambda)}} \mathrm{ and } {{p}} \in H_i \rbrace$ and $T = \lbrace {{p}}(\tau(i)) \mid i \in {{[0..\lambda)}} \mathrm{ and } {{p}} \in T_i \rbrace$ . Under the assumption of strict semantics, the following model correspondence can be proved by structural induction.

Theorem 5

For all metric formulas $\varphi$ , and for all timed traces $(\langle \mathbf{H},\mathbf{T} \rangle, \tau)$ whose corresponding ${{\mathit{QHT}[\preccurlyeq_{\delta}]}}$ interpretation is denoted by $\langle D,H,T \rangle$ and for all $i \in {{[0..\lambda)}}$ .

(22) \begin{eqnarray}(\langle {\bf{H}},{\bf{T}}\rangle ,\tau ),i| = \varphi {\rm{ iff}}\,\langle D,H,T\rangle | = {[\varphi ]_{\tau (i)}}.\end{eqnarray}

5 Related work

Seen from far, we have presented an extension of the logic of Here-and-There with qualitative and quantitative temporal constraints. More closely, our logics ${\mathrm{MHT}}$ and ${{\mathrm{MEL}}}$ can be seen as metric extensions of the linear-time logics ${{\mathrm{THT}}}$ and ${\mathrm{TEL}}$ obtained by constraining temporal operators by intervals over natural numbers. The current approach generalizes the previous metric extension of ${\mathrm{TEL}}$ from (Cabalar et al. 2020) by uncoupling the ordinal position i of a state in the trace from its location in the time line $\tau(i)$ , which indicates now the elapsed time since the beginning of that trace. Thus, while ${{\Diamond}}_{{{[5..5]}}}\; {{p}}$ meant in (Cabalar et al. 2020) that ${{p}}$ must hold exactly after 5 transitions, it means here that there must be some future state (after $n>0$ transitions) satisfying p and located 5 time units later. As a first approach, we have considered time points as natural numbers, $\tau(i) \in \mathbb{N}$ . Our choice of a discrete rather than continuous time domain is primarily motivated by our practical objective to implement the logic programming fragment of ${{\mathrm{MEL}}}$ on top of existing temporal ASP systems, like telingo, and thus to avoid undecidability.

The need for quantitative time constraints is well recognized and many metric extensions have been proposed. For instance, actions with durations are considered in (Son et al. 2004) in an action language adapting a state-based approach. Interestingly, quantitative time constraints also gave rise to combining ASP with Constraint Solving (Baselice et al. 2005); this connection is now semantically reinforced by our translation advocating the enrichment of ASP with difference constraints. Even earlier, metric extensions of Logic Programming were proposed in (Brzoska 1995). As well, metric extensions of Datalog are introduced in (Wa_lega et al. 2019) and applied to stream reasoning in (Wałlega et al. 2019). An ASP-based approach to stream reasoning is elaborated in abundance in (Beck et al. 2018). Streams can be seen as infinite traces. Hence, apart from certain dedicated concepts, like time windows, such approaches bear a close relation to metric reasoning. Detailing this relationship is an interesting topic of future research. More remotely, metric constructs were used in trace alignment (De Giacomo et al. 2020), scheduling (Luo et al. 2016), and an extension to Golog (Hofmann and Lakemeyer 2019).

6 Conclusion

We have developed a metric extension of linear-time temporal equilibrium logic, in which temporal operators are constrained by intervals over natural numbers. The resulting MEL provides the foundation of an ASP-based approach for specifying qualitative and quantitative dynamic constraints. This expressiveness is useful whenever planning and scheduling go hand in hand, like for instance when actions have durations and their effects need to meet deadlines. To the best of our knowledge, our approach is the first that considers the concept of timed traces in the context of temporal ASP.

As future work, we aim to implement our approach by exploiting the provided translation of metric formulas into monadic first-order formulas. We expect that such a translation is tailored for an implementation in terms of ASP modulo difference constraints. A further line of research will be the investigation of the combination of metric concepts with more expressive logics than

$${\mathrm{TEL}}$$

. As a first approach in this direction, we recently proposed an extension of dynamic equilibrium logic to incorporate quantitative temporal constraints, leading to metric dynamic equilibrium logic (Becker et al. 2023).

Supplementary material

To view supplementary material for this article, please visit http://doi.org/10.1017/S1471068424000139.