Department of CSE, Indian Institute of Technology Bombay, Mumbai, India
akshayss@cse.iitb.ac.inhttps://orcid.org/0000-0002-2471-5997 Supported in part
by DST/SERB Matrics Grant MTR/2018/000744. Université Paris-Saclay, ENS Paris-
Saclay, CNRS, LMF, 91190, Gif-sur-Yvette, France and CNRS, ReLaX, IRL 2000,
Siruseri, India paul.gastin@ens-paris-
saclay.frhttps://orcid.org/0000-0002-1313-7722 Uppsala University,
Swedengovind.rajanbabu@it.uu.sehttps://orcid.org/0000-0002-1634-5893 Chennai
Mathematical Institute, India and CNRS, ReLaX, IRL 2000, Siruseri, India
sri@cmi.ac.inhttps://orcid.org/0000-0003-2666-0691 S. Akshay, P. Gastin, R.
Govind and B. Srivathsan 500]Theory of computation Timed and hybrid models
[300]Theory of computation Quantitative automata [100]Theory of computation
Logic and verification

# MITL Model Checking via Generalized Timed Automata and a New Liveness
Algorithm

S. Akshay  Paul Gastin  R. Govind  B. Srivathsan

###### Abstract

The translation of Metric Interval Temporal Logic (MITL) to timed automata is
a topic that has been extensively studied. A key challenge here is the
conversion of future modalities into equivalent automata. Typical conversions
equip the automata with a guess-and-check mechanism to ascertain the truth of
future modalities. Guess-and-check can be naturally implemented via
alternation. However, since timed automata tools do not handle alternation,
existing methods perform an additional step of converting the alternating
timed automata into timed automata. This “de-alternation” step proceeds by an
intricate finite abstraction of the space of configurations of the alternating
automaton.

Recently, a model of generalized timed automata (GTA) has been proposed. The
model comes with several powerful additional features, and yet, the best known
zone-based reachability algorithms for timed automata have been extended to
the GTA model, with the same complexity for all the zone operations. An
attractive feature of GTAs is the presence of future clocks which act like
timers that guess a time to an event and stay alive until a timeout. Future
clocks seem to provide another natural way to implement the guess-and-check:
start the future clock with a guessed time to an event and check its
occurrence using a timeout. Indeed, using this feature, we provide a new
concise translation from MITL to GTA. In particular, for the timed until
modality, our translation offers an exponential improvement w.r.t. the state-
of-the-art.

Thanks to this conversion, MITL model checking reduces to checking liveness
for GTAs. However, no liveness algorithm is known for GTAs. Due to the
presence of future clocks, there is no finite time-abstract bisimulation
(region equivalence) for GTAs, whereas liveness algorithms for timed automata
crucially rely on the presence of the finite region equivalence. As our second
contribution, we provide a new zone-based algorithm for checking Büchi non-
emptiness in GTAs, which circumvents this fundamental challenge.

###### keywords:

MITL model checking, timed automata, zones, liveness

###### category:

[

##  1 Introduction

The translation of Linear Temporal Logic (LTL) [34] to Büchi automata is a
fundamental problem in model checking, with a long history of theoretical
advances [22, 38, 20], tool implementations [27, 16, 20, 32, 13] and practical
applications [35, 36, 28, 29]. In the real-time setting, Metric Interval
Temporal Logic (MITL) is close to LTL, with the modalities Next
($\mathop{\mathsf{X}\vphantom{a}}\nolimits$) and Until
($\mathbin{\mathsf{U}}$) extended with timing intervals — for instance,
$X_{[a,b]}p$ says that the next event is a $p$ and it occurs within a delay
$\theta\in[a,b]$. Model checking for MITL is known to be
$\mathsf{EXPSPACE}$-complete [3]. This has led to the study of “efficient”
conversions from MITL to timed automata, with each new construction aiming to
make the automata more succinct. Our work is another step in this direction.

There are two ways to interpret MITL formulae: over (continuous) timed signals
[3, 31, 17] or (pointwise) timed words [5, 39, 11]. Since the current timed
automata tools work with timed words, we stick with the pointwise semantics.
The state-of-the-art for MITL-to-TA is based on an initial translation of MITL
to one-clock Alternating Timed Automata (OCATA) [33]. It has been shown that
these OCATA can be converted to a network of timed automata [9, 10]. The tool
MightyL [11] implements the entire MITL-to-TA translation. One of the
difficulties in the MITL-to-TA translation is the inherent mismatch between
the logic and the automaton in the way timing constraints are enforced. A
future modality declares that a certain event takes place at a certain timing
distance, _in the future_. In a timed automaton, _clocks_ measure time elapsed
since some event _in the past_ and check constraints on these values. To
implement a future modality, the automaton needs to make a prediction about
the event and verify that the prediction is indeed true. Therefore, each
prediction typically resets a clock and stores a new obligation in the state.
The automaton needs to discharge these obligations at the right times in the
future.

Figure 1: (top left) Büchi transducer (with outputs) for LTL formula
$\mathop{\mathsf{X}\vphantom{a}}\nolimits p$ (right) Timed transducer with
clock $x$ for MITL formula $\mathop{\mathsf{X}\vphantom{a}}\nolimits_{I}p$;
${\color[rgb]{1,0,0}\pi_{1}:=x\in I;[x]}$,
${\color[rgb]{1,0,0}\pi_{2}:=x\notin I;[x]}$ (bottom left) a hypothetical
transducer with a variable $\theta$ that predicts time to next action;
${\color[rgb]{0,0,1}\dagger:={\theta\in I}\,?\,{1}:{0}}$.

Figure 1 (top left) shows an automaton with outputs for the LTL formula
$\mathop{\mathsf{X}\vphantom{a}}\nolimits p$. On an infinite word
$w_{1}w_{2}\dots$ (where each $w_{i}$ is a subset of atomic propositions) the
automaton outputs ${\color[rgb]{0,0,1}1}$ at $w_{i}$ iff $w_{i+1}$ contains
$p$. While reading $w_{i}$, the automaton needs to guess whether $p\in
w_{i+1}$ or not. Depending on the guess, it stores an appropriate obligation.
This is reflected in the states and transitions: transitions with output
${\color[rgb]{0,0,1}1}$ go to a state
$\mathop{\mathsf{X}\vphantom{a}}\nolimits p$ which can only read $p$ next,
whereas those with output ${\color[rgb]{0,0,1}0}$ go to
$\neg\mathop{\mathsf{X}\vphantom{a}}\nolimits p$ which can only read $\neg p$.
The $\mathop{\mathsf{X}\vphantom{a}}\nolimits p$ and
$\neg\mathop{\mathsf{X}\vphantom{a}}\nolimits p$ can be seen as obligations
that the automaton has to discharge from the state.

Now, let us consider a timed version
$\mathop{\mathsf{X}\vphantom{a}}\nolimits_{I}p$ interpreted on timed words. An
automaton for $\mathop{\mathsf{X}\vphantom{a}}\nolimits_{I}p$ needs to guess
whether the next letter is a $p$ _and_ if so, whether it appears within
$\theta$ time units for some $\theta\in I$. Figure 1 (bottom left) represents
a hypothetical automaton that implements this idea: assuming it has access to
a variable $\theta$ which contains the time to the next event, the output
should depend on whether $\theta\in I$ or not. This is exactly what the if-
then-else condition ${\color[rgb]{0,0,1}\dagger}$ does: if $\theta\in I$
output $1$, else output $0$. Classical timed automata do not have direct
access to $\theta$. They implement this idea differently, by making use of
extra states. Figure 1 (right) shows a timed automaton for
$\mathop{\mathsf{X}\vphantom{a}}\nolimits_{I}p$. The state
$\mathop{\mathsf{X}\vphantom{a}}\nolimits p$ is split into two different
obligations: $\mathop{\mathsf{X}\vphantom{a}}\nolimits_{I}p$ where the timing
constraint is satisfied, and $\mathop{\mathsf{X}\vphantom{a}}\nolimits
p\land\neg\mathop{\mathsf{X}\vphantom{a}}\nolimits_{I}p$ where it is not. The
outgoing guards discharge these obligations. This example shows the
convenience of having access to a variable that can predict time to future
events.

This is precisely where the recently proposed model of _Generalized Timed
Automata_ (GTA) [1] enters the picture. This model subsumes event-clock
automata [4] and automata with timers [15]. GTA come equipped with the
additional resources to implement predictions better. GTA have two types of
clocks: _history clocks_ and _future clocks_. History clocks are similar to
the usual clocks of timed automata. Future clocks are like timers, but instead
of starting them at some non-negative value and making them go down to zero,
they get started with some arbitrary negative value and go up until they hit
zero. For example, in Figure 1 (bottom left), each transition can start a
future clock, guessing the time to the next event. This immediately gives us
the required $\theta$. The exact GTA for
$\mathop{\mathsf{X}\vphantom{a}}\nolimits_{I}p$ is quite close to Figure 1
(bottom left) and is given in Figure 8. Apart from the use of future clocks,
the syntax of transitions in a GTA is much richer than a guard-reset pair as
in timed automata. Transitions contain an “instantaneous timed program”, which
consists of a sequence of guards, resets and releases (for future clocks).
When difference constraints are present, the model becomes powerful enough to
encode counter machines and is therefore undecidable. A safe fragment, with a
careful use of diagonal constraints is known to be decidable.

GTAs are advantageous in another sense. In spite of the powerful features, the
best zone-based algorithms from the timed automata literature have been shown
to suitably adapt to the GTA setting, with the same complexity for zone
operations, and have been implemented in the tool TChecker [23]. Therefore, an
MITL to GTA conversion allows us to capitalize on the features and succinct
syntax of GTA, and at the same time, lets us model check MITL directly on
richer GTA models. In summary:

  * •

We provide a translation of MITL formulae to safe GTA. The translation is
compositional and implementable, and yields an _exponential improvement_ in
the number of locations compared to the state-of-the-art technique for
pointwise semantics [11], while the number of clocks remains the same up to a
constant.

  * •

Model checking MITL against GTA requires to solve the liveness problem for
(safe) GTAs, which has been open so far. We settle the liveness question in
this work. Zone based algorithms for event-clock automata have been studied in
[21]. A notion of weak regions has been developed and this can be used for
solving both reachability and liveness using zones. The GTA model that we
consider in this paper strictly subsumes event-clock automata. In particular,
the presence of diagonal constraints makes the problem more challenging. Our
solution to liveness for GTAs therefore gives an alternate liveness procedure
for event-clock automata, and also settles liveness for event-clock automata
with diagonal constraints, a model defined in [8].

We remark that the techniques used in continuous semantics do not extend to
pointwise semantics. In [17] the authors simplify general MITL formulae into
formulae containing only one-sided intervals (of the form $[0,c]$ or
$[c,\infty)$), for which automata are considerably simpler to construct.
However, this simplification at the formula level works _only_ in the
continuous semantics — it does not work in the pointwise-semantics (as Lemma
4.3, 4.4 of [17] do not extend to pointwise-semantics). The fundamental
difference is that in the continuous semantics we can assert a formula at any
time point $t$. However, in pointwise-semantics, we can evaluate a formula
only at _action points_ , i.e., points where there is an actual action. For
example, in continuous semantics one can rewrite
$\mathop{\mathsf{F}\vphantom{a}}\nolimits_{[a+c,b+c]}p$ as
$\mathop{\mathsf{F}\vphantom{a}}\nolimits_{[0,c]}\mathop{\mathsf{G}\vphantom{a}}\nolimits_{[0,c]}\mathop{\mathsf{F}\vphantom{a}}\nolimits_{[a,b]}p$
when $c\leq b-a$ (Lemma 4.3, [17]). However, in the pointwise semantics there
may be no event in the interval $[0,c]$ on which we can evaluate
$\mathop{\mathsf{G}\vphantom{a}}\nolimits_{[0,c]}\mathop{\mathsf{F}\vphantom{a}}\nolimits_{[a,b]}p$.
Therefore, we need a completely different approach to deal with intervals in
the pointwise semantics.

#### Organization of the paper.

We start with preliminary definitions of Generalized Timed Automata (Section
2) and provide our solution to the liveness problem in Section 3. We present
our MITL to GTA translation in Section 4.

##  2 Preliminaries

Let $X=X_{F}\uplus X_{H}$ be a set of real-valued variables called _clocks_ ,
which is further partitioned into _future clocks_ $X_{F}$ and _history clocks_
$X_{H}$. Let $\Phi(X)$ denote a set of _clock constraints_ generated by the
grammar: $\varphi::=x-y\mathrel{\triangleleft}c\mid\varphi\land\varphi$ where
$x,y\in X\cup\\{0\\}$, ${\mathrel{\triangleleft}}\in\\{<,\leq\\}$ and
$c\in\overline{\mathbb{Z}}=\mathbb{Z}\cup\\{-\infty,+\infty\\}$ (the set of
integers equipped with the two special values to say that a clock is
“undefined”). We also allow _renamings_ of clocks. Let $\mathsf{perm}_{X}$ be
the set of permutations $\sigma$ over $X\cup\\{0\\}$ mapping history (resp.
future) clocks to history (resp. future) clocks ($\sigma(X_{F})=X_{F}$ and
$\sigma(X_{H})=X_{H}$).

GTA syntax. A _Generalized Timed Automaton (GTA)_ is given by
$(Q,\Sigma,X,\Delta,\mathcal{I},Q_{f})$ where $Q$ is a finite set of states,
$\Sigma$ is a finite alphabet of actions, $X=X_{F}\uplus X_{H}$ is a set of
clocks partitioned into future clocks $X_{F}$ and history clocks $X_{H}$. The
initialization condition $\mathcal{I}$ is a set of pairs $(q_{0},g_{0})$ where
a pair consists of an initial state $q_{0}\in Q$ and an initial guard
$g_{0}\in\Phi(X)$, and the accepting condition is given by a set
$Q_{f}\subseteq Q$ of Büchi states. The transition relation
$\Delta\subseteq(Q\times\Sigma\times\textrm{Programs}\times Q)$ contains
transitions of the form $(q,a,\mathsf{prog},q^{\prime})$, where $q$ is the
source state, $q^{\prime}$ is the target state, $a$ is the action triggering
the transition, and $\mathsf{prog}$ is an _instantaneous timed program_
generated by the grammar:

$\displaystyle\mathsf{prog}:=\mathsf{guard}\mid\mathsf{change}\mid\mathsf{rename}\mid\mathsf{prog};\mathsf{prog}$

where $\mathsf{guard}=g\in\Phi(X)$, $\mathsf{change}=[R]$ for an $R\subseteq
X$, and $\mathsf{rename}=[\sigma]$ for a $\sigma\in\mathsf{perm}_{X}$.

Figure 8 with the blue parts removed illustrates a GTA. Both states $\ell_{1}$
and $\ell_{2}$ are initial, denoted by incoming arrows to each of them, and
accepting, marked by the double circle. The initial guard is the trivial
_true_ constraint. The alphabet $\Sigma=\\{0,1\\}$ (written in black). The
constraint $-x\in I$ is short form for a conjunction of constraints requiring
the clock to be in the interval $I$. For example, if $I=(4,5]$, then $-x\in I$
is the constraint $4<-x\land-x\leq 5$. During our MITL to GTA translation, we
extend GTAs to include outputs (Definition 4.1. The dagger condition ${(-x\in
I)}\,?\,{1}:{0}$ is a short form for two transitions, one which checks $-x\in
I$ and outputs $1$, and the other which checks $-x\notin I$ and outputs $0$.

GTA semantics. A valuation of clocks is a function $v\colon
X\cup\\{0\\}\mapsto\overline{\mathbb{R}}=\mathbb{R}\cup\\{-\infty,+\infty\\}$
which maps the special clock $0$ to 0, history clocks to $\mathbb{R}_{\geq
0}\cup\\{+\infty\\}$ and future clocks to $\mathbb{R}_{\leq
0}\cup\\{-\infty\\}$. We denote by $\mathbb{V}(X)$ or simply by $\mathbb{V}$
the set of valuations over $X$. For a valuation $v\in\mathbb{V}$, define111To
allow evaluation of all the constraints in $\Phi(X)$, the addition and the
unary minus operation on real numbers is extended [1] with the following
conventions (i)$(+\infty)+\alpha=\alpha+(+\infty)=+\infty$ for all
$\alpha\in\overline{\mathbb{R}}$, (ii)
$(-\infty)+\beta=\beta+(-\infty)=-\infty$, as long as $\beta\neq+\infty$, and
(iii) $-(+\infty)=-\infty$ and $-(-\infty)=+\infty$.  $v\models
y-x\mathrel{\triangleleft}c$ as $v(y)-v(x)\mathrel{\triangleleft}c$. We say
that $v$ _satisfies_ a constraint $\varphi$, denoted as $v\models\varphi$,
when $v$ satisfies all the atomic constraints in $\varphi$. We denote by
$v+\delta$ the _valuation_ obtained from valuation $v$ by increasing by
$\delta\in\mathbb{R}_{\geq 0}$ the value of all clocks in $X$. Note that, from
a given valuation, not all time elapses result in valuations since future
clocks need to stay at most $0$. We now define the _change_ operation that
combines the _reset_ operation for history clocks (which sets history clocks
to 0) and _release_ operation for future clocks (which assigns a non-
deterministic value to a future clock). Given a set of clocks $R\subseteq X$,
we define $R_{F}=R\cap X_{F}$ as the set of future clocks in $R$, and
$R_{H}=R\cap X_{H}$ as the set of history clocks in $R$. Then,
$[R]v:=\\{v^{\prime}\in\mathbb{V}\mid v^{\prime}(x)=0\leavevmode\nobreak\
\forall\leavevmode\nobreak\ x\in R_{H}\text{ and
}v^{\prime}(x)=v(x)\leavevmode\nobreak\ \forall\leavevmode\nobreak\ x\not\in
R\\}$. Observe that $v^{\prime}$ has no constraints for the future clocks in
$R$, as they can take any arbitrary value in $v^{\prime}$. For a valuation
$v\in\mathbb{V}(X)$, and $\sigma\in\mathsf{perm}_{X}$, we define $[\sigma]v$
as $v\circ\sigma$, i.e., $([\sigma]v)(x)=v(\sigma(x))$ for all $x\in
X\cup\\{0\\}$.

For valuations $v,v^{\prime}$ and a guard $g\in\Phi(X)$ we write
$v\xrightarrow{g}v^{\prime}$ when $v^{\prime}=v\models g$, and
$v\xrightarrow{[R]}v^{\prime}$ when $R\subseteq X$ and $v^{\prime}\in[R]v$,
and $v\xrightarrow{[\sigma]}v^{\prime}$ when $\sigma\in\mathsf{perm}_{X}$ and
$v^{\prime}=[\sigma]v$. When
$\mathsf{prog}=\mathsf{prog}_{1};\ldots;\mathsf{prog}_{n}$, we write
$v\xrightarrow{\scriptstyle\mathsf{prog}}v^{\prime}$ when there are valuations
$v_{1},\ldots,v_{n}$ such that
$v\xrightarrow{\scriptstyle\mathsf{prog}_{1}}v_{1}\xrightarrow{\scriptstyle\mathsf{prog}_{2}}\cdots\xrightarrow{\scriptstyle\mathsf{prog}_{n}}v_{n}=v^{\prime}$.
The semantics of the GTA $\mathcal{A}$ defined above is given by a transition
system $\mathbb{TS}_{\mathcal{T}}$ whose states are _configurations_ $(q,v)$
of $\mathcal{A}$, where $q\in Q$ and $v\in\mathbb{V}$ is a valuation. A
configuration $(q,v)$ is initial if $v\models g$ for some
$(q,g)\in\mathcal{I}$, and it is accepting if $q\in Q_{f}$. Transitions of
$\mathbb{TS}_{\mathcal{T}}$ are of two forms: (1) delay transition:
$(q,v)\xrightarrow{\delta}(q,v+\delta)$ if $v+\delta$ is a valuation, i.e.,
$(v+\delta)\models X_{F}\leq 0$, and (2) discrete transition:
$(q,v)\xrightarrow{t}(q^{\prime},v^{\prime})$ if
$t=(q,a,\mathsf{prog},q^{\prime})\in\Delta$ and
$v\xrightarrow{\mathsf{prog}}v^{\prime}$. A _finite (respectively infinite)
run_ $\rho$ of a GTA is a finite (respectively infinite) sequence of
transitions from an initial configuration of $\mathbb{TS}_{\mathcal{A}}$:
$(q_{0},v_{0})\xrightarrow{\delta_{0},t_{0}}(q_{1},v_{1})\xrightarrow{\delta_{1},t_{1}}\cdots$.

For example, consider the run of GTA in Figure 8 on a timed word
$(1,1)(0,2)(1,3)(0,4)\dots$ ($1$ occurs at all odd numbers, and $0$ at all
even numbers, starting from first timestamp $1$). The program $(x=0);[x]$ used
in the transitions first checks if $x$ is $0$, and then releases it to an
arbitrary non-deterministic value. The run on the above word would be:
$(\ell_{1},x=-1)\xrightarrow{1,t_{1}}(\ell_{2},x=-1)\xrightarrow{1,t_{2}}(\ell_{1},x=-1)\cdots$.
A transition $\xrightarrow{\delta,t}$ denotes a time elapse of $\delta$
followed by application of the program associated to transition $t$. At each
point the value of $x$ is released to $-1$, and is checked with the guard
$x=0$ at the next event.

An infinite run is accepting if it visits accepting configurations infinitely
often. The run is said to be _Zeno_ if $\Sigma_{i\geq 0}\delta_{i}$ is bounded
and _non-Zeno_ otherwise. In this work, we will only be interested in non-Zeno
runs (we can force non-Zenoness by ensuring time elapse in every loop of the
automaton [37]).

Liveness problem. The _non-emptiness or liveness problem_ for a GTA asks
whether the given GTA has an accepting non-Zeno run. Unfortunately, the non-
emptiness problem even for finite words turns out to be undecidable for
general GTA [1]. Therefore, we focus our attention on a restricted sub-class
of GTA’s for which non-emptiness in the finite words case is decidable, called
safe GTA [1].

######  Definition 2.1 (Safe GTA [1]).

Given a GTA $\mathcal{A}$, let $X_{D}\subseteq X_{F}$ be the subset of future
clocks used in diagonal guards of $\mathcal{A}$ between future clocks, i.e.,
if $x-y\mathrel{\triangleleft}c$ with $x,y\in X_{F}$ occurs in some guard of
$\mathcal{A}$ then $x,y\in X_{D}$. Then, a program $\mathsf{prog}$ is
$X_{D}$-safe if clocks in $X_{D}$ are checked for being $0$ or $-\infty$
before being released and renamings $[\sigma]$ used in $\mathsf{prog}$
preserve $X_{D}$ clocks ($\sigma(X_{D})=X_{D}$). A GTA $\mathcal{A}$ is safe
if it only uses $X_{D}$-safe programs on its transitions and the initial guard
$g_{0}$ sets each history clock to either $0$ or $\infty$.

The GTA in Figure 8 is vacuously safe, since there are no diagonal constraints
at all.

######  Remark 2.2.

Renaming operations may be considered as syntactic sugar allowing for more
concise representations of GTAs. Indeed, we can transform a GTA $\mathcal{A}$
with renamings to an equivalent GTA $\mathcal{A}^{\prime}$ without renamings
by adding to the state the current permutation of clocks (composition of the
permutations applied since the initial state) and change the programs of
outgoing transitions accordingly. The number of states is multiplied by the
number of permutations that may occur as described above.

Zones for Generalized timed automata. The state-of-the-art approach for
answering the Büchi non-emptiness problem and the reachability problem for
timed automata proceeds via checking reachability in a graph called the _zone
graph_ of a timed automaton [14]. Abstractly, _zones_ [7] are essentially sets
of valuations that can be represented efficiently using constraints between
differences of clocks. Here, we recall the notion of zones for the setting of
generalized timed automata.

######  Definition 2.3 (GTA zones [1]).

A GTA zone is a set of valuations satisfying a conjunction of constraints of
the form $y-x\mathrel{\triangleleft}c$, where $x,y\in X\cup\\{0\\}$,
$c\in\overline{\mathbb{Z}}$ and ${\mathrel{\triangleleft}}\in\\{\leq,<\\}$.

Thus zones are an abstract representation of sets of valuations.

Let $W$ be an arbitrary set of valuations (not necessarily a GTA zone) and $q$
be a state. For a transition $t:=(q,a,\mathsf{prog},q^{\prime})$, we write
$(q,W)$ $\xrightarrow{t}$ $(q^{\prime},W_{t})$ if
$W_{t}=\\{v^{\prime}\mid\text{$v^{\prime}$ is a valuation and
}(q,v)\xrightarrow{t}\xrightarrow{\delta}(q^{\prime},v^{\prime})\text{ for
some }v\in W\text{ and }\delta\in\mathbb{R}_{\geq 0}\\}$. [1] showed that
starting from a GTA zone $Z$, the successors are also event zones:
$(q,Z)\xrightarrow{t}(q^{\prime},Z_{t})$ implies $Z_{t}$ is also a a GTA zone.
This observation is used to define the notion of the _Zone graph_ of a
generalized timed automata.

######  Definition 2.4 (GTA zone graph [1]).

Given a GTA $\mathcal{A}$, its GTA zone graph, denoted
$\mathsf{GZG}$($\mathcal{A}$), is defined as follows: Nodes are of the form
$(q,Z)$ where $q$ is a state and $Z$ is a GTA zone. Initial nodes are pairs
$(q_{0},\overrightarrow{Z_{0}})$ where $(q_{0},g_{0})\in\mathcal{I}$ is an
initial condition and $Z_{0}$ is given by $g_{0}\wedge\big{(}X_{F}\leq
0\big{)}\wedge\big{(}X_{H}\geq 0\big{)}$ ($Z_{0}$ is the set of all valuations
which satisfy the _initial constraint_ $g_{0}$). For every node $(q,Z)$ and
every transition $t:=(q,a,\mathsf{prog},q^{\prime})$ there is a transition
$(q,Z)\xrightarrow{t}(q^{\prime},Z^{\prime})$ in the GTA zone graph.

Finally, just as is the case for zone graphs for timed automata,
$\mathsf{GZG}(\mathcal{A})$ is not guaranteed to be finite. In order to use it
to check Büchi non-emptiness or reachability, we need a finite abstraction of
the zone graph. The standard technique to obtain such finite abstractions is
using the notion of _simulations_ , that we recall next.

######  Definition 2.5 (Simulation).

A (time-abstract) simulation relation on the semantics of a GTA is a
reflexive, transitive relation $(q,v)\preceq(q,v^{\prime})$ relating
configurations with the same control state and

  1. 1.

for every $\delta\in\mathbb{R}_{\geq 0}$ such that $v+\delta\in\mathbb{V}$ is
a valuation, there exists $\delta^{\prime}\in\mathbb{R}_{\geq 0}$ such that
$v^{\prime}+\delta^{\prime}\in\mathbb{V}$ is a valuation and
$(q,v+\delta)\preceq(q,v^{\prime}+\delta^{\prime})$,

  2. 2.

for every transition $t$, if $(q,v)\xrightarrow{t}(q_{1},v_{1})$ for some
valuation $v_{1}$, then $(q,v^{\prime})\xrightarrow{t}(q_{1},v^{\prime}_{1})$
for some valuation $v^{\prime}_{1}$ with
$(q_{1},v_{1})\preceq(q_{1},v^{\prime}_{1})$,

  3. 3.

for all future clock $x\in X_{F}$, if $v(x)=-\infty$ then
$v^{\prime}(x)=-\infty$.

For two GTA zones $Z,Z^{\prime}$, we say $(q,Z)\preceq(q,Z^{\prime})$ if for
every $v\in Z$ there exists $v^{\prime}\in Z^{\prime}$ such that
$(q,v)\preceq(q,v^{\prime})$.

##  3 Liveness for GTA

In this section, we will discuss a zone-based procedure to check liveness for
safe generalized timed automata. We start by explaining how the standard zone
based algorithm for solving liveness in classical timed automata can be
adapted to the setting of safe GTAs. The approach for timed automata crucially
depends on the existence of a finite time-abstract bisimulation between
valuations, namely the region-equivalence [2]. However, there exists no such
finite time-abstract bisimulation for GTAs (extension of a result of [21]), as
illustrated in Figure 2. The issue is that we cannot forget (abstract) the
values of future clocks, unlike history clocks where values above a maximum
constant are equivalent. Therefore, our approach involves a significant
deviation from the standard one.

Figure 2: Example to illustrate no finite bisimulation in GTA; $x$ is a future
clock, $y$ a history clock. The initial transition releases clock $x$ to an
arbitrary value, and resets $y$ to $0$. From configuration
$\langle\ell_{1},x=-n,y=0\rangle$ ($n\in\mathbb{N}$), the only way to reach
$\ell_{2}$ is by executing $b^{n}c$, with $1$ time unit between consecutive
$b$’s. Therefore, $\langle\ell_{1},x=-n,y=0\rangle$ and
$\langle\ell_{1},x=-m,y=0\rangle$ are simulation incomparable, when $n\neq m$.
Hence there is no finite bisimulation.

We fix a safe GTA $\mathcal{A}$ for the rest of this section. In order to
focus on the main difficulties and avoid additional technicalities, we assume
that the GTA $\mathcal{A}$ is without renamings. We start by noting that non-
Zeno runs have a special form: future clocks which are not ultimately
$-\infty$ should be released infinitely often. If not, there is a last point
where a future clock is released to a finite value, and the entire suffix of
the run should fall under this finite time, which contradicts non-Zenoness.

######  Lemma 3.1.

Let
$\rho:=(q_{0},v_{0})\xrightarrow{\delta_{0},t_{0}}(q_{1},v_{1})\xrightarrow{\delta_{1},t_{1}}\cdots$
be a non-Zeno run of the GTA $\mathcal{A}$. Then, for every future clock $x$
of $\mathcal{A}$, and for every index $i\geq 0$, if $v_{i}(x)\neq-\infty$,
there exists $j\geq i$ such that $x$ is released in $t_{j}$.

######  Proof 3.2.

Suppose not. There is a future clock $x$, and an index $i$ such that
$v_{i}(x)=\alpha\neq-\infty$, and $x$ is never released in any later
transition. By the semantics of delay transitions, $\sum_{j\geq
i}\delta_{j}\leq\alpha$. This contradicts the non-Zenoness assumption.

#### Overview of our solution.

In classical timed automata, the liveness problem is solved by enumerating the
zone graph [14, 7], and using a _simulation equivalence_ [25, 6, 18, 19] for
termination: nodes of a zone graph are of the form $(q,Z)$ where $q$ is a
state of the automaton, and $Z$ is a zone; exploration from $(q,Z)$ is stopped
if there exists an already visited node $(q,Z^{\prime})$ such that
$(q,Z)\preceq(q,Z^{\prime})$ and $(q,Z^{\prime})\preceq(q,Z)$ for some
simulation relation $\preceq$. In this case an edge is added between $(q,Z)$
and $(q,Z^{\prime})$ to indicate a simulation equivalence. There is an
(infinite) accepting run iff there is a cycle in the zone graph thus computed,
containing an accepting state. The main point is that, from a cycle in the
zone graph with simulation equivalences, we can conclude the existence of an
infinite run over configurations.

At a high level the proof of this fact is as follows. Let us start by ignoring
simulations for the moment: suppose $(q,Z)\xrightarrow{\sigma}(q,Z)$ for a
sequence of transitions $\sigma$. By definition of successor computation in
the zone graph, for every $v$ in the zone $Z$ (on the right), there exists a
predecessor $u$ in the zone $Z$ (on the left). Repeatedly applying this
argument gives a valuation $u\in Z$ from which $\sigma$ can be iterated $\ell$
times, for any $\ell\geq 1$. When $\ell$ is greater than the number of Alur-
Dill regions [2], we get a run
$(q,u)\xrightarrow{\sigma^{\ell}}(q,u^{\prime})$ such that $u$ and
$u^{\prime}$ are region equivalent. Since the region equivalence is a time-
abstract bisimulation, this shows that we can once again do $\sigma^{\ell}$
from $(q,u^{\prime})$, and so on. This leads to an infinite run from $(q,u)$
where $\sigma$ can be iterated infinitely often. Now, when simulations are
involved, we need to consider sequences of the form
$(q,Z)\xrightarrow{\sigma}(q,Z^{\prime})$ where $(q,Z)\preceq(q,Z^{\prime})$
and $(q,Z^{\prime})\preceq(q,Z)$. An argument similar to the above can be
adapted in this case too [30, 26, 24]. The critical underlying reason that
makes such an argument possible is the presence of a finite time-abstract
bisimulation, which in timed automata, is given by the region equivalence.

The same idea cannot be directly applied in the GTA setting, as there is no
finite time-abstract bisimulation for GTAs, even with the safety assumption
(Figure 2). However, [1] have defined a finite equivalence
$v_{1}\sim_{M}v_{2}$ and shown that the downward closures of the reachable
zones w.r.t. a certain simulation called the
$\mathop{\mathsf{G}\vphantom{a}}\nolimits$ simulation [18, 19] are unions of
$\sim_{M}$ equivalence classes. Therefore, applying an argument of the above
style will give us a run $(q,u)\xrightarrow{\sigma^{\ell}}(q,u^{\prime})$ such
that $u\sim_{M}u^{\prime}$. But we cannot conclude an infinite run immediately
as $\sim_{M}$ is not a bisimulation.

To circumvent this problem, we will define an equivalence $\approx_{M}$ which
is in spirit like the region equivalence in timed automata. As expected,
$\approx_{M}$ will be a bisimulation. However, in accordance with the no
finite timed-bisimulation result, $\approx_{M}$ will have an infinite index.
We make a key observation: if we have a run
$(q,u)\xrightarrow{\sigma}(q,u^{\prime})$ such that $u\sim_{M}u^{\prime}$
_and_ if $\sigma$ releases every future clock, then we can get a run
$(q,u)\xrightarrow{\sigma}(q,u^{\prime\prime})$ where
$u\approx_{M}u^{\prime\prime}$ for a suitably modified valuation
$u^{\prime\prime}$. Since $\approx_{M}$ is a bisimulation, this will then give
an infinite run where $\sigma$ can be iterated infinitely often. As we have
seen from Lemma 3.1, if we are interested in non-Zeno runs, only such cycles
where all future clocks are released (or remain $-\infty$) are relevant.
Therefore, in order to decide liveness for safe GTAs, it suffices to construct
the zone graph with the simulation replaced with the simulation equivalence
and look for a reachable cycle that contains an accepting state such that for
every future clock $x$, either $x$ is released on the cycle, or valuation
$-\infty$ is possible for clock $x$.

This section is organized as follows: we will first define the equivalence
$\approx_{M}$ and show that it is a bisimulation; then we recall $\sim_{M}$,
and prove the key observation mentioned above. One of the main challenges is
in addressing diagonal constraints, which is exactly where the safety
assumption is helpful.

#### A region-like equivalence for GTA.

The definition of $\approx_{M}$ looks like the classical region equivalence
extended from $[0,+\infty)$ to $\overline{\mathbb{R}}$: all clocks which are
lesser than $M$ (which automatically includes all future clocks) have the same
integral values, and the ordering of fractional parts among these clocks is
preserved. To account for diagonal constraints in guards, we explicitly add a
condition to say that all allowed diagonal constraints are satisfied by
equivalent valuations. This new equivalence does not have a finite index, but
it turns out to be a time-abstract bisimulation, similar to the classical
regions.

######  Definition 3.3.

Let $v_{1},v_{2}\in\mathbb{V}$ be valuations. We say $v_{1}\approx_{M}v_{2}$
if for all clocks $x,y$:

  1. 1.

$v_{1}(x)\mathrel{\triangleleft}c$ iff $v_{2}(x)\mathrel{\triangleleft}c$ for
all ${\mathrel{\triangleleft}}\in\\{<,\leq\\}$ and $c\in\\{-\infty,+\infty\\}$
or $c\in\mathbb{Z}$ with $c\leq M$,

  2. 2.

$v_{1}\models x-y\mathrel{\triangleleft}c$ iff $v_{2}\models
x-y\mathrel{\triangleleft}c$ for all
${\mathrel{\triangleleft}}\in\\{<,\leq\\}$ and $c\in\\{-\infty,+\infty\\}$ or
$c\in\mathbb{Z}$ with $|c|\leq M$,

  3. 3.

if $-\infty<v_{1}(x),v_{1}(y)\leq M$ then we have
$\\{v_{1}(x)\\}\leq\\{v_{1}(y)\\}$ iff $\\{v_{2}(x)\\}\leq\\{v_{2}(y)\\}$.

Notice that when $v_{1}\approx_{M}v_{2}$, the first condition implies
$v_{1}(x)=+\infty$ iff $v_{2}(x)=+\infty$, $v_{1}(x)=-\infty$ iff
$v_{2}(x)=-\infty$, $-\infty<v_{1}(x)\leq M$ iff $-\infty<v_{2}(x)\leq M$, and
in this case $\lfloor v_{1}(x)\rfloor=\lfloor v_{2}(x)\rfloor$ and
$\\{v_{1}(x)\\}=0$ iff $\\{v_{2}(x)\\}=0$.

######  Lemma 3.4.

$\approx_{M}$ is a time-abstract bisimulation.

######  Proof 3.5.

Let $v_{1}\approx_{M}v_{2}$. We will show that the equivalence is preserved
under time delays and transitions.

Guard satisfaction.

We consider guards to have constants in
$\\{-\infty,+\infty\\}\cup\\{c\in\mathbb{Z}\mid|c|\leq M\\}$. From Items $1,2$
we directly get $v_{1}\models g$ iff $v_{2}\models g$.

Time elapse.

Let $\delta_{1}\geq 0$. We will construct $\delta_{2}\geq 0$ such that
$v^{\prime}_{1}=v_{1}+\delta_{1}\approx_{M}v_{2}+\delta_{2}=v^{\prime}_{2}$.
Set $\lfloor\delta_{2}\rfloor=\lfloor\delta_{1}\rfloor$. If
$\\{\delta_{1}\\}=0$, then set $\\{\delta_{2}\\}=0$. Now, assume
$0<\\{\delta_{1}\\}<1$.

Let $B=\\{x\mid-\infty<v_{1}(x)\leq M\\}=\\{x\mid-\infty<v_{2}(x)\leq M\\}$.
Let $\\{f_{1},\dots,f_{k}\\}$ $=$ $\\{\\{v_{1}(x)\\}\mid x\in B\\}$ with
$0\leq f_{1}<f_{2}<\cdots<f_{k}<1$. By definition of $v_{1}\approx_{M}v_{2}$,
the set $\\{\\{v_{2}(x)\\}\mid x\in B\\}$ is of the form
$\\{f^{\prime}_{1},\dots,f^{\prime}_{k}\\}$ with $0\leq
f^{\prime}_{1}<f^{\prime}_{2}<\cdots<f^{\prime}_{k}<1$, and $f_{1}=0$ iff
$f^{\prime}_{1}=0$.

Define $f_{0}=f^{\prime}_{0}=0$ and $f_{k+1}=f^{\prime}_{k+1}=1$. Consider the
set $\\{1-f_{k},\dots,1-f_{2},1-f_{1}\\}$. Either $\\{\delta_{1}\\}$ equals
some $1-f_{i}$, or $1-f_{i+1}<\\{\delta_{1}\\}<1-f_{i}$ for some $0\leq i\leq
k$. Choose $\\{\delta_{2}\\}=1-f^{\prime}_{i}$ in the former case, and
$\\{\delta_{2}\\}=\ell$ for some $1-f^{\prime}_{i+1}<\ell<1-f^{\prime}_{i}$ in
the latter case. This choice maintains the following property for all clocks
$x\in B$:

$\displaystyle\\{v_{1}(x)\\}+\\{\delta_{1}\\}<1$ $\displaystyle\text{ iff
}\\{v_{2}(x)\\}+\\{\delta_{2}\\}<1$ (1)
$\displaystyle\\{v_{1}(x)\\}+\\{\delta_{1}\\}\leq 1$ $\displaystyle\text{ iff
}\\{v_{2}(x)\\}+\\{\delta_{2}\\}\leq 1$

Moreover, observe that:

$\displaystyle v^{\prime}_{1}(x)=v_{1}(x)+\delta_{1}$ $\displaystyle=\lfloor
v_{1}(x)\rfloor+\lfloor\delta_{1}\rfloor+\\{v_{1}(x)\\}+\\{\delta_{1}\\}$ (2)
$\displaystyle v^{\prime}_{2}(x)=v_{2}(x)+\delta_{2}$ $\displaystyle=\lfloor
v_{2}(x)\rfloor+\lfloor\delta_{2}\rfloor+\\{v_{2}(x)\\}+\\{\delta_{2}\\}$

For clocks $x\in B$ we already have $\lfloor v_{1}(x)\rfloor=\lfloor
v_{2}(x)\rfloor$ by definition of $v_{1}\approx_{M}v_{2}$. By construction, we
have $\lfloor\delta_{1}\rfloor=\lfloor\delta_{2}\rfloor$. From (1), we deduce
that for all $x\in B$:

$\displaystyle\lfloor v^{\prime}_{1}(x)\rfloor$ $\displaystyle=\lfloor
v^{\prime}_{2}(x)\rfloor$ and $\displaystyle\\{v^{\prime}_{1}(x)\\}=0$
$\displaystyle\text{ iff }\\{v^{\prime}_{2}(x)\\}=0$ (3)

These arguments are sufficient to show items $1$ and $3$ in the definition of
$\approx_{M}$. For item $2$, notice that
$v^{\prime}_{1}(x)-v^{\prime}_{1}(y)=v_{1}(x)-v_{1}(y)$ and
$v^{\prime}_{2}(x)-v^{\prime}_{2}(y)=v_{2}(x)-v_{2}(y)$. Since $v_{1},v_{2}$
satisfy item $2$, we conclude item $2$ for $v^{\prime}_{1}$ and
$v^{\prime}_{2}$.

Reset.

Let $x$ be a history clock, and let $u_{1}\in[x]v_{1}$. Therefore,
$u_{1}(x)=0$, and $u_{1}(y)=v_{1}(y)$ for all other clocks $y$. Let
$u_{2}\in[x]v_{2}$ so that that $u_{2}(x)=0$ and $u_{2}(y)=v_{2}(y)$ for other
clocks $y$. We claim that $u_{1}\approx_{M}u_{2}$. Items $1,3$ of the
definition follow from $v_{1}\approx_{M}v_{2}$, and from the fact that
$u_{1}(x)=u_{2}(x)=0$. Item $2$ trivially holds for pairs of clocks different
from $x$. Now, we consider differences $x-y$ and $y-x$. Notice that
$u_{1}(x-y)=-v_{1}(y)$ and $u_{2}(x-y)=-v_{2}(y)$; and $u_{1}(y-x)=v_{1}(y)$
and $u_{2}(y-x)=v_{2}(y)$. Using item $1$ of $v_{1}\approx_{M}v_{2}$ we get
$u_{1}\models x-y\mathrel{\triangleleft}c$ iff $u_{2}\models
x-y\mathrel{\triangleleft}c$, and $u_{1}\models y-x\mathrel{\triangleleft}c$
iff $u_{2}\models y-x\mathrel{\triangleleft}c$.

Release.

Let $x$ be a future clock and let $u_{1}\in[x]v_{1}$. By definition, $u_{1}$
and $v_{1}$ differ only in the value of clock $x$. Construct valuation
$u_{2}\in[x]v_{2}$ as follows. Set $u_{2}(x)=-\infty$ if $u_{1}(x)=-\infty$.
Otherwise, set $\lfloor u_{2}(x)\rfloor=\lfloor u_{1}(x)\rfloor$; if
$\\{u_{1}(x)\\}=0$, then set $\\{u_{2}(x)\\}=0$; else choose $\\{u_{2}(x)\\}$
in $(0,1)$ such that for all clocks $y\neq x$ with $-\infty<u_{1}(y)\leq M$ we
have: $\\{v_{1}(y)\\}<\\{u_{1}(x)\\}$ iff $\\{v_{2}(y)\\}<\\{u_{2}(x)\\}$, and
$\\{v_{1}(y)\\}=\\{u_{1}(x)\\}$ iff $\\{v_{2}(y)\\}=\\{u_{2}(x)\\}$. By
construction, $u_{2}$ satisfies items 1 and 3 of the definition of
$\approx_{M}$. We prove that item 2 is also satisfied.

Consider a diagonal constraint $y-z\mathrel{\triangleleft}c$ with
${\mathrel{\triangleleft}}\in\\{{<},{\leq}\\}$ and $c\in\\{-\infty,+\infty\\}$
or $c\in\mathbb{Z}$ with $|c|\leq M$. If $x\notin\\{y,z\\}$ then
$u_{1}(y-z)=v_{1}(y-z)$ and $u_{2}(y-z)=v_{2}(y-z)$. Since
$v_{1}\approx_{M}v_{2}$ we obtain $u_{1}\models y-z\mathrel{\triangleleft}c$
iff $u_{2}\models y-z\mathrel{\triangleleft}c$.

Consider the case $y\neq x=z$. We have $u_{1}(y-x)=v_{1}(y)-u_{1}(x)$ and
$u_{2}(y-x)=v_{2}(y)-u_{2}(x)$. If $u_{1}(x)=-\infty$ then $u_{2}(x)=-\infty$.
If $v_{1}(y)\in\\{-\infty,+\infty\\}$ then $v_{2}(y)=v_{1}(y)$. In both cases,
we have $u_{1}(y-x)=u_{2}(y-x)\in\\{-\infty,+\infty\\}$ and we get
$u_{1}\models x-y\mathrel{\triangleleft}c$ iff $u_{2}\models
x-y\mathrel{\triangleleft}c$. In the remaining cases we have
$u_{1}(x),u_{2}(x),v_{1}(y),v_{2}(y)\in\mathbb{R}$.

If $M<v_{1}(y)$ then $M<v_{2}(y)$ and $M<u_{1}(y-x),u_{2}(y-x)<+\infty$.
Hence, $u_{1}\models x-y\mathrel{\triangleleft}c$ iff $u_{2}\models
x-y\mathrel{\triangleleft}c$. Otherwise, $v_{1}(y),v_{2}(y)\leq M$ and
$\lfloor v_{1}(y)\rfloor=\lfloor v_{2}(y)\rfloor$. By construction we have
$\lfloor u_{2}(x)\rfloor=\lfloor u_{1}(x)\rfloor$. We write

$\displaystyle u_{1}(y-x)$ $\displaystyle=v_{1}(y)-u_{1}(x)=\lfloor
v_{1}(y)\rfloor-\lfloor u_{1}(x)\rfloor+\\{v_{1}(y)\\}-\\{u_{1}(x)\\}$
$\displaystyle u_{2}(y-x)$ $\displaystyle=v_{2}(y)-u_{2}(x)=\lfloor
v_{2}(y)\rfloor-\lfloor u_{2}(x)\rfloor+\\{v_{2}(y)\\}-\\{u_{2}(x)\\}\,.$

We know that $\lfloor v_{1}(y)\rfloor-\lfloor u_{1}(x)\rfloor=\lfloor
v_{2}(y)\rfloor-\lfloor u_{2}(x)\rfloor$. By construction,
$\\{v_{1}(y)\\}<\\{u_{1}(x)\\}$ iff $\\{v_{2}(y)\\}<\\{u_{2}(x)\\}$, and
$\\{v_{1}(y)\\}=\\{u_{1}(x)\\}$ iff $\\{v_{2}(y)\\}=\\{u_{2}(x)\\}$. We deduce
once again that $u_{1}\models x-y\mathrel{\triangleleft}c$ iff $u_{2}\models
x-y\mathrel{\triangleleft}c$.

The case $y=x\neq z$ can be proved similarly.

#### The equivalence $\sim_{M}$, and moving from $\sim_{M}$ to $\approx_{M}$.

The equivalence $\sim_{M}$ is defined on the space of all valuations. Our goal
in this part is to start from $v_{1}\sim_{M}v_{2}$ and generate a valuation
$v^{\prime}_{2}$ by modifying some values of $v_{2}$, so that we get
$v_{1}\approx_{M}v^{\prime}_{2}$. Let us first recall the definition of
$\sim_{M}$, with $n$ be the number of clocks in the GTA.

  * •

First, we define $\sim_{M}$ on $\alpha,\beta\in\overline{\mathbb{R}}$ by
$\alpha\sim_{M}\beta$ if
$(\alpha\mathrel{\triangleleft}c\Longleftrightarrow\beta\mathrel{\triangleleft}c)$
for all ${\mathrel{\triangleleft}}\in\\{<,\leq\\}$ and
$c\in\\{-\infty,+\infty\\}$ or $c\in\mathbb{Z}$ with $|c|\leq M$. In
particular, $\alpha\sim_{M}\beta$ implies $\alpha=-\infty$ iff $\beta=-\infty$
and $\alpha=+\infty$ iff $\beta=+\infty$. Also, if $-M\leq\alpha\leq M$ then
$\alpha\sim_{M}\beta$ implies $\lfloor\alpha\rfloor=\lfloor\beta\rfloor$ and
$\\{\alpha\\}=0$ iff $\\{\beta\\}=0$.

  * •

For valuations $v_{1},v_{2}\in\mathbb{V}$ we define $v_{1}\sim_{M}v_{2}$ if
$(i)$ $v_{1}(x)\sim_{nM}v_{2}(x)$ for all $x\in X$, and $(ii)$
$v_{1}(x)-v_{1}(y)\sim_{(n+1)M}v_{2}(x)-v_{2}(y)$ for all pairs of clocks
$x,y\in X$.

Notice that $\approx_{M}$ and $\sim_{M}$ are incomparable, in the sense that
neither of them is a refinement of the other. The equivalence $\approx_{M}$
constrains values up to $M$, whereas $\sim_{M}$ looks at values up to $nM$,
i.e., between $-nM$ and $nM$. For instance, consider $v_{1}:=\langle
x=M+2,y=1\rangle$ and $v_{2}:=\langle x=M+3,y=1\rangle$ for some $M\geq 2$. We
have $v_{1}\approx_{M}v_{2}$, but $v_{1}\not\sim_{M}v_{2}$. For the other way
around, notice that $\sim_{M}$ has finite index, whereas $\approx_{M}$ does
not. So, $v_{1}\sim_{M}v_{2}$ does not imply $v_{1}\approx_{M}v_{2}$. To see
it more closely, $v_{1}\approx_{M}v_{2}$ enforces the same integral values for
all future clocks. For clocks less than $-(n+1)M$, there is no such constraint
on the actual values in $\sim_{M}$.

As mentioned above, our objective is to obtain $\approx_{M}$ equivalent
valuations starting from $\sim_{M}$ equivalent ones. Lemma 3.6 is a first step
in this direction. It essentially shows that, when restricted to clocks within
$-M$ and $+M$, $\sim_{M}$ entails $\approx_{M}$.

######  Lemma 3.6.

Suppose $v_{1}\sim_{M}v_{2}$. Let $x,y$ be clocks such that $-M\leq
v_{1}(x),v_{1}(y)\leq M$. Then, $\lfloor v_{1}(x)\rfloor=\lfloor
v_{2}(x)\rfloor$, $\\{v_{1}(x)\\}=0$ iff $\\{v_{2}(x)\\}=0$, and
$\\{v_{1}(x)\\}\leq\\{v_{1}(y)\\}$ iff $\\{v_{2}(x)\\}\leq\\{v_{2}(y)\\}$.

######  Proof 3.7.

Since $v_{1}\sim_{M}v_{2}$ we have in particular $v_{1}(x)\sim_{M}v_{2}(x)$
and we deduce $\lfloor v_{1}(x)\rfloor=\lfloor v_{2}(x)\rfloor$ and
$\\{v_{1}(x)\\}=0$ iff $\\{v_{2}(x)\\}=0$. For the last statement, observe
that:

$\displaystyle v_{1}(x-y)$ $\displaystyle=\lfloor v_{1}(x)\rfloor-\lfloor
v_{1}(y)\rfloor+\\{v_{1}(x)\\}-\\{v_{1}(y)\\}$ (4) $\displaystyle v_{2}(x-y)$
$\displaystyle=\lfloor v_{2}(x)\rfloor-\lfloor
v_{2}(y)\rfloor+\\{v_{2}(x)\\}-\\{v_{2}(y)\\}$

Let $d:=\lfloor v_{1}(x)\rfloor-\lfloor v_{1}(y)\rfloor=\lfloor
v_{2}(x)\rfloor-\lfloor v_{2}(y)\rfloor$. Since $-M\leq v_{1}(x),v_{1}(y)\leq
M$, we have $-2M\leq v_{1}(x-y)\leq 2M$. Therefore $-2M\leq d\leq 2M$. In the
definition of $v_{1}\sim_{M}v_{2}$, we have
$v_{1}(x-y)\mathrel{\triangleleft}c$ iff $v_{2}(x-y)\mathrel{\triangleleft}c$
for all $c\in\mathbb{Z}$ with $|c|\leq(n+1)M$, where $n\geq 1$ is the number
of clocks. Since $-2M\leq d\leq 2M$, we deduce $v_{1}(x-y)\leq d$ iff
$v_{2}(x-y)\leq d$. Using (4), we deduce $\\{v_{1}(x)\\}\leq\\{v_{1}(y)\\}$
iff $v_{1}(x-y)\leq d$ iff $v_{2}(x-y)\leq d$ iff
$\\{v_{2}(x)\\}\leq\\{v_{2}(y)\\}$.

Lemma 3.6 considers clocks within $-M$ and $+M$. What about clocks above $M$?
Directly from $v_{1}\sim_{M}v_{2}$, we have $M<v_{1}(x)$ iff $M<v_{2}(x)$, and
moreover diagonal constraints up to $M$ are already preserved by $\sim_{M}$.
Therefore, together with Lemma 3.6, $v_{1}\sim_{M}v_{2}$ implies
$v_{1}\approx_{M}v_{2}$ when restricted to clocks greater than $-M$. We cannot
say the same for clocks lesser than $-M$, in particular we may have
$v_{1}(x)=-nM-1$ and $v_{2}(x)=-nM-2$. However, as shown in the lemma below,
we can choose suitable values for clocks lesser than $-M$ to get a
$\approx_{M}$-equivalent valuation from a $\sim_{M}$-equivalent one.

######  Lemma 3.8.

Suppose $v_{1}\sim_{M}v_{2}$, and let $L=\\{x\mid-M\leq v_{1}(x)\\}$. There is
a valuation $v^{\prime}_{2}$ such that
$v^{\prime}_{2}{\downarrow}_{L}=v_{2}{\downarrow}_{L}$ and
$v_{1}\approx_{M}v^{\prime}_{2}$.

######  Proof 3.9.

We will construct a valuation $v^{\prime}_{2}$ as required. For all clocks
$x\in L$, the lemma imposes $v^{\prime}_{2}(x)=v_{2}(x)$. The set $L$ includes
all the history clocks. For $x\in X_{F}$ with $v_{1}(x)=-\infty$ we set
$v^{\prime}_{2}(x)=-\infty$. Let
$\overline{L}=\\{x\mid-\infty<v_{1}(x)<-M\\}\subseteq X\setminus L$ be the
future clocks for which we still need to find a value in $v^{\prime}_{2}$. For
all $x\in\overline{L}$, we set $\lfloor v^{\prime}_{2}(x)\rfloor=\lfloor
v_{1}(x)\rfloor$ and if $\\{v_{1}(x)\\}=0$, set $\\{v^{\prime}_{2}(x)\\}=0$.
It remains to pick fractional parts for clocks in $\overline{L}$ such that
$0<\\{v_{1}(x)\\}<1$.

Let $B=\\{x\mid-\infty<v_{1}(x)\leq M\\}$. From Lemma 3.6, for $x,y\in B\cap
L$, we have $\\{v_{1}(x)\\}\leq\\{v_{1}(y)\\}$ iff
$\\{v_{2}(x)\\}\leq\\{v_{2}(y)\\}$, iff
$\\{v^{\prime}_{2}(x)\\}\leq\\{v^{\prime}_{2}(y)\\}$ (as $v_{2}$ and
$v^{\prime}_{2}$ coincide on $B\cap L$). Moreover, for clocks in
$\overline{L}$ with $\\{v_{1}(x)\\}=0$, we have already chosen
$\\{v^{\prime}_{2}(x)\\}=0$. We can choose fractional values for the other
clocks in $\overline{L}$ so that we get
$\\{v^{\prime}_{2}(x)\\}\leq\\{v^{\prime}_{2}(y)\\}$ iff
$\\{v_{1}(x)\\}\leq\\{v_{1}(y)\\}$ for all $x,y\in B$. We prove that
$v_{1}\approx_{M}v^{\prime}_{2}$.

  * •

Let ${\mathrel{\triangleleft}}\in\\{{<},{\leq}\\}$ and
$c\in\\{-\infty,+\infty\\}$ or $c\in\mathbb{Z}$ with $|c|\leq M$. Since
$v_{1}\sim_{M}v_{2}$, we have $v_{1}(x)\mathrel{\triangleleft}c$ iff
$v_{2}(x)\mathrel{\triangleleft}c$. By construction of $v^{\prime}_{2}$, we
have $v^{\prime}_{2}(x)=v_{2}(x)$ for $x\in L$ and for $x\in X\setminus L$ we
have $v_{1}(x)\not\mathrel{\triangleleft}c$ and
$v^{\prime}_{2}(x)\not\mathrel{\triangleleft}c$. Therefore,
$v_{1}(x)\mathrel{\triangleleft}c$ iff
$v^{\prime}_{2}(x)\mathrel{\triangleleft}c$ for all $x\in X$.

Now, let $c\in\mathbb{Z}$ with $c<-M$. By construction of $v^{\prime}_{2}$,
for all $x\in X\setminus L$ we have $v_{1}(x)\mathrel{\triangleleft}c$ iff
$v^{\prime}_{2}(x)\mathrel{\triangleleft}c$. Also, for all $x\in{L}$ we have
$v_{1}(x)\not\mathrel{\triangleleft}c$ and
$v^{\prime}_{2}(x)\not\mathrel{\triangleleft}c$. Therefore, item 1 of
Definition 3.3 is satisfied.

  * •

Item 3 of Definition 3.3 follows directly by construction of $v^{\prime}_{2}$.

  * •

Let ${\mathrel{\triangleleft}}\in\\{{<},{\leq}\\}$ and
$c\in\\{-\infty,+\infty\\}$ or $c\in\mathbb{Z}$ with $|c|\leq M$. Let $x,y\in
X$.

If $v_{1}(x)\in\\{-\infty,+\infty\\}$ or $v_{1}(y)\in\\{-\infty,+\infty\\}$
then
$v_{1}(x)-v_{1}(y)=v^{\prime}_{2}(x)-v^{\prime}_{2}(y)\in\\{-\infty,+\infty\\}$
and we deduce that $v_{1}\models x-y\mathrel{\triangleleft}c$ iff
$v^{\prime}_{2}\models x-y\mathrel{\triangleleft}c$. We assume below that
$v_{1}(x),v_{1}(y)\in\mathbb{R}$. We have

$\displaystyle v_{1}(x-y)$ $\displaystyle=\lfloor v_{1}(x)\rfloor-\lfloor
v_{1}(y)\rfloor+\\{v_{1}(x)\\}-\\{v_{1}(y)\\}$ $\displaystyle
v^{\prime}_{2}(x-y)$ $\displaystyle=\lfloor v^{\prime}_{2}(x)\rfloor-\lfloor
v^{\prime}_{2}(y)\rfloor+\\{v^{\prime}_{2}(x)\\}-\\{v^{\prime}_{2}(y)\\}$

Since $v_{1}\sim_{M}v_{2}$ and
$v^{\prime}_{2}{\downarrow}_{L}=v_{2}{\downarrow}_{L}$, we get immediately
$v_{1}\models x-y\mathrel{\triangleleft}c$ iff $v^{\prime}_{2}\models
x-y\mathrel{\triangleleft}c$ for all $x,y\in L$. When both $x,y\in B$, we get
this condition from items $1,3$ of $\approx_{M}$.

The two remaining cases is when $-\infty<v_{1}(x)<-M$ and
$M<v_{1}(y)<+\infty$, or when $-\infty<v_{1}(y)<-M$ and $M<v_{1}(x)<+\infty$.
In the first case, $-\infty<v^{\prime}_{2}(x)<-M$ by construction and
$M<v_{2}(y)=v^{\prime}_{2}(y)<+\infty$ since $v_{1}\sim_{M}v_{2}$. Therefore,
$-\infty<v_{1}(x)-v_{1}(y)<-2M$ and
$-\infty<v^{\prime}_{2}(x)-v^{\prime}_{2}(y)<-2M$. We deduce that
$v_{1}\models x-y\mathrel{\triangleleft}c$ iff $v^{\prime}_{2}\models
x-y\mathrel{\triangleleft}c$. The proof is similar in the second case.

Finally, we show that if we have a run between $\sim_{M}$ equivalent
valuations, we can extract a run between $\approx_{M}$ equivalent valuations,
simply by changing the last released values of future clocks. Suppose there is
a run $\rho$ from configuration $(q,v_{1})$ to configuration $(q,v_{k})$ such
that $v_{1}\sim_{M}v_{k}$, and all future clocks are released in $\rho$. By
Lemma 3.8, there is a $v^{\prime}_{k}$ satisfying
$v_{1}\approx_{M}v^{\prime}_{k}$ that differs from $v_{k}$ only in the clocks
that are less than $-M$. In order to reach $v^{\prime}_{k}$ from $v_{1}$ using
the same sequence of transitions as in $\rho$, it is enough to choose a
suitable shifted value during the last release of the clocks that were
modified. This gives a new run $\rho^{\prime}$. The non-trivial part is to
show that $\rho^{\prime}$ is indeed a run, that is: all guards are satisfied
by the new values. We depict this situation in Figure 3. The modified clocks
are those that are less than $-M$ in $v_{k}$. Clock $x$ is one such. The black
dot represents its value in $v_{k}$, and the blue dot is its value in
$v^{\prime}_{k}$. Its new value is still $<-M$. In the run $\rho^{\prime}$,
clock $x$ is released to a suitably shifted value at its last release point.
Notice that from this last release point till $k$, clock $x$ stays below $-M$
in both $\rho$ and $\rho^{\prime}$. Therefore, all non-diagonal constraints
$x\mathrel{\triangleleft}c$ that were originally satisfied in $\rho$ continue
to get satisfied in $\rho^{\prime}$. Showing that all diagonal constraints are
still satisfied is not as easy. Here, we make use of the safety assumption.
Let us look at a diagonal constraint $x-y$, and a situation as in Figure 3
where the last release of $y$ happens after the last release of $x$. For
simplicity, let us assume there is no release of $y$ in between these two
points.

at (1,0) $v_{1}$; at (8.2,0) $v_{k}$, $v^{\prime}_{k}$; [thick, gray] (1.3,0)
to (7.7,0); [thin] (3, 0.1) – (3, -0.1); [thin] (6, 0.1) – (6, -0.1); at (3,
0.4) last release of $x$; at (6, 0.4) last release of $y$;

[thin, gray] (4,-0.5) – (4, -2.3); (3.98, -0.5) – (4.02, -0.5); (3.98, -1) –
(4.02, -1); [left] at (3.98,-0.5) $0$; [left] at (3.98,-1) $-M$; (4, -0.8)
circle (0.8pt); (4, -1.8) circle (0.8pt); [right] at (4,-0.8) $y$; [right] at
(4,-1.8) $x$; [blue] (4, -2.1) circle (0.8pt); [right] at (4, -2.1) $x$;

[xshift=2cm] [thin, gray] (4,-0.5) – (4, -2.3); (3.98, -0.5) – (4.02, -0.5);
(3.98, -1) – (4.02, -1); [left] at (3.98,-0.5) $0$; [left] at (3.98,-1) $-M$;
(4, -0.5) circle (0.8pt); (4, -1.5) circle (0.8pt); [right] at (4,-0.5) $y$;
[right] at (4,-1.5) $x$;

[blue] (4, -1.8) circle (0.8pt); [right] at (4, -1.8) $x$;

[xshift=4cm] [thin, gray] (4,-0.5) – (4, -2.3); (3.98, -0.5) – (4.02, -0.5);
(3.98, -1) – (4.02, -1); [left] at (3.98,-0.5) $0$; [left] at (3.98,-1) $-M$;
(4, -1.2) circle (0.8pt); [right] at (4,-1.2) $x$;

[blue] (4, -1.5) circle (0.8pt); [right] at (4, -1.5) $x$;

Figure 3: An illustration for the proof of Lemma 3.10

We divide the run into three parts: the left part is the one before the last
release of $x$, the middle part is the one between the two release points, and
the right part is the rest of the run, to the right of the release of $y$. In
the left part, the values of $x$ and $y$ are the same in both $\rho$ and
$\rho^{\prime}$, and so the diagonal constraints continue to get satisfied. In
the right part, the value of $x-y$ equals
$v^{\prime}_{k}(x)-v^{\prime}_{k}(y)$. Using $v^{\prime}_{k}\approx_{M}v_{1}$
and $v_{1}\sim_{M}v_{k}$, we can argue that $v^{\prime}_{k}$ and $v_{k}$
satisfy the same diagonal constraints up to constant $M$. This takes care of
the right part. The middle part is the trickiest. In this part, we know that
$x$ remains less than $-M$ in both $\rho$ and $\rho^{\prime}$. The value of
$y$ is the same in both $\rho$ and $\rho^{\prime}$. But what about the
difference $x-y$? Can it be, say $-1$ in $\rho$ and $-2$ in $\rho^{\prime}$?
Here is where we use the safety assumption to infer the value of $x-y$. Before
$y$ is released, its value should be $0$. At that point, $x$ is still less
than $-M$ (in both the runs). Therefore $x-y<-M$ just before $y$ is last
released. As the differences do not change, we see that $x-y<-M$ in the middle
part, for both runs. Hence the diagonal constraints continue to hold in
$\rho^{\prime}$. We formalize these observations in Lemma 3.10, where we
exhaustively argue about all the different cases.

######  Lemma 3.10.

Consider a safe GTA $\mathcal{A}$. Let
$\rho:(q_{1},v_{1})\xrightarrow{\delta_{1},t_{1}}(q_{2},v_{2})\xrightarrow{\delta_{2},t_{2}}\cdots(q_{k},v_{k})$
be a run of $\mathcal{A}$ such that $v_{1}\sim_{M}v_{k}$ and for every future
clock $x$, either $x$ is released in the transition sequence $t_{1}\dots
t_{k-1}$ or $v_{1}(x)=-\infty$. Let $L=\\{x\mid-M\leq v_{1}(x)\\}$. Let
$v^{\prime}_{k}$ be a valuation such that
$v^{\prime}_{k}{\downarrow}_{L}=v_{k}{\downarrow}_{L}$ and
$v_{1}\approx_{M}v^{\prime}_{k}$. Then, there exists a run of the form
$\rho^{\prime}:(q_{1},v_{1})=(q_{1},v^{\prime}_{1})\xrightarrow{\delta_{1},t_{1}}(q_{2},v^{\prime}_{2})\xrightarrow{\delta_{2},t_{2}}\cdots(q_{k},v^{\prime}_{k})$
in $\mathcal{A}$, leading to $(q_{k},v^{\prime}_{k})$ from $(q_{1},v_{1})$.

######  Proof 3.11.

First, the existence of $v^{\prime}_{k}$ comes from Lemma 3.8. Notice that
$\rho^{\prime}$ and $\rho$ have the same time elapse values. Let
$\overline{L}=\\{x\mid-\infty<v_{1}(x),v_{k}(x)<-M\\}$. These are the clocks
where $v^{\prime}_{k}$ may differ from $v_{k}$. To make $\rho^{\prime}$ end
with $v^{\prime}_{k}$, it is enough to correctly choose the last released
values for clocks in $\overline{L}$ along the run.

Without loss of generality, assume that each $t_{i}$ is an atomic program,
consisting of either a guard or a change. If the transition is a “change”, we
can assume the guard to be $\top$. For each future clock $x\in X_{F}$ which is
released in the transition sequence $t_{1}\cdots t_{k-1}$, let $j_{x}$ be the
last index such that $x$ is released in $t_{j_{x}}$. For each clock
$x\in\overline{L}$, we will now give a different released value at $j_{x}$:
set
$v^{\prime}_{j_{x}+1}(x)=v^{\prime}_{k}(x)-\sum_{i=j_{x}+1}^{m-1}\delta_{i}$.
This construction fixes the values of all clocks along the run
$\rho^{\prime}$. However, we need to show that the new valuations still
satisfy the guards along the way. We will prove that $v_{i}$ satisfies an
atomic constraint iff $v^{\prime}_{i}$ does. Let
${\mathrel{\triangleleft}}\in\\{{<},{\leq}\\}$ and
$c\in\\{-\infty,+\infty\\}\cup\\{d\in\mathbb{Z}\mid|d|\leq M\\}$.

Consider a non-diagonal constraint $x\mathrel{\triangleleft}c$ in $t_{i}$. If
$v^{\prime}_{i}(x)=v_{i}(x)$, we are done. Otherwise, $x\in\overline{L}$,
$-\infty<v_{k}(x),v^{\prime}_{k}(x)<-M$ and $j_{x}<i$. As $x$ is not released
in $t_{i},\ldots,t_{k-1}$, we get $-\infty<v_{i}(x)\leq v_{k}(x)<-M$ and
$-\infty<v^{\prime}_{i}(x)\leq v^{\prime}_{k}(x)<-M$. This shows $v_{i}\models
x\mathrel{\triangleleft}c$ iff $v^{\prime}_{i}\models
x\mathrel{\triangleleft}c$.

Consider a diagonal constraint of the form $x-y\mathrel{\triangleleft}c$. If
$v_{i}(x)\in\\{-\infty,+\infty\\}$ then $v^{\prime}_{i}(x)=v_{i}(x)$ and if
$v_{i}(y)\in\\{-\infty,+\infty\\}$ then $v^{\prime}_{i}(y)=v_{i}(y)$. Hence,
if $v_{i}(x)\in\\{-\infty,+\infty\\}$ or $v_{i}(y)\in\\{-\infty,+\infty\\}$)
then
$v_{i}(x)-v_{i}(y)=v^{\prime}_{i}(x)-v^{\prime}_{i}(y)\in\\{-\infty,+\infty\\}$.
We deduce that in this case $v_{i}\models x-y\mathrel{\triangleleft}c$ iff
$v^{\prime}_{i}\models x-y\mathrel{\triangleleft}c$. We assume below that
$v_{i}(x),v_{i}(y),v^{\prime}_{i}(x),v^{\prime}_{i}(y)\in\mathbb{R}$.

If $v_{i}(x)=v^{\prime}_{i}(x)$ and $v_{i}(y)=v^{\prime}_{i}(y)$ then clearly
$v_{i}\models x-y\mathrel{\triangleleft}c$ iff $v^{\prime}_{i}\models
x-y\mathrel{\triangleleft}c$. Otherwise, either $x\in\overline{L}$ and
$j_{x}<i$, or $y\in\overline{L}$ and $j_{y}<i$, or both.

  * •

Suppose $x,y\in X_{F}$ and $j_{x},j_{y}<i$ (right part of Figure 3). Then,
$v_{i}(x-y)=v_{k}(x-y)$ and $v^{\prime}_{i}(x-y)=v^{\prime}_{k}(x-y)$. Observe
that $v_{k}\models x-y\mathrel{\triangleleft}c$ iff $v_{1}\models
x-y\mathrel{\triangleleft}c$ (since $v_{1}\sim_{M}v_{k}$), iff
$v^{\prime}_{k}\models x-y\mathrel{\triangleleft}c$ (since
$v_{1}\approx_{M}v^{\prime}_{k}$). Therefore, $v_{i}\models
x-y\mathrel{\triangleleft}c$ iff $v^{\prime}_{i}\models
x-y\mathrel{\triangleleft}c$.

  * •

Suppose $x\in\overline{L}$, $j_{x}<i$ and $y\in X_{H}$. Then,
$-\infty<v_{i}(x)\leq v_{k}(x)<-M$, and $-\infty<v^{\prime}_{i}(x)\leq
v^{\prime}_{k}(x)<-M$, and $0\leq v_{i}(y)=v^{\prime}_{i}(y)<+\infty$. We
deduce that $v_{i}\models x-y\mathrel{\triangleleft}c$ iff
$v^{\prime}_{i}\models x-y\mathrel{\triangleleft}c$.

  * •

The case $y\in\overline{L}$ with $j_{y}<i$ and $x\in X_{H}$ is proved
similarly.

  * •

Suppose $x,y\in X_{F}$ and $j_{x}<i\leq j_{y}$. Let $i\leq j\leq k-1$ be the
first release of $y$ in the sequence $t_{i}\cdots t_{k-1}$. Notice that
$v_{i}(x-y)=v_{j}(x-y)$ and $v^{\prime}_{i}(x-y)=v^{\prime}_{j}(x-y)$. So, it
is enough to show $v_{j}\models x-y\mathrel{\triangleleft}c$ iff
$v^{\prime}_{j}\models x-y\mathrel{\triangleleft}c$. Since $\mathcal{A}$ is a
safe GTA we have $v_{j}(y)\in\\{-\infty,0\\}$. Since $v_{i}(y)\neq-\infty$ we
get $v_{j}(y)=0$. Since $j\leq j_{y}$ we have $v^{\prime}_{j}(y)=v_{j}(y)=0$.
Therefore, $v_{j}\models x-y\mathrel{\triangleleft}c$ iff $v_{j}\models
x\mathrel{\triangleleft}c$ iff $v^{\prime}_{j}\models
x\mathrel{\triangleleft}c$ (non-diagonal case above) iff
$v^{\prime}_{j}\models x-y\mathrel{\triangleleft}c$.

  * •

The case $x,y\in X_{F}$ with $j_{y}<i\leq j_{x}$ is proved similarly.

We lift this argument to the level of zones, to obtain one of the main results
of this paper. Before showing the result in Lemma 3.14, we first prove an
intermediate result.

######  Lemma 3.12.

Let $Z$ be a non-empty zone and let $R\subseteq X_{F}$ be a set of future
clocks $x$ such that $v_{x}(x)=-\infty$ for some valuation $v_{x}\in Z$. There
are valuations $v\in Z$ such that $v(x)=-\infty$ for all $x\in R$.

######  Proof 3.13.

Let $\mathbb{G}$ be the canonical distance graph for the non-empty zone $Z$.
Since for each $x\in R$ there is a valuation $v_{x}$ in $Z$ such that
$v_{x}(x)=-\infty$ we deduce that for each $x\in R$ we have
$\mathbb{G}_{x0}=(\leq,+\infty)$. Let $\mathbb{G}^{\prime}$ be the distance
graph obtained from $\mathbb{G}$ by setting
$\mathbb{G}^{\prime}_{0x}=(\leq,-\infty)$ for each $x\in R$. The distance
graph $\mathbb{G}^{\prime}$ is in standard form. Moreover,
$\mathbb{G}^{\prime}$ has no negative cycles: a _simple_ cycle in
$\mathbb{G}^{\prime}$ which is not in $\mathbb{G}$ is of the form $0\to x\to
0$ with $x\in R$ and its weight is
$(\leq,-\infty)+(\leq+\infty)=(\leq,+\infty)$. Therefore,
$[\\![\mathbb{G}^{\prime}]\\!]$ is non-empty. Any valuation
$v\in[\\![\mathbb{G}^{\prime}]\\!]\subseteq[\\![\mathbb{G}]\\!]=Z$ is such
that $v(x)=-\infty$ for all $x\in R$.

[state/.style=circle, inner sep=2pt, minimum size = 3pt, draw, thick] [] (0)
at (4,0) $(q,w_{1})$; (1) at (6,0) $(q,u_{0})$; [label=[rotate=90,
anchor=east]below:$\in$] (3) at (4.2,1) $Z$; [label=[rotate=90,
anchor=east]below:$\in$] (3) at (6.2,1) $Z^{\prime}$;

[thick, ->,>=stealth, auto] (0) to node $\sigma$ (1);

[dashed,color=red,-,>=stealth, auto] (4,0) to node $\preceq$ (4,-2); (6,0) to
node $\preceq$ (6,-2);

[yshift=-2cm] (3) at (6,0) $(q,u^{\prime}_{0})$; (2) at (4,0)
$(q,w^{\prime}_{1})$; [label=[rotate=90, anchor=west]above:$\ni$] (6) at
(4.2,-0.8) $Z^{\prime}$;

[thick, ->,>=stealth, auto] (2) to node $\sigma$ (3);

[yshift=-5cm] (3) at (6,0) $(q,u^{\prime}_{0})$; (2) at (4,0)
$(q,w^{\prime}_{1})$; (1) at (2,0) $(q,w_{2})$; [label=[rotate=90,
anchor=east]below:$\in$] (6) at (4.2,0.8) $Z^{\prime}$; [label=[rotate=90,
anchor=east]below:$\in$] (8) at (2.2,0.8) $Z$;

[thick, ->,>=stealth, auto] (2) to node $\sigma$ (3); (1) to node $\sigma$
(2);

[dashed,color=red,-,>=stealth, auto] (4,-5) to node $\preceq$ (4,-7); (6,-5)
to node $\preceq$ (6,-7); (2,-5) to node $\preceq$ (2,-7);

[yshift=-7cm] (3) at (6,0) $(q,u^{\prime\prime}_{0})$; (2) at (4,0)
$(q,w^{\prime\prime}_{1})$; (1) at (2,0) $(q,w^{\prime}_{2})$;
[label=[rotate=90, anchor=west]above:$\ni$] (6) at (2.2,-0.8) $Z^{\prime}$;

[thick, ->,>=stealth, auto] (2) to node $\sigma$ (3); (1) to node $\sigma$
(2);

[yshift=-10cm] (3) at (6,0) $(q,u^{\prime\prime\prime}_{0})$; (1) at (2,0)
$(q,w^{\prime}_{2})$; (0) at (0,0) $(q,w_{3})$; [label=[rotate=90,
anchor=east]below:$\in$] (6) at (2.2,0.8) $Z^{\prime}$; [label=[rotate=90,
anchor=east]below:$\in$] (8) at (0.2,0.8) $Z$;

[thick, ->,>=stealth, auto] (1) to node $\sigma^{2}$ (3); (0) to node $\sigma$
(1);

[dashed,color=red,-,>=stealth, auto] (6,-10) to node $\preceq$ (6,-12);
(0,-10) to node $\preceq$ (0,-12);

[yshift=-12cm] (3) at (6,0) $(q,u^{\prime\prime\prime}_{0})$; (0) at (0,0)
$(q,w^{\prime}_{3})$; [label=[rotate=90, anchor=west]above:$\ni$] (6) at
(0.2,-0.8) $Z^{\prime}$;

[thick, ->,>=stealth, auto] (0) to node $\sigma^{3}$ (3);

(a) at (-2,-11)
$Z\preceq_{\mathop{\mathsf{G}\vphantom{a}}\nolimits(q)}Z^{\prime}$; (a) at
(-2,-6) $Z\preceq_{\mathop{\mathsf{G}\vphantom{a}}\nolimits(q)}Z^{\prime}$;
(a) at (-2,-1)
$Z\preceq_{\mathop{\mathsf{G}\vphantom{a}}\nolimits(q)}Z^{\prime}$; (b) at
(-2,-3.5) Post-property; (b) at (-2,-8.5) Post-property;

Figure 4: Construction of the run iterating the sequence $\sigma=t_{1}\dots
t_{k-1}$.

######  Theorem 3.14.

Let
$(q,Z)=(q_{1},Z_{1})\xrightarrow{t_{1}}(q_{2},Z_{2})\xrightarrow{t_{2}}\cdots\xrightarrow{t_{k-1}}(q_{k},Z_{k})=(q,Z^{\prime})$
be a run in the zone graph such that $(q,Z)\preceq(q,Z^{\prime})$,
$(q,Z^{\prime})\preceq(q,Z)$ and for every future clock $x$, either $x$ is
released in the sequence $t_{1}\dots t_{k-1}$, or there is a valuation
$v_{x}\in Z^{\prime}$ with $v_{x}(x)=-\infty$. Then, there is a valuation
$v\in Z$ and an infinite run starting from $(q,v)$ over the sequence of
transitions $(t_{1}\dots t_{k-1})^{\omega}$.

######  Proof 3.15.

Let $R\subseteq X_{F}$ be the set of future clocks which are not released in
the transition sequence $t_{1}\cdots t_{k-1}$. Using Lemma 3.12, we can pick a
valuation $u_{0}\in Z^{\prime}$ with $u_{0}(x)=-\infty$ for all $x\in R$. By
the post-property of the zone graph, there exists $w_{1}\in Z$ such that
$(q,w_{1})\xrightarrow{t_{1}\dots t_{k-1}}(q,u_{0})$. Note that
$w_{1}(x)=-\infty$ for all $x\in R$. Since $(q,Z)\preceq(q,Z^{\prime})$, there
exists $w^{\prime}_{1}\in Z^{\prime}$ such that
$(q,w_{1})\preceq(q,w^{\prime}_{1})$. From the third condition of a simulation
in Definition 2.5, we get $w^{\prime}_{1}(x)=-\infty$ for all $x\in R$.
Therefore, there is a run $\rho_{1}:=(q,w^{\prime}_{1})\xrightarrow{t_{1}\dots
t_{k-1}}(q,u^{\prime}_{0})$ such that $(q,u_{0})\preceq(q,u^{\prime}_{0})$.

Set $u_{1}=w^{\prime}_{1}$ and repeat the argument above. There exists
$w^{\prime}_{2}\in Z^{\prime}$ from which there exists a run
$\rho_{2}:=(q,w^{\prime}_{2})\xrightarrow{t_{1}\dots
t_{k-1}}(q,w^{\prime\prime}_{1})$ with
$(q,w^{\prime}_{1})\preceq(q,w^{\prime\prime}_{1})$. Using this simulation,
$\rho_{2}$ can be extended with a run similar to $\rho_{1}$ to give:
$(q,w^{\prime}_{2})\xrightarrow{(t_{1}\dots t_{k-1})(t_{1}\dots
t_{k-1})}(q,u^{\prime\prime}_{0})$ with
$(q,u_{0})\preceq(q,u^{\prime\prime}_{0})$.

Repeated application of this argument shows for each $\ell\geq 1$ the
existence of a valuation $v_{\ell}\in Z^{\prime}$ from which $(t_{1}\dots
t_{k-1})$ can be iterated $\ell$ times: $(q,v_{\ell})\xrightarrow{(t_{1}\dots
t_{k-1})}(q,v_{\ell-1})\cdots(q,v_{1})\xrightarrow{t_{1}\dots
t_{k-1}}(q,v_{0})$ with $v_{\ell}(x)=-\infty$ for all $x\in R$. This is
illustrated in Figure 4.

Pick a large $\ell$ which is strictly greater than the number of equivalence
classes of $\sim_{M}$. Therefore there exist $i>j$ such that
$v_{i}\sim_{M}v_{j}$, and there is a run $(q,v_{i})\xrightarrow{(t_{1}\dots
t_{k-1})^{i-j}}(q,v_{j})$ with $v_{i}(x)=-\infty$ for all $x\in R$. By Lemma
3.10, there is a run $(q,v_{i})\xrightarrow{(t_{1}\dots
t_{k-1})^{i-j}}(q,v^{\prime}_{j})$ such that $v_{i}\approx_{M}v^{\prime}_{j}$.
Since $\approx_{M}$ is a bisimulation (Lemma 3.4), this implies there is an
infinite run where the segment $\xrightarrow{(t_{1}\dots t_{k-1})^{i-j}}$ can
be iterated infinitely often. In particular, this gives a run of the required
form.

Finally, combining Theorem 3.14 and Lemma 3.1, we get an algorithm for
liveness: we construct the zone graph with simulation equivalence and check
for a reachable cycle that contains an accepting state and where every future
clock $x$ which is not released during the cycle may take value $-\infty$ in
some valuations of the zones in the cycle.

##  4 Translating MITL to GTA

We first introduce the preliminaries for Metric Interval Temporal Logic. Let
$\mathsf{Prop}$ be a finite nonempty set of atomic propositions. The alphabet
$\Sigma$ that we consider is the set of subsets of $\mathsf{Prop}$. The set of
$\mathsf{MITL}$ formulae over the set of atomic propositions $\mathsf{Prop}$
is defined as

$\varphi:=p\leavevmode\nobreak\ |\leavevmode\nobreak\
\varphi\wedge\varphi\leavevmode\nobreak\ |\leavevmode\nobreak\
\neg\varphi\leavevmode\nobreak\ |\leavevmode\nobreak\
\mathop{\mathsf{X}\vphantom{a}}\nolimits_{I}\varphi\leavevmode\nobreak\
|\leavevmode\nobreak\ \varphi\mathbin{\mathsf{U}}_{I}\varphi$

where $p\in\mathsf{Prop}$, and $I$ is either $[0,0]$, or a non-singleton
(open, or closed) interval whose end-points come from
$\mathbb{N}\cup\\{\infty\\}$. In other words, if the end-points of the
interval are $a$ and $b$ respectively, then either $a=b=0$, or
$a,b\in\mathbb{N}\cup\\{\infty\\}$ and $a<b$.

We will now define the _pointwise semantics_ of MITL formulae inductively as
follows. A timed word
$w=(a_{0},\tau_{0})(a_{1},\tau_{1})(a_{2},\tau_{2})\cdots$ is said to satisfy
the MITL formula $\varphi$ at position $i\geq 0$, denoted as
$(w,i)\models\varphi$ if (omitting the classical boolean connectives)

  * •

$(w,i)\models p$ if $p\in a_{i}$

  * •

$(w,i)\models\mathop{\mathsf{X}\vphantom{a}}\nolimits_{I}\varphi$ if
$(w,i+1)\models\varphi$ and $\tau_{i+1}-\tau_{i}\in I$.

  * •

$(w,i)\models\varphi_{1}\mathbin{\mathsf{U}}_{I}\varphi_{2}$ if there exists
$j\geq i$ s.t. $(w,j)\models\varphi_{2}$, $(w,k)\models\varphi_{1}$ for all
$i\leq k<j$, and $\tau_{j}-\tau_{i}\in I$.

For a formula $\varphi$ we can also define its pointwise semantics as a
function from (non-Zeno) timed words to sequences of Booleans. Let
$T\mathbb{B}^{\omega}$ denote $(\\{0,1\\}\times\mathbb{R})^{\omega}$ and
$(T\mathbb{B}^{2})^{\omega}$ denote
$(\\{0,1\\}^{2}\times\mathbb{R})^{\omega}$, respectively. Then for
$\varphi\in\mathsf{MITL}$, we define $[\\![\varphi]\\!]\colon
T\Sigma^{\omega}\rightarrow T\mathbb{B}^{\omega}$ as a total function, i.e.,
$\mathsf{dom}([\\![\varphi]\\!])=T\Sigma^{\omega}$ and for any
$w=(a_{0},\tau_{0})(a_{1},\tau_{1})\ldots$, we have
$[\\![\varphi]\\!](w)=(b_{0},\tau_{0})(b_{1},\tau_{1})\ldots$, where for all
$i$, $b_{i}=1$ if $(w,i)\models\varphi$ and $b_{i}=0$ otherwise. Finally,
given an $\mathsf{MITL}$ formula $\varphi$ we define its language
$\mathcal{L}(\varphi)=\\{w\in T\Sigma^{\omega}\mid(w,0)\models\varphi\\}$.

Our goal is to construct a GTA with outputs for an MITL formula $\varphi$,
which reads the timed word and outputs $1$ at position $i$ iff
$(w,i)\models\varphi$. More precisely, there is a unique run of the GTA on
$w$:
$(q_{0},v_{0})\xrightarrow{\delta_{0},t_{0}}(q_{1},v_{1})\xrightarrow{\delta_{1},t_{1}}\cdots$,
where the output of each transition $t_{i}$ equals $1$ iff
$(w,i)\models\varphi$. We refer to GTA with outputs as Generalized Timed
Transducers (GTT) and we will formally define them next.

###  4.1 Generalized Timed Transducers (GTT)

######  Definition 4.1 (Generalized Timed Transducer).

A _generalized timed transducer_ (GTT) is a tuple
$\mathcal{T}=(Q,\Sigma,\Gamma,X,\Delta,\mu,\mathcal{I},(Q_{f},g_{f}))$, where
$\Sigma$ and $\Gamma$ are the finite _input_ and _output alphabets_ ,
$\mathcal{A}_{\mathcal{T}}=(Q,\Sigma,X,\Delta,\mathcal{I},(Q_{f},g_{f}))$ is a
GTA, called the _underlying generalized timed automata_ of the GTT
$\mathcal{T}$, and $\mu\colon\Delta\to\Gamma^{*}$ is the _output function_.

$\begin{array}[]{rcccccccc}w:&a&a&a&a&a&a&a&\cdots\\\
\tau:&1.3&5.7&7.8&10&11&21.2&100.7&\cdots\\\
[\\![\mathcal{T}]\\!](w):&1&1&1&1&1&1&1&\cdots\\\
\tau:&1.3&5.7&7.8&10&11&21.2&100.7&\cdots\end{array}$

Figure 5: An generalized timed transducer $\mathcal{T}$ on left, and a run of
$\mathcal{T}$ on a timed word $w$ with the output on right.

Note that associated to each transition of a GTT , we have a tuple consisting
of an input letter, an instantaneous timed program, and an output letter. The
semantics of the GTT $\mathcal{T}$ defined above is given by a transition
system $\mathbb{TS}_{\mathcal{T}}$ whose states are _configurations_ $(q,v)$
of $\mathcal{T}$, where $q\in Q$ and $v\in\mathbb{V}$ is a valuation.

An example of a GTT and its run is given in Figure 5. An accepting run $\rho$
on the input timed word $w=(a_{0},\tau_{0})(a_{1},\tau_{1})\cdots$ and with
sequence of discrete transitions $t_{0}t_{1}\cdots$ produces the output timed
word $\rho(w)=(\mu(t_{0}),\tau_{0})(\mu(t_{1}),\tau_{1})\cdots$. Note that for
a generalized timed transducer $\mathcal{T}$ and an input timed word $w$,
there could be several accepting runs of $\mathcal{T}$ over $w$. Hence, the
semantics of $\mathcal{T}$ is a relation $[\\![\mathcal{T}]\\!]\subseteq
T\Sigma^{\omega}\times T\Gamma^{\omega}$ defined by
$[\\![\mathcal{T}]\\!]=\\{(w,\rho(w))\mid\rho\text{ is an accepting run on
}w\\}$. The _domain_ of $\mathcal{T}$ is the set $\mathsf{dom}(\mathcal{T})$
of timed words $w$ such that $\mathcal{T}$ has an accepting run over $w$. We
say that $\mathcal{T}$ is functional if the relation $[\\![\mathcal{T}]\\!]$
is a partial function. In which case, we write $[\\![\mathcal{T}]\\!]\colon
T\Sigma^{\omega}\to T\Gamma^{\omega}$ and for $w\in\mathsf{dom}(\mathcal{T})$,
we write $[\\![\mathcal{T}]\\!](w)$ for the output word associated with $w$ by
$\mathcal{T}$.

A generalized timed transducer $\mathcal{T}$ is called _unambiguous_ if every
input word $w\in T\Sigma^{\omega}$ admits at most one accepting run. Clearly,
an unambiguous GTT is functional, but the converse need not be true. A
deterministic GTT is unambiguous, hence functional. There is also a dual
notion, generalizing prophetic (untimed) automata from [12], and corresponding
to co-determinism for infinite words, which also implies unambiguity, hence
functionality.

###  4.2 The compositional approach

In this section, we explain the overall approach of our translation that goes
via transducers, assuming that for each timed operator we can build a GTT.

[level distance=0.75cm, level 1/.style=sibling distance=1.5cm, level
2/.style=sibling distance=1.5cm] $\mathbin{\mathsf{U}}_{(1,2)}$ child node
$\neg$ child node $p$ child node
$\mathop{\mathsf{X}\vphantom{a}}\nolimits_{(5,7)}$ child node $\land$ child
node $q$ child node $r$ ;

Figure 6: Parse tree for the MILT formula
$\neg p\mathbin{\mathsf{U}}_{(1,2)}X_{(5,7)}(q\land r)$

At a high level, we will convert an $\mathsf{MITL}$ formula to a generalized
timed transducer (GTT) which uses history and future clocks [1], from which we
obtain a GTA. Our construction can be viewed as structural induction on the
_parse tree_ of the $\mathsf{MITL}$ formula, where we show how to build a GTT
for atomic propositions, and then for each Boolean and temporal operator, and
finally we compose these GTT bottom up to obtain the GTT for each subformula,
which by structural induction finally gives us the GTT for the full formula.

Consider the the $\mathsf{MITL}$ formula $\varphi\equiv\neg
p\leavevmode\nobreak\ \mathbin{\mathsf{U}}_{(1,2)}\leavevmode\nobreak\
\mathop{\mathsf{X}\vphantom{a}}\nolimits_{(5,7)}(q\land r)$, and its parse
tree depicted in Figure 6. Here, the subformulae of $\varphi$ are
$\psi_{0}\equiv\varphi$, $\psi_{1}\equiv\neg p$,
$\psi_{2}\equiv\mathop{\mathsf{X}\vphantom{a}}\nolimits_{(5,7)}(q\land r)$,
$\psi_{3}\equiv p$, $\psi_{4}\equiv q\land r$, $\psi_{5}\equiv q$,
$\psi_{6}\equiv r$. Observe that each node of the parse tree is either an
atomic propositions (at the leaves), or a boolean or temporal operator (at the
non-leaf nodes). Further, each subformula of $\varphi$ corresponds to a node
of the parse tree of $\varphi$ in the sense that the subtree rooted at that
node is the parse tree of the subformula.

We now discuss how the transducers for the subformulae can be combined to get
the transducer for a given formula. This is done by considering two standard
constructions for transducers, namely composition and product, which we
formally define next.

######  Definition 4.2.

Let
$\mathcal{T}_{1}=(Q_{1},A,B,X_{1},\Delta_{1},\mu_{1},\mathcal{I}_{1},(Q^{1}_{f},g^{1}_{f}))$
be a generalized timed transducer from the alphabet $A$ to $B$ and
$\mathcal{T}_{2}=(Q_{2},B,C,X_{2},\Delta_{2},\mu_{2},\mathcal{I}_{2},(Q^{2}_{f},g^{2}_{f}))$
be a generalized timed transducer from the alphabet $B$ to $C$. Then, the
composition of $\mathcal{T}_{1}$ and $\mathcal{T}_{2}$ is a generalized timed
transducer from the alphabet $A$ to $C$ given by
$\mathcal{T}_{2}\circ\mathcal{T}_{1}=(Q_{1}\times Q_{2},A,C,X_{1}\cup
X_{2},\Delta,\mu,\mathcal{I}_{1}\times\mathcal{I}_{2},((Q^{1}_{f}\times
Q_{2},g^{1}_{f})\cup(Q_{1}\times Q^{2}_{f},g^{2}_{f})))$ where the transition
function $\Delta$ and the output function $\mu$ are defined as

$p\xrightarrow{a\mid b}q$ in $\mathcal{T}_{1}$, $p^{\prime}\xrightarrow{b\mid
c}q^{\prime}$ in $\mathcal{T}_{2}$ (1) $(p,p^{\prime})\xrightarrow{a\mid
c}(q,q^{\prime})$ in $\mathcal{T}_{2}\circ\mathcal{T}_{1}$

######  Definition 4.3.

Let
$\mathcal{T}_{1}=(Q_{1},A,B,X_{1},\Delta_{1},\mu_{1},\mathcal{I}_{1},(Q^{1}_{f},g^{1}_{f}))$
be a generalized timed transducer from the alphabet $A$ to $B$ and
$\mathcal{T}_{2}=(Q_{2},B,C,X_{2},\Delta_{2},\mu_{2},\mathcal{I}_{2},(Q^{2}_{f},g^{2}_{f}))$
be a generalized timed transducer from the alphabet $B$ to $C$. Then, the
product of $\mathcal{T}_{1}$ and $\mathcal{T}_{2}$ is a generalized timed
transducer from the alphabet $A$ to $B\times C$ given by
$\mathcal{T}_{1}\times\mathcal{T}_{2}=(Q_{1}\times Q_{2},A,B\times C,X_{1}\cup
X_{2},\Delta,\mu,\mathcal{I}_{1}\times\mathcal{I}_{2},((Q^{1}_{f}\times
Q_{2},g^{1}_{f})\cup(Q_{1}\times Q^{2}_{f},g^{2}_{f})))$ where the transition
function $\Delta$ and the output function $\mu$ are defined as

$p\xrightarrow{a\mid b}q$ in $\mathcal{T}_{1}$, $p^{\prime}\xrightarrow{a\mid
c}q^{\prime}$ in $\mathcal{T}_{2}$ (1)
$(p,p^{\prime})\xrightarrow{a\mid(b,c)}(q,q^{\prime})$ in
$\mathcal{T}_{1}\times\mathcal{T}_{2}$

Let us now examine the first step in more detail. The generalized timed
transducers that we construct are such that if the GTT is for an atomic
proposition, then it reads letters from $\Sigma$ and outputs a Boolean value.
Otherwise, if the GTT is for an operator (either Boolean or temporal), then it
reads letters from $\\{0,1\\}$ (letters from $\\{0,1\\}^{2}$ respectively) if
the operator is unary (binary respectively) and outputs Booleans. The heart of
the construction is thus the following theorem, that we will prove partially
here (for the case of non-temporal operators) leaving the proofs for temporal
cases to next two sections.

Figure 7: Transducers
$\mathcal{T}_{p},\mathcal{T}_{\neg},\mathcal{T}_{\wedge},\mathcal{T}_{\vee}$
for an atomic proposition $p$, and Boolean operators (negation, conjunction
and disjunction, respectively). Recall that $\Sigma\subseteq
2^{\mathsf{Prop}}$, where $\mathsf{Prop}$ is the set of atomic propositions.
Therefore, reading a $p$ in transducer $\mathcal{T}_{p}$ means that we read a
letter $a$ such that $p\in a$.

######  Theorem 4.4.

For each atomic proposition $p$ and each operator
$\mathrm{op}\in\\{\neg,\lor,\land,\mathop{\mathsf{Y}\vphantom{a}}\nolimits_{I},\mathop{\mathsf{X}\vphantom{a}}\nolimits_{I},\mathbin{\mathsf{S}}_{I},\mathbin{\mathsf{U}}_{I}\\}$,

  1. 1.

if $\varphi=p$, with $[\\![p]\\!]:T\Sigma^{\omega}\rightarrow
T\mathbb{B}^{\omega}$, then there exists a safe GTT $\mathcal{T}_{p}$ such
that $[\\![\mathcal{T}_{p}]\\!]=[\\![\varphi]\\!]$.

  2. 2.

if $\varphi=\leavevmode\nobreak\ \mathrm{op}\leavevmode\nobreak\ p$, where
$\mathrm{op}$ is a unary operator, with
$[\\![\varphi]\\!]:T\mathbb{B}^{\omega}\rightarrow T\mathbb{B}^{\omega}$, then
there exists a safe GTT $\mathcal{T}_{\mathrm{op}}$ such that
$[\\![\mathcal{T}_{\mathrm{op}}]\\!]=[\\![\varphi]\\!]$.

  3. 3.

if $\varphi=p_{\ell}\leavevmode\nobreak\ \mathrm{op}\leavevmode\nobreak\
p_{r}$, for atomic propositions $p_{\ell}$ and $p_{r}$, and $\mathrm{op}$ a
binary operator with $[\\![\varphi]\\!]:(T\mathbb{B}^{2})^{\omega}\rightarrow
T\mathbb{B}^{\omega}$, then there exists a safe GTT
$\mathcal{T}_{\mathrm{op}}$ such that
$[\\![\mathcal{T}_{\mathrm{op}}]\\!]=[\\![\varphi]\\!]$.

The proof of Part (1) is easy. For any atomic proposition $p$, the GTT
$\mathcal{T}_{p}$ is shown in the leftmost picture of Figure 7. We remark that
in this transducer $\mathcal{T}_{p}$, a transition labelled $p$ (resp. $\neg
p$) means that we read a letter $a$ such that $p\in a$ (resp. $p\notin a$).
For instance, let $\mathsf{Prop}=\\{p,q\\}$ and $\Sigma=\\{a,b,c,d\\}$ where
the letters are interpreted as $a=\emptyset$, $b=\\{p\\}$, $c=\\{q\\}$ and
$d=\\{p,q\\}$. Then, in $\mathcal{T}_{p}$, the transition $p$ is taken when
$b$ or $d$ is seen, and $\neg p$ is taken on reading $a$ or $c$.

Next, for the Boolean unary operator $\neg$ and binary operators $\land$ and
$\vee$, the respective transducers are also depicted in Figure 7. Since these
are not temporal operators, the GTTs use no clocks. Also, these GTT are
deterministic and hence functional.

Now to complete the proof of the above theorem, it only remains to show Parts
(2) and (3) for the temporal operators in the timed setting.

In the rest of this section we will assume these results and discuss how the
transducers for the subformulae can be combined to get the transducer for a
given formula. We accomplish this by using two standard constructions for
transducers, namely composition and product. For two transducers $\mathcal{T}$
and $\mathcal{T}^{\prime}$, their (sequential) _composition_ is denoted
$\mathcal{T}\circ\mathcal{T}^{\prime}$ and their _product_ is denoted
$\mathcal{T}\times\mathcal{T}^{\prime}$.

Suppose we have an $\mathsf{MITL}$ formula
$\varphi\equiv\mathrm{op}\leavevmode\nobreak\ \psi$, and suppose we have the
GTT $\mathcal{T}_{\psi}$ for $\psi$. By Theorem 4.4, we also have a GTT
$\mathcal{T}_{\mathrm{op}}$ for $\mathrm{op}$. Then, the GTT for $\varphi$ is
obtained by sequentially composing the GTT for $\mathrm{op}$ and the GTT for
$\psi$, i.e.,
$[\\![\varphi]\\!]=[\\![\mathcal{T}_{\mathrm{op}}\circ\mathcal{T}_{\psi}]\\!]$.
Similarly, for an $\mathsf{MITL}$ formula
$\varphi\equiv\psi_{\ell}\leavevmode\nobreak\ \mathrm{op}\leavevmode\nobreak\
\psi_{r}$, if we have the GTT $\mathcal{T}_{\ell}$ for $\psi_{\ell}$ and
$\mathcal{T}_{r}$ for $\psi_{r}$. Again, by Theorem 4.4, for any binary
operators, we have a GTT $\mathcal{T}_{\mathrm{op}}$ for $\mathrm{op}$. Then,
the GTT for $\varphi$ is obtained by taking the product of
$\mathcal{T}_{\ell}$ and $\mathcal{T}_{r}$ and then composing with
$\mathcal{T}_{\mathrm{op}}$, i.e.,
$[\\![\varphi]\\!]=[\\![\mathcal{T}_{\mathrm{op}}\circ(\mathcal{T}_{\ell}\times\mathcal{T}_{r})]\\!]$.
Thus we have the following lemmas.

######  Lemma 4.5.

If $\mathcal{T}_{1}$ and $\mathcal{T}_{2}$ are functional GTTs from alphabets
$A$ to $B$ and $B$ to $C$ respectively, then
$\mathcal{T}_{2}\circ\mathcal{T}_{1}$ is a functional GTT from $A$ to $C$ and
$[\\![\mathcal{T}_{2}\circ\mathcal{T}_{1}]\\!]=[\\![\mathcal{T}_{2}]\\!]\circ[\\![\mathcal{T}_{1}]\\!]$.

######  Lemma 4.6.

If $\mathcal{T}_{1}$ and $\mathcal{T}_{2}$ are functional generalized timed
transducers from alphabets $A$ to $B$ and $A$ to $C$ respectively, then
$\mathcal{T}_{1}\times\mathcal{T}_{2}$ is a functional GTT from $A$ to
$B\times C$ and for each
$(w,\tau)\in\mathsf{dom}(\mathcal{T}_{1})\cap\mathsf{dom}(\mathcal{T}_{2})$,
if
$[\\![\mathcal{T}_{1}]\\!]((w,\tau))=(b_{0},\tau_{0})(b_{1},\tau_{1})\cdots$
and
$[\\![\mathcal{T}_{2}]\\!]((w,\tau))=(c_{0},\tau_{0})(c_{1},\tau_{1})\cdots$
then
$[\\![\mathcal{T}_{1}\times\mathcal{T}_{2}]\\!]((w,\tau))=((b_{0},c_{0}),\tau_{0})((b_{1},c_{1}),\tau_{1})\cdots$.

Finally, we can prove our main translation Theorem 4.7 below.

######  Theorem 4.7.

For any $\mathsf{MITL}$ formula, $\varphi$, we can construct a functional GTT
$\mathcal{T}_{\varphi}$ such that
$[\\![\varphi]\\!]=[\\![\mathcal{T}_{\varphi}]\\!]$.

The proof proceeds by structural induction on $\varphi$, and follows directly
from the correctness of individual GTT (given by Theorem 4.4) and the
correctness and functionality of the composition and product constructions
(given by Lemmas 4.5 and 4.6). Finally, from this GTT we obtain a safe GTA
that recognises the language $\mathcal{L}(\varphi)$, by just looking at the
output on first letter of input. Safety of this GTA follows by the fact that
we ensure safety at every step of the construction.

######  Corollary 4.8.

For any $\mathsf{MITL}$ formula, $\varphi$, we can construct a safe GTA
$\mathcal{A}_{\varphi}$ such that
$\mathcal{L}(\varphi)=\mathcal{L}(\mathcal{A}_{\varphi})$.

###  4.3 Translation of Next and Until operators

Now, we will describe the transducers for the modalities
$\mathop{\mathsf{X}\vphantom{a}}\nolimits_{I}$ and $\mathbin{\mathsf{U}}_{I}$.
We next describe the transducers for
$\mathop{\mathsf{X}\vphantom{a}}\nolimits_{I}$ and $\mathbin{\mathsf{U}}_{I}$.

#### Next operator.

The transducer for $\mathop{\mathsf{X}\vphantom{a}}\nolimits_{I}p$ is given in
Figure 8. It is obtained by extending the untimed variant of the Next-
transducer with a future clock $x$ that predicts the time to the next event.
The idea is the same as explained in Figure 1 of the Introduction. The
prediction of the next event is verified, by having the guard $x=0$ in every
transition. Notice the use of the program syntax in this example: a transition
first checks if $x=0$ (satisfying a previous obligation), and then releases
$x$ to a non-deterministic value guessing the time to the next event, and then
asks for a guard, either $-x\in I$ or $-x\notin I$.

Figure 8: GTT for $\mathop{\mathsf{X}\vphantom{a}}\nolimits_{I}$ using a
future clock $x$. The output is $0$ for transitions to location $\ell_{2}$ and
is the if-then-else $\dagger={(-x\in I)}\,?\,{1}:{0}$ for transitions to
location $\ell_{1}$, where $I$ is some interval.

#### Until operator.

We start by describing the transducer for the untimed $\mathbin{\mathsf{U}}$
modality $p\mathbin{\mathsf{U}}q$ (in other words,
$p\mathbin{\mathsf{U}}_{I}q$ with $I=[0,\infty)$). This is shown in Figure 9.
For simplicity, we have assumed $\mathsf{Prop}=\\{p,q\\}$ and the alphabet is
represented as $(0,0),(1,0),(0,1),(1,1)$ corresponding to $\\{\\}$, $\\{p\\}$,
$\\{q\\}$ and $\\{p,q\\}$. On the word $w$, if $s_{i}$ is the state that reads
$a_{i}$, then the following invariants hold:

  * •

$s_{i}=q$ iff $q\in a_{i}$,

  * •

$s_{i}=\neg q\land(p\mathbin{\mathsf{U}}q)$ iff $q\notin a_{i}$ and
$(w,i)\models p\mathbin{\mathsf{U}}q$,

  * •

$s_{i}=\neg(p\mathbin{\mathsf{U}}q)$ iff $(w,i)\not\models
p\mathbin{\mathsf{U}}q$.

Figure 9: (Left) Transducer for the untimed LTL operator
$p\mathbin{\mathsf{U}}q$.
(Right) Transducer $\mathcal{A}$ tracking the earliest and last $q$ witnesses
for $p\mathbin{\mathsf{U}}q$. Program ${\color[rgb]{1,0,0}\pi_{1}}$ is
${\color[rgb]{1,0,0}x=0;[x]}$ and program ${\color[rgb]{1,0,0}\pi_{2}}$ is
${\color[rgb]{1,0,0}x=0;y=0;[x,y]}$. The outputs $\dagger_{i}$ depend on
interval $I$ in the timed until $p\mathbin{\mathsf{U}}_{I}q$.

At the initial state the automaton makes a guess about position $0$, and then
subsequently on reading every $a_{i}$, it makes a guess about position $i+1$
and moves to the corresponding state. The transitions implement this guessing
protocol. For instance, transitions out of state $q$ read letters with $q=1$,
and also output $1$; transitions out of state $\neg(p\mathbin{\mathsf{U}}q)$
have output $0$. A noteworthy point is that state
$q\land\neg(p\mathbin{\mathsf{U}}q)$ is non-accepting, preventing the
automaton to stay in that state forever. For every word, the transducer has a
unique accepting run and the output at position $i$ is $1$ iff $(w,i)\models
p\mathbin{\mathsf{U}}q$.

Let us move on to the timed until $\mathbin{\mathsf{U}}_{I}$. Let us forget
the specific interval $I$ for the moment. We will come up with a generic
construction, on which the outputs can be appropriately modified for specific
intervals. To start the construction, we need the following notion.

######  Definition 4.9.

Let $w=(a_{0},t_{0})(a_{1},t_{1})\dots$ be a timed word and let $i\geq 0$. The
_earliest_ $q$-witness at position $i$ is the least position $j>i$ such that
$q\in a_{j}$, if it exists. We denote this position $j$ giving the earliest
$q$-witness at $i$ as $i_{f}$. The _last_ $q$-witness is the _least_ position
$j>i$ that satisfies

$\displaystyle\alpha=q\wedge\neg(p\wedge\mathop{\mathsf{X}\vphantom{a}}\nolimits(p\mathbin{\mathsf{U}}q))\equiv(q\land\neg
p)\lor(q\land\mathop{\mathsf{X}\vphantom{a}}\nolimits\neg(p\mathbin{\mathsf{U}}q))$

We denote this position $j$ giving the last $q$-witness at $i$ as $i_{\ell}$.

The earliest and last $q$-witnesses provide a convenient mechanism to check
$p\mathbin{\mathsf{U}}_{I}q$ which, in many cases, can be deduced by knowing
the time to the earliest and last witnesses. Figure 10 illustrates the
interpretation of $x$ and $y$.

[thin, gray] (0.7,0) to (7.2,0); in 1, 2.5, 3, 4.7, 6.1, 7 (, -0.1) to (,
+0.1);

in 2.5, 3, 4.7, 6.1 at (, +0.2) $q$;

at (1, -0.3) $i$; at (2.5, -0.3) $i_{f}$; at (7, +0.2) $\alpha$; at (7, -0.3)
$i_{\ell}$;

[very thin, gray, yshift=0.3cm] (1, 0.3) to node [above] $\neg q$ (2.45,0.3);
(2.55, 0.3) to node [above] $\neg q$ (2.95, 0.3);

(3.05, 0.3) to node [above] $\neg q$ (4.65, 0.3); (4.75, 0.3) to node [above]
$\neg q$ (6.05, 0.3);

(6.15, 0.3) to node [above] $\neg q$ (6.95, 0.3);

(1, 0.8) to node [above] $\neg\alpha$ (6.95, 0.8); [yshift=-0.2cm, very thin,
gray] (1, -0.5) to node [below,black] $x$ (2.45, -0.5);

(1, -0.9) to node [below,black] $y$ (7,-0.9);

Figure 10: Division of $q$ events, and interpretation of $x,y$

Our next task is to extend the $\mathbin{\mathsf{U}}$ transducer of Figure 9
to include two future clocks $x$ and $y$ that predict at each $i$, the time to
$i_{f}$ and $i_{\ell}$, respectively. Figure 9 describes the transducer
$\mathcal{A}$. For clock $x$ to maintain time to $i_{f}$ at each position $i$,
we can do the following: at every transition that reads $q$, the transducer
checks for $x=0$ as guard and releases $x$ (with the time to the next $q$). If
there is no such $q$, then $x$ needs to be released to $-\infty$ in order to
continue the run, as our timed words are non-Zeno. Transitions satisfying
$\neg q$ do not check for a guard on $x$ or release $x$. Therefore, in any
run, the value of $x$ determines the time to the next $q$ event.

In Figure 10, the last witness (property $\alpha$) can be identified by
transitions of the form $(0,1)$ (signifying $q\land\neg p$) and transitions
$(*,1)$ going to state $\neg(p\mathbin{\mathsf{U}}q)$ (for
$q\land\mathop{\mathsf{X}\vphantom{a}}\nolimits\neg(p\mathbin{\mathsf{U}}q)$).
Similar to the previous case of the earliest witness, every time we see such a
transition we check for $y=0$ as a guard and release $y$. No other transition
checks or updates $y$. Notice that only the transitions with $q$ have been
changed. All transitions $(0,1)$ check and release both clocks (program
${\color[rgb]{1,0,0}\pi_{2}}$). Transitions $(1,1)$ that do not go to
$\neg(p\mathbin{\mathsf{U}}q)$ check and release only $x$ (program
${\color[rgb]{1,0,0}\pi_{1}}$), whereas the $(*,1)$ transition that goes to
$\neg(p\mathbin{\mathsf{U}}q)$ does ${\color[rgb]{1,0,0}\pi_{2}}$.

######  Lemma 4.10.

For every timed word $w=(a_{0},\tau_{0})(a_{1},\tau_{1})\cdots$, there is a
unique run of $\mathcal{A}$ of the form:
$(s_{0},v_{0})\xrightarrow{\tau_{0},\theta_{0}}(s_{1},v_{1})\xrightarrow{\tau_{1}-\tau_{0},\theta_{1}}\cdots$
such that for every position $i\geq 0$: (1) $s_{i}$ is state $q$ of
$\mathcal{A}$ iff $w,i\models q$, (2) $s_{i}$ is state $\neg
q\land(p\mathbin{\mathsf{U}}q)$ iff $w,i\models\neg
q\land(p\mathbin{\mathsf{U}}q)$, (3) $s_{i}$ is state
$\neg(p\mathbin{\mathsf{U}}q)$ iff $w,i\models\neg(p\mathbin{\mathsf{U}}q)$,
(4) $v_{i}(x)=\tau_{i}-\tau_{i_{f}}$ and $v_{i}(y)=\tau_{i}-\tau_{i_{\ell}}$.

Using $\mathcal{A}$ we can already answer $p\mathbin{\mathsf{U}}_{I}q$ for
one-sided intervals: $[0,c],[0,c),[b,+\infty),(b,+\infty)$, for natural
numbers $b,c$.

  * •

if $0\in I$: $\dagger_{1}=\dagger_{3}=1$ (current position is a witness), and
$\dagger_{2}={(-x\in I\lor-y\in I)}\,?\,{1}:{0}$,

  * •

if $0\notin I$: $\dagger_{3}=0$, and $\dagger_{1}=\dagger_{2}={(-x\in
I\lor-y\in I)}\,?\,{1}:{0}$.

This is because in one-sided intervals, if at all there is a witness, the
earliest or the last is one of them.

#### Until with a non-singular interval.

We will now deal with the case of intervals $I=[b,c]$ with $0<b<c<\infty$.
Firstly, using $x$ and $y$, some easy cases of $p\mathbin{\mathsf{U}}_{I}q$
can be deduced. Output remains $0$ for transitions starting from
$\neg(p\mathbin{\mathsf{U}}q)$. For other transitions, here are some extra
checks:

  * •

if $-x\in I$ or $-y\in I$, output $1$ (one of the earliest or last witness is
also a witness for $p\mathbin{\mathsf{U}}_{I}q$),

  * •

else, if $-y<b$ or $c<-x$, output $0$ (the time to the last witness is too
small or the time to the earliest witness is too large, so there is no witness
within $I$).

If neither of the above cases hold, then we need guess a potential witness
within $[b,c]$ and verify it. This requires substantial book-keeping which we
will now explain. Assume we are given a timed word
$w=(a_{0},t_{0})(a_{1},t_{1})\cdots$. Let us a call $j\geq 0$ a _difficult
point_ if:

$\displaystyle w,j\models p\mathbin{\mathsf{U}}q\text{ and
}t_{j_{f}}<t_{j}+b\text{ and }t_{j}+c<t_{j_{\ell}}$

This leaves the possibility for a $q$-witness within $[b,c]$. So, for
difficult points, we need to make a prediction whether we have a $q$-witness
within $[t_{j}+b,t_{j}+c]$: guess a time to a witness within
$[t_{j}+b,t_{j}+c]$ and check it. We cannot keep making such predictions for
every difficult point as we have only finitely many clocks. Therefore, we will
guess some special witnesses. First we state a useful property.

######  Lemma 4.11.

Let $j$ be a difficult point. Then, for all $k$ such that $j\leq k\leq
j_{\ell}$, we have $w,k\models p\mathbin{\mathsf{U}}q$.

Therefore, automaton $\mathcal{A}$ stays in the top two states, while reading
$j$ upto $j_{\ell}$.

[thin, gray] (0,0) – (8.5,0); (0,0) to (0, 0.2); at (0, 0.4) $t_{j}$; (7,0) to
(7, 0.2); at (7, 0.4) $t_{j}+c$; (6,0) to (6, -0.2); [red] (6, 0) circle
(1.5pt); at (6, -0.4) $t_{j^{\prime}}$; (1,0) to (1, -0.2); at (1, -0.4)
$t_{j^{\prime}}-b$; [red] (0,-0.1) to (1,-0.1); (8.4, 0) to (8.4, -0.2);
[blue] (8.4,0) circle (1.5pt); at (8.4, -0.4) $t_{j^{\prime\prime}}$;

[blue] (1.4, 0.1) to (3.4, 0.1); (1.4, 0) to (1.4, 0.2); (3.4,0) to (3.4,
0.2); at (1.4, 0.4) $t_{j^{\prime\prime}}-c$; at (3.4, 0.4)
$t_{j^{\prime\prime}}-b$;

Figure 11: Illustration of a point $j$. The point $j^{\prime}$ is the last
$q$-witness before $t_{j}+c$, and $j^{\prime\prime}$ is the first $q$-witness
after $t_{j}+c$.

We will now come back to the idea of choosing special witnesses. This is
illustrated in Figure 11. For a point $j$, we let $j^{\prime}\geq j$ be the
greatest position containing $q$ such that $t_{j^{\prime}}\leq t_{j}+c$. Let
$j^{\prime\prime}>j$ be the least position containing $q$ such that
$t_{j}+c<t_{j^{\prime\prime}}$. So, no position
$j^{\prime}<k<j^{\prime\prime}$ contains $q$. While reading a difficult point
$j$, let us make use of fresh clocks $x_{1}$ and $y_{1}$ to predict these two
witnesses:

$\displaystyle x_{1}=t_{j}-t_{j^{\prime}}\qquad
y_{1}=t_{j}-t_{j^{\prime\prime}}$

For the next important observation, we will once again take the help of Figure
11. Notice that for all points $i$ with $t_{i}\in[t_{j},t_{j^{\prime}}-b]$,
the point $j^{\prime}$ is also a witness for $w,i\models
p\mathbin{\mathsf{U}}_{[b,c]}q$. Similarly, $j^{\prime\prime}$ is a witness
for all $i$ such that
$t_{i}\in[t_{j^{\prime\prime}}-c,t_{j^{\prime\prime}}-c]$. Therefore for all
$i$ such that $t_{i}\in[t_{j},t_{j^{\prime\prime}}-b]$, we have a way to
determine the output: it is $1$ iff while reading $a_{i}$ we have $-x_{1}\in
I$ or $-y_{1}\in I$ (recall we have predicted $x_{1}$ and $y_{1}$ while
reading $a_{j}$ as explained above). So, we do not have to make new guesses at
the difficult points in $[t_{j},t_{j^{\prime\prime}}-b]$. After
$t_{j^{\prime\prime}}-b$ (which can be identified with the constraint
$-b<y_{1}$), we need to make new such guesses, using fresh clocks, say
$x_{2},y_{2}$. We will call the difficult points where we start new guesses as
_special difficult points_. Notice that the distance between two special
difficult points is at least $c-b$ (which is $\geq 1$, as we consider non-
singular intervals with bounds in $\mathbb{N}$). In the figure, if $j$ is a
special point, a new special point will be opened later than
$t_{j^{\prime\prime}}-b$.

This gives a bound on the number of special points that can be open between
$j$ and $j^{\prime\prime}$. Suppose
$j<\ell_{1}<\ell_{2}<\dots<\ell_{i}<j^{\prime\prime}$ be the sequence of
special points between $j$ and $j^{\prime\prime}$. Since $\ell_{1}$ is opened
when time to $j^{\prime\prime}$ is atmost $b$, we get the inequality:
$t_{\ell_{i}}-t_{\ell_{1}}<b$. Since consecutive special points are at least
$c-b$ apart, we have $(i-1)(c-b)<b$. This entails
$i<1+\lceil\dfrac{b}{c-b}\rceil$. By the time we reach $j^{\prime\prime}$, we
need to have opened at most $k=1+\lceil\dfrac{b}{c-b}\rceil$ special points,
and hence we can work with the extra clocks
$x_{1},y_{1},x_{2},y_{2},\dots,x_{k},y_{k}$.

Figure 12: The automaton for predicting $q$-witnesses which are not given by
the earliest and latest. For clarity, not every transition is indicated. All
clocks are future clocks.

All these ideas culminate in the definition of a book-keeping automaton
$\mathcal{B}$ to handle difficult points. This is shown in Figure 12 for
$N=3$. The automaton $\mathcal{B}$ synchronizes with $\mathcal{A}$ (via a
usual cross-product synchronized on transitions). All transitions of
$\mathcal{B}$ other than the self loop on state $(0,1)$ satisfy $p$.
Transitions which satisfy $q$, and $\neg q$ are specifically marked in the
figure.

The automaton $\mathcal{B}$ starts in the initial state $(0,1)$. It moves to
$(1,1)$ on the first difficult point $j$ (which will become special) and comes
back to $(0,1)$ when there are no active special difficult points waiting for
witnesses (a special difficult point $j$ is active at positions $j\leq i\leq
j^{\prime\prime}$). States $(i,1)$ in the top indicate that there are $i$
active special difficult points currently. A state $(i,2)$ indicates that the
$j^{\prime}$ witness for the oldest active point has been seen, and we are
waiting for its $j^{\prime\prime}$ witness (the space between $t_{j^{\prime}}$
and $t_{j^{\prime\prime}}$ in Figure 11).

The red transitions $(i,*)\to(i+1,*)$ open new special difficult points, and
contain the program as illustrated in the figure. At $(i,1)$, suppose
$\ell_{1}<\ell_{2}<\cdots<\ell_{i}$ are the active special difficult points
where we have predicted $x_{1},y_{1},\dots,x_{i},y_{i}$ respectively. We have
the invariant:

$y_{i}<x_{i}\leq y_{i-1}<x_{i-1}\leq\cdots\leq y_{2}<x_{2}\leq y_{1}<x_{1}$

Notice that we may have $x_{i}=y_{i-1}$: the “first” witness of the $i^{th}$
special point ($\ell_{i}^{\prime}$) could coincide with the “second” witness
of the $(i-1)^{th}$ point ($\ell_{i-1}^{\prime}$). This leads to certain
subtleties, which we will come to later.

The blue transitions read the witness for the oldest active special point
(that is, we have reached $\ell_{1}^{\prime}$). Observe that $x_{1}=0$ does
not immediately identify $\ell_{1}^{\prime}$, since there could be a sequence
of positions at the same time, and $\ell^{\prime}_{1}$ is the last of them.
Therefore, we make a non-deterministic choice whether to take the blue
transition (implying that $\ell^{\prime}_{1}$ has been found), or we remain in
the same state. The blue transitions read a $q$, check $x_{1}=0$, and then
releases $x_{1}$ to $-\infty$ (not shown in Figure 11). The black (diagonal)
transitions witness $\ell^{\prime\prime}_{1}$. When this happens,
$x_{1},y_{1}$ are no longer useful, and therefore all the higher clocks are
shifted using the permutation shift which maps $x_{2},y_{2},\dots
x_{k},y_{k},x_{1},y_{1}$ to $x_{1},y_{1},\dots,x_{k},y_{k}$ and keeps the
other clocks unchanged.

There are some subtleties which arise when special points coincide with
witness points, or when the second witness of a special point coincides with
the first witness of the consecutive special point, which we discuss next.
These subtleties do not increase the states, but they result in more
transitions.

#### Subtleties.

The first subtlety arises when we have
$\ell^{\prime\prime}_{j}=\ell^{\prime}_{j+1}$ for consecutive special points.
This will imply $y_{j}=x_{j+1}$. The reverse direction is not true, as there
could be a sequence of positions with the same time, but let us assume we have
dealt with it by the non-deterministic choice. When we actually witness these
points, the clock values would have shifted to lower indices. This situation
will be manifested as $y_{1}=x_{2}=0$. Suppose we are in $(i,2)$ and see a
point $\ell_{j}^{\prime\prime}$ ($y_{1}=0$). The diagonal transition takes the
automaton to $(i-1,1)$ and shifts $x_{2}$ to $x_{1}$. Now, $x_{1}=0$ (as
$\ell^{\prime}_{j+1}=\ell^{\prime\prime}_{j}$). Therefore, we will have to
combine the black-diagonal-left with the downward-blue to get the combined
effect. This leads to these two divisions:

$\displaystyle(i,2)$ $\displaystyle\xrightarrow{y_{1}=0}(i-1,1)$
$\displaystyle(i,2)$ $\displaystyle\xrightarrow{y_{1}=0\land x_{2}=0}(i-1,2)$

The second subtlety is that one of either $\ell_{j}^{\prime}$ or
$\ell^{\prime\prime}_{j}$ witnesses be a new special point (notice that the
red transitions are independent of the blue and black transitions). In such
cases, we can combine the two effects in any order: first discharge $x_{1}$ or
$y_{1}$ verification, and then open a new special point or vice-versa. This
leads to some additional divisions of the form:

$\displaystyle(i,1)$ $\displaystyle\xrightarrow{x_{1}=0\land-b<y_{i}}(i+1,2)$
$\displaystyle(i,2)$ $\displaystyle\xrightarrow{y_{1}=0\land-b<y_{i}}(i,1)$

In the first transition, we have combined a blue and a red (in any order);
whereas in the second, we have combined a red and a black-diagonal, in any
order.

The third subtlety is that the first and second subtleties may occur together!
A point could be $\ell^{\prime\prime}_{j}$, $\ell^{\prime}_{j+1}$ and also a
new special point. We illustrate this on a specific state $(i,2)$. We provide
only the “guards”. The full program is obtained by suitably combining the
effects of the individual transitions:

$\displaystyle(i,2)$ $\displaystyle\xrightarrow{y_{1}=0\land
y_{i}\leq-b}(i-1,1)$ $\displaystyle(i,2)$
$\displaystyle\xrightarrow{y_{1}=0\land-b<y_{i}}(i,1)$ $\displaystyle(i,2)$
$\displaystyle\xrightarrow{y_{1}=0\land x_{2}=0\land y_{i}\leq-b}(i-1,2)$
$\displaystyle(i,2)$ $\displaystyle\xrightarrow{y_{1}=0\land
x_{2}=0\land-b<y_{i}}(i,2)$

We conclude by giving the full construction of $\mathcal{B}$, taking into
account all these subtleties described above. The set of states is
$\\{0,1,\ldots,N\\}\times\\{1,2\\}$ where $N=1+\lceil\dfrac{b}{c-b}\rceil$
(actually state $(0,2)$ is not reachable). The initial state is $(0,1)$ and
all states are accepting.

#### Final description.

The transitions are described in pseudo-code in Algorithm 1. In comments, we
use the terminology introduced before: difficult point, special difficult
point; and we also refer to the color of transitions in Figure 12.

Parsing the pseudo-code from a current state ($(k,m)$ results in a sequence of
guards and releases, an output of a boolean value (output value), and the next
state (goto $(k^{\prime},m^{\prime})$). The most difficult case is for states
$(k,2)$ with $k\geq 2$, where we could generate transitions to states
$(k-1,1),(k-1,2),(k,1),(k,2),(k+1,2)$.

Algorithm 1 Automaton $\mathcal{B}$ (synchronized with $\mathcal{A}$)

1:State $(0,1)$: $\triangleright$ initial state of $\mathcal{B}$

2: if $\mathcal{A}$ at state $\neg(p\mathbin{\mathsf{U}}q)$ then output 0;
goto (0,1) end if

3: if $-x\in I$ or $-y\in I$ then output 1; goto (0,1) end if

4: if $x<-c$ or $-b<y$ then output 0; goto (0,1) end if

5: Release $[x_{1},y_{1}]$ $\triangleright$ Special difficult point

6: Check $y_{1}<-c\leq x_{1}$

7: output $(x_{1}\leq-b)$ $\triangleright$ boolean value

8: goto (1,1) $\triangleright$ red transition

9:State $(k,1)$ with $k>0$: $\triangleright$ waiting for the event predicted
by $x_{1}$

10: $k^{\prime}\leftarrow k$

11: if $y_{k}\leq-b$ then

12: output $(x_{k}\in I)\vee(y_{k}\in I)$ $\triangleright$ boolean value

13: else

14: if $-c\leq y$ then $\triangleright$ not a difficult point

15: output $(y\leq-b)$ $\triangleright$ boolean value ($y\in I$)

16: else$\triangleright$ new special difficult point, red transition,

17: $\triangleright$ possibly combined with a blue transition below

18: $k^{\prime}\leftarrow k+1$;

19: Release $[x_{k},y_{k}]$; Check $y_{k}<-c\leq x_{k}$

20: output $(x_{k}\leq-b)$ $\triangleright$ boolean value

21: end if

22: end if

23: choose non-deterministically

24: when True do goto $(k^{\prime},1)$ $\triangleright$ not the event
predicted by $x_{1}$

25: when $q\wedge(x_{1}=0)$ do Release $[x_{1}]$; $x_{1}=-\infty$; goto
$(k^{\prime},2)$ $\triangleright$ blue transition

26: end choose

27:State $(k,2)$ with $k>0$: $\triangleright$ waiting for the event predicted
by $y_{1}$

28: $k^{\prime}\leftarrow k$

29: if $y_{k}\leq-b$ then

30: output $(x_{k}\in I)\vee(y_{k}\in I)$ $\triangleright$ boolean value

31: else

32: if $-c\leq y$ then $\triangleright$ not a difficult point

33: output $(y\leq-b)$ $\triangleright$ boolean value ($y\in I$)

34: else$\triangleright$ new special difficult point, red transition,

35: $\triangleright$ possibly combined with a black transition below

36: $k^{\prime}\leftarrow k+1$;

37: Release $[x_{k},y_{k}]$; Check $y_{k}<-c\leq x_{k}$

38: output $(x_{k}\leq-b)$ $\triangleright$ boolean value

39: end if

40: end if

41: if $\neg q$ then $\triangleright$ not the event predicted by $y_{1}$

42: goto $(k^{\prime},2)$

43: else$\triangleright$ event predicted by $y_{1}$, black transition

44: $\triangleright$ possibly combined with a blue transition below

45: Check $y_{1}=0$; Release $[y_{1}]$; $y_{1}=-\infty$

46: if $k^{\prime}=1$ then

47: goto $(0,1)$

48: else

49: Shift $x_{2},y_{2},\ldots,x_{k},y_{k},x_{1},y_{1}$ to
$x_{1},y_{1},\ldots,x_{k},y_{k}$

50: end if

51: choose non-deterministically

52: when True do goto $(k^{\prime}-1,1)$ $\triangleright$ not the event
predicted by the new $x_{1}$

53: when $(x_{1}=0)$ do $Release[x_{1}]$; $x_{1}=-\infty$; goto
$(k^{\prime}-1,2)$ $\triangleright$ blue transition

54: end choose

55: end if

This concludes the description of the automaton $\mathcal{B}$. The product
$\mathcal{A}\times\mathcal{B}$ gives the required transducer for
$p\mathbin{\mathsf{U}}_{I}q$.

#### Complexity and comparison with the MightyL approach.

The final automaton $\mathcal{A}\times\mathcal{B}$ has at most $6k$ states,
where $k=1+\lceil\dfrac{b}{c-b}\rceil$ as defined above: automaton
$\mathcal{A}$ has 3 states, and automaton $\mathcal{B}$ has $2k-1$ states (see
Figure 12). In terms of clocks, $\mathcal{A}$ has 2 future clocks $x,y$, and
$\mathcal{B}$ has $2k$ future clocks $x_{1},y_{1},\dots,x_{k},y_{k}$. We have
used a permutation operation shift. As we mention in Remark 2.2, renamings can
be eliminated by maintaining in the current state the composition of
permutations applied since the initial state. Since each permutation does a
cyclic shift, in any composition, the clocks $x_{1},y_{1},\dots,x_{k},y_{k}$
are renamed to some
$x_{i},y_{i},\dots,x_{k},y_{k},x_{1},y_{1},\dots,x_{i-1},y_{i-1}$. Therefore,
there are at most $k$ renamings. Maintaining them in states gives rise to
atmost $\mathcal{O}(k^{2})$ states.

In contrast, the state-of-the-art approach [11] starts with a 1-clock
alternating timed automata for $\mathbin{\mathsf{U}}_{I}$. After reading a
timed word, the 1-ATA reaches a configuration containing several state-
valuation pairs $(q,v)$. A finite abstraction of this set of configurations,
called the interval semantics, has been proposed [9, 10, 11]. This abstraction
is maintained in the states. Overall, the number of locations for
$p\mathbin{\mathsf{U}}_{I}q$ is exponential in $k$, and the number of clocks
is $2k+2$.

Due to the presence of future clocks, we are able to make predictions, as in
Figure 11 and the GTA syntax enables concisely checking these predictions in
the transitions. Therefore, we are able to give a direct construction to the
final automaton, instead of going via an alternating automaton and then
abstracting it.

##  5 Conclusion

In this paper, we have answered two problems: (1) liveness of GTA and (2) MITL
model checking using GTA. The solution to the first problem required to bypass
the technical difficulty of having no finite time-abstract bisimulation for
GTAs. The presence of diagonal constraints adds additional challenges. For
MITL model checking using GTA, we have described the GTA for the
$\mathop{\mathsf{X}\vphantom{a}}\nolimits_{I}$ and $\mathbin{\mathsf{U}}_{I}$
modalities. Indeed, the presence of future clocks allows to make predictions
better and we see an exponential gain over the state-of-the-art, in the number
of states of the final automaton produced. Moreover, our construction is
direct, without having to go via alternation.

The next logical step would be to implement these ideas and see how they
perform in practice, and compare them with existing well-engineered tools
(e.g., [11]). This will require a considerable implementation effort, needing
several optimizations and incorporating of many practical considerations
before it can become scalable. This provides tremendous scope for future work
on these lines.

## References

  * [1] S. Akshay, Paul Gastin, R. Govind, Aniruddha R. Joshi, and B. Srivathsan.  A unified model for real-time systems: Symbolic techniques and implementation.  In CAV (1), volume 13964 of Lecture Notes in Computer Science, pages 266–288. Springer, 2023.
  * [2] Rajeev Alur and David L. Dill.  A theory of timed automata.  Theoretical Computer Science, 126:183–235, 1994.
  * [3] Rajeev Alur, Tomás Feder, and Thomas A. Henzinger.  The benefits of relaxing punctuality.  J. ACM, 43(1):116–146, 1996.
  * [4] Rajeev Alur, Limor Fix, and Thomas A. Henzinger.  Event-clock automata: A determinizable class of timed automata.  Theor. Comput. Sci., 211(1-2):253–273, 1999.
  * [5] Rajeev Alur and Thomas A. Henzinger.  Real-time logics: Complexity and expressiveness.  In LICS, pages 390–401. IEEE Computer Society, 1990.
  * [6] Gerd Behrmann, Patricia Bouyer, Kim G. Larsen, and Radek Pelánek.  Lower and upper bounds in zone-based abstractions of timed automata.  International Journal on Software Tools for Technology Transfer, 8(3):204–215, 2006.
  * [7] Johan Bengtsson and Wang Yi.  Timed automata: Semantics, algorithms and tools.  In ACPN 2003, volume 3098 of Lecture Notes in Computer Science, pages 87–124. Springer, 2003.
  * [8] Laura Bozzelli, Angelo Montanari, and Adriano Peron.  Complexity issues for timeline-based planning over dense time under future and minimal semantics.  Theor. Comput. Sci., 901:87–113, 2022.
  * [9] Thomas Brihaye, Morgane Estiévenart, and Gilles Geeraerts.  On MITL and alternating timed automata.  In FORMATS, volume 8053 of Lecture Notes in Computer Science, pages 47–61. Springer, 2013.
  * [10] Thomas Brihaye, Morgane Estiévenart, and Gilles Geeraerts.  On MITL and alternating timed automata over infinite words.  In FORMATS, volume 8711 of Lecture Notes in Computer Science, pages 69–84. Springer, 2014.
  * [11] Thomas Brihaye, Gilles Geeraerts, Hsi-Ming Ho, and Benjamin Monmege.  Mightyl: A compositional translation from MITL to timed automata.  In CAV (1), volume 10426 of Lecture Notes in Computer Science, pages 421–440. Springer, 2017.
  * [12] Olivier Carton and Max Michel.  Unambiguous büchi automata.  Theor. Comput. Sci., 297(1-3):37–81, 2003.
  * [13] Alessandro Cimatti, Edmund M. Clarke, Fausto Giunchiglia, and Marco Roveri.  NUSMV: A new symbolic model verifier.  In CAV, volume 1633 of Lecture Notes in Computer Science, pages 495–499. Springer, 1999.
  * [14] Conrado Daws and Stavros Tripakis.  Model checking of real-time reachability properties using abstractions.  In TACAS, volume 1384 of Lecture Notes in Computer Science, pages 313–329. Springer, 1998.
  * [15] David L. Dill.  Timing assumptions and verification of finite-state concurrent systems.  In Automatic Verification Methods for Finite State Systems, volume 407 of Lecture Notes in Computer Science, pages 197–212. Springer, 1989.
  * [16] Alexandre Duret-Lutz, Alexandre Lewkowicz, Amaury Fauchille, Thibaud Michaud, Etienne Renault, and Laurent Xu.  Spot 2.0 - A framework for LTL and $\omega$-automata manipulation.  In ATVA, volume 9938 of Lecture Notes in Computer Science, pages 122–129, 2016.
  * [17] Thomas Ferrère, Oded Maler, Dejan Nickovic, and Amir Pnueli.  From real-time logic to timed automata.  J. ACM, 66(3):19:1–19:31, 2019.
  * [18] Paul Gastin, Sayan Mukherjee, and B. Srivathsan.  Reachability in timed automata with diagonal constraints.  In CONCUR, volume 118 of LIPIcs, pages 28:1–28:17. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2018.
  * [19] Paul Gastin, Sayan Mukherjee, and B. Srivathsan.  Fast algorithms for handling diagonal constraints in timed automata.  In CAV (1), volume 11561 of Lecture Notes in Computer Science, pages 41–59. Springer, 2019.
  * [20] Paul Gastin and Denis Oddoux.  Fast LTL to büchi automata translation.  In CAV, volume 2102 of Lecture Notes in Computer Science, pages 53–65. Springer, 2001.
  * [21] Gilles Geeraerts, Jean-François Raskin, and Nathalie Sznajder.  On regions and zones for event-clock automata.  Formal Methods Syst. Des., 45(3):330–380, 2014.
  * [22] Rob Gerth, Doron A. Peled, Moshe Y. Vardi, and Pierre Wolper.  Simple on-the-fly automatic verification of linear temporal logic.  In PSTV, volume 38 of IFIP Conference Proceedings, pages 3–18. Chapman & Hall, 1995.
  * [23] F. Herbreteau and G. Point.  TChecker.  https://github.com/fredher/tchecker, v0.2 - April 2019.
  * [24] Frédéric Herbreteau, B. Srivathsan, Thanh-Tung Tran, and Igor Walukiewicz.  Why liveness for timed automata is hard, and what we can do about it.  ACM Trans. Comput. Log., 21(3):17:1–17:28, 2020.  doi:10.1145/3372310.
  * [25] Frédéric Herbreteau, B. Srivathsan, and Igor Walukiewicz.  Better abstractions for timed automata.  In LICS, pages 375–384. IEEE Computer Society, 2012.
  * [26] Frédéric Herbreteau, B. Srivathsan, and Igor Walukiewicz.  Efficient emptiness check for timed büchi automata.  Formal Methods Syst. Des., 40(2):122–146, 2012.
  * [27] Gerard J. Holzmann.  The model checker SPIN.  IEEE Trans. Software Eng., 23(5):279–295, 1997.
  * [28] Henrik Ejersbo Jensen, Kim G. Larsen, and Arne Skou.  Modelling and analysis of a collision avoidance protocol using spin and uppaal.  In The Spin Verification System, volume 32 of DIMACS Series in Discrete Mathematics and Theoretical Computer Science, pages 33–49. DIMACS/AMS, 1996.
  * [29] Leslie Lamport.  Specifying Systems, The TLA+ Language and Tools for Hardware and Software Engineers.  Addison-Wesley, 2002.
  * [30] Guangyuan Li.  Checking timed büchi automata emptiness using lu-abstractions.  In Joël Ouaknine and Frits W. Vaandrager, editors, Formal Modeling and Analysis of Timed Systems, 7th International Conference, FORMATS 2009, Budapest, Hungary, September 14-16, 2009. Proceedings, volume 5813 of Lecture Notes in Computer Science, pages 228–242. Springer, 2009.  doi:10.1007/978-3-642-04368-0\\_18.
  * [31] Oded Maler, Dejan Nickovic, and Amir Pnueli.  From MITL to timed automata.  In FORMATS, volume 4202 of Lecture Notes in Computer Science, pages 274–289. Springer, 2006.
  * [32] Philipp J. Meyer, Salomon Sickert, and Michael Luttenberger.  Strix: Explicit reactive synthesis strikes back!  In CAV (1), volume 10981 of Lecture Notes in Computer Science, pages 578–586. Springer, 2018.
  * [33] Joël Ouaknine and James Worrell.  On metric temporal logic and faulty turing machines.  In FoSSaCS, volume 3921 of Lecture Notes in Computer Science, pages 217–230. Springer, 2006.
  * [34] Amir Pnueli.  The temporal logic of programs.  In FOCS, pages 46–57. IEEE Computer Society, 1977.
  * [35] Amir Pnueli.  Applications of temporal logic to the specification and verification of reactive systems: A survey of current trends.  In Current Trends in Concurrency, volume 224 of Lecture Notes in Computer Science, pages 510–584. Springer, 1986.
  * [36] Amir Pnueli and Eyal Harel.  Applications of temporal logic to the specification of real-time systems.  In FTRTFT, volume 331 of Lecture Notes in Computer Science, pages 84–98. Springer, 1988.
  * [37] Stavros Tripakis, Sergio Yovine, and Ahmed Bouajjani.  Checking timed büchi automata emptiness efficiently.  Formal Methods Syst. Des., 26(3):267–292, 2005.
  * [38] Moshe Y Vardi.  An automata-theoretic approach to linear temporal logic.  Lecture Notes in Computer Science, 1043:238–266, 1996.
  * [39] Thomas Wilke.  Specifying timed state sequences in powerful decidable logics and timed automata.  In FTRTFT, volume 863 of Lecture Notes in Computer Science, pages 694–715. Springer, 1994.