2.1 The logic of here-and-there (Pearce Reference Pearce 1997 )

A formula over an alphabet ${\mathcal{A}}$ is defined as

\begin{align*} \varphi &::= \bot \mid a \mid \varphi \wedge \varphi \mid \varphi \vee \varphi \mid \varphi \to \varphi \quad \text{ where } a\in \mathcal{A}\ . \end{align*}

We define the derived operators $\neg \varphi =\varphi \to \bot$ and $\top =\neg \bot$ . Elements $a$ of $\mathcal{A}$ are called (Boolean) atoms. A literal is an atom or an atom preceded by negation, viz. $a$ or $\neg a$ . A theory is a set of formulas. We sometimes write $\varphi \leftarrow \psi$ instead of $\psi \to \varphi$ to follow logic programming conventions. A program is a set of implications of the form $\varphi \leftarrow \psi$ where $\varphi$ is a disjunction of literals and $\psi$ is a conjunction of literals.

We represent an interpretation $T$ as a set of atoms $T\subseteq \mathcal{A}$ . An $\textrm {HT}$ -interpretation is a pair $\langle H,T \rangle$ of interpretations such that $H\subseteq T$ ; it is said to be total if $H=T$ . An HT-interpretation $\langle H,T \rangle$ satisfies a formula $\varphi$ , written $\langle H,T \rangle \models \varphi$ , if

1. 1. $\langle H,T \rangle \models a$ if $a \in H$

2. 2. $\langle H,T \rangle \models \varphi \wedge \psi$ if $\langle H,T \rangle \models \varphi$ and $\langle H,T \rangle \models \psi$

3. 3. $\langle H,T \rangle \models \varphi \vee \psi$ if $\langle H,T \rangle \models \varphi$ or $\langle H,T \rangle \models \psi$

4. 4. $\langle H,T \rangle \models \varphi \to \psi$ if $\langle H',T \rangle \not \models \varphi$ or $\langle H',T \rangle \models \psi$ for each $H'\in \{H, T\}$

An $\textrm {HT}$ -interpretation $\langle H,T \rangle$ is an $\textrm {HT}$ -model of a theory $\Gamma$ if $\langle H,T \rangle \models \varphi$ for each $\varphi \in \Gamma$ . A total model $\langle T,T \rangle$ of a theory $\Gamma$ is an equilibrium model if there is no other model $\langle H,T \rangle$ of $\Gamma$ with $H \subset T$ ; $T$ is also called a stable model of $\Gamma$ .

2.2 The logic of here-and-there with constraints (Cabalar et al. Reference Cabalar, Kaminski, Ostrowski and Schaub 2016 )

The syntax of $\textrm {HT}_{\!c}$ relies on a signature $\langle \mathcal{X},\mathcal{D},\mathcal{C} \rangle$ , similar to constraint satisfaction problems, where elements of set $\mathcal{X}$ represent variables and elements of $\mathcal{D}$ are domain values (usually identified with their respective constants). The constraint atoms in $\mathcal{C}$ provide an abstract way to relate values of variables and constants according to the atom’s semantics. For instance, difference constraint atoms are expressions of the form “ $x - y \leq d$ ,” containing variables $x,y\in \mathcal{X}$ and the domain value $d\in \mathcal{D}$ . A constraint formula $\varphi$ over $\mathcal{C}$ is defined as

\begin{align*} \varphi &::= \bot \mid c \mid \varphi \wedge \varphi \mid \varphi \vee \varphi \mid \varphi \rightarrow \varphi \quad \text{ where } c\in \mathcal{C} \end{align*}

Concepts like defined operators, programs, theories, etc. are analogous to $\textrm {HT}$ . Variables can be assigned some value from $\mathcal{D}$ or left undefined. For the latter, we use the special symbol $\boldsymbol{u}\not \in \mathcal{D}$ and the extended domain $\mathcal{D}_u = \mathcal{D} \cup \{\boldsymbol{u}\}$ . A valuation $v$ is a function $v:\mathcal{X}\rightarrow \mathcal{D}_u$ . We let $\mathbb{V}$ stand for the set of all valuations. We sometimes represent a valuation $v$ as a set $ \{ (x,v(x)) \mid x\in \mathcal{X}, v(x)\in \mathcal{D}\}$ of pairs, so that $(x,\boldsymbol{u})$ is never formed. This allows us to use standard set inclusion, $v\subseteq v'$ , for comparing $v,v'\in \mathbb{V}$ .

The semantics of constraint atoms is defined in $\textrm {HT}_{\!c}$ via denotations, that is, functions $ [\![ \, \cdot \, ]\!]:\mathcal{C}\rightarrow 2^{\mathbb{V}}$ mapping each constraint atom to a set of valuations. An $\textrm {HT}_{\!c}$ -interpretation is a pair $\langle h,t \rangle$ of valuations such that $h\subseteq t$ ; it is total if $h=t$ . Given a denotation $[\![ \, \cdot \, ]\!]$ , an $\textrm {HT}_{\!c}$ -interpretation $\langle h,t \rangle$ satisfies a constraint formula $\varphi$ , written $\langle h,t \rangle \models \varphi$ , ifFootnote ²

1. 1. $\langle h,t \rangle \models c \text{ if } h\in [\![ \, c \, ]\!]$

2. 2. $\langle h,t\rangle \models \varphi \wedge \psi \text{ if } \langle h,t\rangle \models \varphi \text{ and } \langle h,t\rangle \models \psi$

3. 3. $\langle h,t\rangle \models \varphi \vee \psi \text{ if } \langle h,t\rangle \models \varphi \text{ or } \langle h,t\rangle \models \psi$

4. 4. $\langle h,t\rangle \models \varphi \rightarrow \psi \text{ if }\langle v,t\rangle \not \models \varphi \text{ or }\langle v,t\rangle \models \psi \text{ for each }v\in \{h,t\}$

An $\textrm {HT}_{\!c}$ -interpretation $\langle h,t \rangle$ is an $\textrm {HT}_{\!c}$ -model of a theory $\Gamma$ if $\langle h,t \rangle \models \varphi$ for every $\varphi \in \Gamma$ . A total model $\langle t,t\rangle$ of a theory $\Gamma$ is a constraint equilibrium model if there is no other model $\langle h,t \rangle$ of $\Gamma$ with $h\subset t$ .

2.3 The metric temporal logic of here-and-there (Cabalar et al. Reference Cabalar, Diéguez, Schaub and Schuhmann 2020b ; Becker et al. Reference Becker, Cabalar, Diéguez, Schaub and Schuhmann 2024 )

Given an alphabet $\mathcal{A}$ and $ \mathbb{I}=\{ [m..n)\mid m\in \mathbb{N}, n\in \mathbb{N}\cup \{\omega \}\}$ , a metric temporal formula is defined asFootnote ³

\begin{align*} \varphi &::= \bot \mid a \mid \varphi \wedge \varphi \mid \varphi \vee \varphi \mid \varphi \to \varphi \mid \boldsymbol{\mathsf{I}} \mid {\bigcirc}_{I} \varphi \mid \square _{I} \varphi \mid {\Diamond }_{I} \varphi \quad \text{ where } a\in \mathcal{A}, I\in \mathbb{I} \end{align*}

The last three cases deal with metric temporal operators, which are indexed by some interval $I$ . In words, $ {\bigcirc}_{I}$ , $\square _{I}$ , and ${\Diamond }_{I}$ are called next, always, and eventually. $\boldsymbol{\mathsf{I}}$ simply refers to the initial state. We write $ {\bigcirc}$ , $\square$ , $\Diamond$ for $ {\bigcirc}_{[0..\omega )}$ , $\square _{[0..\omega )}$ , $\Diamond _{[0..\omega )}$ , respectively. In addition to the aforedefined Boolean operators, we define $\boldsymbol{\mathsf{F}} = \neg {\bigcirc} \top$ , which allow us to refer to the final state. Concepts like programs, theories, etc. are analogous to $\textrm {HT}$ .

The semantics of temporal formulas is defined via traces, being sequences $\mathbf{T}=(T_i)_{i \in [0..\lambda )}$ of interpretations $T_i\subseteq \mathcal{A}$ ; $\lambda$ is the length of $\mathbf{T}$ . Here, we consider only traces of finite length. We define the ordering $\mathbf{H}\leq \mathbf{T}$ between traces of the same length $\lambda$ as $H_i\subseteq T_i$ for each $i \in [0..\lambda )$ , and $\mathbf{H}\lt \mathbf{T}$ as both $\mathbf{H}\leq \mathbf{T}$ and $\mathbf{H}\neq \mathbf{T}$ . An $\textrm {HT}$ -trace over $\mathcal{A}$ of length $\lambda$ is a sequence of pairs $ (\langle H_i,T_i \rangle )_{i \in [0..\lambda )}$ with $H_i\subseteq T_i$ for any $0 \leq i \lt \lambda$ ; it is total if $H_i=T_i$ . For convenience, we represent it as the pair $\langle \mathbf{H},\mathbf{T} \rangle$ of traces $\mathbf{H} = (H_i)_{i \in [0..\lambda )}$ and $\mathbf{T} = (T_i)_{i \in [0..\lambda )}$ .

