\item[$\dagger_{4}$] Either $Z_{0\prophecy{x}}=(\leq,-\infty)$ or
$(<,-M)\leq Z_{0\prophecy{x}}\leq(\leq,0)$.

\item[$\dagger_{5}$] Either $Z_{0\prophecy{y}}=(\leq,-\infty)$
or $Z_{x0} + (<,-M) \leq Z_{x\prophecy{y}}$ for all $x\in X$ with $x\neq\prophecy{y}$.

\item[$\dagger_{6}$] Either
or $(<,-M) \leq Z_{\prophecy{x}\prophecy{y}} \leq (\leq,M)$.
\end{enumerate}
\end{lemma}

\begin{proof}
\begin{enumerate}
\item[$\dagger_{1}$] Assume that $Z_{\prophecy{x}0}=(<,\infty)$ and let $y\neq\prophecy{x}$.
Consider first the case $Z_{0y}=(\leq,-\infty)$, i.e., $y$ is a prophecy clock which
is undefined in $Z$.  Then, since $\graph{Z}$ is in normal form, we have
$Z_{\prophecy{x}y}\leq Z_{\prophecy{x}0}+Z_{0y}=(<,\infty)+(\leq,-\infty)=(\leq-\infty)$.

The second case is when $Z_{0y}\neq(\leq,-\infty)$.
This implies $Z_{\prophecy{x}y}\neq(\leq,-\infty)$ since otherwise we would get $Z_{0y}\leq
We claim that there is a valuation $v\in Z$ with $-\infty<v(y)$ and

