# Metric Dynamic Equilibrium Logic

Arvid Beckera, Pedro Cabalarb, Martín Diéguezc, Luis Fariñasd, Torsten
Schauba, Anna Schuhmanna CONTACT Arvid Becker. Email: arvid.becker@uni-
potsdam.de aUniversity of Potsdam, Germany; bUniversity of Corunna, Spain;
cUniversité d’Angers, France; dUniversité de Toulouse, France

###### 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. In many applications, however, timing
constraints are important like, for instance, when planning and scheduling go
hand in hand. We address this by developing a metric extension of linear-time
Dynamic Equilibrium Logic, in which dynamic operators are constrained by
intervals over integers. The resulting Metric Dynamic Equilibrium Logic
provides the foundation of an ASP-based approach for specifying qualitative
and quantitative dynamic constraints. As such, it constitutes the most general
among a whole spectrum of temporal extensions of Equilibrium Logic. In detail,
we show that it encompasses Temporal, Dynamic, Metric, and regular Equilibrium
Logic, as well as its classic counterparts once the law of the excluded middle
is added.

##  1 Introduction

Reasoning about action and change, or more generally reasoning about dynamic
systems, is not only central to knowledge representation and reasoning but at
the heart of computer science (Fisher ., 2005). In practice, this often
requires both qualitative as well as quantitative dynamic constraints. For
instance, when planning and scheduling go hand in hand, actions may have
durations and their effects may need to meet deadlines.

Over the last years, we addressed qualitative dynamic constraints by combining
traditional approaches, like Dynamic and Linear Temporal Logic (DL (Harel .,
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 ., 2018; Cabalar, Diéguez Schaub, 2019) and TEL (Cabalar
Vega, 2007; Aguado ., 2013; Cabalar ., 2018; Aguado ., 2023)) that gave rise
to the temporal ASP system telingo (Cabalar, Kaminski ., 2019; Cabalar,
Diéguez ., 2020) extending the ASP system clingo (Gebser ., 2016).

A commonality of 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 at any time 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 logics, TEL and DEL, on the same
linear-time semantics embodied by sequences of states. We continued to
maintain the same linear-time semantics when elaborating upon a first “light-
weight” metric temporal extension of HT (Cabalar, Diéguez ., 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 expressing that, if the machine is used, it has to be cleaned
within the next 3 states, viz.
$\square(\mathit{use}\to{\Diamond}_{(1..3)}\mathit{clean})$. Although this
permits the restriction of temporal operators to subsequences of states, no
fine-grained timing constraints are expressible.

In (Cabalar ., 2022), we filled this gap in the context of temporal logic by
associating each state with its _time_ , as done in Metric Temporal Logic (MTL
(Koymans, 1990)). This resulted in a non-monotonic metric temporal extension
of HT, referred to as MEL. It 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:

$\displaystyle\square(\mathit{use}\to{\Diamond}_{(60..120)}\mathit{clean})\ .$
(1)

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 (that is, using real numbers). We rather
adapt a discrete approach that offers a sequence of snapshots of a dynamic
system.

In this paper, we combine the aforementioned temporal, dynamic, and (time-
based) metric extensions of the logic of Here-and-There and its non-monotonic
extension Equilibrium logic within a single logical setting by extending the
dynamic variants with time-based metrics. This results in the Metric Dynamic
logic of Here-and-There ($\mathrm{MDHT}$) and its non-monotonic extension of
Metric Dynamic Equilibrium Logic ($\mathrm{MDEL}$). In this setting, we can
express the statement in (1) as

$\displaystyle[{\uptau}^{\ast}]_{(-\omega..\omega)}\,{\left([\mathit{use}?]_{(-\omega..\omega)}\,{\langle{\uptau}^{\ast}\rangle_{(60..120)}\,{\mathit{clean}}}\right)}\
.$

As detailed below, we may thus formulate temporal, metric, as well as Boolean
operators in terms of metric dynamic ones. This already hints at the great
expressive power of $\mathrm{MDHT}$ and $\mathrm{MDEL}$.

The main contribution of the paper is the definition of $\mathrm{MDHT}$
itself. Its syntax and semantics were carefully designed to cover _both_ the
dynamic operators and the metric intervals, that constituted different and
independent extensions, in a way that their combination could also provide
other meaningful representational choices. In this way, for instance, we
propose intervals that may use negative positions (something uncommon in the
literature) not only to accommodate past time operators in a more natural way,
but also to offer more flexibility to treat relative time windows for a given
expression. The main results prove that the previous temporal approaches, TEL,
DEL and MEL, are now fragments of the more general formalism $\mathrm{MDEL}$.

The rest of the paper is organized as follows. We start by defining the
syntax, semantics, and some properties of $\mathrm{MDHT}$ in Section 2 and
define $\mathrm{MDEL}$ in Section 3. We then show in Section 4 how an existing
(monotonic) metric dynamic logic (Basin ., 2017) as well as the various
aforementioned extensions can be captured in $\mathrm{MDHT}$. We conclude with
a brief summary in Section 5.

##  2 Metric Dynamic Logic of Here-and-There

We start by providing some notation for intervals used in the rest of the
paper. Given $m\in\mathbb{Z}\cup\\{-\omega\\}$ and
$n\in\mathbb{Z}\cup\\{\omega\\}$, we let $(m..n)$ stand for the set
$\\{i\in\mathbb{Z}\mid m<i<n\\}$, $[m..n)$ for $\\{i\in\mathbb{Z}\mid m\leq
i<n\\}$, $(m..n]$ for $\\{i\in\mathbb{Z}\mid m<i\leq n\\}$, and $[m..n]$ for
$\\{i\in\mathbb{Z}\mid m\leq i\leq n\\}$. For simplicity, in what follows, we
refrain from distinguishing intervals and integers from their syntactic
representation.

###  2.1 Syntax

Given a set $\mathcal{A}$ of propositional variables (called _alphabet_), a
_metric dynamic formula_ $\varphi$ and a _path expression_ $\rho$ are mutually
defined by the following pair of grammar rules:

$\displaystyle\varphi$
$\displaystyle::=p\mid\bot\mid\;\langle\rho\rangle_{I}\,{\varphi}\;\mid\;[\rho]_{I}\,{\varphi}$
$\displaystyle\rho$
$\displaystyle::=\uptau\mid\varphi?\mid\rho+\rho\mid\rho\mathrel{;}\rho\mid{\rho}^{\ast}\mid{\rho}^{-}\
.$

where $p\in\mathcal{A}$ is an atom and $I$ is an interval of the form $(m..n)$
with $m\in\mathbb{Z}\cup\\{-\omega\\}$ and $n\in\mathbb{Z}\cup\\{\omega\\}$.

This syntax combines aspects from metric (Koymans, 1990) and dynamic logic
(Pratt, 1976). The metric component manifests itself in the interval attached
to the two dynamic modal operators. Apart from this, the syntax is similar to
the one of Dynamic Logic (DL; Harel . 2000) but differs in the construction of
(atomic) path expressions: While DL uses a separate alphabet for “atomic
actions”, we follow the approach of De Giacomo Vardi in LDL (2013) and use a
single alphabet $\mathcal{A}$ along with a single atomic path expression given
by the (transition) constant $\uptau\not\in\mathcal{A}$ (read as “step”).
Thus, each path expression $\rho$ is a regular expression formed with the
constant $\uptau$ plus the test construct $\varphi?$ that may refer to
propositional atoms in alphabet $\mathcal{A}$.

As regards syntactic metric aspects, we allow subindex intervals $I$ to use
some forms of closed ends so that we let $[m..n]$ stand for $(m{-}1..n{+}1)$
provided $m\neq-\omega$ and $n\neq\omega$, $[m..n)$ for $(m{-}1..n)$ if
$m\neq-\omega$, and $(m..n]$ for $(m..n{+}1)$ if $n\neq\omega$. Also, we
sometimes use the subindices ‘${}\leq n$’ and ‘${}\geq m$’ as abbreviations of
intervals $(-\omega..n]$ and $[m..\omega)$, respectively, whenever
$m\neq-\omega$ and $n\neq\omega$. On the other hand, when
$I=(-\omega..\omega)$, we simply omit the subindex $I$ so that:

$\displaystyle\langle\rho\rangle\,{\varphi}$
$\displaystyle\mathbin{\raisebox{-1.0pt}[-3.0pt][0.0pt]{$\stackrel{{\scriptstyle\mathit{def}}}{{=}}$}}\langle\rho\rangle_{(-\omega..\omega)}\,{\varphi}$
$\displaystyle[\rho]\,{\varphi}$
$\displaystyle\mathbin{\raisebox{-1.0pt}[-3.0pt][0.0pt]{$\stackrel{{\scriptstyle\mathit{def}}}{{=}}$}}[\rho]_{(-\omega..\omega)}\,{\varphi}.$
(2)

More generally, we refer to interval-free formulas as _dynamic formulas_.
Finally, we define the inversion of an interval as
${(m..n)}^{-}\mathbin{\raisebox{-1.0pt}[-3.0pt][0.0pt]{$\stackrel{{\scriptstyle\mathit{def}}}{{=}}$}}({-n}..{-m})$.
Note that $I={({I}^{-})}^{-}$ and $i\in I$ iff $-i\in{I}^{-}$ for any interval
$I$.

As usual, a _metric dynamic theory_ is a (possibly infinite) set of metric
dynamic formulas. We sometimes drop the adjectives and simply use the terms
formula and theory, whenever it is clear from context.

As we show below, the above language allows us to capture several derived
operators, like the Boolean ones:

$\displaystyle\varphi\to\psi$
$\displaystyle\mathbin{\raisebox{-1.0pt}[-3.0pt][0.0pt]{$\stackrel{{\scriptstyle\mathit{def}}}{{=}}$}}[\varphi?]\,\psi$
$\displaystyle\varphi\wedge\psi$
$\displaystyle\mathbin{\raisebox{-1.0pt}[-3.0pt][0.0pt]{$\stackrel{{\scriptstyle\mathit{def}}}{{=}}$}}\langle\varphi?\rangle\,\psi$
(3) $\displaystyle\top$
$\displaystyle\mathbin{\raisebox{-1.0pt}[-3.0pt][0.0pt]{$\stackrel{{\scriptstyle\mathit{def}}}{{=}}$}}\bot\to\bot$
$\displaystyle\varphi\vee\psi$
$\displaystyle\mathbin{\raisebox{-1.0pt}[-3.0pt][0.0pt]{$\stackrel{{\scriptstyle\mathit{def}}}{{=}}$}}\langle\varphi?+\psi?\rangle\,\top$
(4) $\displaystyle\neg\varphi$
$\displaystyle\mathbin{\raisebox{-1.0pt}[-3.0pt][0.0pt]{$\stackrel{{\scriptstyle\mathit{def}}}{{=}}$}}\varphi\to\bot$
(5)

All Boolean connectives $\wedge$, $\vee$, and $\to$ are defined in terms of
the essentially dynamic operators $[\cdot]\,$ and $\langle\cdot\rangle\,$
without any reference to a restricted underlying interval111No additional
expressive power is gained by adding intervals to Boolean operators, since
they all depend on modalities for test expressions, checked in the current
state. For instance, $p\to_{\leq 20}q$ would amount to $[p?]\,_{\leq 20}\,q$
and we see below that this is equivalent to $[p?]\,q\equiv p\to q$. Similarly,
$p\to_{>20}q$ would amount to $\top$.. Among them, the definition of $\to$ is
most noteworthy since it hints at the implicative nature of $[\cdot]\,$.
Negation $\neg$ is then expressed via implication, as usual in HT.

A formula is _propositional_ , if all its connectives are Boolean. A formula
is said to be _conditional_ if it contains some occurrence of an atom
$p\in\mathcal{A}$ inside an operator of form $[\cdot]_{\cdot}\,{}$; it is
called _unconditional_ otherwise. Note that formulas with atoms in implication
antecedents or negated formulas are also conditional, since they are derived
from $[\cdot]_{\cdot}\,{}$. For instance, $[p?]\,\bot$ is conditional, and is
actually the same as $p\to\bot$ and $\neg p$.

As with LDL, we sometimes use a propositional formula $\phi$ as a path
expression and let it stand for $(\phi?;\uptau)$. Accordingly, we use the
following abbreviations:

$\displaystyle\langle\phi\rangle_{I}\,{\varphi}$
$\displaystyle\mathbin{\raisebox{-1.0pt}[-3.0pt][0.0pt]{$\stackrel{{\scriptstyle\mathit{def}}}{{=}}$}}\langle\phi?;\uptau\rangle_{I}\,{\varphi}$
$\displaystyle[\phi]_{I}\,{\varphi}$
$\displaystyle\mathbin{\raisebox{-1.0pt}[-3.0pt][0.0pt]{$\stackrel{{\scriptstyle\mathit{def}}}{{=}}$}}[\phi?;\uptau]_{I}\,{\varphi}.$
(6)

This also means that the reading of $\top$ as a path expression amounts to
$(\top?;\uptau)$ which is just equivalent to $\uptau$. Another abbreviation is
the sequence of $n$ repetitions of some expression $\rho$ defined as
$\rho^{0}\mathbin{\raisebox{-1.0pt}[-3.0pt][0.0pt]{$\stackrel{{\scriptstyle\mathit{def}}}{{=}}$}}\top?$
and
$\rho^{n+1}\mathbin{\raisebox{-1.0pt}[-3.0pt][0.0pt]{$\stackrel{{\scriptstyle\mathit{def}}}{{=}}$}}\rho;\rho^{n}$.
For instance, $\rho^{3}$ unfolds to $\rho;\rho;\rho;\top?$ and amounts to
$\rho;\rho;\rho$.

######  Example 1.

As soon as an accident ($a$) happens onboard, a boat starts sending an SOS
($s$) during the next 10 minutes, while no help ($h$) reply is received. When
the rescue station receives an SOS, it sends back a help reply no later than 2
minutes. However, the rescue station has only begun working at minute $t=50$.
If an accident happened at time instant $t=40$, would the boat receive a
$\mathit{help}$ reply and, if so, when?

A possible formalization of the example could be:

$\displaystyle\square(\ a\to[(\neg h)^{*};\neg h]\,_{\leq 10}\,s\ )$ (7)
$\displaystyle\square_{\geq 50}(s\to\Diamond_{\leq 2}\,h)$ (8)
$\displaystyle\Diamond_{40}\,a$ (9)

Negation in (7) acts as a default: we send the SOS while _no evidence about
help_ is derived. That formula also combines path expressions from LDL with
metric information.

###  2.2 Semantics

The traditional semantics of linear-time logics, like LTL (Pnueli, 1977), LDL
(De Giacomo Vardi, 2013), and MTL (Koymans, 1990), rely on the concept of a
_trace_ , a (possibly infinite) sequence of _states_ , each of which is
represented by a set of atoms. More precisely, a _trace_ $\mathbf{T}$ of
length $\lambda$ over alphabet $\mathcal{A}$ is a sequence
$\mathbf{T}=(T_{i})_{i\in[0..\lambda)}$ of sets $T_{i}\subseteq\mathcal{A}$.
We sometimes use the notation
$|\mathbf{T}|\mathbin{\raisebox{-1.0pt}[-3.0pt][0.0pt]{$\stackrel{{\scriptstyle\mathit{def}}}{{=}}$}}\lambda$
to stand for the length of the trace. We say that $\mathbf{T}$ is _infinite_
if $|\mathbf{T}|=\omega$ and _finite_ if $|\mathbf{T}|\in\mathbb{N}$. To
represent traces, we write a sequence of sets of atoms concatenated with
‘$\cdot$’. For instance, the finite trace
$\\{a\\}\cdot\emptyset\cdot\\{a\\}\cdot\emptyset$ has length 4 and makes $a$
true at even time steps and false at odd ones. For infinite traces, we
sometimes use $\omega$-regular expressions like, for instance, in the infinite
trace $(\\{a\\}\cdot\emptyset)^{\omega}$ where all even positions make $a$
true and all odd positions make it false.

At each state $T_{i}$ in a trace, an atom $a$ can only be true, viz. $a\in
T_{i}$, or false, $a\not\in T_{i}$. Temporal logics based on the logic of
Here-and-There, like THT (Aguado ., 2013, 2023), DHT (Bosser ., 2018; Cabalar,
Diéguez Schaub, 2019), and MHT (Cabalar, Diéguez ., 2020; Cabalar ., 2021,
2022), weaken such truth assignments, following the same intuitions as the
(non-temporal) logic of HT: An atom can have one of three truth-values in each
state, namely, _false_ , _assumed_ (or true by default) or _proven_ (or
certainly true). Anything proved has to be assumed, but the opposite does not
necessarily hold. Following this idea, a state at time step $i$ is represented
as a pair of sets of atoms $\langle H_{i},T_{i}\rangle$ with $H_{i}\subseteq
T_{i}\subseteq\mathcal{A}$ where $H_{i}$ (standing for “here”) contains the
proven atoms, whereas $T_{i}$ (standing for “there”) contains the assumed
atoms. On the other hand, false atoms are just the ones not assumed, captured
by $\mathcal{A}\setminus T_{i}$. Accordingly, a _Here-and-There trace_ (for
short _HT -trace_) of length $\lambda$ 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}$ for any $i\in[0..\lambda)$. For convenience, we usually
represent the HT-trace 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)}$. Given
$\mathbf{M}=\langle\mathbf{H},\mathbf{T}\rangle$, we also denote its length as
$|\mathbf{M}|\mathbin{\raisebox{-1.0pt}[-3.0pt][0.0pt]{$\stackrel{{\scriptstyle\mathit{def}}}{{=}}$}}|\mathbf{H}|=|\mathbf{T}|=\lambda$.
Note that the two traces $\mathbf{H}$, $\mathbf{T}$ must satisfy a kind of
order relation, since $H_{i}\subseteq T_{i}$ for each time step $i$. Formally,
we define the ordering $\mathbf{H}\leq\mathbf{T}$ between two traces of the
same length $\lambda$ as $H_{i}\subseteq T_{i}$ for each $i\in[0..\lambda)$.
Furthermore, we define $\mathbf{H}<\mathbf{T}$ whenever both
$\mathbf{H}\leq\mathbf{T}$ and $\mathbf{H}\neq\mathbf{T}$. Thus, an HT-trace
can also be defined as any pair $\langle\mathbf{H},\mathbf{T}\rangle$ of
traces such that $\mathbf{H}\leq\mathbf{T}$. The particular type of HT-traces
satisfying $\mathbf{H}=\mathbf{T}$ are called _total_.