Metric information is captured by timing functions. Given $\lambda \in \mathbb{N}$ , we say that $ {\tau }: [0..\lambda ) \to \mathbb{N}$ is a (strict) timing function wrt $\lambda$ if ${\tau }(0)=0$ and ${\tau }(k)\lt {\tau }(k+1)$ for $0\leq k\lt \lambda -1$ . A timed $\textrm {HT}$ -trace $(\langle \mathbf{H},\mathbf{T} \rangle ,{\tau })$ over $\mathcal{A}$ and $(\mathbb{N},\lt )$ of length $\lambda$ is a pair consisting of an $\textrm {HT}$ -trace $\langle \mathbf{H},\mathbf{T} \rangle$ over $\mathcal{A}$ of length $\lambda$ and a timing function $\tau$ wrt $\lambda$ . A timed $\textrm {HT}$ -trace $\mathbf{M}=(\langle \mathbf{H},\mathbf{T} \rangle , {\tau })$ of length $\lambda$ over alphabet $\mathcal{A}$ satisfies a metric formula $\varphi$ at $k \in [0..\lambda )$ , written $\mathbf{M},k \models \varphi$ , if

1. 1. $\mathbf{M},k \models a$ if $a \in H_k$

2. 2. $\mathbf{M}, k \models \varphi \wedge \psi$ if $\mathbf{M}, k \models \varphi$ and $\mathbf{M}, k \models \psi$

3. 3. $\mathbf{M}, k \models \varphi \vee \psi$ if $\mathbf{M}, k \models \varphi$ or $\mathbf{M}, k \models \psi$

4. 4. $\mathbf{M}, k \models \varphi \to \psi$ if $\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 })$

5. 5. $\mathbf{M}, k \models \boldsymbol{\mathsf{I}}$ if $k =0$

6. 6. $\mathbf{M}, k \models {\bigcirc}_{I}\, \varphi$ if $k+1\lt \lambda$ and $\mathbf{M}, k{+}1 \models \varphi$ and ${\tau }(k{+}1)-{\tau }(k) \in I$

7. 7. $\mathbf{M}, k \models {\Diamond }_{I}\, \varphi$ if $\mathbf{M}, i \models \varphi$ for some $i$ with $k \leq i \lt \lambda$ and ${\tau }(i)-{\tau }(k) \in I$

8. 8. $\mathbf{M}, k \models \square _{I}\, \varphi$ if $\mathbf{M}, i \models \varphi$ for all $i$ with $k \leq i \lt \lambda$ and ${\tau }(i)-{\tau }(k) \in I$

A timed $\textrm {HT}$ -trace $\mathbf{M}$ is an MHT-model of a metric theory $\Gamma$ if $\mathbf{M},0 \models \varphi$ for all $\varphi \in \Gamma$ . A total $\textrm {MHT}$ -model $(\langle \mathbf{T}, \mathbf{T} \rangle , \tau )$ of a theory $\Gamma$ is a metric equilibrium model if there is no other model $(\langle \mathbf{H},\mathbf{T} \rangle , {\tau })$ of $\Gamma$ with $\mathbf{H}\lt \mathbf{T}$ .

For illustration, let us consider the formalization of the dentist scenario in equations (1) to (9). We assume that variables $L$ and $L'$ are substituted by distinct locations $\textit {office}$ , $\textit {atm}$ , $\textit {dentist}$ , and $\textit {home}$ ; and variable $I$ by items $\textit {cash}$ and $\textit {icard}$ . We use $\delta \langle L,L'\rangle$ to refer to the distance between two locations from Table 1. As in Mellarkod (Reference Mellarkod2007), we assume that Ram is automatically picking up items when being at the same position.

(1) \begin{align} \square (\textit {at}(\textit {ram},\textit {office}) &\leftarrow \boldsymbol{\mathsf{I}}) \end{align}

(2) \begin{align} \square (\textit {at}(\textit {cash},\textit {atm}) &\leftarrow \boldsymbol{\mathsf{I}}) \end{align}

(3) \begin{align} \square (\textit {at}(\textit {icard},\textit {home}) &\leftarrow \boldsymbol{\mathsf{I}}) \end{align}

(4) \begin{align} \square (\textstyle \bigvee _{L'\neq L} \textit {go}(\textit {ram},L') &\leftarrow \textit {at}(\textit {ram},L)\wedge \neg \boldsymbol{\mathsf{F}}) \end{align}

(5) \begin{align} \square (\textit {has}(\textit {ram},I) &\leftarrow \textit {at}(\textit {ram},L) \wedge \textit {at}(I,L)) \end{align}

(6) \begin{align} \square (\textit {at}(I,L) &\leftarrow \textit {at}(\textit {ram},L) \wedge \textit {has}(\textit {ram},I)) \end{align}