Consider the distance graph $\GG'$ obtained from $\graph{Z}$ by setting the weight of
edge $y\to 0$ to $\min(Z_{y0},(<,\infty))$ and of edge $0\to\prophecy{x}$ to
$\min(Z_{0\prophecy{x}},(<,-M))$.  Notice that $\GG'$ is in standard form.
We show that $\GG'$ has no negative cycles.
Since $\graph{Z}$ is in normal form,
the candidates for being negative must use the new weight
$(<,-M)$ of $0\to\prophecy{x}$ or the new weight $(<,\infty)$ of $y\to 0$ or both. This
gives the cycle $0\to\prophecy{x}\to 0$ with weight $(<,-M)+Z_{\prophecy{x}0}=(<,\infty)$,
the cycle $0 \to y \to 0$ with weight $Z_{0y}+(<,\infty)$ which is not negative since
$Z_{0y}\neq(\leq,-\infty)$, and the cycle $y \to 0 \to \prophecy{x} \to y$ with weight
which is not negative since $Z_{\prophecy{x}y}\neq(\le,-\infty)$.
Since $\GG'$ is standard and has no negative cycle,
Lemma~\ref{lem:empty-iff-negative-cycle} implies $\sem{\GG'}\neq\emptyset$.  Note that
$\sem{\GG'}\subseteq\sem{\graph{Z}}=Z$.  Finally, $-\infty<v(y)$ and
$-\infty<v(\prophecy{x})<-M$ for all $v\in\GG'$, which proves the claim.

By Lemma~\ref{lem:reachable-zones-prophecy-clocks},
$v_{\alpha}=v[\prophecy{x}\mapsto\alpha]\in Z$ for all $-\infty<\alpha<-M$.  Now,
$v_{\alpha}(y)-v_{\alpha}(\prophecy{x})=v(y)-\alpha$ satisfies the constraint
$Z_{\prophecy{x}y}$.  We deduce that $Z_{\prophecy{x}y}$ is either $(<,\infty)$ or

\item[$\dagger_{2}$]  Suppose $(\leq,M)<Z_{\prophecy{x}0}<(<,\infty)$.  By
Lemma~\ref{lem:weight-properties}, we find $\alpha$ such that $(\leq,\alpha)\leq
Z_{\prophecy{x}0}$, $(\leq,-\alpha)\leq Z_{0\prophecy{x}}$ and $\alpha\not\leq M$.  Now, by
Lemma~\ref{lem:fixing-values-distance-graph}, we find $v\in Z$ with
By Lemma~\ref{lem:reachable-zones-prophecy-clocks},
$v[\prophecy{x}\mapsto\alpha]\in Z$ for all $-\infty < \alpha < -M$, a contradiction with
$Z_{\prophecy{x}0}$ finite.

\item[$\dagger_{3}$] Assume $Z_{\prophecy{x}\history{y}}<(<,\infty)$ is finite. Since
$\graph{Z}$ is standard, we get $Z_{\prophecy{x}0}\neq(\leq,\infty)$. Now, $\dagger_{1}$
implies $Z_{\prophecy{x}0}<(<,\infty)$. We conclude with $\dagger_{2}$.

\item[$\dagger_{4}$]
The proof is similar to $\dagger_{2}$. Suppose $(\leq,-\infty)<Z_{0\prophecy{x}}<(<,-M)$.  By
Lemma~\ref{lem:weight-properties}, we find $\alpha$ such that $(\leq,\alpha)\leq
Z_{0\prophecy{x}}$, $(\leq,-\alpha)\leq Z_{\prophecy{x}0}$ and $\alpha\neq-\infty$.  Now, by
Lemma~\ref{lem:fixing-values-distance-graph}, we find $v\in Z$ with
$-\infty<v(\prophecy{x})=-\alpha<-M$. Since $Z_{0\prophecy{x}}<(<,-M)$, we can
find $-\infty\neq\beta<-M$ such that $Z_{0\prophecy{x}}<(\leq,\beta)$. Now,
Lemma~\ref{lem:reachable-zones-prophecy-clocks} implies that
$v[\prophecy{x}\mapsto\beta]\in Z$, which is a contradiction with

\item[$\dagger_5$]  Suppose $Z_{0\prophecy{y}}\neq(\leq,-\infty)$.
If $Z_{x0}=(\leq,-\infty)$ or $Z_{x\prophecy{y}}=(\leq,\infty)$, the condition is
trivially true. So we also assume in the following that $Z_{x0}\neq(\leq,-\infty)$
and $Z_{x\prophecy{y}}\neq(\leq,\infty)$. Since $\graph{Z}$ is in standard form, we get
$Z_{x0}\neq(\leq,\infty)$. By Lemma~\ref{lem:reachable-properties}, we also have

Consider the distance graph $\GG'$ obtained from the canonical graph $\graph{Z}$ by
setting $\GG'_{0x}=\min(Z_{0x},(<,\infty))$,
$\GG'_{\prophecy{y}0}=\min(Z_{\prophecy{y}0},(<,\infty))$, and keeping other weights unchanged.
The graph $\GG'$ is in standard form. Moreover, it has no negative cycles. Indeed,
since $\graph{Z}$ is in normal form, the new cycles that we have to check in $\GG'$
are $0\to x\to 0$, $0\to\prophecy{y}\to 0$ and $\prophecy{y}\to 0\to x\to \prophecy{y}$.
Since $Z_{x0}\neq(\leq,-\infty)$, $Z_{0\prophecy{y}}\neq(\leq,-\infty)$ and
$Z_{x\prophecy{y}}\neq(\leq,-\infty)$, these cycles are non-negative.
Let $\GG''$ be the normalization of $\GG'$.  Since $Z_{x0}\neq(\leq,\infty)$, we have
$\GG''_{x0}=\GG'_{x0}=Z_{x0}$.  Notice that $\GG''\leq\GG'\leq\graph{Z}$, hence
$\sem{\GG''}\subseteq\sem{\GG'}\subseteq Z$.

We claim that for all $\varepsilon>0$ and all $c\in\mathbb{R}$ with $(\leq,c)<Z_{x0}$
we have $(\leq,c-M-\varepsilon)<Z_{x\prophecy{y}}$.  Indeed, if
$(\leq,c)<Z_{x0}=\GG''_{x0}$ then by Lemma~\ref{lem:weight-properties} we find
$\alpha$ such that $(\leq,\alpha)\leq\GG''_{x0}$, $(\leq,-\alpha)\leq\GG''_{0x}$ and
$c<\alpha$.  Next, by Lemma~\ref{lem:fixing-values-distance-graph}, we find
$v\in\sem{\GG''}\subseteq Z$ such that $v(x)=-\alpha$.  If $v(\prophecy{y})<-M$ then by
Lemma~\ref{lem:reachable-zones-prophecy-clocks} we get
$v'=v[\prophecy{y}\mapsto-M-\varepsilon]\in Z$. Otherwise, we let $v'=v$. We have
$c-M-\varepsilon<\alpha-M-\varepsilon\leq v'(\prophecy{y})-v'(x)$. We obtain
$(\leq,c-M-\varepsilon)<(\leq,v'(\prophecy{y})-v'(x))\leq Z_{x\prophecy{y}}$ and the claim is

Finally, if $Z_{x0}=(<,\infty)$ then we may take $c$ arbitrarily large and the claim
implies $(<,\infty)\leq Z_{x\prophecy{y}}$.  Otherwise, $Z_{x0}=(\leqlt,d)$ is finite and
taking $c=d-\varepsilon$ we obtain $(\leq,d-M-2\varepsilon)<Z_{x\prophecy{y}}$ for all
$\varepsilon>0$. This implies $Z_{x0}+(<,-M)=(<,d-M)\leq Z_{x\prophecy{y}}$.

\item[$\dagger_{6}$] Assume that
Since $\graph{Z}$ is in standard form, we have $Z_{\prophecy{x}0}\neq(\leq,\infty)$.
Now, $(\leq,-\infty)\neq Z_{\prophecy{x}\prophecy{y}}\leq
Z_{\prophecy{x}0}+Z_{0\prophecy{y}}$ implies that
Next, since $Z_{0 \prophecy{y}}\neq(\leq,-\infty)$ and
$Z_{\prophecy{x}\prophecy{y}}\notin\{(<,\infty),(\leq,\infty)\}$, by
$\dagger_{1}$ we deduce that $Z_{\prophecy{x}0}\neq(<,\infty)$.

Applying $\dagger_5$, we deduce that
$(<,-M)\leq Z_{\prophecy{x}0}+(<,-M)\leq Z_{\prophecy{x}\prophecy{y}}$.

Finally, $Z_{\prophecy{x}\prophecy{y}}\leq Z_{\prophecy{x}0}+Z_{0\prophecy{y}}\leq
Z_{\prophecy{x}0}\leq(\leq,M)$ by $\dagger_{2}$.
\qedhere
\end{enumerate}
\end{proof}

We now see that the $(\dagger)$ conditions imply that the weight of edges of the form $0 \to \prophecy{x}$, $\prophecy{x} \to 0$ and $\prophecy{x} \to \prophecy{y}$ belong to the finite set
\{(\leq,-\infty),(<,\infty),(\leq,\infty)\}\cup \{(\leqlt,c)\mid
c\in\mathbb{Z} \wedge -M\leq c\leq M\} \,.
For an example, see Figure~\ref{fig:eca-zone-graph-ex-2}.  Thus, we obtain as a corollary
that, for event-predicting automata (EPA), we do not even need simulation to obtain

\begin{corollary}
Let $\A$ be an EPA. The zone graph $\ezg(\A)$ is finite.
\end{corollary}

\begin{figure}[!h]
\centering
\begin{subfigure}[b]{\textwidth}
\centering
\begin{tikzpicture}
[state/.style={draw, thick, circle, inner sep=4pt}]
\begin{scope}[xshift=1cm, yshift=0cm]
\begin{scope}[every node/.style={state}]
\node (q0) at (4, 3) {\scriptsize $q_0$};
\node (q1) at (6, 3) {\scriptsize $q_1$};
\node (q2) at (8, 3) {\scriptsize $q_2$};
\end{scope}

\begin{scope}[->, >=stealth, thick]
\draw (3.25, 3) to (q0);
\draw (q0) to [out=120,in=60,looseness=8] (q0);
\draw (q2) to [out=120,in=60,looseness=8] (q2);
\draw (q0) to (q1);
\draw (q1) to (q2);
\draw (q2) to (8.75,3);
\end{scope}

\node at (6, 2) {\footnotesize $\Aa_2$};

\node at (4, 4.6) {\footnotesize $b$};
\node at (4, 4.25) {\scriptsize $\prophecy{b}=-1 \wedge \prophecy{a}<-1$};
\node at (5, 3.25) {\footnotesize $b$};
\node at (5, 2.75) {\scriptsize $\prophecy{a}=-1$};

\node at (7, 3.25) {\footnotesize $a$};

\node at (8, 4.25) {\footnotesize $d$};
\end{scope}

\begin{scope}[xshift=0cm, yshift=0cm, zone/.style={draw,rectangle,minimum width=2.3cm, minimum height=2cm, rounded corners}]
\node [zone] (z0) at (1, 0) {};
\node [zone] (z1) at (1, 3) {};
\node [zone] (z2) at (4.5, 0) {};
\node [zone] (z3) at (8, 0) {};
\end{scope}

\begin{scope}[->, >=stealth, thick]
\draw (-1,0) to (z0);
\draw (z0) to (z1);
\draw (z0) to (z2);
\draw (z1) to (z2);
\draw (z2) to (z3);
\draw (z1) to [out=120,in=180,looseness=4] (z1);
\draw (z3) to [out=55,in=30,looseness=4] (z3);
\draw (z3) to (10,0);
\end{scope}

\node at (0.25, 0) {\footnotesize $q_0$};
\node at (1.2, 0.5) {\scriptsize $\prophecy{a} \leq 0$};
\node at (1.2, 0) {\scriptsize $\prophecy{b} \leq 0$};
\node at (1.2, -0.5) {\scriptsize $\prophecy{d} \leq 0$};

\node at (0.2, 3) {\footnotesize $q_0$};
\node at (1.2, 3.7) {\scriptsize $-1 \leq \prophecy{b} \leq 0$};
\node at (1.2, 3.2) {\scriptsize $\prophecy{a} - \prophecy{b} < 0$};
\node at (1.2, 2.7) {\scriptsize $\prophecy{d} - \prophecy{b} \leq 1$};
\node at (1.2, 2.2) {\scriptsize $\prophecy{a} < 0, ~ \prophecy{d} \leq 0 $};

\node at (3.6, 0) {\footnotesize $q_1$};
\node at (4.7, 0.75) {\scriptsize $-1 \leq \prophecy{a} \leq 0$};
\node at (4.7, 0.25) {\scriptsize $\prophecy{b} - \prophecy{a} \leq 1$};
\node at (4.7, -0.25) {\scriptsize $\prophecy{d} - \prophecy{a} \leq 1$};
\node at (4.7, -0.75) {\scriptsize $\prophecy{b} \leq 0, ~ \prophecy{d} \leq 0 $};

\node at (7.3, 0) {\footnotesize $q_2$};
\node at (8.2, 0.5) {\scriptsize $\prophecy{a} \leq 0$};
\node at (8.2, 0) {\scriptsize $\prophecy{b} \leq 0$};
\node at (8.2, -0.5) {\scriptsize $\prophecy{d} \leq 0$};

\node at (1.25, 1.5) {\footnotesize $b$};
\node at (0.2, 1.65) {\scriptsize $\prophecy{b}=-1~\wedge$};
\node at (0.2, 1.35) {\scriptsize $\prophecy{a}<-1$};

\node at (-1, 4.25) {\footnotesize $b$};
\node at (-1, 4.75) {\scriptsize $\prophecy{b}=-1 \wedge \prophecy{a}<-1$};

\node at (2.75, 0.25) {\footnotesize $b$};
\node at (2.75, -0.25) {\scriptsize $\prophecy{a}=-1$};

\node at (2.5, 1.5) {\footnotesize $b$};
\node at (3.2, 1.75) {\scriptsize $\prophecy{a}=-1$};

\node at (6.25, 0.25) {\footnotesize $a$};
\node at (9.6, 1.5) {\footnotesize $d$};
\end{tikzpicture}
\end{subfigure}
\caption[]{Event-\emph{predicting} automaton $\A_2$, for which there exists no finite
time abstract bisimulation on valuations, and its (finite) event zone graph $\ezg(\A_{2})$.
\label{fig:eca-zone-graph-ex-2}
\end{figure}

Thus, for EPA, one could simply construct the event-zone graph
without simulations to solve the reachability problem: more
precisely, the reachability algorithm of
Definition~\ref{def:reach-algo} can be modified by taking equality
$=$ instead of simulation $\preceq$. At the same time, notice that
in the definition of $v \preceq_G v'$, we have $v(\prophecy{a}) =
v'(\prophecy{a})$ for prophecy clocks. Therefore, for EPA, the check
$v \preceq_G v'$ boils down to $v = v'$ and the check $Z \preceq_G
Z'$ amounts to checking $Z \incl Z'$, an inclusion between

We can also see that Theorem~\ref{thm:simulation-check}
when restricted to prophecy clocks boils down to mere inclusion. We
provide a short explanation for this fact. The first two conditions
of Theorem simply
check ~\ref{thm:simulation-check} $Z'_{x0} < Z_{x0}$ and $Z'_{0y} <
Z_{0y}$ when there are only prophecy clocks. In the third
condition, it remains to show that the extra
tests (1) $(\le, 0) \le Z_{x0} + (\leqlt_1, c)$ and (2) $Z'_{xy} +
(\leqlt_2, -d) < Z_{x0}$ are true whenever $Z'_{xy} < Z_{xy}$, and
$x, y$ are prophecy clocks. So
there is no need to check the extra conditions separately.

When $x$ and $y$ are prophecy clocks, we have $x \le 0$
and $0 \le y$ in $G$. By definition of standard form, we have $(\le,
0) \le Z_{x0}$. This automatically gives (1). For (2), since
$Z'_{xy} < Z_{xy}$ and $Z_{xy} \le Z_{x0} + Z_{0y}$, we have
$Z'_{xy} < Z_{x0} + Z_{0y}$. But $Z_{0y} \le (\le, 0)$ since $\GG(Z)$ is
in standard form. Therefore, we deduce $Z_{xy} \le Z'_{x0}$.

For general ECA, i.e., when we have both history and prophecy clocks, we need to make sure
that the finiteness of the simulation that we do for handling history clocks does not get
affected in the presence of prophecy clocks.  We turn to this issue in the next section.

\subsection{An equivalence relation of finite index on valuations}
\label{sec:eqreln}

We define an equivalence relation of finite index
$\sim_{M}$ on valuations.
First, we define $\sim_{M}$ on
by $\alpha\sim_{M}\beta$ if
$(\alpha\leqlt c \Longleftrightarrow \beta\leqlt c)$ for all
$(\leqlt,c)$ with ${\leqlt}\in\{<,\leq\}$ and
$c\in\{-\infty,\infty\}\cup\{d\in\mathbb{Z}\mid|d|\leq M\}$.  In
particular, if $\alpha\sim_{M}\beta$ then
$(\alpha=-\infty \Longleftrightarrow \beta=-\infty)$ and
$(\alpha=\infty \Longleftrightarrow \beta=\infty)$.

Next, for valuations $v_{1},v_{2}\in\V$, we define
$v_{1}\sim_{M}v_{2}$ by two conditions: $v_{1}(x)\sim_{M}v_{2}(x)$ and
$v_{1}(x)-v_{1}(y)\sim_{2M}v_{2}(x)-v_{2}(y)$ for all clocks
$x,y\in X$. Notice that we use $2M$ for differences of values.
Clearly, $\sim_{M}$ is an equivalence relation of finite index on

The next result relates the equivalence relation $\sim_{M}$ and the simulation relation
$\preceq_{G}$ when the finite constants used in the constraints are bounded by $M$.
Recall from Section~\ref{sec:distance graph for up G v} the definition of the distance
graph $\graphv{G}{v}$ for the set of valuations $\ua_{G}v$.

\begin{lemma}\label{lem:sim_M and graphv}
Let $v_{1},v_{2}\in\V$ be valuations with $v_{1}\sim_{M}v_{2}$ and
let $G$ be a set of atomic constraints using constants in
$\{-\infty,\infty\}\cup\{c\in\mathbb{Z}\mid|c|\leq M\}$.  By
replacing the weights $(\leq,v_{1}(x))$ (resp.\ $(\leq,-v_{1}(x))$)
by $(\leq,v_{2}(x))$ (resp.\ $(\leq,-v_{2}(x))$) in the graph
$\graphv{G}{v_{1}}$ we obtain the graph $\graphv{G}{v_{2}}$.
\end{lemma}

\begin{proof}
This is clear by definition for edges $\prophecy{x}\to 0$ and
$0\to\prophecy{x}$ adjacent to a prophecy clock. We consider now edges
adjacent to history clocks $\history{x}$.
\begin{itemize}
\item Consider the edge $0\to\history{x}$.
\begin{itemize}
\item If its weight is $(\leq,v_{1}(\history{x}))$ in
$\graphv{G}{v_{1}}$ then there is some $\history{x}\leqlt c\in G$
with $(\leqlt,c)<(<,\infty)$ and $v_{1}(\history{x})\leqlt c$.
Since $v_{1}\sim_{M}v_{2}$ we deduce that
$v_{2}(\history{x})\leqlt c$ and the edge $0\to\history{x}$ has weight
$(\leq,v_{2}(\history{x}))$ in $\graphv{G}{v_{2}}$.

\item If its weight is $(<,\infty)$ in $\graphv{G}{v_{1}}$ then we
are not in the case above and $\history{x}<\infty \in G$,
$v_{1}(\history{x})<\infty$.  Since $v_{1}\sim_{M}v_{2}$ we deduce
that $v_{2}(\history{x})<\infty$ and the edge $0\to\history{x}$ has
weight $(<,\infty)$ in $\graphv{G}{v_{2}}$.

\item Otherwise, the weight is $(\leq,\infty)$ in both
$\graphv{G}{v_{1}}$ and $\graphv{G}{v_{2}}$.
\end{itemize}

\item Consider the edge $\history{x}\to 0$.
\begin{itemize}
\item If its weight is $(\leq,-\infty)$ in $\graphv{G}{v_{1}}$
then $\infty\leq\history{x} \in G$ and $v_{1}(\history{x})=\infty$.
Since $v_{1}\sim_{M}v_{2}$ we deduce that
$v_{2}(\history{x})=\infty$ and the edge $\history{x}\to0$ has weight
$(\leq,-\infty)$ in $\graphv{G}{v_{2}}$.

\item If its weight is $(\leqlt,-c)$ in $\graphv{G}{v_{1}}$ then
we are not in the case above and there is some
$c\leqlt\history{x}\in G$ with $(c,\leqlt)<(\infty,\leq)$ and
$c\leqlt v_{1}(\history{x})$.  Since $v_{1}\sim_{M}v_{2}$ we deduce
that $c\leqlt v_{2}(\history{x})$ and the edge $\history{x}\to0$ has
weight $(\leqlt,-c)$ in $\graphv{G}{v_{2}}$.

\item If its weight is $(\leq,-v_{1}(\history{x}))$ in
$\graphv{G}{v_{1}}$ then we are not in the cases above and there
is some $c\leqlt\history{x}\in G$ with $(c,\leqlt)<(\infty,\leq)$
and $c\not\leqlt v(\history{x})$, Since $v_{1}\sim_{M}v_{2}$ we
deduce that $c\not\leqlt v_{2}(\history{x})$ and the edge
$\history{x}\to0$ has weight $(\leq,-v_{2}(\history{x}))$ in

\item Otherwise, the weight is $(\leq,0)$ in both
$\graphv{G}{v_{1}}$ and $\graphv{G}{v_{2}}$.  \qedhere
\end{itemize}
\end{itemize}
\end{proof}

Next we state the central lemma that says that $\da_{G}Z$ is a union of $\sim_{M}$
equivalence classes.

\begin{lemma}\label{lem:sim_M main property}
Let $v_{1},v_{2}\in\V$ be valuations with $v_{1}\sim_{M}v_{2}$ and
let $G$ be a set of atomic constraints using constants in
$\{-\infty,\infty\}\cup\{c\in\mathbb{Z}\mid|c|\leq M\}$.
Let $Z$ be a zone with a canonical distance graph $\graph{Z}$ satisfying
$(\dagger)$.  Then,
$v_{1}\in\da_{G}Z$ iff $v_{2}\in\da_{G}Z$.
\end{lemma}

\begin{proof}
Notice that $v\in\da_{G}Z$ iff $\ua_{G}v\cap Z\neq\emptyset$.
The proof is by contradiction.
We assume that $\ua_{G}v_{1}\cap Z\neq\emptyset$ and
$\ua_{G}v_{2}\cap Z=\emptyset$.  By Lemma~\ref{lem:negative-cycles-v-Z}
we find a negative cycle $C_{2}$ using one edge from
$\graph{Z}$ and one or two edges from $\graphv{G}{v_{2}}$.  By
Lemma~\ref{lem:sim_M and graphv}, we have a corresponding cycle
$C_{1}$ using the same edge from $\graph{Z}$ and the same one or two
edges from $\graphv{G}{v_{1}}$.  The cycle $C_{1}$ is not negative
since $\ua_{G}v_{1}\cap Z\neq\emptyset$.  Therefore, the negative
cycle $C_{2}$ should use at least one edge labelled
$(\leq,v_{2}(x))$ or $(\leq,-v_{2}(x))$.  We consider the different
\begin{enumerate}
\item Cycle
$C_{2}=0 \xra{(\leq,v_{2}(\history{y}))} \history{y} \xra{Z_{\history{y}0}}
0$.  We have
$C_{1}=0 \xra{(\leq,v_{1}(\history{y}))} \history{y} \xra{Z_{\history{y}0}}

Since we have the edge $0 \xra{(\leq,v_{1}(\history{y}))} \history{y}$ in
$\graphv{G}{v_{1}}$, there is a constraint $\history{y}\leqlt' c'$ in
$G$ with $(\leqlt',c')<(<,\infty)$ and $v_{1}(\history{y})\leqlt' c'$.
We deduce that $0\leq v_{1}(\history{y})\leq M$.

Let $Z_{\history{y}0}=(\leqlt,c)$.
Since $C_{1}$ is not a negative cycle, we get
$(\leq,0)\leq(\leqlt,c+v_{1}(\history{y}))$, which is equivalent to
$-c\leq v_{1}(\history{y})$. Using $0\leq v_{1}(\history{y})\leq M$ and
$v_{1}\sim_{M}v_{2}$ we deduce that $-c\leq v_{2}(\history{y})$.  This
is equivalent to $(\leq,0)\leq(\leqlt,c+v_{2}(\history{y}))$, a
contradiction with $C_{2}$ being a negative cycle.

\item Cycle
$C_{2}=0 \xra{Z_{0\history{y}}} \history{y} \xra{(\leq,-v_{2}(\history{y}))}
0$.  We have
$C_{1}=0 \xra{Z_{0\history{y}}} \history{y} \xra{(\leq,-v_{1}(\history{y}))}

Since we have the edge $\history{y} \xra{(\leq,-v_{1}(\history{y}))} 0$ in
$\graphv{G}{v_{1}}$, there is a constraint $c'\leqlt'\history{y}$ in
$G$ with $(c',\leqlt')<(\infty,\leq)$ and
$c'\not\leqlt' v_{1}(\history{y})$.  We deduce that
$0\leq v_{1}(\history{y})\leq M$.

Let $Z_{0\history{y}}=(\leqlt,c)$.
Since $C_{1}$ is not a negative cycle, we get
$(\leq,0)\leq(\leqlt,c-v_{1}(\history{y}))$, which is equivalent to
$v_{1}(\history{y})\leq c$.  Using $v_{1}\sim_{M}v_{2}$ and
$0\leq v_{1}(\history{y})\leq M$, we deduce that
$v_{2}(\history{y})\leq c$.  This is equivalent to
$(\leq,0)\leq(\leqlt,c-v_{2}(\history{y}))$, a contradiction with
$C_{2}$ being a negative cycle.

\item Cycle
$C_{2}=0 \xra{(\leq,v_{2}(\prophecy{x}))} \prophecy{x} \xra{Z_{\prophecy{x}0}}
0$.  We have
$C_{1}=0 \xra{(\leq,v_{1}(\prophecy{x}))} \prophecy{x} \xra{Z_{\prophecy{x}0}}

Since $C_{2}$ is negative, we have $Z_{\prophecy{x}0}\neq(\leq,\infty)$.  Also, if
$Z_{\prophecy{x}0}=(<,\infty)$ then we must have $v_{2}(\prophecy{x})=-\infty$, which implies
$v_{1}(\prophecy{x})=-\infty$ since $v_{1}\sim_{M}v_{2}$, a contradiction with $C_{1}$
being non-negative.  Hence, $Z_{\prophecy{x}0}=(\leqlt,c)<(<,\infty)$ and by
$(\dagger_{2})$, we infer $0\leq c\leq M$.

Since $C_{1}$ is not negative, we get
$(\leq,0)\leq(\leqlt,c+v_{1}(\prophecy{x}))$, which is equivalent to
$-c\leq v_{1}(\prophecy{x})$.  Using $v_{1}\sim_{M}v_{2}$ and
$0\leq c\leq M$ we deduce that $-c\leq v_{2}(\prophecy{x})$.  This is
equivalent to $(\leq,0)\leq(\leqlt,c+v_{2}(\prophecy{x}))$, a
contradiction with $C_{2}$ being a negative cycle.

\item Cycle
$C_{2}=0 \xra{Z_{0\prophecy{x}}} \prophecy{x} \xra{(\leq,-v_{2}(\prophecy{x}))}
0$.  We have
$C_{1}=0 \xra{Z_{0\prophecy{x}}} \prophecy{x} \xra{(\leq,-v_{1}(\prophecy{x}))}

Let $Z_{0\prophecy{x}}=(\leqlt,c)$.  Since $C_{2}$ is negative, we
deduce that $v_{2}(\prophecy{x})\neq-\infty$.  Using
$v_{1}\sim_{M}v_{2}$, we infer $v_{1}(\prophecy{x})\neq-\infty$.  Since
$C_{1}$ is not negative, we get $Z_{0\prophecy{x}}\neq(\leq,-\infty)$.
$(\dagger_{4})$, we infer
$(<,-M)\leq Z_{0\prophecy{x}}$ and $-M\leq c\leq 0$.

Since $C_{1}$ is not a negative cycle, we get
$(\leq,0)\leq(\leqlt,c-v_{1}(\prophecy{x}))$, which is equivalent to
$v_{1}(\prophecy{x})\leq c$.
Using $v_{1}\sim_{M}v_{2}$ and $-M\leq c\leq 0$, we deduce that
$v_{2}(\prophecy{x})\leq c$.  This is equivalent to
$(\leq,0)\leq(\leqlt,c-v_{2}(\prophecy{x}))$, a contradiction with
$C_{2}$ being a negative cycle.

\item Cycle
$C_{2}=0 \xra{(\leq,v_{2}(\history{y}))} \history{y}
\xra{Z_{\history{y}\prophecy{x}}} \prophecy{x} \xra{(\leq,-v_{2}(\prophecy{x}))} 0$.

We have
$C_{1}=0 \xra{(\leq,v_{1}(\history{y}))} \history{y}
\xra{Z_{\history{y}\prophecy{x}}} \prophecy{x} \xra{(\leq,-v_{1}(\prophecy{x}))} 0$.

Let $Z_{\history{y}\prophecy{x}}=(\leqlt,c)$.  As in case 1 above, we get
$0 \leq v_{1}(\history{y}) \leq M$.  From the fact that the cycle
$0 \xra{(\leq,v_{1}(\history{y}))} \history{y} \xra{Z_{\history{y}0}} 0$ is
not negative, we get $(\leq,-M)\leq Z_{\history{y}0}$.  Since $C_{2}$
is negative, we get $v_{2}(\prophecy{x})\neq-\infty$.  Using
$v_{1}\sim_{M}v_{2}$, we infer $v_{1}(\prophecy{x})\neq-\infty$.  From
the fact that the cycle
$0 \xra{Z_{0\prophecy{x}}} \prophecy{x} \xra{(\leq,-v_{1}(\prophecy{x}))} 0$ is
not negative, we deduce $Z_{0\prophecy{x}}\neq(\leq,-\infty)$.  Using
we obtain
(\leq,-M)+(<,-M)\leq Z_{\history{y}0}+(<,-M) \leq Z_{\history{y}\prophecy{x}}
and we deduce that $-2M\leq c\leq 0$.

Since $C_{1}$ is not a negative cycle, we get
$(\leq,0)\leq(\leqlt,c+v_{1}(\history{y})-v_{1}(\prophecy{x}))$, which is
equivalent to $v_{1}(\prophecy{x})-v_{1}(\history{y})\leq c$.  Using
$v_{1}\sim_{M}v_{2}$ and $-2M\leq c\leq 0$ we deduce that
$v_{2}(\prophecy{x})-v_{2}(\history{y})\leq c$.  We conclude as in the
previous cases.

\item Cycle
$C_{2}=0 \xra{(\leq,v_{2}(\prophecy{x}))} \prophecy{x}
\xra{Z_{\prophecy{x}\history{y}}} \history{y} \xra{(\leq,-v_{2}(\history{y}))} 0$.

We have
$C_{1}=0 \xra{(\leq,v_{1}(\prophecy{x}))} \prophecy{x}
\xra{Z_{\prophecy{x}\history{y}}} \history{y} \xra{(\leq,-v_{1}(\history{y}))} 0$.

Since $C_{2}$ is negative but not $C_{1}$, we get first
$Z_{\prophecy{x}\history{y}}\neq(\leq,\infty)$ and then $v_{1}(\prophecy{x})\neq-\infty$.
As in case 2 above, we get $0\leq v_{1}(\history{y})\leq M$.
We deduce that $Z_{\prophecy{x}\history{y}}=(\leqlt,c)<(<,\infty)$ and $c\neq\infty$.
From $(\dagger_{3})$ we obtain $Z_{\prophecy{x}0}\leq(\leq,M)$.
Since $0 \xra{(\leq,v_{1}(\prophecy{x}))} \prophecy{x} \xra{Z_{\prophecy{x}0}} 0$ is
not a negative cycle, we get $-M\leq v_{1}(\prophecy{x})\leq 0$.
Finally, we obtain $0\leq v_{1}(\history{y})-v_{1}(\prophecy{x})\leq 2M$.

Since $C_{1}$ is not a negative cycle, we get
$(\leq,0)\leq(\leqlt,c+v_{1}(\prophecy{x})-v_{1}(\history{y}))$, which is
equivalent to $v_{1}(\history{y})-v_{1}(\prophecy{x})\leq c$.  Using
$v_{1}\sim_{M}v_{2}$ and
$0\leq v_{1}(\history{y})-v_{1}(\prophecy{x})\leq 2M$, we deduce that
$v_{2}(\history{y})-v_{2}(\prophecy{x})\leq c$.  We conclude as in the
previous cases.

\item Cycle
$C_{2}=0 \xra{(\leq,v_{2}(\prophecy{x}))} \prophecy{x}
\xra{Z_{\prophecy{x}\history{y}}} \history{y} \xra{(\leqlt',-c')} 0$.

We have
$C_{1}=0 \xra{(\leq,v_{1}(\prophecy{x}))} \prophecy{x}
\xra{Z_{\prophecy{x}\history{y}}} \history{y} \xra{(\leqlt',-c')} 0$.

Let $Z_{\prophecy{x}\history{y}}=(\leqlt,c)$.
As in case 6 above, we show that $c\neq\infty$ and $-M\leq v_{1}(\prophecy{x})\leq 0$.

Since $C_{1}$ is not a negative cycle, we get
$0\leq c+v_{1}(\prophecy{x})-c'$, which is equivalent to
$c'-c\leq v_{1}(\prophecy{x})$.  Using $v_{1}\sim_{M}v_{2}$ and
$-M\leq v_{1}(x)\leq 0$, we deduce that $c'-c\leq v_{2}(\prophecy{x})$,
which is equivalent to $0\leq c+v_{2}(\prophecy{x})-c'$, a
contradiction with $C_{2}$ being a negative cycle.

\item Cycle
$C_{2}=0 \xra{(\leq,v_{2}(\prophecy{x}))} \prophecy{x}
\xra{Z_{\prophecy{x}\prophecy{y}}} \prophecy{y} \xra{(\leq,-v_{2}(\prophecy{y}))} 0$
with $x\neq y$.

We have
$C_{1}=0 \xra{(\leq,v_{1}(\prophecy{x}))} \prophecy{x}
\xra{Z_{\prophecy{x}\prophecy{y}}} \prophecy{y} \xra{(\leq,-v_{1}(\prophecy{y}))} 0$.

Since $C_{2}$ is negative but not $C_{1}$, using $v_{1}\sim_{M}v_{2}$ we get
successively $Z_{\prophecy{x}\prophecy{y}}\neq(\leq,\infty)$, $v_{2}(\prophecy{y})\neq-\infty\neq
v_{1}(\prophecy{y})$, $v_{1}(\prophecy{x})\neq-\infty\neq v_{2}(\prophecy{x})$, and finally
$(\leq,-\infty)< Z_{\prophecy{x}\prophecy{y}}<(<,\infty)$.

Let $Z_{\prophecy{x}\prophecy{y}}=(\leqlt,c)$.
From $(\dagger_{6})$, we deduce that $-M\leq c \leq M$.

Since $C_{1}$ is not a negative cycle, we get
$(\leq,0)\leq(\leqlt,c+v_{1}(\prophecy{x})-v_{1}(\prophecy{y}))$, which is
equivalent to $v_{1}(\prophecy{y})-v_{1}(\prophecy{x})\leq c$.  Using
$v_{1}\sim_{M}v_{2}$ and $-M\leq c \leq M$, we deduce that
$v_{2}(\prophecy{y})-v_{2}(\prophecy{x})\leq c$.  We conclude as in the
previous cases.

\item Cycle
$C_{2}=0 \xra{(\leq,v_{2}(\history{x}))} \history{x}
\xra{Z_{\history{x}\history{y}}} \history{y} \xra{(\leq,-v_{2}(\history{y}))} 0$
with $x\neq y$.

We have
$C_{1}=0 \xra{(\leq,v_{1}(\history{x}))} \history{x}
\xra{Z_{\history{x}\history{y}}} \history{y} \xra{(\leq,-v_{1}(\history{y}))} 0$.

As in case 1 above, we get $0\leq v_{1}(\history{x})\leq M$.  As in
case 2 above, we get $0\leq v_{1}(\history{y})\leq M$.  We obtain
$-M\leq v_{1}(\history{y})-v_{1}(\history{x}) \leq M$.

Let $Z_{\history{x}\history{y}}=(\leqlt,c)$.  Since $C_{1}$ is not
negative, we get
$(\leq,0)\leq(\leqlt,c+v_{1}(\history{x})-v_{1}(\history{y}))$, which is
equivalent to $v_{1}(\history{y})-v_{1}(\history{x})\leq c$.  Using
$v_{1}\sim_{M}v_{2}$ and
$-M\leq v_{1}(\history{y})-v_{1}(\history{x}) \leq M$, we deduce that
$v_{2}(\history{y})-v_{2}(\history{x})\leq c$.  We conclude as in the
previous cases.

\item Cycle
$C_{2}=0 \xra{(\leq,v_{2}(\history{x}))} \history{x}
\xra{Z_{\history{x}\history{y}}} \history{y} \xra{(\leqlt',-c')} 0$ with
$x\neq y$.

We have
$C_{1}=0 \xra{(\leq,v_{1}(\history{x}))} \history{x}
\xra{Z_{\history{x}\history{y}}} \history{y} \xra{(\leqlt',-c')} 0$.

As in case 1 above, we get $0\leq v_{1}(\history{x})\leq M$.

Let $Z_{\history{x}\history{y}}=(\leqlt,c)$.  Since $C_{1}$ is not
negative, we get $0\leq c+v_{1}(\history{x})-c'$, which is equivalent
to $c'-c\leq v_{1}(\history{x})$.  Using $v_{1}\sim_{M}v_{2}$ and
$0\leq v_{1}(\history{x})\leq M$, we deduce that
$c'-c\leq v_{2}(\history{x})$, which is equivalent to
$0\leq c+v_{2}(\history{x})-c'$, a contradiction with $C_{2}$ being a
negative cycle.
\end{enumerate}
Notice that we have crucially used the ``$2M$'' occurring in  the
definition of $v_1 \sim_M v_2$ (as $v_1(x) - v_1(y)
\sim_{2M} v_2(x) - v_2(y)$) in the cases where we deal with
cycles containing one prophecy clock and one history clock (Cases
5 and 6). In the rest of the cases, it was sufficient to use
$v_1(x) \sim_M v_2(x)$.\qedhere
\end{proof}

Finally, from Lemmas~\ref{lem:dagger} and \ref{lem:sim_M main property}, we obtain our
main theorem of the section.

\begin{theorem}\label{thm:simulation finite}
The simulation relation $\preceq_{\A}$ is finite.
\end{theorem}

\begin{proof}
Let $(q,Z_{0}),(q,Z_{1}),(q,Z_{2}),\ldots$ be an infinite sequence
of \emph{reachable} nodes in $\ezg(\A)$.  By Lemma~\ref{lem:dagger},
for all $i$, the distance graph $\graph{Z_{i}}$ in canonical form
satisfies conditions $(\dagger)$.

The atomic constraints in $G=\G(q)$ use constants in
$\{-\infty,\infty\}\cup\{c\in\mathbb{Z}\mid|c|\leq M\}$.
From Lemma~\ref{lem:sim_M main property} we deduce that for all $i$,
$\da_{G}Z_{i}$ is a union of $\sim_{M}$-classes.
Since $\sim_{M}$ is of finite index, there are only finitely many
unions of $\sim_{M}$-classes.  Therefore, we find $i<j$ with
$\da_{G}Z_{i}=\da_{G}Z_{j}$, which implies $Z_{j}\preceq_{G}Z_{i}$.
\end{proof}

Note that the number of enumerated zones is bounded by $2^r$
where $r$ is the number of equivalence classes of $\sim_M$. This is
similar to the known upper bound in classical timed automata, where
instead of $r$, we can use the number of regions as defined
Indeed, despite this blow up the interest in zone algorithms is that, at least
in the timed setting, they work significantly better in practice.  We hope the above
zone-based approach for ECA will also pave the way for fast implementations for ECA.

\section{Conclusion}
In this paper, we propose a simulation based approach for reachability
in ECAs. The main difficulty and difference from timed automata is the
use of prophecy clocks and undefined values. We believe that the
crux of our work has been in identifying the new representation for
prophecy clocks and undefined values. With this as the starting point,
we have been able to adapt the zone graph computation and the
$\Gg$-simulation technique to the ECA setting. This process required
us to closely study the mechanics of prophecy clocks in the zone
computations and we discovered this surprising property that prophecy
clocks by themselves do not create a problem for finiteness.

The final reachability algorithm looks almost identical to the timed
automata counterpart and hence provides a mechanism to
transfer timed automata technology to the ECA setting. The performance
benefits observed for the $LU$ and $\Gg$-simulation-based reachability
procedures for timed automata encourages us to believe that an
implementation of our algorithm would also yield good results, thereby
providing a way to efficiently check event-clock specifications on timed
automata models.
We also hope that our framework can be extended to other verification
problems, like liveness and to extended models like ECA with diagonal
constraints that have been studied in the context of timeline based
planning~\cite{DBLP:conf/fsttcs/BozzelliMP19a, DBLP:journals/tcs/BozzelliMP22}.

\bibliography{eca-simulations-arxiv-v2.bib}

\end{document}