In metric logics, each state is further associated with a _time point_. For
this, we use a function $\tau$ that 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. All this leads to the concept of a timed HT-trace.

######  Definition 1.

A _timed HT-trace_ over $(\mathbb{N},<)$ is is a triple
$\langle\mathbf{H},\mathbf{T},\tau\rangle$ where

  1. 1.

$\langle\mathbf{H},\mathbf{T}\rangle=(\langle
H_{i},T_{i}\rangle)_{i\in[0..\lambda)}$ is an HT-trace and

  2. 2.

$\tau:[0..\lambda)\to\mathbb{N}$ is a function such that222This condition
correspond to _strict_ time traces, which are the ones we use in the current
paper. Non-strict traces would allow $\tau(i)\leq\tau(i{+}1)$, meaning that,
at the same time point, more than one transition could occur, even an infinite
number of them. This seems a less practical possibility, and is left for
future study. $\tau(i)<\tau(i{+}1)$,
for all $i\in[0..\lambda)$ with $i+1<\lambda$.

We assume w.l.o.g. that $\tau(0)=0$.

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

######  Definition 2 ($\mathrm{MDHT}$ satisfaction).

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

  1. 1.

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

  2. 2.

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

  3. 3.

$\mathbf{M},k\models\langle\rho\rangle_{I}\,{\varphi}$ if
$\mathbf{M},i\models\varphi$ for some $i$ with
$(k,i)\in{\parallel}{\rho}{\parallel}^{\mathbf{M}}$ and $\tau(i)-\tau(k)\in I$

  4. 4.

$\mathbf{M},k\models[\rho]_{I}\,{\varphi}$ if
$\mathbf{M}^{\prime},i\models\varphi$ for all $i$ with
$(k,i)\in{\parallel}{\rho}{\parallel}^{\mathbf{M}^{\prime}}$ and
$\tau(i)-\tau(k)\in I$ for both $\mathbf{M}^{\prime}=\mathbf{M}$ and
$\mathbf{M}^{\prime}=\langle\mathbf{T},\mathbf{T},\tau\rangle$

where, for any timed HT-trace $\mathbf{M}$,
${\parallel}{\rho}{\parallel}^{\mathbf{M}}\subseteq\mathbb{N}^{2}$ is a
relation on pairs of time steps inductively defined as follows.

  1. 5.

${\parallel}{\uptau}{\parallel}^{\mathbf{M}}\
\mathbin{\raisebox{-1.0pt}[-3.0pt][0.0pt]{$\stackrel{{\scriptstyle\mathit{def}}}{{=}}$}}\
\\{(k,k+1)\mid k,k+1\in[0..\lambda)\\}$

  2. 6.

${\parallel}{\varphi?}{\parallel}^{\mathbf{M}}\
\mathbin{\raisebox{-1.0pt}[-3.0pt][0.0pt]{$\stackrel{{\scriptstyle\mathit{def}}}{{=}}$}}\
\\{(k,k)\mid\mathbf{M},k\models\varphi\\}$

  3. 7.

${\parallel}{\rho_{1}\mathrel{+}\rho_{2}}{\parallel}^{\mathbf{M}}\
\mathbin{\raisebox{-1.0pt}[-3.0pt][0.0pt]{$\stackrel{{\scriptstyle\mathit{def}}}{{=}}$}}\
{\parallel}{\rho_{1}}{\parallel}^{\mathbf{M}}\cup{\parallel}{\rho_{2}}{\parallel}^{\mathbf{M}}$

  4. 8.

${\parallel}{\rho_{1}\mathrel{;}\rho_{2}}{\parallel}^{\mathbf{M}}\
\mathbin{\raisebox{-1.0pt}[-3.0pt][0.0pt]{$\stackrel{{\scriptstyle\mathit{def}}}{{=}}$}}\
\\{(k,i)\mid{(k,j)\in{\parallel}{\rho_{1}}{\parallel}^{\mathbf{M}}}\text{and
}{(j,i)\in{\parallel}{\rho_{2}}{\parallel}^{\mathbf{M}}}\text{for some }j\\}$

  5. 9.

${\parallel}{{\rho}^{\ast}}{\parallel}^{\mathbf{M}}\
\mathbin{\raisebox{-1.0pt}[-3.0pt][0.0pt]{$\stackrel{{\scriptstyle\mathit{def}}}{{=}}$}}\
\bigcup_{n\geq 0}{\parallel}{\rho^{n}}{\parallel}^{\mathbf{M}}$

  6. 10.

${\parallel}{{\rho}^{-}}{\parallel}^{\mathbf{M}}\
\mathbin{\raisebox{-1.0pt}[-3.0pt][0.0pt]{$\stackrel{{\scriptstyle\mathit{def}}}{{=}}$}}\
\\{(k,i)\mid(i,k)\in{\parallel}{\rho}{\parallel}^{\mathbf{M}}\\}$

This definition accommodates traces of arbitrary length $\lambda$, including
both infinite ($\lambda=\omega$) and finite ($\lambda\in\mathbb{N}$) ones. The
most significant feature introduced by the HT part of this semantics is the
treatment of the always operator $[\rho]_{I}\,{\varphi}$, which is analogous
to the handling of implication333In fact, this is further inherited from the
behavior of implication in intuitionistic logic, whose satisfaction must be
checked in all accessible worlds. In this case, the accessibility relation of
traces is reflexive and, additionally, $\mathbf{T}$ is accessible from
$\mathbf{H}$. in the propositional intermediate logic of HT. It requires that
$\varphi$ is satisfied in “both dimensions” $\mathbf{H}$ (here) and
$\mathbf{T}$ (there) of the trace, using
$\langle\mathbf{T},\mathbf{T},\tau\rangle$ in addition to
$\langle\mathbf{H},\mathbf{T},\tau\rangle$ as with the other connectives.

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{MDHT}$ 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{MDHT}$  _model_ of a metric dynamic theory
$\Gamma$ if $\mathbf{M},0\models\varphi$ for all $\varphi\in\Gamma$. The set
of $\mathrm{MDHT}$ models of $\Gamma$ having length $\lambda$ is denoted as
$\mathrm{MDHT}(\Gamma,\lambda)$, whereas
$\mathrm{MDHT}(\Gamma)\mathbin{\raisebox{-1.0pt}[-3.0pt][0.0pt]{$\stackrel{{\scriptstyle\mathit{def}}}{{=}}$}}\bigcup_{\lambda=0}^{\omega}\mathrm{MDHT}(\Gamma,\lambda)$
is the set of all $\mathrm{MDHT}$ models of $\Gamma$ of any length. We may
obtain fragments of any metric dynamic logic by imposing restrictions on the
timed traces used for defining tautologies and models. We indicate the
restriction to finite (resp. infinite) traces by using subscript $f$ (resp.
$\omega$). That is, $\mathrm{MDHT}_{\\!f}$ stands for the restriction of
$\mathrm{MDHT}$ to traces of any finite length $\lambda\in\mathbb{N}$ and
$\mathrm{MDHT}_{\\!\omega}$ corresponds to the restriction to traces of
infinite length $\lambda=\omega$.

As we saw, Boolean operators are actually derived. This allows us to simplify
the number of cases to be checked in proofs by structural induction. Yet,
interpreting derived operators by unfolding their definitions can become, in
general, a bit cumbersome. The following proposition provides a direct
semantic characterization for Boolean connectives and it can be easily deduced
from their definitions as derived operators:

######  Proposition 1 (Satisfaction of Boolean formulas).

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

  1. (i)

$\mathbf{M},k\models\top$

  2. (ii)

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

  3. (iii)

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

  4. (iv)

$\mathbf{M},k\models\varphi\to\psi$ iff
$\mathbf{M}^{\prime},k\not\models\varphi$ or
$\mathbf{M}^{\prime},k\models\psi$, for both $\mathbf{M}^{\prime}=\mathbf{M}$
and $\mathbf{M}^{\prime}=\langle\mathbf{T},\mathbf{T},\tau\rangle$

  5. (v)

$\mathbf{M},k\models\neg\varphi$ iff
$\langle\mathbf{T},\mathbf{T},\tau\rangle,k\not\models\varphi$

###  2.3 Properties

We prove next that a pair of basic properties from HT are maintained in the
current extension of $\mathrm{MDHT}$.

######  Proposition 2 (Persistence).

Let $\langle\mathbf{H},\mathbf{T},\tau\rangle$ be a timed HT-trace of length
$\lambda$ over $\mathcal{A}$ and let $\varphi$ be a formula over
$\mathcal{A}$.

Then, for any $k\in[0..\lambda)$,

  1. 1.

if $\langle\mathbf{H},\mathbf{T},\tau\rangle,k\models\varphi$ then
$\langle\mathbf{T},\mathbf{T},\tau\rangle,k\models\varphi$ and

  2. 2.

${\parallel}{\rho}{\parallel}^{\langle\mathbf{H},\mathbf{T},\tau\rangle}\subseteq{\parallel}{\rho}{\parallel}^{\langle\mathbf{T},\mathbf{T},\tau\rangle}$.

Persistence is a property known from intuitionistic logic; it expresses that
accessible worlds satisfy the same or more formulas than the current world,
where $\mathbf{T}$ is “accessible” from $\mathbf{H}$ in HT. This also explains
the semantics of $[\cdot]_{\cdot}\,{}$, which behaves as a kind of
intuitionistic implication (used to define ‘$\to$’ as a derived operator) and
so, it must hold for all accessible worlds, viz.
$\langle\mathbf{H},\mathbf{T},\tau\rangle$ and
$\langle\mathbf{T},\mathbf{T},\tau\rangle$.

##  3 Metric Dynamic Equilibrium Logic

Given a set of models in $\mathrm{MDHT}$, we define the ones in equilibrium as
follows.

######  Definition 3 ($\mathfrak{S}$-Equilibrium/$\mathfrak{S}$-Stability).

Let $\mathfrak{S}$ be some set of timed HT-traces. A total timed HT-trace of
the form $\langle\mathbf{T},\mathbf{T},\tau\rangle$ is said to be in
_equilibrium_ in $\mathfrak{S}$ iff
$\langle\mathbf{T},\mathbf{T},\tau\rangle\in\mathfrak{S}$ and there is no
other $\langle\mathbf{H},\mathbf{T},\tau\rangle\in\mathfrak{S}$ such that
$\mathbf{H}<\mathbf{T}$. When this happens, the timed trace
$\langle\mathbf{T},\tau\rangle$ is said to be _stable_ in $\mathfrak{S}$. ∎

When $\mathfrak{S}=\mathrm{MDHT}(\Gamma)$, the timed HT-traces in equilibrium
are called the _metric dynamic equilibrium models_ of $\Gamma$, and denoted as
$\mathrm{MDEL}(\Gamma)$. Similarly, $\mathrm{MDEL}(\Gamma,\lambda)$ denotes
the HT-traces in equilibrium for $\mathrm{MDHT}(\Gamma,\lambda)$. Since the
ordering relation among traces is only defined for a fixed $\lambda$, the
following can be easily observed:

######  Proposition 3.

The set of metric dynamic equilibrium models of a theory $\Gamma$ can be
partitioned by the trace length $\lambda$, that is,
$\bigcup_{\lambda=0}^{\omega}\mathrm{MDEL}(\Gamma,\lambda)=\mathrm{MDEL}(\Gamma)$.
∎

_Metric Dynamic Equilibrium Logic_ ($\mathrm{MDEL}$) is the (non-monotonic)
logic induced by metric dynamic equilibrium models. We can also define the
variants ${\mathrm{MDEL}}_{\omega}$ and ${\mathrm{MDEL}}_{\\!f}$ by applying
the corresponding restriction to infinite and finite traces, respectively.

######  Example 2 (Example 1 continued).

Back to our example, suppose we have the theory $\Gamma$ consisting of the
formulas (7)-(9) and let us informally analyze the obtained metric dynamic
equilibrium models, or equilibrium models for short. Let us consider first the
possible untimed traces, forgetting the metric subindices by now. In other
words, consider the temporal equilibrium models of:

$\displaystyle\square(\ a\to[(\neg h)^{*};\neg h]\,\,s\ )$ (10)
$\displaystyle\square(s\to\Diamond\,h)$ (11) $\displaystyle\Diamond\,a$ (12)

Formula (12) forces us to include at least an atom $a$ in some state at time
step $i$. Other total models $\langle\mathbf{T},\mathbf{T},\tau\rangle$ may
include more occurrences of $a$ in other states, but they are not in
equilibrium, since we can always form a smaller model
$\langle\mathbf{H},\mathbf{T},\tau\rangle$ where those additional $a$’s are
removed in $\mathbf{H}$. This is because, apart from (12), atom $a$ only
occurs in the antecedent of the implication in (10). Now, after some analysis
(see (Cabalar, Diéguez Schaub, 2019)), it can be seen that (10) is equivalent
to the conjunction of temporal rules of the form:

$\displaystyle\square(\ a\wedge\neg h$ $\displaystyle\to$
$\displaystyle\widehat{}s\ )$ (13) $\displaystyle\square(\ a\wedge\neg
h\wedge\widehat{}\neg h$ $\displaystyle\to$ $\displaystyle\widehat{}^{2}s\ )$
(14) $\displaystyle\square(\ a\wedge\neg h\wedge\widehat{}\neg
h\wedge\widehat{}^{2}\neg h$ $\displaystyle\to$ $\displaystyle\widehat{}^{3}s\
)$ (15) $\displaystyle\square(\ a\wedge\neg h\wedge\widehat{}\neg
h\wedge\widehat{}^{2}\neg h\wedge\widehat{}^{3}\neg h$ $\displaystyle\to$
$\displaystyle\widehat{}^{4}s\ )$ $\displaystyle\vdots$

As an illustration of their behavior, these rules have a direct correspondence
to the ASP program:

    s(T+1) :- a(T), not h(T), step(T+1).
    s(T+2) :- a(T), not h(T), not h(T+1), step(T+2).
    s(T+3) :- a(T), not h(T), not h(T+1), not h(T+2), step(T+3).
    s(T+4) :- a(T), not h(T), not h(T+1), not h(T+2), not h(T+3), step(T+4).
    ...

where we use a time argument for all atoms and a predicate step to describe
the existing time points from $0$ to $|\mathbf{T}|-1$. Since $a$ only holds at
state $i$, the first possible justified occurrence of $s$ could only appear
from $i+1$ on. This means that any occurrence of $s$ up to $i$ can be removed
in a smaller $\mathbf{H}$ because, apart from (10), $s$ only occurs in the
antecedent of (11). But this allows us to conclude that there is no evidence
for $h$ at $i$, since (11) has a false antecedent at that state. In other
words, any equilibrium model begins with a prefix $\emptyset^{*}\cdot\\{a\\}$.
Implication (13) at $i$ forces the existence of a state $i+1$ where $s$ must
hold, but then, (11) allows us to conclude $\Diamond h$ at $i+1$. By a similar
reason as we followed for (12), we conclude that $h$ is true at exactly one
state $j\geq i+1$. Since all the states between $i+1$ and $j-1$ satisfy $\neg
h$, the boat keeps sending an SOS due to (10). To sum up, the possible
temporal equilibrium models have one of the forms:

$\displaystyle\emptyset^{*}\cdot\\{a\\}$
$\displaystyle\emptyset^{*}\cdot\\{a\\}\cdot\\{s\\}^{*}\cdot\\{s,h\\}\cdot\emptyset^{*}$

where, we use $T^{*}$ to mean any (possibly empty) sequence of repetitions of
state $T$. The first case corresponds to finite-length stable models where the
accident just happens at the end of the trace. In the second case, when the
boat receives the help reply, it still sends a last SOS since in the previous
state, $h$ was false yet.

Now, let us see what happens when we consider the metric information. Formula
(9) fixes the time point $\tau(i)=40$ for the state $i$ at which $a$ is made
true. Implication (7) is weaker now, since it is only applicable if the states
in which we send the SOS are 10 minutes ago from the accident at $i$. Further
than that, the boat stops sending messages. One new possible outcome, for
instance, is that there is no transition at all within the next 10 minutes,
and so, no SOS is ever emitted. This leads to equilibrium models of the form
$\emptyset^{*}\cdot\\{a\\}$ (when the accident is at the last step) or the
form