(7) \begin{align} \square ( {\bigcirc}_{[\delta \langle L,L'\rangle ..\delta \langle L,L'\rangle +1)}{\textit {at}(\textit {ram},L')}&\leftarrow \textit {at}(\textit {ram},L) \wedge \textit {go}(\textit {ram},L')) \end{align}

(8) \begin{align} \square ( {\bigcirc}{\textit {has}(\textit {ram},I)} &\leftarrow \textit {has}(\textit {ram},I) \wedge \neg \boldsymbol{\mathsf{F}}) \end{align}

(9) \begin{align} \square ( {\bigcirc}{\textit {at}(I,L)} &\leftarrow \neg \textit {has}(\textit {ram},I) \wedge \textit {at}(I,L) \wedge \neg \boldsymbol{\mathsf{F}}) \end{align}

In brief, Rules equations (1) to (3) give the initial situation. Rule equation (4) delineates possible actions. Rules equations (5) and (6) capture indirect effects. Rule equation (7) is the effect of moving from location $L$ to $L'$ : it uses the next operator restricted by the duration between locations. Rules equations (8) and (9) address inertia.

3.1 Translation of plain metric logic programs to $\textrm {HT}$

We begin by formalizing timing functions $\tau$ via Boolean atoms in $ {\mathcal{T}}=\{t_{k,d} \mid k,d\in \mathbb{N} \}.$ An atom like $t_{k,d}$ represents that $\tau (k)=d$ . To obtain finite theories, we furthermore impose an upper bound $\nu \in \mathbb{N}$ on the range of $\tau$ . Hence, together with the trace length $\lambda$ , our formalization $\Delta _{\lambda ,\nu }$ only captures timing functions $\tau$ satisfying ${\tau }(\lambda -1)\leq \nu$ .

Given $\lambda ,\nu \in \mathbb{N}$ , we let

(13) \begin{align} \Delta _{\lambda ,\nu } &= \{ t_{0,0} \} \cup \{ \textstyle \bigvee _{d\lt d'\leq \nu }t_{k+1,d'}\leftarrow t_{k,d} \mid 0 \leq k \lt \lambda -1, 0 \leq d \leq \nu \} \end{align}

Starting from $\tau (0)=0$ , represented by $t_{0,0}$ , the rule in equation (13) assigns strictly increasing time points to consecutive states, reflecting that ${\tau }(k)\lt {\tau }(k+1)$ for $0\leq k\lt \lambda -1$ .

The last part of our formalization accounts for the interplay of the timing function with the interval conditions imposed in the program. Given $\lambda ,\nu \in \mathbb{N}$ and a plain metric program $P$ , we let

(14) \begin{align} \Psi _{\lambda ,\nu }({P}) = &\ \{ \bot \leftarrow (\beta )_{k} \wedge t_{k,d} \wedge t_{k+1,d'} \mid 0 \leq k \lt \lambda -1, 0\leq d\lt d'\leq \nu , \\ &\qquad \qquad \nonumber \phantom {n\in \mathbb{N}, }d'-d \lt m, \square ( {\bigcirc}_{[m..n)} a \leftarrow \beta ) \in {P} \}\;\cup \end{align}

(15) \begin{align} &\ \{ \bot \leftarrow (\beta )_{k} \wedge t_{k,d} \wedge t_{k+1,d'} \mid 0 \leq k \lt \lambda -1, 0\leq d\lt d'\leq \nu , \\&\qquad \qquad \nonumber n\in \mathbb{N}, d'-d \geq n, \square ({\bigcirc}_{[m..n)} a \leftarrow \beta ) \in {P} \} \end{align}

The integrity constraints ensure that for every plain metric rule $\square ( {\bigcirc}_{[m..n)} a \leftarrow \beta )$ the duration between the $k$ th and $(k+1)$ st state in a trace falls within interval $[m..n)$ . With ${\tau }(k) =d$ and ${\tau }(k+1) =d'$ , this amounts to checking whether $ d+m \leq d' \lt d+n$ , if $n$ is finite; otherwise, the verification of the upper bound in equation (15) is dropped for $n=\omega$ .

Note that the size of both $\Delta _{\lambda ,\nu }$ and $\Psi _{\lambda ,\nu }({P})$ is proportional to $\mathcal{O}(\lambda \cdot \nu ^2)$ . Hence, long traces and even more severely fine-grained timing functions lead to a significant blow up when translating plain metric programs into regular ones with the above formalization.

For the rule in equation (10), we get

(16) \begin{align} \bot &\leftarrow \textit {at}(\textit {ram},\textit {office})_k\wedge \textit {go}(\textit {ram},\textit {home})_k\wedge t_{k,d}\wedge t_{k+1,d'} \quad \text{ for } d'-d \lt 15 \end{align}

(17) \begin{align} \bot &\leftarrow \textit {at}(\textit {ram},\textit {office})_k\wedge \textit {go}(\textit {ram},\textit {home})_k\wedge t_{k,d}\wedge t_{k+1,d'} \quad \text{ for } d'-d \geq 16 \end{align}

and $0\leq k \lt \lambda -1$ , $0\leq d\lt d'\leq \nu$ . For $\lambda =100$ and $\nu =1000$ , this then amounts to roughly $10^8$ instances for each of the above constraints.

In what follows, we characterize the effect of our formalization in terms of $\textrm {HT}$ -models, and ultimately show the completeness and correctness of our translation.

Definition 1. An $\textrm {HT}$ interpretation $\langle H,T \rangle$ over $\mathcal{A}$ with $\mathcal{T}\subseteq \mathcal{A}$ , is $\text{timed}$ wrt $\lambda \in \mathbb{N}$ ,

if there is a timing function $\tau$ wrt $\lambda$ such that for all $0\leq k\lt \lambda$ , $d \in \mathbb{N}$ , we have

\begin{align*} \langle H,T \rangle \models t_{k,d}\text{ iff }{\tau }(k)=d \quad \text{ and }\quad \langle T,T \rangle \models t_{k,d}\text{ iff }{\tau }(k)=d \end{align*}

We also call $\tau$ the timing function induced by $\langle H,T \rangle$ .

Clearly, the last proposition extends to equilibrium models.

Given a timed $\textrm {HT}$ -trace $\mathbf{M} = (\langle H_k,T_k \rangle _{k \in [0..\lambda )},{\tau })$ of length $\lambda$ over $\mathcal{A}$ , we define $\theta (\mathbf{M})$ as $\textrm {HT}$ interpretation $ \langle H\cup X ,T\cup X \rangle$ where

\begin{align*} H &=\{a_k\in \mathcal{A}_k \mid 0 \leq k \lt \lambda , a\in H_k \} & T &=\{a_k\in \mathcal{A}_k \mid 0 \leq k \lt \lambda , a\in T_k \} \\ X &=\{t_{k, d} \mid {\tau }(k)=d, 0\leq k\lt \lambda , d\in \mathbb{N}\} \end{align*}

Note that $\theta (\mathbf{M})$ is an $\textrm {HT}$ interpretation timed wrt $\lambda$ .

Conversely, given an $\textrm {HT}$ interpretation $\langle H,T \rangle$ timed wrt $\lambda$ over $\mathcal{A}^{*}\cup {\mathcal{T}}$ and its induced timing function $\tau$ , we define $\sigma (\langle H,T \rangle )$ as the timed $\textrm {HT}$ -trace

\begin{align*} (\langle \{a\in \mathcal{A}\mid a_k\in H\}, \{a\in \mathcal{A}\mid a_k\in T\} \rangle _{k \in [0..\lambda )}, {\tau }) \end{align*}

In fact, both functions $\sigma$ and $\theta$ are invertibles, and we get a one-to-one correspondence between $\textrm {HT}$ interpretations timed wrt $\lambda$ and timed $\textrm {HT}$ -traces of length $\lambda$ .

Finally, we have the following completeness and correctness result.

3.2 Translation of plain metric logic programs to $\textrm {HT}_{\!c}$

We now present an alternative, refined formalization of the second and third parts, utilizing integer variables and difference constraints to capture the timing function more effectively. To this end, we use the logic of $\textrm {HT}_{\!c}$ to combine the Boolean nature of ASP with constraints on integer variables.

Given base alphabet $\mathcal{A}$ and $\lambda \in \mathbb{N}$ , we consider the $\textrm {HT}_{\!c}$ signature $\langle \mathcal{X},\mathcal{D},\mathcal{C} \rangle$ whereFootnote ⁵

\begin{align*} \mathcal{X} &= \mathcal{A}^{*} \cup \{ t_k \mid 0\leq k\lt \lambda \} \\ \mathcal{D} &= \{\boldsymbol{t}\}\cup \mathbb{N}\\ \mathcal{C} &= \{a=\boldsymbol{t}\mid a\in \mathcal{A}^{*}\} \cup \{x=d \mid x \in \mathcal{X}\setminus \mathcal{A}^{*},d\in \mathbb{N} \}\;\cup \\ &\quad \;\{x-{y}\leq d \mid x,{y} \in \mathcal{X}\setminus \mathcal{A}^{*}\in \mathbb{N}, d\in \mathbb{Z} \} \end{align*}

Rather than using Boolean variables, this signature represents timing functions $\tau$ directly by integer variables $t_k$ , capturing that $\tau (k)=t_k$ for $0\leq k\lt \lambda$ . This is enforced by the integer constraints in $\mathcal{C}$ , whose meaning is defined by the following denotations:

\begin{align*} [\![ \, a=\boldsymbol{t} \, ]\!] &= \{v\in \mathbb{V}\mid v(a)=\boldsymbol{t}\} \qquad \qquad \qquad \text{ for all }a\in \mathcal{A}^{*}\\ [\![ \, x=d \, ]\!] &= \{v\in \mathbb{V}\mid v(x), d\in \mathbb{N},\ v(x)= d\}\\ [\![ \, x-{y}\leq d \, ]\!] &= \{v\in \mathbb{V}\mid v(x),v({y})\in \mathbb{N},d\in \mathbb{Z},\ v(x)-v({y})\leq d\} \end{align*}

When dealing with Boolean variables, we simplify notation by representing $a=\boldsymbol{t}$ as $a$ .

This leads us to the following counterpart of $\Delta _{\lambda ,\nu }$ in equation (13). Given $\lambda \in \mathbb{N}$ , we define

(18) \begin{align} \Delta ^{c}_{\lambda } &= \{ t_{0} = 0 \} \cup \{ t_{k}-t_{k{+}1} \leq -1 \mid 0 \leq k \lt \lambda -1 \} \end{align}

Starting from $t_0=0$ , the difference constraints in equation (18) enforce that $t_{k}\lt t_{k{+}1}$ reflecting that $\tau (0)=0$ and ${\tau }(k)\lt {\tau }(k+1)$ for $0\leq k\lt \lambda -1$ . Moreover, $\Delta ^{c}_{\lambda }$ is unbound and thus imposes no restriction on timing functions. And no variable $t_{k}$ is ever undefined:

We also have $t(t_{k})\in \mathbb{N}$ by definition of $\textrm {HT}_{\!c}$ interpretations, that is, since $h\subseteq t$ .

Our variant of the third part of our translation re-expresses the ones in equations (14/15) in terms of integer variables and difference constraints. Given $\lambda \in \mathbb{N}$ and a plain metric logic program $P$ , we define

(19) \begin{align} \Psi ^{c}_{\lambda }({P}) = &\ \{ \bot \leftarrow (\beta )_{k} \wedge \neg (t_{k}-t_{k+1} \leq -m) \mid 0 \leq k \lt \lambda -1, \\ &\qquad \qquad \nonumber \phantom {n\in \mathbb{N},} \square ( {\bigcirc}_{[m..n)} a \leftarrow \beta ) \in {P}\} \; \cup \end{align}

(20) \begin{align} &\ \{ \bot \leftarrow (\beta )_{k} \wedge \neg (t_{k+1} - t_{k} \leq n - 1) \mid 0 \leq k \lt \lambda -1, \\&\qquad \qquad \nonumber n\in \mathbb{N}, \square ( {\bigcirc}_{[m..n)} a \leftarrow \beta ) \in {P}\} \end{align}

In fact, both $\Delta ^{c}_{\lambda }$ and $\Psi ^{c}_{\lambda }({P})$ drop the upper bound on the range of a timing function, as required in their Boolean counterparts. Hence, their size is only proportional to $\mathcal{O}(\lambda )$ , and thus considerably smaller than their purely Boolean counterparts.

For the rule in equation (10), we get

(21) \begin{align} \bot &\leftarrow \textit {at}(\textit {ram},\textit {office})_k\wedge \textit {go}(\textit {ram},\textit {home})_k\wedge \neg (t_{k}-t_{k+1} \leq -15) \end{align}

(22) \begin{align} \bot &\leftarrow \textit {at}(\textit {ram},\textit {office})_k\wedge \textit {go}(\textit {ram},\textit {home})_k\wedge \neg (t_{k+1} - t_{k} \leq 15) \end{align}

for $0 \leq k \lt \lambda -1$ . Given $\lambda =100$ , this only amounts to $10^2$ instances.

Mirroring our approach in Section 3.1, we capture the meaning of $\Delta ^{c}_{\lambda }$ using specialized $\textrm {HT}_{\!c}$ -models. This leads to the completeness and correctness of our translation.

As above, we call $\tau$ the timing function induced by $\langle h,t \rangle$ .

Unlike Proposition1, the latter refrain from requiring $\textrm {HT}_{\!c}$ -interpretations in equilibrium.

Given an $\textrm {HT}$ -trace $\mathbf{M} = (\langle H_k,T_k \rangle _{0 \leq k \lt \lambda },{\tau })$ of length $\lambda$ , we define $\theta ^c(\mathbf{M})$ as the $\textrm {HT}_{\!c}$ interpretation $ \langle h\cup x,t\cup x \rangle$ where $h,t,x$ are valuations such that

\begin{align*} h &=\{(a_k,\boldsymbol{t}) \mid 0 \leq k \lt \lambda , a\in H_k \} & t &=\{(a_k,\boldsymbol{t}) \mid 0 \leq k \lt \lambda , a\in T_k \} \\ x &= \{(t_{k},d) \mid {\tau }(k)=d, 0\leq k\lt \lambda , d\in \mathbb{N} \} \end{align*}

Similar to above, $\theta ^c(\mathbf{M})$ is an $\textrm {HT}_{\!c}$ interpretation timed wrt $\lambda$ .

Conversely, given an $\textrm {HT}_{\!c}$ interpretation $\langle h,t \rangle$ timed wrt $\lambda$ and its induced timing function $\tau$ , we define $\sigma ^c(\langle h,t \rangle )$ as the timed $\textrm {HT}$ -trace

\begin{align*} (\langle \{a\mid h(a_k)=\boldsymbol{t}\}, \{a\mid t (a_k)=\boldsymbol{t}\} \rangle _{0 \leq k \lt \lambda }, {\tau }) \end{align*}

As above, functions $\sigma ^c$ and $\theta ^c$ are invertibles. Hence, we get a one-to-one correspondence between $\textrm {HT}_{\!c}$ interpretations timed wrt $\lambda$ and timed $\textrm {HT}$ -traces of length $\lambda$ .

Finally, we have the following completeness and correctness result.

4.1 Base translation of general metric logic programs

Analogous to Section 3, our translation of general metric logic programs is divided into two parts: a basic temporal component that addresses state transitions, and metric components that map timing functions to either $\textrm {HT}$ or $\textrm {HT}_{\!c}$ . The metric components are detailed in Sections 4.2 and 4.3. In the following, we focus on the basic temporal component.

Given a metric logic program $P$ over $\mathcal{A}$ and $\lambda \in \mathbb{N}$ , we define

(29) \begin{align} {\boldsymbol{\Pi }}_\lambda ({P}) & = \{ (r)_{k} \mid \square {r} \in P, 0 \leq k \lt \lambda \} \cup \textstyle \bigcup _{\varphi \in r, \square {r} \in {P}, 0 \leq k \lt \lambda } \eta _k^*(\varphi ) \end{align}

where $(r)_{k}$ is obtained from $r$ by replacing in $r$ each metric atom $\mu$ by $L_{\mu }^{k}$ .

The Tseitin-style translation of each metric formula in $r$ is given in the right column of Table 3. It relies on additional auxiliary atoms of form ${L_{\varphi }^{k}}$ , ${L_{\varphi }^{k,j}}$ and $\delta _{I}^{k,j}$ . Atoms of form ${L_{\varphi }^{k}}$ provide an equivalence to the satisfaction of $\varphi$ at state $k$ . Atoms of form ${L_{\varphi }^{k,j}}$ are used to define ${L_{\varphi }^{k}}$ and indicate state $j$ as a witness to the truth of $\varphi$ at state $k$ . Atoms of form $\delta _{I}^{k,j}$ provide the link to the respective encoding of metric information, defined in the next two sections. Specifically, $\delta _{I}^{k,j}$ indicates whether a transition between states $k$ and $j$ fails to be done within the time allotted by interval $I$ , viz. ${\tau }(j)-{\tau }(k)\notin I$ . Interestingly, such atoms only occur in rule bodies in $\eta ^*_k(\varphi )$ .

Table 3.

Definition of sets $\eta _k(\varphi )$ and $\eta _k^*(\varphi )$ for any metric atom $\varphi$ and $0 \leq k \lt \lambda$

Table 3. Long description

The table presents the Tseitin-style translation of metric formulas. It includes a left column with formulas and a right column with their translations. The translations use auxiliary atoms of different forms. Atoms of the form a_k raised to the power of L_a_k are used for equivalence to the satisfaction of a at state k. Atoms of the form L_k_f are used to define and indicate state k as a witness to the truth of F at state k. Atoms of the form L_k_I provide the link to the respective encoding of metric information. The table also includes rules for different types of formulas, such as conjunctions, disjunctions, implications, and negations. Each rule shows how the formulas are translated into the auxiliary atoms.

For illustration consider the metric rule in equation (27). Our translation first yields:

(30) \begin{align} {{L_{\bot }^{k}}} &\leftarrow {{L_{\boldsymbol{\mathsf{I}}}^{k}}} \wedge \neg {{L_{\Diamond _{\leq 60}\,\textit {goal}}^{k}}}& \quad \text{ for }0 \leq k \lt \lambda \end{align}

Followed by the implications obtained from the translation of each metric formula in the rule:

(31) \begin{align} {{L_{\bot }^{k}}} &\leftrightarrow \bot & \quad \text{ for }0 \leq k \lt \lambda \end{align}

(32) \begin{align} L_{\boldsymbol{\mathsf{I}}}^{0} &\leftrightarrow \top & \end{align}

(33) \begin{align} L_{\boldsymbol{\mathsf{I}}}^{k} &\leftrightarrow \bot & \quad \text{ for }{{0 \leq k \lt \lambda -1}} \end{align}

(34) \begin{align} L_{\textit {goal}}^{k} &\leftrightarrow \textit {goal}_k & \quad \text{ for }0 \leq k \lt \lambda \end{align}

(35) \begin{align} L_{\Diamond _{\leq 60\,\textit {goal}}}^{k} &\leftrightarrow \bigvee _{j=k}^{\lambda -1} {{L_{{\Diamond }_{I} \textit {goal}}^{k,j}}} & \quad \text{ for }0 \leq k \lt \lambda \end{align}

(36) \begin{align} L_{\Diamond _{\leq 60\,\textit {goal}}}^{k,j}& \leftrightarrow \neg {\delta _{I}^{k,j}} \wedge L_{\textit {goal}}^{j} & \quad \text{ for }0 \leq k \lt \lambda ,{{k \leq j \lt \lambda }} \end{align}

Observe that when $\delta _{I}^{k,j}$ is false, the witness of truth for $\Diamond _{\leq 60}\,\textit {goal}$ at state $j$ in equation (36) simplifies to $L_{\Diamond _{\leq 60}\,\textit {goal}}^{k,j}\leftrightarrow L_{\textit {goal}}^{j}$ . This indicates that the metric condition over the interval is trivially satisfied, allowing any state that meets the goal condition to serve as a witness, regardless of its associated time point. Conversely, for the $\square$ operator, such a simplification of $\delta _{I}^{k,j}$ would imply that all states lie within the interval. This would strengthen the witness requirements, enforcing compliance with the condition across all future states.

Clearly, our translation still bears redundancies and can be further optimized.

4.2 Translation of general metric logic programs to $\textrm {HT}$

This section extends the definition of timing functions within $\textrm {HT}$ from plain to general metric logic programs. Timing functions are formalized as in Section 3.1, utilizing a set of atoms $ {\mathcal{T}}=\{t_{k,d} \mid k,d\in \mathbb{N} \}$ and the axioms of $\Delta _{\lambda ,\nu }$ in equation (13). Each atom $t_{k,d}$ represents that $\tau (k)=d$ . The key distinction lies in the formalization of how these timing functions interact with the interval conditions specified in the program.

To this end, let $\mathbb{I}|_{{P}}$ stand for all intervals occurring in a metric logic program $P$ .

Given $\lambda ,\nu \in \mathbb{N}$ and a general metric program $P$ , we let

(37) \begin{align} {\boldsymbol{\Psi }}_{\lambda ,\nu }({P}) = & \ \{ \delta _{[m..n)}^{k,j} \leftarrow t_{k,d} \wedge t_{j,d'} \mid 0 \leq k \leq j \lt \lambda -1, 0\leq d\lt d'\leq \nu , \\ &\qquad \qquad d'-d \lt m, [m..n) \in \mathbb{I}|_{{P}} \}\; \cup \nonumber \end{align}

(38) \begin{align} & \ \{ \delta _{[m..n)}^{k,j} \leftarrow t_{k,d} \wedge t_{j,d'} \mid 0 \leq k \leq j \lt \lambda -1, 0\leq d\lt d'\leq \nu , \\ &\qquad \qquad d'-d \geq n, [m..n) \in \mathbb{I}|_{{P}}, n\in \mathbb{N} \}\;\nonumber \end{align}

Differing from the rule-oriented integrity constraints used to define $\Psi _{\lambda ,\nu }({P})$ in equations (14) and (15), we now utilize rules that directly signal interval condition violations. Each such violation is indicated by an atom $\delta _{I}^{k,j}$ , which signifies that the difference ${\tau }(j)-{\tau }(k)$ falls outside the interval $I$ , where $k$ and $j$ are indices representing specific time points.

For the interval $[15..16)$ in rule equation (10), we get

(39) \begin{align} \delta _{[15..16)}^{k,j}& \leftarrow t_{k,d} \wedge t_{j,d'} \quad \text{ for } d'-d \lt 15 \end{align}

(40) \begin{align} \delta _{[15..16)}^{k,j}& \leftarrow t_{k,d} \wedge t_{j,d'} \quad \text{ for } d'-d \geq 16 \end{align}

and $0 \leq k \leq j \lt \lambda -1$ , $0\leq d\lt d'\leq \nu$ . For $\lambda =100$ and $\nu =1000$ , this then amounts to roughly $10^{10}$ instances for each of the above constraints. Showing an increase by a factor of $10^2$ wrt. Section 3.1 which amounts for the addition of $j$ ranging from $k$ to $100$ . Since $\delta _{I}^{k,j}$ is used to express falling outside the interval, intervals like $[15..16)$ , with a distance of 1, generate the largest number of rules. On the other hand, the interval $[0..\omega )$ , used in rules equations (8) and (9), does not yield a single rule. Furthermore, the instance of rule equation (7) for moving from $\textit {atm}$ to $\textit {home}$ uses the same interval as rule equation (10), since the distance between these locations is the same. In contrast to Section 3.1, the rules for this interval condition are reused.

This approach culminates in the following completeness and correctness result.

The restriction to $\langle T,T \rangle |_{\mathcal{A}^{*}\cap {\mathcal{T}}}$ allows us to ignore auxiliary atoms.

4.3 Translation of general metric logic programs to $\textrm {HT}_{\!c}$

This section adapts the framework of the preceding one, utilizing $\textrm {HT}_{\!c}$ as the target system instead of $\textrm {HT}$ , for extending the definitions of plain metric programs from Section 3.2 to general ones. Specifically, we keep the $\textrm {HT}_{\!c}$ signature $\langle \mathcal{X},\mathcal{D},\mathcal{C} \rangle$ and extend the set $\mathcal{X}$ to include Boolean variables of the form $L_{\mu }^{k}$ $L_{\mu }^{k,j}$ and ${{\delta _{k}^{j,I}}}$ . The denotation for Boolean atoms, equalities, and difference constraints remains as defined in Section 3.2. Furthermore, we keep employing integer variables $ {\mathcal{T}}^c=\{ t_k \mid 0\leq k\lt \lambda \}$ to directly represent timing functions, such that $\tau (k)=t_k$ for $0\leq k\lt \lambda$ , adhering to the axioms of $\Delta ^{c}_{\lambda }$ in equation (18).

However, to formalize the interaction between these timing functions and the interval conditions specified in the program, we adopt the approach of the preceding section, deriving atoms of the form $\delta _{I}^{k,j}$ indicating that the difference ${\tau }(j)-{\tau }(k)$ falls outside interval $I$ .

(41) \begin{align} {\boldsymbol{\Psi }}^{c}_{\lambda }({P}) = & \ \{ \delta _{[m..n)}^{k,j} \leftarrow \neg (t_{k}-t_{j} \leq -m) \mid 0 \leq k \leq j \lt \lambda -1, [m..n) \in \mathbb{I}|_{{P}} \}\; \cup \end{align}

(42) \begin{align} & \ \{ \delta _{[m..n)}^{k,j} \leftarrow \neg (t_{j} - t_{k} \leq n - 1) \mid 0 \leq k \leq j \lt \lambda -1, [m..n) \in \mathbb{I}|_{{P}}, n\in \mathbb{N} \} \end{align}

For the interval $[15..16)$ in rule equation (10), we get

(43) \begin{align} \delta _{[15..16)}^{k,j}& \leftarrow \neg (t_{k}-t_{j} \leq -15) \end{align}

(44) \begin{align} \delta _{[15..16)}^{k,j}& \leftarrow \neg (t_{j} - t_{k} \leq 15) \end{align}

for $0 \leq k \leq j \lt \lambda -1$ . Given $\lambda =100$ , this amounts to $10^4$ instances, showing the same increase proportional $\lambda$ as in the $\textrm {HT}$ approach with respect to the plain metric fragment for $\textrm {HT}_{\!c}$ , due to the inclusion of $j$ .

To show completeness and correctness, we define the restriction of an $\textrm {HT}_{\!c}$ interpretation to an alphabet $\mathcal{A}$ as $ \langle h,t \rangle |_{\mathcal{A}} = {{\langle h|_{\mathcal{A}},t|_{\mathcal{A}} \rangle }}$ where $f|_{\mathcal{A}}$ is defined such that $f|_{\mathcal{A}}(a) = f(a)$ for all $a\in \mathcal{A}$ .

5.1 Implementation of plain metric logic programs

Lines 1 and 2 of Listing 5 realize the metric next operator, $ {\bigcirc}_{I}a$ , represented by term next(I,a). Together, Listing 3, 4 and 5 account for $\Pi _\lambda ({P})$ .

Listing 3.

Timed meta-encoding (meta.lp)

Listing 4.

Meta encoding for base metric operators (bounded-base.lp)

When expressing time via Boolean variables, the previous listings are combined with Listing 6 and 7 below, which realize $\Delta _{\lambda ,\nu }$ and $\Psi _{\lambda ,\nu }({P})$ , respectively. Atoms $t_{k,d}$ in $\mathcal{T}$ are represented by t(k,d). The upper bound $\nu$ on the timing function’s range is given by v, and $\omega$ is represented by w. The two encodings directly mirror the definitions of $\Delta _{\lambda ,\nu }$ and $\Psi _{\lambda ,\nu }({P})$ , with one key difference: the rule bodies in equations (14) and (15) are replaced in Lines 1 and 2 of Listing 7 by auxiliary atoms of predicate true/2.

Listing 5.

Meta encoding for metric operators of $\Pi _\lambda ({P})$ (bounded.lp)

Listing 6.

Meta encoding for $\Delta _{\lambda ,\nu }$ (time.lp)

Listing 7.

Meta encoding for $\Psi _{\lambda ,\nu }({P})$ (interval.lp)

When expressing time in terms of integer variables, we rely on difference constraints for modeling timing functions. Such simplified linear constraints have the form “ $x - y \leq d$ ” for $x,y\in \mathcal{X}$ and $d\in \mathbb{Z}$ and are supported by the clingo extensions clingcon (Banbara et al. Reference Banbara, Kaufmann, Ostrowski and Schaub2017) and clingo[dl] (Janhunen et al. Reference Janhunen, Kaminski, Ostrowski, Schellhorn, Wanko and Schaub2017). We use below clingcon’s syntax and represent them as “&sum x ; $y$ <= $d$ .” A Boolean atom $a$ can be seen as representing “ $a=\boldsymbol{t}$ .” In the case at hand, Listing 3, 4 and 5 are now completed by Listing 8 and 9 below. As above, they faithfully replicate the definitions of $\Delta ^{c}_{\lambda }$ and $\Psi ^{c}_{\lambda }({P})$ . Unlike above, however, the timing function is now captured by integer variables of form t(k) and its range restriction is now obsolete. The rules in Listing 8 mirror the two conditions on timing functions, namely, that t(0) equals zero and that the instances of t(K + 1) receive a strictly greater integer than the ones of t(K) for K ranging from 0 to lambda-1. Similarly, given that w stands for $\omega$ , the two rules in Listing 9 correspond to the difference constraints in equations (19) and (20).

Listing 8.

Meta encoding for $\Delta ^{c}_{\lambda }$ (time-c.lp)

Listing 9.

Meta encoding for $\Psi ^{c}_{\lambda }({P})$ (interval-c.lp)

As in Listing 7, we use auxiliary atoms of predicate true/2 rather than the corresponding rule bodies. Notably, we shifted in Listing 9 the difference constraints in equations (19) and (20) from the body to the head. This preserves (strong) equivalence in $\textrm {HT}_{\!c}$ whenever all variables comprised in a constraint atom are defined, as guaranteed by Proposition3.

In the two approaches at hand, we may compensate the lack of global metric operators in out example by replacing Line 1 by :- finally, not goal and enforcing the time limit either by setting $\nu$ to 60 in our $\textrm {HT}$ -based approach or by extending Listing 5 with &sumt(K) <= 60 :- time(K), not time(K + 1). in our $\textrm {HT}_{\!c}$ -based approach. However, this is only effective when the goal is achieved at the final step.

The example in Listing 1 is addressed with clingo in the following way.

When using clingcon instead, it suffices to replace the second line with:

Our choices of lambda and v allow for all movement combinations within the 4 steps required to reach the goal; we obtain in each case 27 solutions. Once we include the query-oriented additions from above, we obtain a single model instead.

5.2 Implementation of general metric logic programs

Listing 10 extends Listing 4 to account for the metric next operator $ {\bigcirc}_{I}b$ in Lines 1 to 5, the metric always operator $\square _{I}b$ in Lines 7 to 16, and the metric eventually operator ${\Diamond }_{I}b$ in Lines 18 to 25. These rules mirror the definitions of $\eta ^*_k(\varphi )$ in Table 3,Footnote ⁹ where atoms true(m,k) correspond to ${L_{\varphi }^{k}}$ , witnesses ${L_{\varphi }^{k,j}}$ are expressed via the atom wit(m,(k,j)), and interval violations ${{\delta _{i}^{k,j}}}$ are represented by iv(i,(k,j)). Together, Listings 3, 4, and 10 account for ${\boldsymbol{\Pi }}_\lambda ({P})$ .

Listing 10.

Meta encoding for metric operators of ${\boldsymbol{\Pi }}_\lambda ({P})$ (bounded.lp)

Listing 11.

Meta encoding for ${\boldsymbol{\Psi }}_{\lambda ,\nu }({P})$ (interval.lp)

Listing 12.

Meta encoding for ${\boldsymbol{\Psi }}^{c}_{\lambda }({P})$ (interval-c.lp)

When expressing time via Boolean variables, we reuse Listing 6 to implement $\Delta _{\lambda ,\nu }$ and define ${\boldsymbol{\Psi }}_{\lambda ,\nu }({P})$ in Listing 11 below. The two rules in Lines (1/2) and Lines (3/4) correspond to equation (37) and (38), respectively, where predicate i/1 collects the intervals in $\mathbb{I}|_{{P}}$

When expressing time using integer variables, we rely on difference constraints to model timing functions, as described in the previous section. We reuse Listing 8 to implement $\Delta ^{c}_{\lambda }$ and define ${\boldsymbol{\Psi }}^{c}_{\lambda }({P})$ in Listing 12 below. The two rules in Listing 12 correspond to rules equations (41) and (42).

The example in Listing 1 can be addressed using clingo and clingcon in the same manner as before. However, this fragment accommodates the goal condition from Listing 2. Listing 13 displays the corresponding clingo output. For readability, we ordered the output atoms and omitted all predicates except t/2, go/3, and at/3. The output presents the expected optimal plan for reaching the dentist on time. Line 6 details Ram’s actions (traveling from the office to the ATM, then home, and finally to the dentist), while Lines 7–9 track his location and the items he acquires. The timing function is encoded as normal atoms over the predicate t/2 (Line 11); the time difference between consecutive states corresponds to the distance between locations, achieving the goal in 55 minutes.

Listing 13.

System output showcasing the dentist example using clingo

The clingcon output (Listing 14) differs only in its representation of the timing function, which utilizes integer variables and is presented separately as assignments in Lines 11 and 12.

Listing 14.

System output showcasing the dentist example using clingcon

5.3 Results

In this section, we present some empirical results on the scalability of both approaches. We use clingo 5.8.0 (Kaminski et al. Reference Kaminski, Romero, Schaub and Wanko2023) for $\textrm {HT}$ , and clingcon 5.2.1 (Banbara et al. Reference Banbara, Kaufmann, Ostrowski and Schaub2017) and clingo[dl] 1.5.0 (Janhunen et al. Reference Janhunen, Kaminski, Ostrowski, Schellhorn, Wanko and Schaub2017) for $\textrm {HT}_{\!c}$ . In our setting, the solutions computed by clingcon coincide with those defined by $\textrm {HT}_{\!c}$ , while clingo[dl] returns only assignments where the time points take the smallest possible positive integer values.

Experimental setup. We evaluated our implementation on three problem domains. For each of them, we developed a novel metric encoding. The first is the dentist scenario, used to compare both metric fragments, plain ( $P$ ) and general ( $G$ ), and to study the scalability of each approach and the overhead introduced by the general fragment. In this domain, we enumerate all models to ensure full inspection of the search space, with and without the goal condition. Since the formalization uses only intervals of size one, the minimality condition of clingo[dl] does not reduce the number of models. The second domain is Multi-Agent Path Finding (Stern et al. Reference Stern, Sturtevant, Felner, Koenig, Ma, Walker, Li, Atzmon, Cohen, Kumar, Barták and Boyarski2019). It is evaluated only for the general fragment, because the representation requires global temporal operators ( $\Diamond _I$ , $\Box _I$ ) to express multi-agent coordination and goal conditions, which are not available in the plain fragment. In this domain, we analyze the scalability of the general fragment across all approaches in a more complex setting. We compute a single model, as enumeration would lead to a very large number of models, so the minimality imposed by clingo[dl] only affects which model is returned. The metric representation is based on the ASP encoding from Behrens et al. (Reference Behrens, Kaminski, Schaub, Son, Švancara and Wanko2024). The third domain is Job-Shop Scheduling. It is evaluated in the general fragment, computing a single model. Here, we analyze the impact of varying the horizon on the overall scalability of each approach. The metric encoding is inspired by Hustadt et al. (Reference Hustadt, Ozaki and Dixon2020).

We conducted all experiments on a clusterFootnote ¹⁰ with Intel Xeon E5-2650v4@2.9 GHz CPUs and 64 GB of memory, running Debian Linux 10, imposing per instance a timeout of 20 minutes and a memory limit of 20 GB.

Table 4.

Results for clingo, clingcon and clingo[dl] without goal condition (times in seconds; – represents a memout)

Table 4. Long description

The table compares the performance metrics for clingo, clingcon, and clingo[dl] without goal condition. It has 10 rows and 12 columns. The columns are labeled as Solve, Ground, and #Rules for each of the three tools. The rows are labeled with numbers 1, 4, 7, and 10. Row 1: P, 0.03, 1.07, 297,383, 0.01, 0.14, 2337, 0.01, 0.14, 2337. Row 1: G, 0.29, 0.61, 334,458, 0.01, 0.22, 2572, 0.01, 0.16, 2572. Row 4: P, 1.65, 21.61, 4,812,563, 0.01, 0.18, 2337, 0.01, 0.14, 2337. Row 4: G, 36.37, 15.80, 5,395,908, 0.01, 0.19, 2572, 0.01, 0.19, 2572. Row 7: P, 16.58, 79.35, 14,772,743, 0.01, 0.14, 2337, 0.01, 0.13, 2337. Row 7: G, 81.56, 67.55, 16,555,758, 0.02, 0.21, 2572, 0.01, 0.16, 2572. Row 10: P, 0.01, 0.15, 2337, 0.01, 0.18, 2337, 0.02, 0.23, 2572. Row 10: G, 0.02, 0.19, 2572, 0.01, 0.23, 2572.

5.3.1 Dentist scenario

In our first setting, we use the running example from Listing 1. As explained before, we select lambda = 4 and v = 110 to generate all movement combinations within the 4 steps required to reach the goal, resulting in 27 solutions. To investigate scalability, we multiply both the durations in Table 1 and the time limit v by a factor $f\in \{1, 4, 7, 10\}$ . The results are summarized in Table 4. They show that clingo does not scale well. This is most clear at $f=10$ , where it reaches the memory limit while grounding. In contrast, the performance of clingcon and clingo[dl] is independent of the time granularity, for both fragments $P$ and $G$ . The inner workings of both systems differ, but in this simple example their behavior is essentially the same. As anticipated in Sections 4.2 and 4.3, there is a linear increase in the number of rules of $G$ with respect to $P$ . The additional rules enable the next operator $ {\bigcirc}_{I}$ in the body and define auxiliary atoms representing interval violations. These additions may explain why the general fragment relies more on solving than the plain one, as observed in Table 4. Note that the global metric operators ${\Diamond }_{I}$ and $\square _{I}$ are not used in this setting, and consequently the intelligent grounder does not produce the corresponding ground rules.

In our second setting, we include the goal constraint from Listing 2, which can only be handled by the general fragment. We use the same parameters as before. In particular, we enumerate all models, but in this case there is always a single one. The results are summarized in Table 5. As before, clingo does not scale well, while the performance of clingcon and clingo[dl] is independent of the time granularity. The number of rules increases as expected, due to the goal constraint and the rules required to account for the metric eventually ${\Diamond }_{I}$ occurring in it. For clingo the inclusion of the goal condition leads to a slight increase in grounding time, while solving time decreases since the goal constraint significantly reduces the number of models.

Table 5.

Results for clingo, clingcon and clingo[dl] with goal condition, (times in seconds; – indicates the memory limit was reached)

Table 5. Long description

The table compares the performance of clingo, clingcon, and clingo[dl] with a goal condition. It has 4 rows and 10 columns. The columns are labeled as follows: f, Solve (clingo), Ground (clingo), #Rules (clingo), Solve (clingcon), Ground (clingcon), #Rules (clingcon), Solve (clingo[dl]), Ground (clingo[dl]), and #Rules (clingo[dl]). The row labels are 1, 4, 7, and 10. Row 1: f, 0.10, 0.73, 377301, 0.01, 0.19, 2731, 0.01, 0.20, 2731. Row 4: G, 28.33, 15.69, 6092421, 0.01, 0.21, 2731, 0.01, 0.19, 2731. Row 7: G, 17.20, 77.04, 18694341, 0.01, 0.18, 2731, 0.01, 0.21, 2731. Row 10: G, 0.01, 0.23, 2731, 0.01, 0.19, 2731. The table shows the solving and grounding times in seconds and the number of rules for each method and granularity level.

5.3.2 Multi-agent path finding

Multi-Agent Path Finding (MAPF, Stern et al. (Reference Stern, Sturtevant, Felner, Koenig, Ma, Walker, Li, Atzmon, Cohen, Kumar, Barták and Boyarski2019)) is the problem of finding a plan for a set of agents that move from their start to goal positions. The agents move on a map represented as a graph $({{\mathcal{V}}},{{\mathcal{E}}})$ where vertices in ${\mathcal{V}}$ represent locations and edges in ${\mathcal{E}}$ represent movements between locations, each with a duration. A valid plan is a sequence of movements for each agent, free of vertex conflicts and swap conflicts. Vertex conflicts occur when two agents occupy the same vertex at the same time, and swap conflicts occur when two agents traverse the same edge in opposite directions at the same time.

Our formalization adapts the ASP encoding of (Behrens et al. (Reference Behrens, Kaminski, Schaub, Son, Švancara and Wanko2024), Listing 5) to the metric logic program in equations (45)–(53), capturing movement durations by the timing function. We use letters $\textit {U}$ and $\textit {V}$ to denote vertices from ${\mathcal{V}}$ , and if $(\textit {U}, \textit {V}) \in {{\mathcal{E}}}$ , the duration of the movement is given by $\delta (\textit {U},\textit {V})$ . We use letters $A$ and $B$ to denote agents, and each agent $A$ has a start vertex $S_A \in {{\mathcal{V}}}$ and a goal vertex $G_A \in {{\mathcal{V}}}$ .

Rule equation (45) captures the initial position of each agent. Rule equation (46) chooses a possible movement along an edge $(\textit {U},\textit {V})$ . Rule equation (47) captures the effect of moving from $\textit {U}$ to $\textit {V}$ , which takes exactly $\delta (\textit {U},\textit {V})$ time units. We use the eventually operator rather than the next operator so that different agents may move asynchronously. Rule equation (48) captures inertia: an agent remains at its current vertex $\textit {U}$ if it does not move along any edge $(\textit {U}, \textit {V})$ . Following (Behrens et al. Reference Behrens, Kaminski, Schaub, Son, Švancara and Wanko2024), an agent is at no vertex while moving, but reappears at the target vertex $\textit {V}$ upon arrival. Rule equation (49) ensures that a movement is only possible if the agent is currently at the source vertex $\textit {U}$ . This also prevents another action from being taken until the current movement is completed. Rule equation (50) enforces that each agent moves at most once per time point, given that $(\textit {U},\textit {V})$ and $(\textit {U\,}',\textit {V\,}')$ are distinct edges. Rule equation (51) enforces the absence of vertex conflicts, given that $A \neq B$ . Rule equation (52) enforces the absence of swap conflicts using the eventually operator to ensure that no swap conflict arises during the traversal of an edge. Finally, Rule equation (53) enforces the goal condition: every agent must be at its goal vertex at the end of the plan.

(45) \begin{align} \square (\textit {at}(A, S_A) &\leftarrow \boldsymbol{\mathsf{I}}) \end{align}

(46) \begin{align} \square (\textit {move}(A,\textit {U},\textit {V}) \vee \neg \textit {move}(A,\textit {U},\textit {V}) &\leftarrow \neg \boldsymbol{\mathsf{F}}) \quad \quad \quad \quad \quad \quad (\textit {U},\textit {V})\in {{\mathcal{E}}} \end{align}

(47) \begin{align} \square (\Diamond _{{{[\delta (\textit {U},\textit {V})..\delta (\textit {U},\textit {V})+1)}}}{\textit {at}(A,\textit {V})} &\leftarrow \textit {move}(A,\textit {U},\textit {V})) \end{align}

(48) \begin{align} \square ( {\bigcirc}_{[0..\omega )}{\textit {at}(A,\textit {U})} &\leftarrow \neg \boldsymbol{\mathsf{F}} \wedge \textit {at}(A,\textit {U}) \wedge \bigwedge _{(\textit {U},\textit {V})\in {{\mathcal{E}}}} \neg \textit {move}(A,\textit {U},\textit {V})) \end{align}

(49) \begin{align} \square (\bot &\leftarrow \textit {move}(A,\textit {U},\textit {V}) \wedge \neg \textit {at}(A,\textit {U})) \end{align}

(50) \begin{align} \square (\bot &\leftarrow \textit {move}(A,\textit {U},\textit {V}) \wedge \textit {move}(A,\textit {U\,}',\textit {V\,}')) \quad (\textit {U},\textit {V})\neq (\textit {U\,}',\textit {V\,}') \end{align}

(51) \begin{align} \square (\bot &\leftarrow \textit {at}(A,\textit {U}) \wedge \textit {at}(B,\textit {U})) \quad \quad \quad \quad \quad \quad \quad \quad \ \ A\neq B \end{align}

(52) \begin{align} \square (\bot &\leftarrow \textit {move}(A,\textit {U},\textit {V}) \wedge \Diamond _{{{[0..\delta (\textit {U},\textit {V}))}}}{\textit {move}(B,\textit {V},\textit {U})}) \end{align}

(53) \begin{align} \square (\bot &\leftarrow \textit {goal}(A,\textit {U}) \wedge \neg \textit {at}(A,\textit {U}) \wedge \boldsymbol{\mathsf{F}}) \end{align}

Experiments. We conducted experiments in two settings using the encoding in Listing 15, which is a direct mapping of the rules above. In each case, we computed one solution.

Listing 15.

Metric logic program for MAPF

A preliminary evaluation showed that clingcon was not able to find a solution without a time-point limit. The reason is that the MAPF encoding allows all agents to remain idle, resulting in an unbounded timing function $\tau$ . This is not the case in the dentist scenario, where at each state there must be a movement that constrains $\tau$ . This poses a challenge for clingcon, which attempts to assign times to states without a bound, and stalls during solving. In contrast, clingo[dl] selects the smallest possible positive values, naturally bounding the search space. To address this issue while ensuring a fair comparison across all approaches, we impose the time-point limit $\nu$ (used in the $\textrm {HT}$ approach) also for clingcon and clingo[dl] in the $\textrm {HT}_{\!c}$ approach, by adding a numerical constraint enforcing assignments to be smaller than $\nu$ .

Fig. 2.

Empty grid (6 × 6).

Fig. 3.

Random grid (8 × 8).

In the first setting, we study the scalability of the general fragment and test the time-granularity independence of the $\textrm {HT}_{\!c}$ approach in a more complex scenario. We use an empty grid map of size $6 \times 6$ (Figure 2) generated by the framework of Behrens et al. (Reference Behrens, Kaminski, Schaub, Son, Švancara and Wanko2024). We connect vertices with edge durations ranging from 1 to 5 time units, vary the number of agents from 1 to 4, and scale edge durations by a factor $f \in \{1, 5, 10, 15, 20, 25, 30, 35\}$ , solving all combinations with $\lambda = 10$ and $\nu = 15 \cdot f$ . Figure 6 shows the performance of each approach across the different scaling factors. The reported time is the total time to find the first solution, and the shaded area below each line indicates the grounding time. The $\textrm {HT}$ approach using clingo exhibits behavior similar to before: larger edge durations lead to higher runtimes and early timeouts, as well as higher grounding times, visible in the light green shaded area for the single-agent case but not for larger instances due to timeouts. In contrast, the $\textrm {HT}_{\!c}$ approaches with clingcon and clingo[dl] show stable performance across all scaling factors, confirming their independence from time granularity. Their grounding time is negligible across all agent counts, but the total time increases with the number of agents, as expected. Overall, clingo[dl] performs better than clingcon. Figure 7 shows the number of ground rules generated by each approach. The number of rules for clingo grows rapidly as the factor increases, while for clingcon and clingo[dl] the number of rules remains independent of the time granularity, growing only slightly with the number of agents due to the additional rules introduced per agent. The instances where clingo timed out are also plotted, as the timeout was reached during solving rather than grounding.

Fig. 4.

Room grid (8 × 8).

Fig. 5.

Warehouse grid (8 × 8).

Fig. 6.

Total times for empty 6 × 6 grid MAPF instances with increasing number of agents. The shaded areas under the lines represent grounding time.

Fig. 6. Long description

Four line graphs depict the total times for empty 6 by 6 grid MAPF instances with an increasing number of agents. Each graph represents a different number of agents: 1, 2, 3, and 4. The x-axis is labeled ‘“and the y-axis is labeled ”Time (s)’. The graphs compare the performance of three systems: clingo, clingcon, and clingo-dl. The legend indicates that green squares represent clingo, black dots represent clingcon, and blue crosses represent clingo-dl. Red crosses indicate timeout, and yellow circles indicate memout. The shaded areas under the lines represent grounding time. In the graph for 1 agent, clingo shows a significant increase in time as ‘“ increases, while clingcon and clingo-dl maintain relatively low and stable times. For 2 agents, clingo again shows a sharp increase in time, with clingcon and clingo-dl remaining low and stable. For 3 agents, clingo times out for higher values of ”’, while clingcon and clingo-dl continue to perform consistently. For 4 agents, clingo times out for all values of “f” above 10, with clingcon and clingo-dl showing stable and low times throughout.”, “EDH”: ”

Fig. 7.

Number of ground rules for empty 6 × 6 grid MAPF instances with increasing number of agents.

Fig. 8.

Total times for 8 × 8 grid MAPF instances with increasing horizon. The shaded areas under the lines represent grounding time.

Fig. 8. Long description

Three line graphs depict the total times for 8 by 8 grid multi-agent pathfinding (MAPF) instances with increasing horizons. Each graph represents a different scenario: Random, Room, and Warehouse. The x-axis in all graphs represents the horizon (λ) ranging from 15 to 45, and the y-axis represents time in seconds. The graphs compare three systems: clingo, clingcon, and clingo-dl, with clingo represented by green squares, clingcon by dark blue circles, and clingo-dl by light blue triangles. Red crosses indicate timeouts. The shaded areas under the lines represent grounding time. In the Random scenario, clingo shows high variability and frequent timeouts, while clingcon and clingo-dl maintain lower and more consistent times. In the Room scenario, all systems perform relatively consistently with minor fluctuations. In the Warehouse scenario, clingo initially shows high times and timeouts but improves with increasing horizon, while clingcon and clingo-dl remain stable and low throughout.

In the second setting, we study the effect of relaxing the horizon on solver performance across different map structures. We generated three MAPF instances on $8 \times 8$ grids, each with a different map layout: random, room, and warehouse (Figures 3, 4, and 5, respectively), fixing the number of agents to three, and sampling edge durations between 1 and 5 time units. We set a time-point limit of $\nu = 100$ and vary the horizon $\lambda$ from $15$ to $45$ in steps of $5$ . The results are shown in Figure 8. Compared to the previous setting, grounding has a more pronounced impact, reflecting the larger map size and higher time-point limit. Clingo[dl] achieves the best performance across all three layouts. The behavior of clingcon is more irregular across layouts and values of $\lambda$ , and requires further investigation. In general, as $\lambda$ increases, solving becomes faster because the problem becomes less constrained. However, clingo’s grounding time grows with $\lambda$ , creating a tradeoff that yields an optimal operating point, beyond which total time increases again. This underscores the importance of selecting an appropriate horizon $\lambda$ .

5.3.3 Job-shop scheduling

In the Job-Shop Scheduling problem, there is a set of jobs $\mathcal{J}$ , operations $\mathcal{O}$ and machines $\mathcal{M}$ . Each job $J\in \mathcal{J}$ consists of a sequence of operations. Each operation $O\in \mathcal{O}$ belongs to a single job and must be processed on machine $\mu (O)$ for a duration $\delta (O)$ . By $\textit {prev}(O)$ we denote the operation that precedes $O \in \mathcal{O}$ in the sequence, if it exists. The goal is to find a schedule such that all operations are completed in order within the given time.

Our formalization as a general metric logic program is shown in equations (54)–(59). For some operation $O$ , the atom $\textit {start_run}_{O}$ represents its start, $\textit {run}_{O}$ represents that it is running, $\textit {has_run}_O$ that it has already run, and $\textit {wait}_{O}$ that it is waiting. Rule equation (54) captures the non-deterministic choice to start an operation, provided it has not yet completed. Rule equation (55) represents the execution of an operation for its duration, and Rule equation (56) captures its completion after that duration. Rule equation (57) prevents two distinct operations from running on the same machine at the same time, and Rule equation (58) prevents an operation from starting if its preceding operation in the job has not yet completed. Finally, Rule equation (59) enforces that all operations complete by the end of the trace.

(54) \begin{align} \square (\textit {wait}(\textit {O})\vee \textit {start_run}_{\textit {O}} &\leftarrow \neg \textit {has_run}_{\textit {O}}) \end{align}

(55) \begin{align} \square (\square _{{{[0..\delta (\textit {O}))}}}{\textit {run}_{\textit {O}}} &\leftarrow \textit {start_run}_{\textit {O}}) \end{align}

(56) \begin{align} \square (\square _{{{[\delta (\textit {O})..\omega )}}}{\textit {has_run}_{\textit {O}}} &\leftarrow \textit {start_run}_{\textit {O}}) \end{align}

(57) \begin{align} \square (\bot &\leftarrow \textit {run}_{\textit {O}} \wedge \textit {run}_{\textit {O}'}) \quad \quad \quad O \neq O'\text{ and }\mu (\textit {O})=\mu (\textit {O}') \end{align}

(58) \begin{align} \square (\bot &\leftarrow \textit {start_run}_{\textit {O}} \wedge \neg \textit {has_run}_{\textit {prev}(\textit {O})}) \end{align}

(59) \begin{align} \square (\bot &\leftarrow \neg \textit {has_run}_{\textit {O}} \wedge \boldsymbol{\mathsf{F}}) \end{align}

Experiments. We study the impact of varying the horizon on the overall scalability of each approach. We evaluate the benchmark instance ft06 from Muth and Thompson (Reference Muth and Thompson1963), which consists of $6$ jobs, $6$ machines, and $36$ operations. The experiments were performed with the known optimal makespan of $55$ , and in a relaxed setting with a time-point limit of $110$ (double the optimal makespan), to analyze the impact of enforcing optimality via the time-point limit. The benchmark instance is translated into ASP facts using predicates operation/1 for $\text{\em O}$ , machine/2 for $\mu$ , duration/2 for $\delta$ , and job/2 for the job assignment. The order of operations is captured by incremental numerical identifiers. The encoding, shown in Listing 16, is a direct mapping of Rules equations (54)–(59).

Listing 16.

Metric logic program for Job-Shop Scheduling

Fig. 9.

Total times for ft06 with time-point limit $\nu = 55$ .

Fig. 9. Long description

A line graph with the horizontal axis labeled lambda and the vertical axis labeled Time in seconds. The graph includes three data series: clingo, clingcon, and clingo-dl, each represented by different markers and colors. The legend indicates the markers for each series: squares for clingo, circles for clingcon, and triangles for clingo-dl. Additionally, there are vertical dashed lines indicating UNSAT and red crosses indicating timeouts. The clingo series shows a peak around lambda values 15 to 30, with timeouts beyond lambda 30. The clingcon series fluctuates with lower times compared to clingo, without any timeouts. The clingo-dl series also shows fluctuations, with timeouts around lambda values 20 to 30. The UNSAT lines appear around lambda values 10 and 15.

Figure 9 shows the performance of each approach across different values of $\lambda$ , with the time-point limit $\nu$ fixed to the known optimal makespan of $55$ . The problem is unsatisfiable for $\lambda \in \{10, 15\}$ ; with the optimal time-point limit of $55$ , a horizon of $\lambda \gt 15$ is required to obtain a solution. Clingo times out for $\lambda \in \{20, 25, 30\}$ , while clingcon and clingo[dl] time out at $\lambda = 25$ . For all other satisfiable instances, clingcon and clingo[dl] are significantly faster than clingo. Unlike in the previous applications, clingcon shows overall better performance than clingo[dl] in this setting, though this warrants further analysis of the constraint solvers’ internal behavior. The solving time for clingo generally decreases as $\lambda$ increases beyond $35$ , which can be attributed to the fact that a smaller horizon makes the problem harder to solve, similarly to the MAPF results. The fast response observed at $\lambda = 50$ for all approaches can be attributed to the fact that, with a time-point limit of $55$ , this horizon is very close to an identity mapping for $\tau$ , which simplifies the search considerably. The grounding time is negligible for all approaches, as this job-shop instance is designed to be hard to solve but not to ground.

Figure 10 shows the results with a relaxed time-point limit of $110$ . Relaxing the time-point limit eliminates most of the timeouts observed for clingo and removes the erratic behavior seen in Figure 9, with only $\lambda = 10$ remaining unsolvable within the time limit. The $\textrm {HT}_{\!c}$ approach finds a solution immediately across all satisfiable instances. As in the previous applications, the grounding time for clingo grows with the horizon, so the relaxed time-point limit benefits smaller horizons where solutions can be found, but introduces overhead for larger ones. Figures 11 and 12 show that the number of ground rules for clingo grows linearly with $\lambda$ , reflecting the propositional grounding of time-step constraints, whereas clingcon and clingo[dl] maintain a compact representation independent of the time-point limit.

Fig. 10.

Total times for ft06 with relaxed time-point limit $\nu = 110$ .

Fig. 11.

Number of ground rules for ft06 with time-point limit $\nu = 55$ .

Fig. 12.

Number of ground rules for ft06 with relaxed time-point limit $\nu = 110$ .