---
$\textstyle{\emptyset^{*}}$$\textstyle{\cdot}$$\textstyle{\\{a\\}}$$\textstyle{\cdot}$$\textstyle{\emptyset}$$\textstyle{\cdot}$$\textstyle{\emptyset^{*}}$$\textstyle{i\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{i+1\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$

for the state $i$ where $a$ occurs, with $\tau(i)=40$ and $\tau(i+1)>50$. If,
on the contrary, there is at least one transition in the next 10 minutes, we
must note now that (8) is only effective now at points $j$ where $\tau(j)\geq
50$. So, the rescue station does not attend to any signal before $t=50$. A
second possibility is, therefore, that the boat sends one or more SOS calls,
but at transitions that do not reach moment $t=50$. This would correspond to
equilibrium models of the form

---
$\textstyle{\emptyset^{*}}$$\textstyle{\cdot}$$\textstyle{\\{a\\}}$$\textstyle{\cdot}$$\textstyle{\\{s\\}^{*}}$$\textstyle{\cdot}$$\textstyle{\\{s\\}}$$\textstyle{\cdot}$$\textstyle{\emptyset^{*}}$$\textstyle{i\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{j\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$

where, $j>i$, $\tau(i)=40$ and $\tau(j)<50$ and the SOS calls are never
attended. Finally, it may be the case that the last SOS call within the 10
minutes interval happens exactly at $t=50$, when the rescue station begins
operating. If so, a help reply must be sent within the next 2 minutes. This
final group of equilibrium models would have either the form:

---
$\textstyle{\emptyset^{*}}$$\textstyle{\cdot}$$\textstyle{\\{a\\}}$$\textstyle{\cdot}$$\textstyle{\\{s\\}^{*}}$$\textstyle{\cdot}$$\textstyle{\\{s,h\\}}$$\textstyle{\cdot}$$\textstyle{\emptyset^{*}}$$\textstyle{i\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{j\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$

with $\tau(i)=40$ and $\tau(j)=50$, meaning that the help is immediate, or
perhaps:

|
---|---
$\textstyle{\emptyset^{*}}$$\textstyle{\cdot}$$\textstyle{\\{a\\}}$$\textstyle{\cdot}$$\textstyle{\\{s\\}^{*}}$$\textstyle{\cdot}$$\textstyle{\\{s\\}}$$\textstyle{\cdot}$$\textstyle{\emptyset^{*}}$$\textstyle{\cdot}$$\textstyle{\\{h\\}}$$\textstyle{\cdot}$$\textstyle{\emptyset^{*}}$$\textstyle{i\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{j\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{k\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$

where $\tau(i)=40$, $\tau(j)=50$ and $\tau(k)\leq 52$.

##  4 Relationships

In this section we show that $\mathrm{MDHT}$ constitutes an umbrella where
different logics for temporal ASP, most of them previously introduced in the
literature, can be simply identified as fragments.

###  4.1 Metric Dynamic Logic

An interesting subset of $\mathrm{MDHT}$ is the one formed by total timed
traces $\langle\mathbf{T},\mathbf{T},\tau\rangle$. In the non-metric version
of temporal and dynamic HT, viz. THT and DHT, the restriction to total models
corresponds to Linear Temporal and Dynamic Logic (LTL and LDL (Pnueli, 1977;
De Giacomo Vardi, 2013)). In our case, the restriction to total traces defines
a metric version of LDL, that we simply call _Metric Dynamic Logic_
($\mathrm{MDL}$ for short). 444This designation is somewhat justified in view
of Corollary 1.

For simplicity, we refrain from an explicit introduction of the semantics of
$\mathrm{MDL}$, since it just corresponds to $\mathrm{MDHT}$ on total traces
$\langle\mathbf{T},\mathbf{T},\tau\rangle$, as stated below. Let us simply use
$\langle\mathbf{T},\tau\rangle,k\models\varphi$ to denote the satisfaction of
$\varphi$ by a timed trace $\langle\mathbf{T},\tau\rangle$ at point $k$ in
$\mathrm{MDL}$ and
${\parallel}{\rho}{\parallel}^{\langle\mathbf{T},\tau\rangle}$ the
$\mathrm{MDL}$ accessibility relation for $\rho$ and
$\langle\mathbf{T},\tau\rangle$. In fact,
$\langle\mathbf{T},\tau\rangle,k\models\varphi$ is obtained from
$\mathbf{M},k\models\varphi$ in Definition 2 by replacing $\mathbf{M}$ by
$\langle\mathbf{T},\tau\rangle$ and by dropping Condition 4 and rather
defining $\mathbf{M},k\models[\rho]_{I}\,{\varphi}$ as
$\mathbf{M},k\models\neg\langle\rho\rangle_{I}\,{\neg\varphi}$.

######  Proposition 4.

For any total timed HT-trace $\langle\mathbf{T},\mathbf{T},\tau\rangle$ of
length $\lambda$, any formula $\varphi$ and any path expression $\rho$, we
have that

  1. 1.

$\langle\mathbf{T},\mathbf{T},\tau\rangle,k\models\varphi$ iff
$\langle\mathbf{T},\tau\rangle,k\models\varphi$, for all $k\in[0..\lambda)$;
and

  2. 2.

${\parallel}{\rho}{\parallel}^{\langle\mathbf{T},\mathbf{T},\tau\rangle}={\parallel}{\rho}{\parallel}^{\langle\mathbf{T},\tau\rangle}$.

Accordingly, any total timed HT-trace
$\langle\mathbf{T},\mathbf{T},\tau\rangle$ can be seen as the timed trace
$\langle\mathbf{T},\tau\rangle$. In fact, under total models, the satisfaction
of dynamic operators $\langle\cdot\rangle_{\cdot}\,$ and $[\cdot]_{\cdot}\,$
in $\mathrm{MDHT}$ collapses to that in $\mathrm{MDL}$.

This gives rise to the following result.

######  Proposition 5.

Let $\varphi$ and $\psi$ be unconditional,555That is, formulas without
implication, and so, without negation either. metric dynamic formulas. Then,
$\varphi\equiv\psi$ in $\mathrm{MDL}$ iff $\varphi\equiv\psi$ in
$\mathrm{MDHT}$.

Moreover, the first item (along with Proposition 2) implies that any
$\mathrm{MDHT}$ tautology is also an $\mathrm{MDL}$ tautology, so the former
constitutes a weaker logic. To show that, in fact, $\mathrm{MDHT}$ is
_strictly_ weaker, note that it does not satisfy some classical tautologies
like the _excluded middle_ $\varphi\vee\neg\varphi$, while $\mathrm{MDL}$ is a
proper extension of classical logic. In fact, the addition of the axiom schema

$\displaystyle\square(a\vee\neg a)\quad\text{ for each atom
}a\in\mathcal{A}\text{ in the alphabet}$ ($\mathrm{EM}$)

forces total models and so, makes $\mathrm{MDHT}$ collapse to $\mathrm{MDL}$.
Propositions 2 and 4 imply that $\varphi$ is $\mathrm{MDHT}$ satisfiable iff
it is $\mathrm{MDL}$ satisfiable.

In this context, it may also be interesting to recall item (v) in Proposition
1, showing that the satisfaction of negated formulas amounts to checking the
formulas’ dissatisfaction in the total trace obtained from the ‘there’ world,
namely, $\langle\mathbf{H},\mathbf{T},\tau\rangle,k\models\neg\varphi$ iff
$\langle\mathbf{T},\mathbf{T},\tau\rangle,k\not\models\varphi$ iff
$\langle\mathbf{T},\tau\rangle,k\not\models\varphi$. In other words, the
satisfaction of negated formulas amounts to that in $\mathrm{MDL}$.

In fact, the metric dynamic logic defined in (Basin ., 2017) corresponds to a
fragment of $\mathrm{MDHT}$ when restricting ourselves to total traces. Metric
dynamic formulas are defined in (Basin ., 2017) over intervals of natural
numbers using negation, disjunction as well as a future- and past-oriented
eventually operator. The latter can be expressed in $\mathrm{MDHT}$ by
applying the converse operator to the path expression and by inverting the
interval, viz. $\langle{\rho}^{-}\rangle_{{I}^{-}}\,{\varphi}$.

In the next result, we use $\varphi^{-}$ to denote the result of replacing
accordingly in formula $\varphi$ each subformula with such a past-oriented
eventually operator.

######  Corollary 1.

Let $\varphi$ be a metric dynamic formula restricted to the fragment used in
(Basin ., 2017), $\langle\mathbf{T},\tau\rangle$ a timed trace and $k\geq 0$.

Then, $\langle\mathbf{T},\tau\rangle,k\models\varphi$ under $\mathrm{MDL}$
satisfaction as in (Basin ., 2017) iff
$\langle\mathbf{T},\mathbf{T}\rangle,k\models\varphi^{-}$ under
$\mathrm{MDHT}$ satisfaction.

###  4.2 The Dynamic Logic of Here-and-There and Dynamic Equilibrium Logic

We consider now the (non-metric) linear dynamic extension of HT introduced in
(Cabalar, Diéguez Schaub, 2019) known as DHT. A formula is called _dynamic_ ,
if all its intervals equal $(-\omega..\omega)$, in which case we also drop all
intervals.

######  Proposition 6 (DHT-satisfaction of dynamic formulas).

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

  1. 1.

$\mathbf{M},k\models\langle\rho\rangle\,{\varphi}$ iff
$\mathbf{M},i\models\varphi$ for some $i$ with
$(k,i)\in{\parallel}{\rho}{\parallel}^{\mathbf{M}}$

  2. 2.

$\mathbf{M},k\models[\rho]\,{\varphi}$ iff
$\mathbf{M}^{\prime},i\models\varphi$ for all $i$ with
$(k,i)\in{\parallel}{\rho}{\parallel}^{\mathbf{M}^{\prime}}$
for both $\mathbf{M}^{\prime}=\mathbf{M}$ and
$\mathbf{M}^{\prime}=\langle\mathbf{T},\mathbf{T},\tau\rangle$

where ${\parallel}{\rho}{\parallel}^{\mathbf{M}}$ is defined as in Definition
2.

Note that, for the syntactic fragment dynamic formulas, the time function
$\tau$ is never used and can be dropped. As a consequence:

######  Corollary 2.

Let $\varphi$ be a dynamic formula and $\mathbf{M}$ a timed HT-trace and
$k\geq 0$.

Then, $\mathbf{M},k\models\varphi$ under DHT satisfaction iff
$\mathbf{M},k\models\varphi$ under $\mathrm{MDHT}$ satisfaction.

and, since THT can be defined as a fragment of DHT we also obtain:

######  Corollary 3.

Let $\varphi$ be a temporal formula and $\mathbf{M}$ a timed HT-trace and
$k\geq 0$.

Then, $\mathbf{M},k\models\varphi$ under THT satisfaction iff
$\mathbf{M},k\models\varphi$ under $\mathrm{MDHT}$ satisfaction.

Since the models selection of $\mathrm{MDEL}$ for dynamic and temporal
formulas respectively collapse to the model selection of DEL and TEL, we can
directly conclude:

######  Corollary 4.

Let $\varphi$ be a dynamic (resp. temporal) formula. A total timed trace
$\langle\mathbf{T},\mathbf{T},\tau\rangle$ is a metric dynamic equilibrium
model of $\varphi$ under $\mathrm{MDEL}$ definition iff it is a dynamic (resp.
temporal) equilibrium logic of $\varphi$ under DEL (resp. TEL) definition.

###  4.3 The Metric Logic of Here-and-There and Metric Equilibrium Logic

Similar to the expression of Boolean operators in terms of (metric) dynamic
formulas, we can also express metric and temporal formulas.

Given an interval $I$, operators $[\cdot]_{I}\,$ and
$\langle\cdot\rangle_{I}\,$ allow us also to define future metric operators
$\bm{\mathsf{F}}$, I, ${\widehat{}}_{I}$, ${\Diamond}_{I}$, ${\square}_{I}$,
${\mathbin{\bm{\mathsf{U}}}}_{I}$, standing for _final, next, weak next,
eventually, always, until,_ and their past-oriented counterparts:
$\bm{\mathsf{I}}$, ${\text{\rm\raisebox{-0.5pt}{\Large\textbullet}}}_{I}$,
${\widehat{\text{\rm\raisebox{-0.5pt}{\Large\textbullet}}}}_{I}$,
${\blacklozenge}_{I}$, ${\blacksquare}_{I}$,
${\mathbin{\bm{\mathsf{S}}}}_{I}$.

$\displaystyle\bm{\mathsf{F}}$
$\displaystyle\mathbin{\raisebox{-1.0pt}[-3.0pt][0.0pt]{$\stackrel{{\scriptstyle\mathit{def}}}{{=}}$}}[\uptau]\,{\bot}$
$\displaystyle\bm{\mathsf{I}}$
$\displaystyle\mathbin{\raisebox{-1.0pt}[-3.0pt][0.0pt]{$\stackrel{{\scriptstyle\mathit{def}}}{{=}}$}}[{\uptau}^{-}]\,{\bot}$
(17) $\displaystyle{}_{I}\varphi$
$\displaystyle\mathbin{\raisebox{-1.0pt}[-3.0pt][0.0pt]{$\stackrel{{\scriptstyle\mathit{def}}}{{=}}$}}\langle\uptau\rangle_{I}\,{\varphi}$
$\displaystyle{\text{\rm\raisebox{-0.5pt}{\Large\textbullet}}}_{I}\varphi$
$\displaystyle\mathbin{\raisebox{-1.0pt}[-3.0pt][0.0pt]{$\stackrel{{\scriptstyle\mathit{def}}}{{=}}$}}\langle{\uptau}^{-}\rangle_{{I}^{-}}\,{\varphi}$
(18) $\displaystyle{\widehat{}}_{I}\varphi$
$\displaystyle\mathbin{\raisebox{-1.0pt}[-3.0pt][0.0pt]{$\stackrel{{\scriptstyle\mathit{def}}}{{=}}$}}[\uptau]_{I}\,{\varphi}$
$\displaystyle{\widehat{\text{\rm\raisebox{-0.5pt}{\Large\textbullet}}}}_{I}\varphi$
$\displaystyle\mathbin{\raisebox{-1.0pt}[-3.0pt][0.0pt]{$\stackrel{{\scriptstyle\mathit{def}}}{{=}}$}}[{\uptau}^{-}]_{{I}^{-}}\,{\varphi}$
(19) $\displaystyle{\Diamond}_{I}\varphi$
$\displaystyle\mathbin{\raisebox{-1.0pt}[-3.0pt][0.0pt]{$\stackrel{{\scriptstyle\mathit{def}}}{{=}}$}}\langle{\uptau}^{\ast}\rangle_{I}\,{\varphi}$
$\displaystyle{\blacklozenge}_{I}\varphi$
$\displaystyle\mathbin{\raisebox{-1.0pt}[-3.0pt][0.0pt]{$\stackrel{{\scriptstyle\mathit{def}}}{{=}}$}}\langle{{\uptau}^{\ast}}^{-}\rangle_{{I}^{-}}\,{\varphi}$
(20) $\displaystyle{\square}_{I}\varphi$
$\displaystyle\mathbin{\raisebox{-1.0pt}[-3.0pt][0.0pt]{$\stackrel{{\scriptstyle\mathit{def}}}{{=}}$}}[{\uptau}^{\ast}]_{I}\,{\varphi}$
$\displaystyle{\blacksquare}_{I}\varphi$
$\displaystyle\mathbin{\raisebox{-1.0pt}[-3.0pt][0.0pt]{$\stackrel{{\scriptstyle\mathit{def}}}{{=}}$}}[{{\uptau}^{\ast}}^{-}]_{{I}^{-}}\,{\varphi}$
(21) $\displaystyle\varphi{\mathbin{\bm{\mathsf{U}}}}_{I}\psi$
$\displaystyle\mathbin{\raisebox{-1.0pt}[-3.0pt][0.0pt]{$\stackrel{{\scriptstyle\mathit{def}}}{{=}}$}}\langle{(\varphi?;\uptau)}^{\ast}\rangle_{I}\,{\psi}$
$\displaystyle\varphi{\mathbin{\bm{\mathsf{S}}}}_{I}\psi$
$\displaystyle\mathbin{\raisebox{-1.0pt}[-3.0pt][0.0pt]{$\stackrel{{\scriptstyle\mathit{def}}}{{=}}$}}\langle{{(\uptau;\varphi?)}^{\ast}}^{-}\rangle_{{I}^{-}}\,{\psi}$
(22)

This syntax essentially coincides with the metric (timed) extension of HT
presented in (Cabalar ., 2022) called MHT. A formula is called _metric_ , if
it includes only Boolean and metric operators. A metric formula is called
_temporal_ , if furthermore all its intervals equal $(-\omega..\omega)$, in
which case we drop them once more.

Note that _initial_ and _final_ only depend on the state of the trace and not
on the actual time that this state is mapped to. Hence, they are not indexed
by any interval.

The weak one-step operators, $\widehat{}$ and
$\widehat{\text{\rm\raisebox{-0.5pt}{\Large\textbullet}}}$, are of particular
interest when dealing with finite traces, since their behavior differs from
their genuine counterparts only at the ends of a trace. In fact,
${\widehat{}}_{I}\varphi$ can also be expressed as
${}_{I}\varphi\vee\neg{}_{I}\top$ (and
${\widehat{\text{\rm\raisebox{-0.5pt}{\Large\textbullet}}}}_{I}$ as
${\text{\rm\raisebox{-0.5pt}{\Large\textbullet}}}_{I}\varphi\vee\neg{\text{\rm\raisebox{-0.5pt}{\Large\textbullet}}}_{I}\top$)
However, it can no longer be defined in terms of _final_ , as done in (Cabalar
., 2018) with non-metric $\widehat{}\varphi\equiv\varphi\vee\bm{\mathsf{F}}$
(the same applies to weak _previous_ and _initial_).

The $\mathrm{MDHT}$ definition of ${\mathbin{\bm{\mathsf{R}}}}_{I}$ and
${\mathbin{\bm{\mathsf{T}}}}_{I}$ is not as immediate as for the other MHT
operators, since they cannot be directly defined in terms of the remaining
connectives. In LTL, it is well-known that the formulas
$\varphi\mathbin{\bm{\mathsf{R}}}\psi$ (resp.
$\varphi\mathbin{\bm{\mathsf{T}}}\psi$) and
$\neg\left(\neg\varphi\mathbin{\bm{\mathsf{U}}}\neg\psi\right)$ (resp.
$\neg\left(\neg\varphi\mathbin{\bm{\mathsf{S}}}\neg\psi\right)$) are
equivalent. Consequently, $\varphi\mathbin{\bm{\mathsf{R}}}\psi$ corresponds
to the LDL expression $[(\neg\varphi?;\uptau)^{*}]\,\psi$ while
$\varphi\mathbin{\bm{\mathsf{T}}}\psi$ corresponds to
$[(\neg\varphi?;\uptau^{-})^{*}]\,\psi$. When we move to DHT, those previous
equivalences do not hold any more because of the constructive behavior of the
negation but, yet, release and trigger can still be defined as derived
operators thanks to the equivalences (Bosser ., 2018):

$\displaystyle\varphi\mathbin{\bm{\mathsf{R}}}\psi\mathbin{\raisebox{-1.0pt}[-3.0pt][0.0pt]{$\stackrel{{\scriptstyle\mathit{def}}}{{=}}$}}(\psi\mathbin{\bm{\mathsf{U}}}(\varphi\wedge\psi))\vee\square\psi$
$\displaystyle\varphi\mathbin{\bm{\mathsf{T}}}\psi\mathbin{\raisebox{-1.0pt}[-3.0pt][0.0pt]{$\stackrel{{\scriptstyle\mathit{def}}}{{=}}$}}(\psi\mathbin{\bm{\mathsf{S}}}(\varphi\wedge\psi))\vee\blacksquare\psi.$

Unfortunately, once we add the intervals, it is easy to see that:

$\displaystyle\varphi{\mathbin{\bm{\mathsf{R}}}}_{I}\psi\not\equiv(\psi{\mathbin{\bm{\mathsf{U}}}}_{I}(\varphi\wedge\psi))\vee{\square}_{I}\psi$
and
$\displaystyle\varphi{\mathbin{\bm{\mathsf{T}}}}_{I}\psi\not\equiv(\psi{\mathbin{\bm{\mathsf{S}}}}_{I}(\varphi\wedge\psi))\vee{\blacksquare}_{I}\psi.$

To put a counter example for the $\mathbin{\bm{\mathsf{R}}}_{I}$ equivalence
(the one for $\mathbin{\bm{\mathsf{T}}}_{I}$ follows a similar reasoning),
consider the timed HT-trace $\langle\mathbf{H},\mathbf{T},\tau\rangle$ of
length $\lambda=3$, where $T_{0}=\\{a\\}$, $T_{1}=T_{2}=\emptyset$,
$\tau(0)=0$, $\tau(1)=1$ and $\tau(2)=4$. It can be easily checked that
$\langle\mathbf{H},\mathbf{T},\tau\rangle,0\models
a\mathbin{\bm{\mathsf{R}}}_{[3,5]}b$ but
$\langle\mathbf{H},\mathbf{T},\tau\rangle,0\not\models
b\mathbin{\bm{\mathsf{U}}}_{[3,5]}(a\wedge b)$ and
$\langle\mathbf{H},\mathbf{T},\tau\rangle,0\not\models\square_{[3,5]}b$.

In (Becker ., 2023) it is shown that ${\mathbin{\bm{\mathsf{R}}}}_{I}$ (resp.
${\mathbin{\bm{\mathsf{T}}}}_{I}$) can be defined in terms of the unary timed
operators and the (untimed) $\mathbin{\bm{\mathsf{R}}}$ (resp.
$\mathbin{\bm{\mathsf{T}}}$), which are $\mathrm{MDHT}$-definable.

$\displaystyle\varphi\mathbin{\bm{\mathsf{R}}}_{[m..n)}\psi$
$\displaystyle\equiv\square_{[m..n)}\psi\vee\Diamond_{[0..m)}\left(\varphi\mathbin{\bm{\mathsf{R}}}\left(\varphi\vee\widehat{}\psi\right)\right)$
$\displaystyle\varphi\mathbin{\bm{\mathsf{R}}}_{[0..n)}\psi$
$\displaystyle\equiv\square_{[0..n)}\psi\vee\varphi\mathbin{\bm{\mathsf{R}}}\psi$
$\displaystyle\varphi\mathbin{\bm{\mathsf{R}}}_{[m..n]}\psi$
$\displaystyle\equiv\square_{[m..n]}\psi\vee\Diamond_{[0..m)}\left(\varphi\mathbin{\bm{\mathsf{R}}}\left(\varphi\vee\widehat{}\psi\right)\right)$
$\displaystyle\varphi\mathbin{\bm{\mathsf{R}}}_{[0..n]}\psi$
$\displaystyle\equiv\square_{[0..n]}\psi\vee\varphi\mathbin{\bm{\mathsf{R}}}\psi$
$\displaystyle\varphi\mathbin{\bm{\mathsf{R}}}_{(m..n)}\psi$
$\displaystyle\equiv\square_{(m..n)}\psi\vee\Diamond_{[0..m]}\left(\varphi\mathbin{\bm{\mathsf{R}}}\left(\varphi\vee\widehat{}\psi\right)\right)$
$\displaystyle\varphi\mathbin{\bm{\mathsf{R}}}_{(0..n)}\psi$
$\displaystyle\equiv\square_{(0..n)}\psi\vee\varphi\mathbin{\bm{\mathsf{R}}}\left(\varphi\vee\widehat{}\psi\right)$
$\displaystyle\varphi\mathbin{\bm{\mathsf{R}}}_{(m..n]}\psi$
$\displaystyle\equiv\square_{(m..n]}\psi\vee\Diamond_{[0..m]}\left(\varphi\mathbin{\bm{\mathsf{R}}}\left(\varphi\vee\widehat{}\psi\right)\right)$
$\displaystyle\varphi\mathbin{\bm{\mathsf{R}}}_{(0..n]}\psi$
$\displaystyle\equiv\square_{(0..n]}\psi\vee\varphi\mathbin{\bm{\mathsf{R}}}\left(\varphi\vee\widehat{}\psi\right)$
$\displaystyle\varphi\mathbin{\bm{\mathsf{T}}}_{[m..n)}\psi$
$\displaystyle\equiv\blacksquare_{[m..n)}\psi\vee\blacklozenge_{[0..m)}\left(\varphi\mathbin{\bm{\mathsf{T}}}\left(\varphi\vee\widehat{\text{\rm\raisebox{-0.5pt}{\Large\textbullet}}}\psi\right)\right)$
$\displaystyle\varphi\mathbin{\bm{\mathsf{T}}}_{[0..n)}\psi$
$\displaystyle\equiv\blacksquare_{[0..n)}\psi\vee\varphi\mathbin{\bm{\mathsf{T}}}\psi$
$\displaystyle\varphi\mathbin{\bm{\mathsf{T}}}_{[m..n]}\psi$
$\displaystyle\equiv\blacksquare_{[m..n]}\psi\vee\blacklozenge_{[0..m)}\left(\varphi\mathbin{\bm{\mathsf{T}}}\left(\varphi\vee\widehat{\text{\rm\raisebox{-0.5pt}{\Large\textbullet}}}\psi\right)\right)$
$\displaystyle\varphi\mathbin{\bm{\mathsf{T}}}_{[0..n]}\psi$
$\displaystyle\equiv\blacksquare_{[0..n]}\psi\vee\varphi\mathbin{\bm{\mathsf{T}}}\psi$
$\displaystyle\varphi\mathbin{\bm{\mathsf{T}}}_{(m..n)}\psi$
$\displaystyle\equiv\blacksquare_{(m..n)}\psi\vee\blacklozenge_{[0..m]}\left(\varphi\mathbin{\bm{\mathsf{T}}}\left(\varphi\vee\widehat{\text{\rm\raisebox{-0.5pt}{\Large\textbullet}}}\psi\right)\right)$
$\displaystyle\varphi\mathbin{\bm{\mathsf{T}}}_{(0..n)}\psi$
$\displaystyle\equiv\blacksquare_{(0..n)}\psi\vee\varphi\mathbin{\bm{\mathsf{T}}}\left(\varphi\vee\widehat{\text{\rm\raisebox{-0.5pt}{\Large\textbullet}}}\psi\right)$
$\displaystyle\varphi\mathbin{\bm{\mathsf{T}}}_{(m..n]}\psi$
$\displaystyle\equiv\blacksquare_{(m..n]}\psi\vee\blacklozenge_{[0..m]}\left(\varphi\mathbin{\bm{\mathsf{T}}}\left(\varphi\vee\widehat{\text{\rm\raisebox{-0.5pt}{\Large\textbullet}}}\psi\right)\right)$
$\displaystyle\varphi\mathbin{\bm{\mathsf{T}}}_{(0..n]}\psi$
$\displaystyle\equiv\blacksquare_{(0..n]}\psi\vee\varphi\mathbin{\bm{\mathsf{T}}}\left(\varphi\vee\widehat{\text{\rm\raisebox{-0.5pt}{\Large\textbullet}}}\psi\right)$

From the unary normalform it is quite forward to get the respective MDHT
translation, since $\mathbin{\bm{\mathsf{R}}}$ and $\mathbin{\bm{\mathsf{T}}}$
are definable according to (Bosser ., 2018).

Finally, note that the converse operator ${\rho}^{-}$ is essential for
expressing all metric past operators, whose addition in temporal logic is
exponentially more succinct than using only future operators (Aguado ., 2017).

######  Proposition 7 (MHT-satisfaction of metric temporal logic).

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

  1. 1.

$\mathbf{M},k\models\bm{\mathsf{I}}$ iff $k=0$

  2. 2.

$\mathbf{M},k\models{\text{\rm\raisebox{-0.5pt}{\Large\textbullet}}}_{I}\,\varphi$
iff $k>0$ and $\mathbf{M},k{-}1\models\varphi$ and $\tau(k)-\tau(k{-}1)\in I$

  3. 3.

$\mathbf{M},k\models{\widehat{\text{\rm\raisebox{-0.5pt}{\Large\textbullet}}}}_{I}\,\varphi$
iff $k=0$ or $\mathbf{M},k{-}1\models\varphi$ or $\tau(k)-\tau(k{-}1)\not\in
I$

  4. 4.

$\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$

  5. 5.

$\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$

  6. 6.

$\mathbf{M},k\models\varphi{\mathbin{\bm{\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]$

  7. 7.

$\mathbf{M},k\models\varphi{\mathbin{\bm{\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]$

  8. 8.

$\mathbf{M},k\models\bm{\mathsf{F}}$ iff $k+1=\lambda$

  9. 9.

$\mathbf{M},k\models{}_{I}\,\varphi$ iff $k+1<\lambda$ and
$\mathbf{M},k{+}1\models\varphi$ and $\tau(k{+}1)-\tau(k)\in I$

  10. 10.

$\mathbf{M},k\models{\widehat{}}_{I}\,\varphi$ iff $k+1=\lambda$ or
$\mathbf{M},k{+}1\models\varphi$ or $\tau(k{+}1)-\tau(k)\not\in I$

  11. 11.

$\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$

  12. 12.

$\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$

  13. 13.

$\mathbf{M},k\models\varphi{\mathbin{\bm{\mathsf{U}}}}_{I}\psi$ 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)$

  14. 14.

$\mathbf{M},k\models\varphi{\mathbin{\bm{\mathsf{R}}}}_{I}\psi$ 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)$ ∎

######  Corollary 5.

Let $\varphi$ be a metric formula, $\mathbf{M}$ a timed HT-trace and $k\geq
0$.

Then, $\mathbf{M},k\models\varphi$ under MHT satisfaction iff
$\mathbf{M},k\models\varphi$ under $\mathrm{MDHT}$ satisfaction.

Since the models selection of $\mathrm{MDEL}$ for this syntactic fragment
collapses to the model selection of MEL, we can directly conclude:

######  Corollary 6.

Let $\varphi$ be a metric formula. A total timed trace
$\langle\mathbf{T},\mathbf{T},\tau\rangle$ is a metric dynamic equilibrium
model of $\varphi$ (under $\mathrm{MDEL}$ definition) iff it is a metric
equilibrium model of $\varphi$ (under MEL definition).

##  5 Conclusions

An important first step towards a logical formalization of temporal ASP
systems was initiated with the linear-time temporal extension of Equilibrium
Logic and its monotonic basis, the logic of Here-and-There (HT), respectively
called _Temporal Equilibrium Logic_ (TEL) and _Temporal Here-and-There_ (THT)
(Aguado ., 2023). This extension allowed defining temporal stable models for
arbitrary theories for the syntax of the well-known Linear-Time Temporal Logic
(LTL) (Pnueli, 1977) and gave rise to the implementation of the temporal ASP
tool telingo (Cabalar, Kaminski ., 2019; Cabalar, Diéguez ., 2020). In our
previous work, we explored extending the LTL syntax in two different
directions. On the one hand, we studied the use of path expressions from
Dynamic Logic (Harel ., 2000), adopting the syntax and principles of Linear
Dynamic Logic (LDL) (De Giacomo Vardi, 2013). This led to the extensions
called _Dynamic HT_ (DHT) and _Dynamic Equilibrium Logic_ (DEL) that, despite
of allowing a richer syntax and expressiveness, used the same semantic
structures as LTL, since a temporal stable model is just a (finite or
infinite) trace. On the other hand, in a somehow orthogonal way, we also
studied the incorporation in THT of metric information, by extending modal
operators with time intervals as in Metric Temporal Logic (MTL) (Koymans,
1990), leading to _Metric HT_ (MHT) and _Metric Equilibrium Logic_ (MEL)
(Cabalar ., 2022). This meant not only a syntax extension with respect to LTL
operators, but also a generalization of the semantic structure of a temporal
stable model, that had in this case the form of a _timed_ trace, that is, a
trace where each state has an associated time point from an external clock.

In this paper, we have presented a unification of both extensions, namely, the
use of dynamic operators and path expressions with the extension for metric
intervals and timed traces. The new formalism, we call _Metric Dynamic Here-
and-There_ ($\mathrm{MDHT}$) and its non-monotonic version _Metric Dynamic
Equilibrium Logic_ ($\mathrm{MDEL}$), acts as an umbrella for all the
mentioned previous logics, that become now fragments of the new approach. One
interesting feature is that, as happens with DHT, both future and past
operators are accommodated into the two standard dynamic modalities,
$[\cdot]\,_{I}$ and $\langle\cdot\rangle\,_{I}$ that have now a metric
interval $I$ as a subindex. This is achieved by a combination of the converse
operator $\rho^{-}$ in path expressions with the use of negative values in the
interval $I$. To put an example, the usual encoding of the (non-metric) past
temporal formula $\blacklozenge p$ in LDL is
$\langle(\uptau^{*})^{-}\rangle\,{}p$, using the converse operator. If we add
a metric interval, as in $\blacklozenge_{[2..9]}p$, then the encoding into
$\mathrm{MDHT}$ also reverses the interval ends (switching their roles and
their signs) leading to $\langle(\uptau^{*})^{-}\rangle\,_{[-9..-2]}\,p$. This
extension of intervals with negative numbers has been mostly thought for
encoding standard past temporal operators, but also offers new expressive
flexibility. For instance, we can now deal with quite complex and compact
formulas like:

$\square\ (\ \blacklozenge\langle(a;b)^{*}\rangle\,_{[-5..5]}\,p\to q\ )$

meaning that it is always true that if there was some point in the past where
$p$ held in the middle of an alternation of $a$ and $b$ that occurred between
5 minutes before and five minutes after $p$, then $q$ must hold now.

For future work, we plan to study different properties of the new formalism,
such as strong equivalence, reduction to normal forms, translations of
$\mathrm{MDHT}$ and $\mathrm{MDEL}$ respectively into First and Second Order
Logic, or encodings into logic programming. Another important topic is
exploring the relation with ASP with Constraint Solving (Baselice ., 2005),
and exploiting its use for implementation purposes.

### Acknowledgments

This work was supported by MICINN, Spain, grant PID2020-116201GB-I00, Xunta de
Galicia, Spain (GPC ED431B 2019/03), Fundación BBVA (LIANDA research project),
Spain, Région Pays de la Loire, France (EL4HC and étoiles montantes CTASP),
DFG grant SCHA 550/15, Germany, and European Union COST action CA-17124.

## References

  * Aguado . (2023) agcadipescscvi20aAguado, F., Cabalar, P., Diéguez, M., Pérez, G., Schaub, T., Schuhmann, A. Vidal, C.  2023\.  Linear-Time Temporal Answer Set Programming Linear-time temporal answer set programming.  Theory and Practice of Logic Programming2312-56.  10.1017/S1471068421000557
  * Aguado . (2013) agcadipevi13aAguado, F., Cabalar, P., Diéguez, M., Pérez, G. Vidal, C.  2013\.  Temporal equilibrium logic: a survey Temporal equilibrium logic: a survey.  Journal of Applied Non-Classical Logics231-22-24.  10.1080/11663081.2013.798985
  * Aguado . (2017) agcadipevi17aAguado, F., Cabalar, P., Diéguez, M., Pérez, G. Vidal, C.  2017\.  Temporal Equilibrium Logic with Past Operators Temporal equilibrium logic with past operators.  Journal of Applied Non-Classical Logics273-4161-177.
  * Balduccini . (2019) lpnmr19Balduccini, M., Lierler, Y. Woltran, S. ().  2019\.  Proceedings of the Fifteenth International Conference on Logic Programming and Nonmonotonic Reasoning (LPNMR’19) Proceedings of the fifteenth international conference on logic programming and nonmonotonic reasoning (lpnmr’19) ( 11481).  Springer-Verlag.
  * Baselice . (2005) baboge05aBaselice, S., Bonatti, P. Gelfond, M.  2005\.  Towards an Integration of Answer Set and Constraint Solving Towards an integration of answer set and constraint solving.  M. Gabbrielli G. Gupta (), Proceedings of the Twenty-first International Conference on Logic Programming (ICLP’05) Proceedings of the twenty-first international conference on logic programming (iclp’05) ( 3668, 52-66).  Springer-Verlag.
  * Basin . (2017) bakrtr17aBasin, D., Krstic, S. Traytel, D.  2017\.  Almost Event-Rate Independent Monitoring of Metric Dynamic Logic Almost event-rate independent monitoring of metric dynamic logic.  S. Lahiri G. Reger (), Proceedings if the Seventeenth International Conference on Runtime Verification (RV’17) Proceedings if the seventeenth international conference on runtime verification (rv’17) ( 10548, 85-102).  Springer-Verlag.  10.1007/978-3-319-67531-2_6
  * Becker . (2023) becadiscsc23Becker, A., Cabalar, P., Diéguez, M., Schaub, T. Schuhmann, A.  2023\.  Metric Temporal Equilibrium Logic over Timed Traces Metric temporal equilibrium logic over timed traces.  CoRRabs/2304.14778.  https://arxiv.org/abs/2304.14778
  * Bosser . (2018) bocadisc18aBosser, A., Cabalar, P., Diéguez, M. Schaub, T.  2018\.  Introducing Temporal Stable Models for Linear Dynamic Logic Introducing temporal stable models for linear dynamic logic.  M. Thielscher, F. Toni F. Wolter (), Proceedings of the Sixteenth International Conference on Principles of Knowledge Representation and Reasoning (KR’18) Proceedings of the sixteenth international conference on principles of knowledge representation and reasoning (kr’18) ( 12-21).  AAAI Press.
  * Cabalar, Diéguez . (2020) cadilasc20aCabalar, P., Diéguez, M., Laferriere, F. Schaub, T.  2020\.  Implementing Dynamic Answer Set Programming over finite traces Implementing dynamic answer set programming over finite traces.  G. De Giacomo . (), Proceedings of the Twenty-fourth European Conference on Artificial Intelligence (ECAI’20) Proceedings of the twenty-fourth european conference on artificial intelligence (ecai’20) ( 656-663).  IOS Press.  10.3233/FAIA200151
  * Cabalar, Diéguez Schaub (2019) cadisc19aCabalar, P., Diéguez, M. Schaub, T.  2019\.  Towards Dynamic Answer Set Programming over finite traces Towards dynamic answer set programming over finite traces.  M. Balduccini, Y. Lierler S. Woltran (), Proceedings of the Fifteenth International Conference on Logic Programming and Nonmonotonic Reasoning (LPNMR’19) Proceedings of the fifteenth international conference on logic programming and nonmonotonic reasoning (lpnmr’19) ( 11481, 148-162).  Springer-Verlag.  10.1007/978-3-030-20528-7_12
  * Cabalar, Diéguez . (2020) cadiscsc20aCabalar, P., Diéguez, M., Schaub, T. Schuhmann, A.  2020\.  Towards Metric Temporal Answer Set Programming Towards metric temporal answer set programming.  Theory and Practice of Logic Programming205783-798.
  * Cabalar . (2021) cadiscsc21aCabalar, P., Diéguez, M., Schaub, T. Schuhmann, A.  2021\.  Metric Temporal Answer Set Programming over Timed Traces (extended abstract) Metric temporal answer set programming over timed traces (extended abstract).  Stream Reasoning Workshop. Stream reasoning workshop.
  * Cabalar . (2022) cadiscsc22aCabalar, P., Diéguez, M., Schaub, T. Schuhmann, A.  2022\.  Metric Temporal Answer Set Programming over Timed Traces Metric temporal answer set programming over timed traces.  G. Gottlob, D. Inclezan M. Maratea (), Proceedings of the Sixteenth International Conference on Logic Programming and Nonmonotonic Reasoning (LPNMR’22) Proceedings of the sixteenth international conference on logic programming and nonmonotonic reasoning (lpnmr’22) ( 13416, 117-130).  Springer-Verlag.
  * Cabalar, Kaminski . (2019) cakamosc19aCabalar, P., Kaminski, R., Morkisch, P. Schaub, T.  2019\.  telingo = ASP + Time telingo = ASP + time.  M. Balduccini, Y. Lierler S. Woltran (), Proceedings of the Fifteenth International Conference on Logic Programming and Nonmonotonic Reasoning (LPNMR’19) Proceedings of the fifteenth international conference on logic programming and nonmonotonic reasoning (lpnmr’19) ( 11481, 256-269).  Springer-Verlag.  10.1007/978-3-030-20528-7_19
  * Cabalar . (2018) cakascsc18aCabalar, P., Kaminski, R., Schaub, T. Schuhmann, A.  2018\.  Temporal Answer Set Programming on Finite Traces Temporal answer set programming on finite traces.  Theory and Practice of Logic Programming183-4406-420.  10.1017/S1471068418000297
  * Cabalar Vega (2007) cabper07aCabalar, P. Vega, GP.  2007\.  Temporal Equilibrium Logic: A First Approach Temporal equilibrium logic: A first approach.  R. Moreno-Díaz, F. Pichler A. Quesada-Arencibia (), Proceedings of the Eleventh International Conference on Computer Aided Systems Theory (EUROCAST’17) Proceedings of the eleventh international conference on computer aided systems theory (eurocast’17) ( 4739, 241-248).  Springer-Verlag.
  * De Giacomo Vardi (2013) giavar13aDe Giacomo, G. Vardi, M.  2013\.  Linear Temporal Logic and Linear Dynamic Logic on Finite Traces Linear temporal logic and linear dynamic logic on finite traces.  F. Rossi (), Proceedings of the Twenty-third International Joint Conference on Artificial Intelligence (IJCAI’13) Proceedings of the twenty-third international joint conference on artificial intelligence (ijcai’13) ( 854-860).  IJCAI/AAAI Press.
  * Fisher . (2005) TIMEHandbookFisher, M., Gabbay, D. Vila, L. ().  2005\.  Handbook of Temporal Reasoning in Artificial Intelligence Handbook of temporal reasoning in artificial intelligence ( 1).  Elsevier Science.
  * Gebser . (2016) gekakaosscwa16aGebser, M., Kaminski, R., Kaufmann, B., Ostrowski, M., Schaub, T. Wanko, P.  2016\.  Theory Solving Made Easy with Clingo 5 Theory solving made easy with clingo 5.  M. Carro A. King (), Technical Communications of the Thirty-second International Conference on Logic Programming (ICLP’16) Technical communications of the thirty-second international conference on logic programming (iclp’16) ( 52, 2:1-2:15).  Schloss Dagstuhl–Leibniz-Zentrum fuer Informatik.
  * Harel . (2000) hatiko00aHarel, D., Tiuryn, J. Kozen, D.  2000\.  Dynamic Logic Dynamic logic.  MIT Press.  10.1145/568438.568456
  * Heyting (1930) heyting30aHeyting, A.  1930\.  Die formalen Regeln der intuitionistischen Logik Die formalen Regeln der intuitionistischen Logik.  Sitzungsberichte der Preussischen Akademie der Wissenschaften Sitzungsberichte der preussischen akademie der wissenschaften ( 42-56).  Deutsche Akademie der Wissenschaften zu Berlin.
  * Koymans (1990) koymans90aKoymans, R.  1990\.  Specifying Real-Time Properties with Metric Temporal Logic Specifying real-time properties with metric temporal logic.  Real-Time Systems24255-299.
  * Lifschitz (1999) lifschitz99bLifschitz, V.  1999\.  Answer set planning Answer set planning.  D. de Schreye (), Proceedings of the International Conference on Logic Programming (ICLP’99) Proceedings of the international conference on logic programming (iclp’99) ( 23-37).  MIT Press.
  * Pearce (1997) pearce96aPearce, D.  1997\.  A New Logical Characterisation of Stable Models and Answer Sets A new logical characterisation of stable models and answer sets.  J. Dix, L. Pereira T. Przymusinski (), Proceedings of the Sixth International Workshop on Non-Monotonic Extensions of Logic Programming (NMELP’96) Proceedings of the sixth international workshop on non-monotonic extensions of logic programming (nmelp’96) ( 1216, 57-70).  Springer-Verlag.  10.1007/BFb0023801
  * Pnueli (1977) pnueli77aPnueli, A.  1977\.  The Temporal Logic of Programs The temporal logic of programs.  Proceedings of the Eight-teenth Symposium on Foundations of Computer Science (FOCS’77) Proceedings of the eight-teenth symposium on foundations of computer science (focs’77) ( 46-57).  IEEE Computer Society Press.  10.1109/SFCS.1977.32
  * Pratt (1976) pratt76aPratt, V.  1976\.  Semantical Consideration on Floyd-Hoare Logic Semantical consideration on floyd-hoare logic.  Proceedings of the Seventeenth Annual Symposium on Foundations of Computer Science (SFCS’76) Proceedings of the seventeenth annual symposium on foundations of computer science (sfcs’76) ( 109-121).  IEEE Computer Society Press.

##  Appendix A Auxiliary results

######  Definition 4 (Well-founded subexpression Harel . (2000)).

In Dynamic Logic, an _expression_ can be either a path expression or a
formula. Either one can be a subexpression of the other because of the mixed
operators ${[~{}]\,}_{I}$, ${\langle~{}\rangle\,}_{I}$ and the test $?$.

######  Remark 1.

For all $a,b,c\in\mathbb{Z}$, the following relations hold:

  * •

$a-b<c$ iff $b-a>-c$

  * •

$a-b\leq c$ iff $b-a\geq-c$

  * •

$a-b>c$ iff $b-a<-c$

  * •

$a-b\leq-c$ iff $b-a\geq c$

######  Proposition 8.

For all $x\in\mathbb{N}$ and for all traces $\mathbf{M}$,
${\parallel}{\uptau^{x}}{\parallel}^{\mathbf{M}}=\\{(a,a+x)\\}$

######  Proposition 9.

For all formulas $\varphi$ and for all traces $\mathbf{M}$,

${\parallel}{(\varphi?;\uptau)^{*}}{\parallel}^{\mathbf{M}}=\\{(a,b)\mid a\leq
b\text{ and }\mathbf{M},i\models\varphi\text{ for all }a\leq i<b\\}.$

######  Proposition 10.

For all formulas $\varphi$ and for all traces $\mathbf{M}$,

${\parallel}{(\varphi?;\uptau^{-})^{*}}{\parallel}^{\mathbf{M}}=\\{(a,b)\mid
a\geq b\text{ and }\mathbf{M},i\models\varphi\text{ for all }b<i\leq a\\}.$

##  Appendix B Proofs

###### Proof.

(Proposition 1)

We consider all the cases next:

  * •

Case $\varphi\wedge\psi$. We remind the reader that
$\varphi\wedge\psi\mathbin{\raisebox{-1.0pt}[-3.0pt][0.0pt]{$\stackrel{{\scriptstyle\mathit{def}}}{{=}}$}}\langle\varphi?\rangle\,{\psi}$.
The proof goes as follows:

$\displaystyle\phantom{\text{iff}}\mathbf{M},k\models\langle\varphi?\rangle\,{\psi}$
$\displaystyle\text{ iff
}\mathbf{M},k\models\langle\varphi?\rangle_{(-\omega..\omega)}\,{\psi}$
$\displaystyle\text{by definition of }\langle\rho\rangle\,{\varphi}\text{ in
}\eqref{def:dht:mdht}$ $\displaystyle\text{ iff }\mathbf{M},i\models\psi\text{
for some }i\text{ with }(k,i)\in{\parallel}{\varphi?}{\parallel}^{\mathbf{M}}$
$\displaystyle\quad\text{ and }\tau(i)-\tau(k)\in(-\omega..\omega)$
$\displaystyle\text{by
Definition}~{}\ref{def:mdht:satisfaction}\eqref{def:mdhtsat:eventually:f}$
$\displaystyle\text{ iff }\mathbf{M},i\models\psi\text{ for some }i\text{ with
}(k,i)\in{\parallel}{\varphi?}{\parallel}^{\mathbf{M}}$ $\displaystyle\text{
since }\tau(i)-\tau(k)\in\mathbb{Z}$ $\displaystyle\text{ iff
}\mathbf{M},k\models\varphi\text{ and }\mathbf{M},k\models\psi$
$\displaystyle\text{ since
}(k,k)\in{\parallel}{\varphi?}{\parallel}^{\mathbf{M}}$ $\displaystyle\text{
iff }\mathbf{M},k\models\varphi\wedge\psi.$

  * •

Case $\varphi\vee\psi$. We remind the reader that
$\varphi\vee\psi\mathbin{\raisebox{-1.0pt}[-3.0pt][0.0pt]{$\stackrel{{\scriptstyle\mathit{def}}}{{=}}$}}\langle\varphi?+\psi?\rangle\,\top$.
The proof is presented below.

$\displaystyle\phantom{\text{iff}}\mathbf{M},k\models\langle\varphi?+\psi?\rangle\,\top$
$\displaystyle\text{ iff
}\mathbf{M},k\models\langle\varphi?+\psi?\rangle_{(-\omega..\omega)}\,{\top}$
$\displaystyle\text{by definition of }\langle\rho\rangle\,{\varphi}\text{ in
}\eqref{def:dht:mdht}$ $\displaystyle\text{ iff }\mathbf{M},i\models\top\text{
for some }(k,i)\in{\parallel}{\varphi?+\psi?}{\parallel}^{\mathbf{M}}$
$\displaystyle\quad\text{ and }\tau(i)-\tau(k)\in(-\omega..\omega)$
$\displaystyle\text{by
Definition}~{}\ref{def:mdht:satisfaction}\eqref{def:mdhtsat:eventually:f}$
$\displaystyle\text{ iff }\text{ there exists
}(k,i)\in{\parallel}{\varphi?+\psi?}{\parallel}^{\mathbf{M}}$
$\displaystyle\text{ since }\tau(i)-\tau(k)\in\mathbb{Z}$ $\displaystyle\text{
iff there exists
}(k,i)\in{\parallel}{\varphi?}{\parallel}^{\mathbf{M}}\cup{\parallel}{\psi?}{\parallel}^{\mathbf{M}}$
$\displaystyle{\parallel}{\varphi?+\psi?}{\parallel}^{\mathbf{M}}\mathbin{\raisebox{-1.0pt}[-3.0pt][0.0pt]{$\stackrel{{\scriptstyle\mathit{def}}}{{=}}$}}{\parallel}{\varphi?}{\parallel}^{\mathbf{M}}\cup{\parallel}{\psi?}{\parallel}^{\mathbf{M}}$
$\displaystyle\text{ iff }k=i\text{ and }\mathbf{M},k\models\varphi\hbox{ or
}\mathbf{M},k\models\psi$ $\displaystyle\text{ definition of
}{\parallel}{\varphi?}{\parallel}^{\mathbf{M}}\text{ and
}{\parallel}{\psi?}{\parallel}^{\mathbf{M}}$
$\displaystyle\mathbf{M},k\models\varphi\vee\psi$

  * •

Case $\varphi\to\psi$. We remind the reader that
$\varphi\to\psi\mathbin{\raisebox{-1.0pt}[-3.0pt][0.0pt]{$\stackrel{{\scriptstyle\mathit{def}}}{{=}}$}}[\varphi?]\,\psi$
and we present the proof next

$\displaystyle\phantom{\text{iff}}\mathbf{M},k\models[\varphi?]\,\psi$
$\displaystyle\text{ iff
}\mathbf{M},k\models[\varphi?]_{(-\omega..\omega)}\,{\psi}$
$\displaystyle\text{by definition of }[\rho]\,{\varphi}\text{ in
}\eqref{def:dht:mdht}$ $\displaystyle\text{ iff
}\mathbf{M}^{\prime},i\models\psi\text{ for all
}(k,i)\in{\parallel}{\varphi?}{\parallel}^{\mathbf{M}^{\prime}}\text{
satisfying }$ $\displaystyle\quad\tau(i)-\tau(k)\in(-\omega..\omega)\text{ and
for both }$ $\displaystyle\quad\mathbf{M}^{\prime}=\mathbf{M}\text{ and
}\mathbf{M}^{\prime}=\langle\mathbf{T},\mathbf{T},\tau\rangle$
$\displaystyle\text{by
Definition}~{}\ref{def:mdht:satisfaction}\eqref{def:mdhtsat:always:f}$
$\displaystyle\text{ iff for all }i\text{ we have
}\mathbf{M}^{\prime},i\models\psi\text{ if }i=k\text{ and
}\mathbf{M}^{\prime}\models\varphi$ $\displaystyle\text{ since
}(k,i)\in{\parallel}{\varphi?}{\parallel}^{\mathbf{M}^{\prime}}$
$\displaystyle\quad\text{for both }\mathbf{M}^{\prime}=\mathbf{M}\text{ and
}\mathbf{M}^{\prime}=\langle\mathbf{T},\mathbf{T},\tau\rangle$
$\displaystyle\text{ and }\tau(i)-\tau(k)\in\mathbb{Z}$ $\displaystyle\text{
iff }\mathbf{M}^{\prime},k\models\psi\text{ if
}\mathbf{M}^{\prime}\models\varphi\text{ for both }$
$\displaystyle\quad\mathbf{M}^{\prime}=\mathbf{M}\text{ and
}\mathbf{M}^{\prime}=\langle\mathbf{T},\mathbf{T},\tau\rangle$
$\displaystyle\text{ since }i=k$ $\displaystyle\text{ iff
}\mathbf{M},k\models\varphi\rightarrow\psi.$

∎

###### Proof.

(Proposition 2)

We proceed by induction on the well-founded subexpression relation taking into
account the following considerations: for any arbitrary subexpression $\gamma$
of an expression $\varphi$:

  * (A)

Persistence holds if $\gamma$ is a formula and

  * (B)

${\parallel}{\gamma}{\parallel}^{\langle{\mathbf{H},\mathbf{T}},\tau\rangle}\subseteq{\parallel}{\gamma}{\parallel}^{\langle{\mathbf{T},\mathbf{T}},\tau\rangle}$
holds if $\gamma$ is a path expression.

First we show (A) by assuming that the induction hypothesis (A) and (B) hold
for proper subexpressions of $\varphi$.

  * •

Case of $\varphi=a\in\mathcal{A}$: if
$\langle\mathbf{H},\mathbf{T},\tau\rangle,k\models a$ then
$a\in\mathbf{H}_{k}$ by the HT semantics. Since
$\mathbf{H}_{k}\subseteq\mathbf{T}_{k}$ then $a\in\mathbf{T}_{k}$. Finally,
$\langle\mathbf{T},\mathbf{T},\tau\rangle,k\models a$ because of the HT
semantics.

  * •

Case of $\varphi=\bot$: it trivially holds that
$\langle\mathbf{T},\mathbf{T},\tau\rangle,k\not\models\bot$.

  * •

Case of $\varphi=\langle\rho\rangle_{I}\,\varphi$: if
$\langle\mathbf{H},\mathbf{T},\tau\rangle,k\models\langle\rho\rangle_{I}\,\varphi$
then $\langle\mathbf{H},\mathbf{T},\tau\rangle,i\models\varphi$ for some
$(k,i)\in{\parallel}{\rho}{\parallel}^{\langle\mathbf{H},\mathbf{T},\tau\rangle}$
and $\tau(i)-\tau(k)\in I$, because of the HT semantics.

By applying the induction hypothesis (A) on $\varphi$ and (B) on $\rho$ we get
that $\langle\mathbf{T},\mathbf{T},\tau\rangle,i\models\varphi$ and
$(k,i)\in{\parallel}{\rho}{\parallel}^{\langle\mathbf{T},\mathbf{T},\tau\rangle}$.
Finally, by the HT semantics we get
$\langle\mathbf{T},\mathbf{T},\tau\rangle,k\models\langle\rho\rangle_{I}\,\varphi$.

  * •

Case of $\varphi=[\rho]_{I}\,\varphi$: if
$\langle\mathbf{H},\mathbf{T},\tau\rangle,k\models[\rho]_{I}\,\varphi$ then
$\langle\mathbf{H},\mathbf{T},\tau\rangle,i\models\varphi$ for all
$(k,i)\in{\parallel}{\rho}{\parallel}^{\mathbf{M}^{\prime}}$ satisfying
$\tau(i)-\tau(k)\in I$ and for both
$\mathbf{M}^{\prime}=\langle\mathbf{H},\mathbf{T},\tau\rangle$ and
$\mathbf{M}^{\prime}=\langle\mathbf{T},\mathbf{T},\tau\rangle$. By the HT
semantics we directly get
$\langle\mathbf{T},\mathbf{T},\tau\rangle,k\models[\rho]_{I}\,\varphi$666Notice
that the HT semantics forces formulas of the type $[\rho]_{I}\,\varphi$ to be
satisfied in the “there” component. Therefore no induction hypothesis is
needed in this case.

To prove the property (B) we prove the following equivalent property: for all
$(k,i)\in\mathbb{N}\times\mathbb{N}$ and for all path expressions $\rho$

$(k,i)\in{\parallel}{\rho}{\parallel}^{\langle\mathbf{H},\mathbf{T},\tau\rangle}\hbox{
implies
}(k,i)\in{\parallel}{\rho}{\parallel}^{\langle\mathbf{T},\mathbf{T},\tau\rangle}.$

  * •

Case $\rho=\uptau$: if
$(k,i)\in{\parallel}{\uptau}{\parallel}^{\langle\mathbf{H},\mathbf{T},\tau\rangle}$
then, by definition, $i=k+1$. Again, by the definition of
${\parallel}{\uptau}{\parallel}^{\langle\mathbf{T},\mathbf{T},\tau\rangle}$,
$(k,i)\in{\parallel}{\uptau}{\parallel}^{\langle\mathbf{T},\mathbf{T},\tau\rangle}$.

  * •

Case $\rho=\varphi?$: if
$(k,i)\in{\parallel}{\varphi?}{\parallel}^{\langle\mathbf{H},\mathbf{T},\tau\rangle}$
then, by definition $i=k$ and
$\langle\mathbf{H},\mathbf{T},\tau\rangle,k\models\varphi$. By applying the
induction hypothesis (A) on $\varphi$ we get
$\langle\mathbf{T},\mathbf{T},\tau\rangle,k\models\varphi$. Finally, by the
definition of
${\parallel}{\varphi?}{\parallel}^{\langle\mathbf{H},\mathbf{T},\tau\rangle}$,
$(k,i)\in{\parallel}{\varphi?}{\parallel}^{\langle\mathbf{T},\mathbf{T},\tau\rangle}$.

  * •

Case $\rho=\rho_{1}+\rho_{2}$: if
$(k,i)\in{\parallel}{\rho_{1}\mathrel{+}\rho_{2}}{\parallel}^{\langle\mathbf{H},\mathbf{T},\tau\rangle}$
then, by the definition of
${\parallel}{\rho_{1}\mathrel{+}\rho_{2}}{\parallel}^{\langle\mathbf{H},\mathbf{T},\tau\rangle}$,
either
$(k,i)\in{\parallel}{\rho_{1}}{\parallel}^{\langle\mathbf{H},\mathbf{T},\tau\rangle}$
or
$(k,i)\in{\parallel}{\rho_{2}}{\parallel}^{\langle\mathbf{H},\mathbf{T},\tau\rangle}$.
By applying the induction hypothesis (B) on $\rho_{1}$ and $\rho_{2}$ we
obtain that either
$(k,i)\in{\parallel}{\rho_{1}}{\parallel}^{\langle\mathbf{T},\mathbf{T},\tau\rangle}$
or
$(k,i)\in{\parallel}{\rho_{2}}{\parallel}^{\langle\mathbf{T},\mathbf{T},\tau\rangle}$.
By the definition of
${\parallel}{\rho_{1}\mathrel{+}\rho_{2}}{\parallel}^{\langle\mathbf{T},\mathbf{T},\tau\rangle}$
it follows that
$(k,i)\in{\parallel}{\rho_{1}\mathrel{+}\rho_{2}}{\parallel}^{\langle\mathbf{H},\mathbf{T},\tau\rangle}$

  * •

Case $\rho=\rho_{1};\rho_{2}$: if
$(k,i)\in{\parallel}{\rho_{1};\rho_{2}}{\parallel}^{\langle\mathbf{H},\mathbf{T},\tau\rangle}$
then
$(k,j)\in{\parallel}{\rho_{1}}{\parallel}^{\langle\mathbf{H},\mathbf{T},\tau\rangle}$
and
$(j,i)\in{\parallel}{\rho_{2}}{\parallel}^{\langle\mathbf{H},\mathbf{T},\tau\rangle}$
for some $i\in\mathbb{N}$. If we apply the induction hypothesis (B) on
$\rho_{1}$ and $\rho_{2}$ we get
$(k,j)\in{\parallel}{\rho_{1}}{\parallel}^{\langle\mathbf{T},\mathbf{T},\tau\rangle}$
and
$(j,i)\in{\parallel}{\rho_{2}}{\parallel}^{\langle\mathbf{T},\mathbf{T},\tau\rangle}$.
By the definition of
${\parallel}{\rho_{1};\rho_{2}}{\parallel}^{\langle\mathbf{H},\mathbf{T},\tau\rangle}$
we get
$(k,i)\in{\parallel}{\rho_{1};\rho_{2}}{\parallel}^{\langle\mathbf{T},\mathbf{T},\tau\rangle}$

  * •

Case $\rho=\rho^{-}$: if
$(k,i)\in{\parallel}{{\rho}^{-}}{\parallel}^{\langle\mathbf{H},\mathbf{T},\tau\rangle}$
then
$(i,k)\in{\parallel}{\rho}{\parallel}^{\langle\mathbf{H},\mathbf{T},\tau\rangle}$
by definition. By applying the induction hypothesis (B) on $\rho$ we get that
$(i,k)\in{\parallel}{\rho}{\parallel}^{\langle\mathbf{T},\mathbf{T},\tau\rangle}$
and, again, by definition
$(k,i)\in{\parallel}{{\rho}^{-}}{\parallel}^{\langle\mathbf{T},\mathbf{T},\tau\rangle}$

  * •

Case $\rho=\rho^{*}$: Let us claim that :

$\text{for all
}n\in\mathbb{N},\;{\parallel}{\rho^{n}}{\parallel}^{\langle\mathbf{H},\mathbf{T},\tau\rangle}\subseteq{\parallel}{\rho^{n}}{\parallel}^{\langle\mathbf{T},\mathbf{T},\tau\rangle}$
(23)

holds. If
$(k,i)\in{\parallel}{\rho^{*}}{\parallel}^{\langle\mathbf{H},\mathbf{T},\tau\rangle}$
then
$(k,i)\in{\parallel}{\rho^{n}}{\parallel}^{\langle\mathbf{H},\mathbf{T},\tau\rangle}$
for some $n\in\mathbb{N}$. By (23),
$(k,i)\in{\parallel}{\rho^{n}}{\parallel}^{\langle\mathbf{T},\mathbf{T},\tau\rangle}$.By
the definition of
${\parallel}{\rho^{*}}{\parallel}^{\langle\mathbf{T},\mathbf{T},\tau\rangle}$,
$(k,i)\in{\parallel}{\rho^{*}}{\parallel}^{\langle\mathbf{T},\mathbf{T},\tau\rangle}$.

To finish the proof of the property (B) we need to prove (23), which is done
by induction on $\mathbb{N}$.

    * –

Case $n=0$: if
$(k,i)\in{\parallel}{\rho^{0}}{\parallel}^{\langle\mathbf{H},\mathbf{T},\tau\rangle}$
then
$(k,i)\in{\parallel}{\top?}{\parallel}^{\langle\mathbf{H},\mathbf{T},\tau\rangle}$.
By definition, $i=k$. By the definition of
${\parallel}{\rho^{0}}{\parallel}^{\langle\mathbf{T},\mathbf{T},\tau\rangle}$
it follows that
$(k,i)\in{\parallel}{\rho^{0}}{\parallel}^{\langle\mathbf{T},\mathbf{T},\tau\rangle}$

    * –

inductive step: Assume that (23) holds for all $0\leq i\leq n$ and let us
prove it for $n+1$. If
$(k,i)\in{\parallel}{\rho^{n+1}}{\parallel}^{\langle\mathbf{H},\mathbf{T},\tau\rangle}$
then
$(k,i)\in{\parallel}{\rho;\rho^{n}}{\parallel}^{\langle\mathbf{H},\mathbf{T},\tau\rangle}$
by definition. Consequently,
$(k,j)\in{\parallel}{\rho}{\parallel}^{\langle\mathbf{H},\mathbf{T},\tau\rangle}$
and
$(j,i)\in{\parallel}{\rho^{n}}{\parallel}^{\langle\mathbf{H},\mathbf{T},\tau\rangle}$
for some $j\in\mathbb{N}$. By applying the induction hypothesis (B) on $\rho$
and the induction on $n$ we conclude that
$(k,j)\in{\parallel}{\rho}{\parallel}^{\langle\mathbf{T},\mathbf{T},\tau\rangle}$
and
$(j,i)\in{\parallel}{\rho^{n}}{\parallel}^{\langle\mathbf{T},\mathbf{T},\tau\rangle}$.
By definition of
${\parallel}{\rho^{n+1}}{\parallel}^{\langle\mathbf{T},\mathbf{T},\tau\rangle}$
we get that
$(k,i)\in{\parallel}{\rho^{n+1}}{\parallel}^{\langle\mathbf{T},\mathbf{T},\tau\rangle}$.

∎

###### Proof.

(Proposition 4)

Proof by induction on the well-founded subexpression relation. As a remark,
note that under the assumption of total traces, the law of excluded middle is
satisfied and this makes that $\mathrm{MDHT}$ formulas to be satisfied as in
$\mathrm{MDL}$. ∎

###### Proof.

(Proposition 5)

By induction on the well-founded subexpression relation. Note that the absence
of implications implies that the world ‘here’ is the only one used in the
evaluation of a formula. ∎

###### Proof.

(Proposition 6)

We consider all the cases below:

  * •

Case $\langle\rho\rangle\,{\varphi}$: we remind the reader that
$\langle\rho\rangle\,{\varphi}\mathbin{\raisebox{-1.0pt}[-3.0pt][0.0pt]{$\stackrel{{\scriptstyle\mathit{def}}}{{=}}$}}\langle\rho\rangle_{(-\omega..\omega)}\,{\varphi}$.
The proof is presented next.

$\displaystyle\mathbf{M},k\models\langle\rho\rangle_{(-\omega..\omega)}\,{\varphi}$
$\displaystyle\text{ iff }\mathbf{M},i\models\varphi\text{ for some
}(k,i)\in{\parallel}{\rho}{\parallel}^{\mathbf{M}}$ $\displaystyle\quad\text{
such that }\tau(i)-\tau(k)\in(-\omega..\omega)$ $\displaystyle\text{by
Definition}~{}\ref{def:mdht:satisfaction}\eqref{def:mdhtsat:eventually:f}$
$\displaystyle\text{ iff }\mathbf{M},i\models\varphi\text{ for some
}(k,i)\in{\parallel}{\rho}{\parallel}^{\mathbf{M}}$ $\displaystyle\text{since
}\tau(i)-\tau(k)\in\mathbb{Z}$

  * •

Case $[\rho]\,{\varphi}$: we remind the reader that
$[\rho]\,{\varphi}\mathbin{\raisebox{-1.0pt}[-3.0pt][0.0pt]{$\stackrel{{\scriptstyle\mathit{def}}}{{=}}$}}[\rho]_{(-\omega..\omega)}\,{\varphi}$.
The proof is presented below.

$\displaystyle[\rho]_{(-\omega..\omega)}\,{\varphi}$ $\displaystyle\text{ iff
}\mathbf{M}^{\prime},i\models\varphi\text{ for all
}(k,i)\in{\parallel}{\rho}{\parallel}^{\mathbf{M}^{\prime}}$
$\displaystyle\quad\text{satisfying }\tau(i)-\tau(k)\in(-\omega..\omega)$
$\displaystyle\quad\text{and for both
}\mathbf{M}^{\prime}=\langle\mathbf{H},\mathbf{T},\tau\rangle\text{ and
}\mathbf{M}^{\prime}=\langle\mathbf{T},\mathbf{T},\tau\rangle$
$\displaystyle\text{by
Definition}~{}\ref{def:mdht:satisfaction}\eqref{def:mdhtsat:always:f}$
$\displaystyle\text{ iff }\mathbf{M}^{\prime},i\models\varphi\text{ for all
}(k,i)\in{\parallel}{\rho}{\parallel}^{\mathbf{M}^{\prime}}$
$\displaystyle\quad\text{and for both
}\mathbf{M}^{\prime}=\langle\mathbf{H},\mathbf{T},\tau\rangle\text{ and
}\mathbf{M}^{\prime}=\langle\mathbf{T},\mathbf{T},\tau\rangle$
$\displaystyle\text{since }\tau(i)-\tau(k)\in\mathbb{Z}$

∎

###### Proof.

(Proposition 7)

Before presenting the proof, let us introduce the following considerations:

  1. 1.

We will work with a timed trace $\mathbf{M}=$ of length $\lambda$;

  2. 2.

We will denote by
$\mathbb{D}\mathbin{\raisebox{-1.0pt}[-3.0pt][0.0pt]{$\stackrel{{\scriptstyle\mathit{def}}}{{=}}$}}\\{i\mid
0\leq i<\lambda\\}$ the possible states of $\mathbf{M}$ and

  3. 3.

We will implicitly consider that $m,n\in\mathbb{N}$.

Notice that, for any path expression $\rho$ and for any model $\mathbf{M}$,
${\parallel}{\rho}{\parallel}^{\mathbf{M}}\subseteq\mathbb{D}\times\mathbb{D}$.
We consider all cases next:

  * •

Case $\bm{\mathsf{I}}$: note that
$\bm{\mathsf{I}}\mathbin{\raisebox{-1.0pt}[-3.0pt][0.0pt]{$\stackrel{{\scriptstyle\mathit{def}}}{{=}}$}}[{\uptau}^{-}]\,{\bot}$
by Definition (17). Therefore
$\bm{\mathsf{I}}\mathbin{\raisebox{-1.0pt}[-3.0pt][0.0pt]{$\stackrel{{\scriptstyle\mathit{def}}}{{=}}$}}[{\uptau}^{-}]_{(-\omega..\omega)}\,{\bot}$
because of Definition (4). The rest of the proof goes as follows:

$\displaystyle\mathbf{M},k\models[{\uptau}^{-}]_{(-\omega..\omega)}\,{\bot}\text{
iff }\mathbf{M}^{\prime},i\models\bot\text{ if
}(k,i)\in{\parallel}{{\uptau}^{-}}{\parallel}^{\mathbf{M}^{\prime}}\text{ and
}$ $\displaystyle\quad\tau(i)-\tau(k)\in(-\omega..\omega),\;\text{for all
}(k,i)\in\mathbb{D}\times\mathbb{D}$ $\displaystyle\quad\text{ and
}\mathbf{M}^{\prime}\in\\{\mathbf{M},\langle\mathbf{T},\mathbf{T},\tau\rangle\\}$
$\displaystyle\text{by the satisfaction of }{[\rho]\,}_{I}\varphi$
$\displaystyle\text{ iff }\mathbf{M}^{\prime},i\models\bot\text{ if
}(i,k)\in{\parallel}{\uptau}{\parallel}^{\mathbf{M}^{\prime}}\text{ and
}\tau(i)-\tau(k)\in(-\omega..\omega),$ $\displaystyle\quad\text{for all
}(k,i)\in\mathbb{D}\times\mathbb{D}\text{ and
}\mathbf{M}^{\prime}\in\\{\mathbf{M},\langle\mathbf{T},\mathbf{T},\tau\rangle\\}$
$\displaystyle\text{by the definition of
}{\parallel}{\uptau^{-}}{\parallel}^{\mathbf{M}^{\prime}}$
$\displaystyle\text{ iff }\mathbf{M}^{\prime},i\models\bot\text{ if
}i=k-1\text{ and }\tau(i)-\tau(k)\in(-\omega..\omega),$
$\displaystyle\quad\text{for all }(k,i)\in\mathbb{D}\times\mathbb{D}\text{ and
}\mathbf{M}^{\prime}\in\\{\mathbf{M},\langle\mathbf{T},\mathbf{T},\tau\rangle\\}$
$\displaystyle\text{by the definition of
}{\parallel}{\uptau}{\parallel}^{\mathbf{M}^{\prime}}$ $\displaystyle\text{
iff }\mathbf{M}^{\prime},i\models\bot\text{ if }i=k-1\text{ for all
}(k,i)\in\mathbb{D}\times\mathbb{D}$ $\displaystyle\quad\text{ and
}\mathbf{M}^{\prime}\in\\{\mathbf{M},\langle\mathbf{T},\mathbf{T},\tau\rangle\\}$
$\displaystyle\tau(i)-\tau(k)\in(-\omega..\omega)$ $\displaystyle\text{ iff
}k=0.$

  * •

Case of $\bm{\mathsf{F}}$: note that
$\bm{\mathsf{F}}\mathbin{\raisebox{-1.0pt}[-3.0pt][0.0pt]{$\stackrel{{\scriptstyle\mathit{def}}}{{=}}$}}[\uptau]\,{\bot}$
by Definition of $\bm{\mathsf{F}}$. Since
$[\uptau]\,{\bot}\equiv[\uptau]_{(-\omega..\omega)}\,{\bot}$, we conclude that
$\bm{\mathsf{F}}\equiv[\uptau]_{(-\omega..\omega)}\,{\bot}$. The rest of the
proof goes as follows.

$\displaystyle\mathbf{M},k\models[\uptau]_{(-\omega..\omega)}\,{\bot}\text{
iff }\mathbf{M}^{\prime},i\models\bot\text{ if
}(k,i)\in{\parallel}{\uptau}{\parallel}^{\mathbf{M}^{\prime}}\text{ and }$
$\displaystyle\quad\tau(i)-\tau(k)\in(-\omega..\omega),\;\text{for all
}(k,i)\in\mathbb{D}\times\mathbb{D}$ $\displaystyle\quad\text{ and
}\mathbf{M}^{\prime}\in\\{\mathbf{M},\langle\mathbf{T},\mathbf{T},\tau\rangle\\}$
$\displaystyle\text{by the satisfaction of }{[\rho]\,}_{I}\varphi$
$\displaystyle\text{ iff }\mathbf{M}^{\prime},i\models\bot\text{ if
}i=k+1\text{ and }\tau(i)-\tau(k)\in(-\omega..\omega)$
$\displaystyle\quad\text{for all }(k,i)\in\mathbb{D}\times\mathbb{D}\text{ and
}\mathbf{M}^{\prime}\in\\{\mathbf{M},\langle\mathbf{T},\mathbf{T},\tau\rangle\\}$
$\displaystyle\text{by definition of
}{\parallel}{\uptau}{\parallel}^{\mathbf{M}^{\prime}}$ $\displaystyle\text{
iff }\mathbf{M}^{\prime},i\models\bot\text{ if }i=k+1,\;\text{ for all
}(k,i)\in\mathbb{D}\times\mathbb{D}$ $\displaystyle\quad\text{ and
}\mathbf{M}^{\prime}\in\\{\mathbf{M},\langle\mathbf{T},\mathbf{T},\tau\rangle\\}$
$\displaystyle\tau(i)-\tau(k)\in(-\omega..\omega)$ $\displaystyle\text{ iff
}k=\lambda-1.$

  * •

Case of ${}_{[m,n)}\varphi$: note that
${}_{[m,n)}\varphi\mathbin{\raisebox{-1.0pt}[-3.0pt][0.0pt]{$\stackrel{{\scriptstyle\mathit{def}}}{{=}}$}}\langle\uptau\rangle\,_{[m,n)}\varphi$.
Having this in mind, we present the proof below

$\displaystyle\mathbf{M},k\models\langle\uptau\rangle\,_{[m,n)}\varphi$
$\displaystyle\text{ iff }\mathbf{M},i\models\varphi\text{ for some
}(k,i)\in{\parallel}{\uptau}{\parallel}^{\mathbf{M}}$
$\displaystyle\quad\text{ and }\tau(i)-\tau(k)\in[m,n)$ $\displaystyle\text{by
the satisfaction of}{\langle\rho\rangle\,}_{I}\varphi$ $\displaystyle\text{
iff }\mathbf{M},i\models\varphi\text{ and }0\leq i=k+1<\lambda\text{ and }$
$\displaystyle\quad\tau(i)-\tau(k)\in[m,n)$ $\displaystyle\text{by the
definition of }{\parallel}{\uptau}{\parallel}^{\mathbf{M}}$
$\displaystyle\text{ iff }k+1<\lambda\text{ and }\mathbf{M},k+1\models\varphi$
$\displaystyle\quad\text{ and }\tau(k+1)-\tau(k)\in[m,n)$ $\displaystyle
i=k+1<\lambda$ $\displaystyle\text{ iff }\mathbf{M},k\models_{[m,n)}\varphi.$

  * •

Case of $\widehat{}_{[m,n)}\varphi$: note that
$\widehat{}_{[m,n)}\varphi\mathbin{\raisebox{-1.0pt}[-3.0pt][0.0pt]{$\stackrel{{\scriptstyle\mathit{def}}}{{=}}$}}[\uptau]\,_{[m,n)}\varphi$.
Having this in mind, we present the proof below

$\displaystyle\mathbf{M},k\models[\uptau]\,_{[m,n)}\varphi$
$\displaystyle\text{ iff }\mathbf{M}^{\prime},i\models\varphi\text{ if
}(k,i)\in{\parallel}{\uptau}{\parallel}^{\mathbf{M}^{\prime}}\text{ and }$
$\displaystyle\quad\tau(i)-\tau(k)\in[m,n)\text{ for all
}(k,i)\in\mathbb{D}\times\mathbb{D}$ $\displaystyle\quad\text{ and
}\mathbf{M}^{\prime}\in\\{\mathbf{M},\langle\mathbf{T},\mathbf{T},\tau\rangle\\}$
$\displaystyle\text{satisfaction of }{[\rho]\,}_{I}\varphi$
$\displaystyle\text{ iff }\mathbf{M}^{\prime},i\models\varphi\text{ if }0\leq
i=k+1<\lambda\text{ and }$ $\displaystyle\quad\tau(i)-\tau(k)\in[m,n),\text{
for all
}\mathbf{M}^{\prime}\in\\{\mathbf{M},\langle\mathbf{T},\mathbf{T},\tau\rangle\\}$
$\displaystyle\text{definition of
}{\parallel}{\uptau}{\parallel}^{\mathbf{M}^{\prime}}$ $\displaystyle\text{
iff }\mathbf{M}^{\prime},k+1\models\varphi\text{ if }k+1<\lambda\text{ and }$
$\displaystyle\quad\tau(k+1)-\tau(k)\in[m,n)\text{ for all
}\mathbf{M}^{\prime}\in\\{\mathbf{M},\langle\mathbf{T},\mathbf{T},\tau\rangle\\}$
$\displaystyle i=k+1$ $\displaystyle\text{ iff
}\mathbf{M},k\models\widehat{}_{[m,n)}\varphi$

  * •

Case of $\text{\rm\raisebox{-0.5pt}{\Large\textbullet}}_{[m,n)}\varphi$: note
that
$\text{\rm\raisebox{-0.5pt}{\Large\textbullet}}_{[m,n)}\varphi\mathbin{\raisebox{-1.0pt}[-3.0pt][0.0pt]{$\stackrel{{\scriptstyle\mathit{def}}}{{=}}$}}\langle{\uptau}^{-}\rangle\,_{(-n,-m]}\varphi$.
Having this in mind, we present the proof below

$\displaystyle\mathbf{M},k\models\langle{\uptau}^{-}\rangle\,_{(-n,-m]}\varphi$
$\displaystyle\text{ iff }\mathbf{M},i\models\varphi\text{ for some
}(k,i)\in{\parallel}{{\uptau}^{-}}{\parallel}^{\mathbf{M}}$
$\displaystyle\quad\text{ and }\tau(i)-\tau(k)\in(-n,-m]$
$\displaystyle\text{by the satisfaction of}{\langle\rho\rangle\,}_{I}\varphi$
$\displaystyle\text{ iff }\mathbf{M},i\models\varphi\text{ for some
}(i,k)\in{\parallel}{\uptau}{\parallel}^{\mathbf{M}}$
$\displaystyle\quad\text{ and }\tau(i)-\tau(k)\in(-n,-m]$
$\displaystyle\text{by the definition of
}{\parallel}{{\uptau}^{-}}{\parallel}^{\mathbf{M}}$ $\displaystyle\text{ iff
}\mathbf{M},i\models\varphi\text{ and }\lambda>i=k-1\geq 0\text{ and }$
$\displaystyle\quad\tau(i)-\tau(k)\in(-n,-m]$ $\displaystyle\text{by
Definition of }{\parallel}{\uptau}{\parallel}^{\mathbf{M}}$
$\displaystyle\text{ iff }\mathbf{M},i\models\varphi\text{ and
}\lambda>i=k-1\geq 0\text{ and }$ $\displaystyle\quad\tau(k)-\tau(i)\in[m,n)$
by Remark 1 $\displaystyle\text{ iff }\lambda>k-1\geq 0\text{ and
}\mathbf{M},k-1\models\varphi$ $\displaystyle\quad\text{ and
}\tau(k)-\tau(k-1)\in[m,n)$ $\displaystyle i=k-1>0$ $\displaystyle\text{ iff
}\mathbf{M},k\models\text{\rm\raisebox{-0.5pt}{\Large\textbullet}}_{[m,n)}\varphi.$

  * •

Case of
$\widehat{\text{\rm\raisebox{-0.5pt}{\Large\textbullet}}}_{[m,n)}\varphi$:
note that
$\widehat{\text{\rm\raisebox{-0.5pt}{\Large\textbullet}}}_{[m,n)}\varphi\mathbin{\raisebox{-1.0pt}[-3.0pt][0.0pt]{$\stackrel{{\scriptstyle\mathit{def}}}{{=}}$}}[{\uptau}^{-}]\,_{(-n,-m]}\varphi$.
Having this in mind, we present the proof below

$\displaystyle\mathbf{M},k\models[{\uptau}^{-}]\,_{(-n,-m]}\varphi$
$\displaystyle\text{ iff }\mathbf{M}^{\prime},i\models\varphi\text{ if
}(k,i)\in{\parallel}{{\uptau}^{-}}{\parallel}^{\mathbf{M}^{\prime}}$
$\displaystyle\quad\text{ and }\tau(i)-\tau(k)\in(-n,-m],$
$\displaystyle\quad\text{ for all }(k,i)\in\mathbb{D}\times\mathbb{D}\text{
and
}\mathbf{M}^{\prime}\in\\{\mathbf{M},\langle\mathbf{T},\mathbf{T},\tau\rangle\\}$
$\displaystyle\text{satisfaction of }{[\rho]\,}_{I}\varphi$
$\displaystyle\text{ iff }\mathbf{M}^{\prime},i\models\varphi\text{ if
}(i,k)\in{\parallel}{\uptau}{\parallel}^{\mathbf{M}^{\prime}}$
$\displaystyle\quad\text{ and }\tau(i)-\tau(k)\in(-n,-m],$
$\displaystyle\quad\text{ for all }(k,i)\in\mathbb{D}\times\mathbb{D}\text{
and
}\mathbf{M}^{\prime}\in\\{\mathbf{M},\langle\mathbf{T},\mathbf{T},\tau\rangle\\}$
$\displaystyle\text{definition of
}{\parallel}{{\rho}^{-}}{\parallel}^{\mathbf{M}^{\prime}}$
$\displaystyle\text{ iff }\mathbf{M}^{\prime},i\models\varphi\text{ if
}\lambda>i=k-1\geq 0\text{ and }$
$\displaystyle\quad\tau(i)-\tau(k)\in(-n,-m],$ $\displaystyle\quad\text{ for
all
}\mathbf{M}^{\prime}\in\\{\mathbf{M},\langle\mathbf{T},\mathbf{T},\tau\rangle\\}$
$\displaystyle\text{definition of
}{\parallel}{\rho}{\parallel}^{\mathbf{M}^{\prime}}$ $\displaystyle\text{ iff
}\mathbf{M}^{\prime},i\models\varphi\text{ if }\lambda>i=k-1\geq 0\text{ and
}$ $\displaystyle\quad\tau(k)-\tau(i)\in[m,n)\text{, for all
}\mathbf{M}^{\prime}\in\\{\mathbf{M},\langle\mathbf{T},\mathbf{T},\tau\rangle\\}$
by Remark 1 $\displaystyle\text{ iff
}\mathbf{M}^{\prime},k-1\models\varphi\text{ if }k-1\geq 0\text{ and }$
$\displaystyle\quad\tau(k)-\tau(k-1)\in[m,n),$ $\displaystyle\quad\text{ for
all
}\mathbf{M}^{\prime}\in\\{\mathbf{M},\langle\mathbf{T},\mathbf{T},\tau\rangle\\}$
$\displaystyle i=k-1$

  * •

Case of $\Diamond_{[m,n)}\varphi$: as a reminder,
$\Diamond_{[m,n)}\varphi\mathbin{\raisebox{-1.0pt}[-3.0pt][0.0pt]{$\stackrel{{\scriptstyle\mathit{def}}}{{=}}$}}\langle\uptau^{*}\rangle\,_{[m,n)}\varphi$
as follows

$\displaystyle\mathbf{M},k\models\langle\uptau^{*}\rangle\,_{[m,n)}\varphi$
$\displaystyle\text{ iff }\mathbf{M},i\models\varphi\text{ for some
}(k,i)\in{\parallel}{\uptau^{*}}{\parallel}^{\mathbf{M}}$
$\displaystyle\quad\text{ with }\tau(i)-\tau(k)\in[m,n)$
$\displaystyle\text{satisfaction of }{\langle\rho\rangle\,}_{I}\varphi$
$\displaystyle\text{ iff }\mathbf{M},i\models\varphi\text{ for some
}(k,i)\in{\parallel}{\uptau^{x}}{\parallel}^{\mathbf{M}}$
$\displaystyle\quad\text{ with }x\geq 0\text{ and }\tau(i)-\tau(k)\in[m,n)$
$\displaystyle\text{definition of
}{\parallel}{\rho^{*}}{\parallel}^{\mathbf{M}}$ $\displaystyle\text{ iff
}\mathbf{M},i\models\varphi\text{ for some }0\leq i=k+x<\lambda$
$\displaystyle\quad\text{ with }x\geq 0\text{ and }\tau(i)-\tau(k)\in[m,n)$ by
Proposition 8 $\displaystyle\text{ iff }\mathbf{M},i\models\varphi\text{ for
some }i-k\geq 0\text{ satisfying }0\leq i<\lambda$ $\displaystyle\quad\text{
and }\tau(i)-\tau(k)\in[m,n)$ $\displaystyle i=k+x$ $\displaystyle\text{ iff
}\mathbf{M},i\models\varphi\text{ for some }0\leq k\leq i<\lambda$
$\displaystyle\quad\text{ and }\tau(i)-\tau(k)\in[m,n)$ $\displaystyle i-k\geq
0$ $\displaystyle\text{ iff }\mathbf{M},k\models\Diamond_{[m,n)}\varphi.$

  * •

Case of $\square_{[m,n)}\varphi$: as a reminder,
$\square_{[m,n)}\varphi\mathbin{\raisebox{-1.0pt}[-3.0pt][0.0pt]{$\stackrel{{\scriptstyle\mathit{def}}}{{=}}$}}[\uptau^{*}]\,_{[m,n)}\varphi$
as follows

$\displaystyle\mathbf{M},k\models[\uptau^{*}]\,_{[m,n)}\varphi$
$\displaystyle\text{ iff }\mathbf{M}^{\prime},i\models\varphi\text{ if
}(k,i)\in{\parallel}{\uptau^{*}}{\parallel}^{\mathbf{M}^{\prime}}$
$\displaystyle\quad\text{ and }\tau(i)-\tau(k)\in[m,n)\text{, for all }$
$\displaystyle\quad(k,i)\in\mathbb{D}\times\mathbb{D}\text{ and
}\mathbf{M}^{\prime}\in\\{\mathbf{M},\langle\mathbf{T},\mathbf{T},\tau\rangle\\}$
$\displaystyle\text{satisfaction of }{[\rho]\,}_{I}\varphi$
$\displaystyle\text{ iff }\mathbf{M}^{\prime},i\models\varphi\text{ if }x\geq
0\text{, }(k,i)\in{\parallel}{\uptau^{x}}{\parallel}^{\mathbf{M}^{\prime}}$
$\displaystyle\quad\text{ and }\tau(i)-\tau(k)\in[m,n)\text{, for all
}x\in\mathbb{N},$ $\displaystyle\quad(k,i)\in\mathbb{D}\times\mathbb{D}\text{
and
}\mathbf{M}^{\prime}\in\\{\mathbf{M},\langle\mathbf{T},\mathbf{T},\tau\rangle\\}$
$\displaystyle\text{definition of
}{\parallel}{\rho^{*}}{\parallel}^{\mathbf{M}^{\prime}}$ $\displaystyle\text{
iff }\mathbf{M}^{\prime},i\models\varphi\text{ if }x\geq 0,\ 0\leq
i=k+x<\lambda$ $\displaystyle\quad\text{ and }\tau(i)-\tau(k)\in[m,n)\text{,
for all }x\in\mathbb{N}$ $\displaystyle\quad\text{ and
}\mathbf{M}^{\prime}\in\\{\mathbf{M},\langle\mathbf{T},\mathbf{T},\tau\rangle\\}$
By Proposition 8 $\displaystyle\text{ iff
}\mathbf{M}^{\prime},i\models\varphi\text{ if }i-k\geq 0,\ 0\leq
i<\lambda\text{ and }$ $\displaystyle\quad\tau(i)-\tau(k)\in[m,n),\text{ for
all
}\mathbf{M}^{\prime}\in\\{\mathbf{M},\langle\mathbf{T},\mathbf{T},\tau\rangle\\}$
$\displaystyle i=k+x$ $\displaystyle\text{ iff
}\mathbf{M}^{\prime},i\models\varphi\text{ if }k\leq i<\lambda\text{ and
}\tau(i)-\tau(k)\in[m,n),$ $\displaystyle\quad\hbox{ for all
}\mathbf{M}^{\prime}\in\\{\mathbf{M},\langle\mathbf{T},\mathbf{T},\tau\rangle\\}$
$\displaystyle i-k\geq 0$ $\displaystyle\text{ iff
}\mathbf{M},k\models\square_{[m,n)}\varphi$

  * •

Case of $\blacklozenge_{[m,n)}\varphi$: as a reminder,
$\blacklozenge_{[m,n)}\varphi\mathbin{\raisebox{-1.0pt}[-3.0pt][0.0pt]{$\stackrel{{\scriptstyle\mathit{def}}}{{=}}$}}\langle(\uptau^{*})^{-}\rangle\,_{(-n,-m]}$
as follows

$\displaystyle\mathbf{M},k\models\langle(\uptau^{*})^{-}\rangle\,_{[m,n)}\varphi$
$\displaystyle\text{ iff }\mathbf{M},i\models\varphi\text{ for some
}(k,i)\in{\parallel}{(\uptau^{*})^{-}}{\parallel}^{\mathbf{M}}$
$\displaystyle\quad\text{ with }\tau(k)-\tau(i)\in(-n,-m]$
$\displaystyle\text{satisfaction of }{\langle\rho\rangle\,}_{I}\varphi$
$\displaystyle\text{ iff }\mathbf{M},i\models\varphi\text{ for some
}(i,k)\in{\parallel}{\uptau^{*}}{\parallel}^{\mathbf{M}}$
$\displaystyle\quad\text{ with }\tau(i)-\tau(k)\in(-n,-m]$
$\displaystyle\text{definition of
}{\parallel}{\rho^{-}}{\parallel}^{\mathbf{M}}$ $\displaystyle\text{ iff
}\mathbf{M},i\models\varphi\text{ for some
}(i,k)\in{\parallel}{\uptau^{x}}{\parallel}^{\mathbf{M}}$
$\displaystyle\quad\text{ with }x\geq 0\text{ and }\tau(i)-\tau(k)\in(-n,-m]$
$\displaystyle\text{definition of
}{\parallel}{\rho^{*}}{\parallel}^{\mathbf{M}}$ $\displaystyle\text{ iff
}\mathbf{M},i\models\varphi\text{ for some }0\leq i=k-x<\lambda$
$\displaystyle\quad\text{ with }x\geq 0\text{ and }\tau(i)-\tau(k)\in(-n,-m]$
by Proposition 8 $\displaystyle\text{ iff }\mathbf{M},i\models\varphi\text{
for some }0\leq i<\lambda$ $\displaystyle\quad\text{ with }k-i\geq 0\text{ and
}\tau(i)-\tau(k)\in(-n,-m]$ $\displaystyle i=k-i$ $\displaystyle\text{ iff
}\mathbf{M},i\models\varphi\text{ for some }0\leq i\leq k<\lambda$
$\displaystyle\quad\text{ with }\tau(i)-\tau(k)\in(-n,-m]$
$\displaystyle\text{since }k-i\geq 0$ $\displaystyle\text{ iff
}\mathbf{M},i\models\varphi\text{ for some }0\leq i\leq k<\lambda$
$\displaystyle\quad\text{ with }\tau(k)-\tau(i)\in[m,n)$ because of Remark 1
$\displaystyle\text{ iff }\mathbf{M},k\models\blacklozenge_{[m,n)}\varphi$

  * •

Case of $\blacksquare_{[m,n)}\varphi$: as a reminder,
$\blacksquare_{[m,n)}\varphi\mathbin{\raisebox{-1.0pt}[-3.0pt][0.0pt]{$\stackrel{{\scriptstyle\mathit{def}}}{{=}}$}}[(\uptau^{*})^{-}]\,_{(-n,-m]}\varphi$
as follows

$\displaystyle\mathbf{M},k\models[(\uptau^{*})^{-}]\,_{(-n,-m]}\varphi$
$\displaystyle\text{ iff }\mathbf{M}^{\prime},i\models\varphi\text{ if
}(k,i)\in{\parallel}{(\uptau^{*})^{-}}{\parallel}^{\mathbf{M}^{\prime}}$
$\displaystyle\quad\text{ and }\tau(i)-\tau(k)\in(-n,-m]\text{, for all }$
$\displaystyle\quad(k,i)\in\mathbb{D}\times\mathbb{D}\text{ and
}\mathbf{M}^{\prime}\in\\{\mathbf{M},\langle\mathbf{T},\mathbf{T},\tau\rangle\\}$
$\displaystyle\text{satisfaction of }{[\rho]\,}_{I}\varphi$
$\displaystyle\text{ iff }\mathbf{M}^{\prime},i\models\varphi\text{ if both
}(i,k)\in{\parallel}{\uptau^{*}}{\parallel}^{\mathbf{M}^{\prime}}$
$\displaystyle\quad\text{ and }\tau(i)-\tau(k)\in(-n,-m]\text{, for all }$
$\displaystyle\quad(k,i)\in\mathbb{D}\times\mathbb{D}\text{ and
}\mathbf{M}^{\prime}\in\\{\mathbf{M},\langle\mathbf{T},\mathbf{T},\tau\rangle\\}$
$\displaystyle\text{satisfaction of }{[\rho^{-}]\,}_{I}\varphi$
$\displaystyle\text{ iff }\mathbf{M}^{\prime},i\models\varphi\text{ if both
}(i,k)\in{\parallel}{\uptau^{*}}{\parallel}^{\mathbf{M}^{\prime}}$
$\displaystyle\quad\text{ and }\tau(k)-\tau(i)\in[m,n)\text{, for all }$
$\displaystyle\quad(k,i)\in\mathbb{D}\times\mathbb{D}\text{ and
}\mathbf{M}^{\prime}\in\\{\mathbf{M},\langle\mathbf{T},\mathbf{T},\tau\rangle\\}$
by Remark 1 $\displaystyle\text{ iff
}\mathbf{M}^{\prime},i\models\varphi\text{ if }x\geq 0\text{,
}(i,k)\in{\parallel}{\uptau^{x}}{\parallel}^{\mathbf{M}^{\prime}}$
$\displaystyle\quad\text{ and }\tau(k)-\tau(i)\in[m,n)\text{, for all
}x\in\mathbb{N},$ $\displaystyle\quad(k,i)\in\mathbb{D}\times\mathbb{D}\text{
and
}\mathbf{M}^{\prime}\in\\{\mathbf{M},\langle\mathbf{T},\mathbf{T},\tau\rangle\\}$
$\displaystyle\text{definition of
}{\parallel}{\rho^{*}}{\parallel}^{\mathbf{M}^{\prime}}$ $\displaystyle\text{
iff }\mathbf{M}^{\prime},i\models\varphi\text{ if }x\geq 0,\ 0\leq
i=k-x<\lambda$ $\displaystyle\quad\text{ and }\tau(k)-\tau(i)\in[m,n)\text{,
for all }x\in\mathbb{N}$ $\displaystyle\quad\text{ and
}\mathbf{M}^{\prime}\in\\{\mathbf{M},\langle\mathbf{T},\mathbf{T},\tau\rangle\\}$
by Proposition 8 $\displaystyle\text{ iff
}\mathbf{M}^{\prime},i\models\varphi\text{ if }k-i\geq 0,\ 0\leq i<\lambda$
$\displaystyle\quad\text{ and }\tau(k)-\tau(i)\in[m,n)\text{, for all }$
$\displaystyle\quad(k,i)\in\mathbb{D}\times\mathbb{D}\text{ and
}\mathbf{M}^{\prime}\in\\{\mathbf{M},\langle\mathbf{T},\mathbf{T},\tau\rangle\\}$
$\displaystyle i=k-x$ $\displaystyle\text{ iff
}\mathbf{M}^{\prime},i\models\varphi\text{ if }0\leq i\leq k<\lambda\text{ and
}$ $\displaystyle\quad\tau(k)-\tau(i)\in[m,n),\hbox{ for all
}(k,i)\in\mathbb{D}\times\mathbb{D}$ $\displaystyle\quad\text{ and
}\mathbf{M}^{\prime}\in\\{\mathbf{M},\langle\mathbf{T},\mathbf{T},\tau\rangle\\}$
$\displaystyle k-i\geq 0$ $\displaystyle\text{ iff
}\mathbf{M},k\models\blacksquare_{[m,n)}\varphi$

  * •

Case $\varphi\mathbin{\bm{\mathsf{U}}}_{[m,n)}\psi$: we remark that
$\varphi\mathbin{\bm{\mathsf{U}}}_{[m,n)}\psi\mathbin{\raisebox{-1.0pt}[-3.0pt][0.0pt]{$\stackrel{{\scriptstyle\mathit{def}}}{{=}}$}}\langle(\varphi?;\uptau)^{*}\rangle\,_{[m,n)}\psi$.
The proof goes as follows:

$\displaystyle\mathbf{M},k\models\langle(\varphi?;\uptau)^{*}\rangle\,_{[m,n)}\psi$
$\displaystyle\text{ iff }\mathbf{M},i\models\psi\text{ for some
}(k,i)\in{\parallel}{(\varphi?;\uptau)^{*}}{\parallel}^{\mathbf{M}}$
$\displaystyle\quad\text{ with }\tau(i)-\tau(k)\in[m,n)$
$\displaystyle\text{satisfaction of }{\langle\rho\rangle\,}_{I}\varphi$
$\displaystyle\text{ iff }\mathbf{M},i\models\psi\text{ for some }i\geq k$
$\displaystyle\quad\text{ s.t. }\tau(i)-\tau(k)\in[m,n)$ $\displaystyle\text{
and }\mathbf{M},j\models\varphi\hbox{ for all }j\in[k,i)$ Proposition 9
$\displaystyle\text{ iff
}\mathbf{M},k\models\varphi\mathbin{\bm{\mathsf{U}}}_{[m,n)}\psi$

  * •

Case $\varphi\mathbin{\bm{\mathsf{S}}}_{[m,n)}\psi$: we remark that
$\varphi\mathbin{\bm{\mathsf{S}}}_{[m,n)}\psi\mathbin{\raisebox{-1.0pt}[-3.0pt][0.0pt]{$\stackrel{{\scriptstyle\mathit{def}}}{{=}}$}}\langle(\varphi?;\uptau^{-})^{*}\rangle\,_{[m,n)}\psi$.
The proof goes as follows:

$\displaystyle\mathbf{M},k\models\langle(\varphi?;\uptau^{-})^{*}\rangle\,_{[m,n)}\psi$
$\displaystyle\text{ iff }\mathbf{M},i\models\psi\text{ for some
}(k,i)\in{\parallel}{(\varphi?;\uptau^{-})^{*}}{\parallel}^{\mathbf{M}}$
$\displaystyle\quad\text{ with }\tau(k)-\tau(i)\in(-n,-m]$
$\displaystyle\text{satisfaction of }{\langle\rho\rangle\,}_{I}\varphi$
$\displaystyle\text{ iff }\mathbf{M},i\models\psi\text{ for some }i\leq
k\text{ with }$ $\displaystyle\quad\tau(i)-\tau(k)\in(-n,-m]$
$\displaystyle\quad\text{ and }\mathbf{M},j\models\varphi\text{ for all
}j\in(i,k]$ by Proposition 10 $\displaystyle\text{ iff
}\mathbf{M},i\models\psi\text{ for some }i\leq k\text{ with }$
$\displaystyle\quad\tau(k)-\tau(i)\in[m,n)$ $\displaystyle\quad\text{ and
}\mathbf{M},j\models\varphi\text{ for all }j\in(i,k]$ by Remark 1

  * •

Case $\varphi\mathbin{\bm{\mathsf{R}}}_{[m,n)}\psi$: we remark that in (Becker
., 2023) it is shown that

$\varphi\mathbin{\bm{\mathsf{R}}}_{[m..n)}\psi\equiv\square_{[m..n)}\psi\vee\Diamond_{[0..m)}\left(\varphi\mathbin{\bm{\mathsf{R}}}\left(\varphi\vee\widehat{}\psi\right)\right).$

In the previous cases we have shown that $\square_{[m..n)}$ and
$\Diamond_{[0..m)}$ are $\mathrm{MDHT}$-definable. Furthermore
$\mathbin{\bm{\mathsf{R}}}$ is $\mathrm{MDHT}$-definable by Corollary 3.

  * •

The case $\varphi\mathbin{\bm{\mathsf{T}}}_{[m,n)}\psi$ follows a similar
reasoning as for $\varphi\mathbin{\bm{\mathsf{R}}}_{[m,n)}\psi$.

∎

###### Proof.

(Corollary 3)

The fact that $\textrm{THT}=\textrm{DHT}$ for the case of temporal formulas
has been proved in Bosser . (2018). The proof that
$\textrm{DHT}=\mathrm{MDHT}$ for the case of dynamic formulas corresponds to
Corollary 2. ∎