
\section{Introduction}\label{sec:intro}

Timed automata (TA)~\cite{Alur:TCS:1994} are a well-established model
for real-time systems and form the basis for employing model-checking
techniques.  The most popular property that has been considered in
these systems is control state reachability. Reachability in timed
automata is a well-studied problem and was shown to be decidable (and
PSPACE-complete) using the so-called region
construction~\cite{Alur:TCS:1994}. This construction was primarily of
theoretical interest, as the number of regions, which are collections
of reachable configurations, explodes both in theory and in
practice. On the other hand, timed automata have been implemented in
several tools: UPPAAL~\cite{Larsen:1997:UPPAAL,BehrmannDLHPYH06},
KRONOS~\cite{KRONOS}, PAT~\cite{PAT}, RED~\cite{RED},
TChecker~\cite{TChecker}, Theta~\cite{Theta}, LTS-Min~\cite{LTSmin},
Symrob~\cite{RoussanalySM19},
MCTA~\cite{DBLP:conf/cav/KupferschmidWNP08}, etc. Most of these tools
have a common underlying algorithm which is an explicit
enumeration of reachable configurations stored as
\emph{zones}~\cite{Bengtsson:LCPN:2003}.
Since the late 90s, a substantial effort has been invested in
improving zone enumeration techniques, the common challenge being how
to get a sound and complete enumeration while exploring as few zones
as possible.

The more general model checking problem of whether the system
represented by TA $\mathcal{A}$ satisfies the specification given by TA $\mathcal{B}$
reduces to the language inclusion problem $\mathcal{L}(\mathcal{A}) \subseteq
\mathcal{L}(\mathcal{B})$. There are two challenges here: first, the inclusion problem
is undecidable in its full generality, and second, having clocks,
though excellent for timed implementations, are often less than ideal
for modeling timed specifications. This has led to the introduction of
event-clocks and the corresponding model of \emph{event-clock
  automaton (ECA)}~\cite{AlurFH99}. Event-clock automata make use of
special clocks that track the time since the last occurrence of an
event (history clocks) or the time until the next occurrence of an
event (prophecy clocks). On one hand this makes writing timed
specifications more natural. Indeed, the role of prophecy clocks is in
the same spirit as future modalities in temporal logics. This has led
to several extensions of temporal logics with
event-clocks~\cite{abs-cs-0601096,AkshayBG13,RaskinS99},
which are often used as specification languages and can be converted
into ECA. On the other hand, ECA can be determinized and hence
complemented. 
Observe that model-checking event-clock specifications over TA models can be reduced to the reachability problem on the product of the TA with an ECA. This product contains usual clocks, history clocks and prophecy clocks. The usual clocks can be treated in the same way as history clocks for the zone analysis. Therefore, if we solve ECA reachability (with history and prophecy clocks) using zones, we can incorporate usual clocks into the procedure seamlessly. 
The bottomline is that the well-motivated problem of model-checking
event-clock specifications over TA models can be reduced to an ECA
reachability problem.

Thus, in this paper, we focus on the core problem of building
efficient, zone-based algorithms for reachability in ECA. This problem
turns out to be significantly different compared to zone based
reachability algorithms in usual TA, precisely due to prophecy
clocks. Our goal is to align the zone-based reachability algorithms
for ECA with recent approaches for TA that have shown significant
gains.

As mentioned earlier, the core of an efficient TA reachability
algorithm is an enumeration of zones, where the central challenge is
that na\"ive enumeration does not terminate. One approach to guarantee
termination is to make use of an \emph{extrapolation} operation on
zones: each new zone that is enumerated is extrapolated to a bigger
zone. Any freshly enumerated zone that is contained in an existing
zone is discarded. 
More recently, a new \emph{simulation} approach to zone enumeration
has been designed, where enumerated zones are left unchanged. Instead,
with each fresh zone it is checked whether the fresh zone is simulated
by an already seen zone. If yes, the fresh zone is
discarded. Otherwise, it is kept for further exploration. Different
simulations have been considered: the
$LU$-simulation~\cite{HerbreteauSW12} which is based on $LU$-bounds,
or the $\mathcal{G}$-simulation~\cite{Gastin0S20}, which is based on a
carefully-chosen set of constraints. Coarser simulations lead to fewer
zones being enumerated.
The $\mathcal{G}$-simulation is currently the coarsest-known simulation that
can be efficiently applied in the simulation approach. The simulation
based approach offers several gains over the extrapolation approach:
(1) since concrete zones are maintained, one could use dynamic
simulation parameters and dynamic simulations, starting from a coarse
simulation and refining whenever
necessary~\cite{DBLP:conf/cav/HerbreteauSW13}, (2) the simulation
approach has been extended to richer models like timed automata with
diagonal constraints~\cite{Gastin0S19,GastinMS18}, updatable timed
automata~\cite{Gastin0S20}, weighted timed
automata~\cite{DBLP:conf/cav/BouyerCM16} and pushdown timed
automata~\cite{AkshayGP21}. In these richer models, extrapolation has
either been shown to be impossible~\cite{Bouyer04} or is unknown.


Surprisingly, for ECA, an arguably more basic and well-known model, it
turns out that there are no existing simulation-based
approaches. However, an extrapolation approach using maximal constants
has been studied for ECA in~\cite{GeeraertsRS11,GeeraertsRS14}. In
this work, the authors start by showing that prophecy clocks exhibit
fundamental differences as compared to usual clocks. To begin with, it
was shown that there is no finite time-abstract bisimulation for ECA
in general. This is in stark contrast to TA where the region
equivalence forms a finite time-abstract bisimulation. The correctness
of extrapolation
is strongly dependent on the region equivalence. Therefore, in order
to get an algorithm, the authors define a weak semantics for ECA and a
corresponding notion of weak regions which is a finite time-abstract
bisimulation for the weak semantics and show that the weak semantics
is sound for reachability. Building on this, they define an
extrapolation operation for the zone enumeration.
\medskip

\noindent \textbf{Contributions.} Given the advantages of using
simulations with respect to extrapolations in the TA setting described above,
we extend the $\mathcal{G}$-simulation approach to
ECA. 
Here are the technical contributions leading to the result.
\begin{itemize}
\item We start with a slightly modified presentation of zones in ECA
  and provide a clean algebra for manipulating weights in the graph
  representation for such ECA-zones. This simplifies the reasoning and
  allows us to adapt many ideas for simulation developed in the TA
  setting directly to the ECA setting.
  
\item The $\mathcal{G}$-simulation is parameterized by a set of constraints at
  each state of the automaton. We adapt the constraint computation and
  the definition of the simulation to the context of ECA, the main
  challenge being the handling of prophecy clocks.

\item We give a simulation test between two zones that runs in time
  quadratic in the number of clocks. This is an extension of the
  similar test that exists for timed automata, but now it incorporates
  new conditions that arise due to prophecy clocks.
  
\item Finally, we show that the reachability algorithm using the
  $\mathcal{G}$-simulation terminates for ECA: for every sequence
  $Z_0, Z_1, \dots$ of zones that are \emph{reachable} during a zone
  enumeration of an ECA, there exist $i < j$ such that
  $Z_j$ is simulated by $Z_i$. This is a notable
  difference to the existing methods in TA, where finiteness is
  guaranteed for all zones, not only the reachable zones. In the ECA
  case, this is not true: we can construct an infinite sequence of
  zones which are incomparable with respect to the new
  $\mathcal{G}$-simulation.  However, we show that finiteness does hold when
  restricting to reachable zones, and this is sufficient to prove
  termination of the zone enumeration algorithm. Our argument involves
  identifying some crucial invariants in reachable zones, specially,
  involving the prophecy clocks.
 


\end{itemize}

The fundamental differences in the behaviour of prophecy clocks as
compared to usual clocks constitute the major challenge in developing
efficient procedures for the analysis of ECAs.  In our work, we have
developed methods to incorporate prophecy clocks alongside the usual
clocks. We prove a surprising property:
in all \emph{reachable} ECA-zones, the constraints involving \emph{prophecy} clocks
come from a finite set.  A direct consequence of this observation is
that the event zone graph of an ECA containing only prophecy clocks
(known 
as Event-Predicting Automata EPA) is always finite.  We wish to 
emphasize that, in 
this work, we are moving a step towards implementability, and at the
same time towards more expressivity, since simulation approaches are
amenable to extensions, e.g., with diagonal constraints.

\medskip

\noindent \textbf{Organization of the paper.}
Section~\ref{sec:prelims} recalls ECA and describes a slightly
modified presentation of the ECA
semantics. Section~\ref{sec:event-zones} introduces event zones, event
zone graph and the simulation based reachability
framework. Section~\ref{sec:DBM} introduces the new algebra for
representing event zones and describes some operations needed to build
the zone graph.  Section~\ref{sec:simulation} introduces the
$\mathcal{G}$-simulation for event-clock automata and gives the simulation
test. Section \ref{sec:termination} proves finiteness of the
simulation when restricted to reachable zones.
\section{Event Clock Automata and Valuations}\label{sec:prelims}
Let $X$ be a finite set of variables called \emph{clocks}.  Let
$\Phi(X)$ denote a set of clock constraints generated by the following
grammar: $\varphi ::= x \mathrel{\triangleleft} c \mid c \mathrel{\triangleleft} x \mid \varphi \land \varphi$
where $x \in X$,
$c \in \overline{\mathbb{Z}}=\mathbb{Z}\cup\{-\infty,+\infty\}$ and
${\mathrel{\triangleleft}} \in \{<, \le\}$.  The base constraints of the form
$x \mathrel{\triangleleft} c$ and $c \mathrel{\triangleleft} x$ will be called \emph{atomic
  constraints}.  Constraints $x< -\infty$ and $+\infty<x$ are
equivalent to \emph{false} and constraints $-\infty\leq x$ and
$x\leq +\infty$ are equivalent to \emph{true}.

Given a finite alphabet $\Sigma$, we define a set 
$X_H = \{\ola{a} \mid a \in \Sigma\}$ of \emph{history clocks} 
and a set $X_P = \{\ora{a} \mid a \in \Sigma\}$ of \emph{prophecy clocks}. 
Together, history and prophecy clocks are called \emph{event clocks}.  In this paper, all
clocks will be event clocks, thus we set $X = X_H \cup X_P$.

\begin{wrapfigure}{r}{5cm}
  \centering
  \gusepicture{event-clocks}
  \captionof{figure}{Valuations for event clocks.}
  \label{fig:event-clocks}
\end{wrapfigure}

\begin{definition}[Valuation]
  A valuation of event clocks is a function
  $v\colon X \mapsto \overline{\mathbb{R}}=\mathbb{R}\cup\{-\infty,+\infty\}$ which
  maps history clocks to $\RR_{\ge 0}\cup\{+\infty\}$ and prophecy clocks to
  $\RR_{\le 0} \cup \{-\infty\}$.  
  We say a history clock $\ola{a}$, for some $a\in \Sigma$ is \emph{undefined} (resp.\
  \emph{defined}) when $v(\ola{a}) = +\infty$ (resp.\ $v(\ola{a}) < +\infty$) and a
  prophecy clock $\ora{a}$ is undefined (resp.\ defined) when $v(\ora{a}) = -\infty$
  (resp.\ $-\infty< v(\ora{a})$).
  We denote by $\mathbb{V}(X)$ or simply by $\mathbb{V}$ the set of valuations over $X$.
\end{definition}

We remark that the history clock and the prophecy clock of an event
$a$ are symmetric notions.  In the semantics that we introduce in this
paper, history clock $\ola{a}$ stores the amount of time elapsed after
seeing the last $a$, measuring how far ahead in the
future we are w.r.t.\ the last occurrence of $a$. Before we see an $a$
for the first time, $\ola{a}$ is set to $+\infty$.  The prophecy clock
$\ora{a}$ stores the negative of the amount of time that needs to be
elapsed before seeing the next $a$.  In other words, $-\ora{a}$ tells
us how far behind in the past we are w.r.t.\ the next occurrence of
$a$. If no more $a$'s are going to be seen, then the prophecy clock 
of $a$ is set to $-\infty$, i.e., $\ora{a} = -\infty$.

Notice that for history (resp.\ prophecy) clocks, \emph{useful}
constraints use non-negative (resp.\ non-positive) constants. Also,
$\ola{a}<0$ and $0<\ora{a}$ are equivalent to \emph{false} whereas
$0 \le \ola{a}$, $\ola{a}\leq\infty$, $\ora{a} \le 0$ and 
$-\infty\leq\ora{a}$ are equivalent to \emph{true}. A
constraint $c\mathrel{\triangleleft}\ola{a}$ does not imply that the history clock
$\ola{a}$ is defined, whereas a constraint $\ola{a}\mathrel{\triangleleft} c$ with
$(\mathrel{\triangleleft},c)\neq(\leq,\infty)$ does.  The same applies to prophecy
clocks where a constraint $c\mathrel{\triangleleft}\ora{a}$ with
$(c,\mathrel{\triangleleft})\neq(-\infty,\leq)$ implies that $\ora{a}$ is defined,
whereas $\ora{a}\mathrel{\triangleleft} c$ does not;
in fact, $\ora{a}\leq-\infty$ states that $\ora{a}$ is undefined.

\begin{remark}
  In the earlier works on ECA~\cite{AlurFH99,GeeraertsRS14}, prophecy
  clocks assumed non-negative values and decreased along with time.  This allowed to
  write guards on prophecy clocks with non-negative constants, e.g., $\ora{a} \le 5$ means
  that the next $a$ occurs in at most $5$ time units.  In our convention, this would be
  written as $-5 \le \ora{a}$.  Secondly, an undefined clock (history or prophecy) was
  assigned a special symbol $\bot$ in earlier works.  We have changed this to use
  $-\infty$ and $+\infty$ for undefined prophecy and history clocks respectively.
  We adopt these new conventions as they allow to treat both history clocks and prophecy
  clocks in a symmetric fashion, and a clean integration of undefined values
  when we describe zones and simulations.
\end{remark}

We say that a valuation $v$ satisfies a constraint $\varphi$, denoted as $v \models \varphi$, if
$\varphi$ evaluates to \emph{true}, when each variable $x$ in $\varphi$ is replaced by its value
$v(x)$.

We write $[\ola{a}]v$ to denote the valuation $v'$ obtained from $v$
by resetting the history clock $\ola{a}$ to $0$, keeping the value of
other clocks unchanged.  We denote by $[\ora{a}]v$ the \emph{set} of
valuations $v'$ obtained from $v$ by setting the prophecy clock
$\ora{a}$ non-deterministically to some value in $[-\infty,0]$,
keeping the value of other clocks unchanged.
We denote by $v + \d$ the valuation obtained by increasing the value
of all clocks from the valuation $v$ by $\d \in \RR_{\ge 0}$. Not every time
elapse may be possible from a valuation, since prophecy clocks need to
stay at most $0$. For example, if there are two events $a,b$, then
a valuation with $v(\ora{a}) = -3$ and $v(\ora{b}) = -2$ can elapse at
most $2$ time units.


\begin{definition}[Event-clock automata~\cite{AlurFH99}]\label{defn:eca}
  An \emph{event-clock automaton (ECA) } $\mathcal{A}$ is given by a tuple
  $(Q, \Sigma, X, T, q_0, F)$, where $Q$ is a finite set of states,
  $\Sigma$ is a finite alphabet of actions, $X$ is the set of event
  clocks for $\Sigma$, $q_0 \in Q$ is the initial state,
  $F \subseteq Q$ is the set of accepting states and
  $T \subseteq Q \times \Sigma \times \Phi(X) \times Q$ is a
  finite set of transitions.

  \noindent  The semantics of an ECA $\mathcal{A}=(Q,\Sigma,X,T,q_0,F)$ is given by a
  transition system $S_{\mathcal{A}}$ whose
  states are \emph{configurations} $(q,v)$ of $\mathcal{A}$, where $q \in Q$ and $v$ is a
  valuation.
  A configuration $(q,v)$ is initial if $q=q_{0}$, $v(x)=\infty$ for all $x\in X_H$ and
  $-\infty \leq v(x) \leq 0$ for all $x \in X_P$.
  A configuration $(q,v)$ is accepting if $q\in F$, and $v(x)=-\infty$ for all
  $x\in X_P$ and 
  $0 \leq v(x) \leq \infty$  
  for all $x \in X_H$.
  Transitions of $S_{\mathcal{A}}$ are of two forms:
  \begin{itemize}
    \item \textbf{Delay transition}:
      $(q,v) \xra{\delta} (q, v + \delta)$, if
      $(v + \delta)(x) \leq 0$ for all $x \in X_P$.
      
    \item \textbf{Action transition}: $(q,v) \xra{t} (q',[\ola{a}]v')$
      if $t=(q,a,g,q')$ is a transition in $\mathcal{A}$, $v(\ora{a})=0$,
      $v'\in[\ora{a}]v$ and $v'\models g$.
      
      A transition with action $a$ can be taken when the value of the
      prophecy clock $\ora{a}$ is $0$, then a new value in
      $[-\infty,0]$ for $\ora{a}$ is non-deterministically guessed so
      that the resulting valuation $v'$ satisfies the guard $g$,
      and finally, the history clock $\ola{a}$ is reset to $0$.
    \end{itemize}
\end{definition}

An ECA is called an event recording automaton (ERA) if it only contains history clocks and
event predicting automaton (EPA) if it only contains prophecy clocks.  A \emph{run} of an
event-clock automaton is a finite sequence of transitions from an initial configuration of
$S_{\mathcal{A}}$.  A run is said to be \emph{accepting} if its last configuration is
accepting.  We are interested in the \emph{reachability problem} of an event clock
automaton. Formally, 

\begin{definition}[Reachability problem for ECA]\label{defn:reach-problem}
  The reachability problem for an event-clock automaton $\mathcal{A}$ is to
  decide whether $\mathcal{A}$ has an accepting run.
\end{definition}

Different solutions based on regions and zones have been proposed in
\cite{AlurFH99,GeeraertsRS11,GeeraertsRS14}.  For ERA, the standard region and zone based
algorithms for timed automata work directly.  However, for EPA (and ECA), this is not the
case.  In fact,~\cite{GeeraertsRS11} show that the standard region abstraction is not
possible, as there exists no finite bisimulation due to the behavior of prophecy clocks.
Also, the standard definition of zones used for timed automata is not sufficient to handle
valuations with undefined clocks.  The papers \cite{GeeraertsRS11,GeeraertsRS14} make use
of special symbols $\bot$ and $?$ for this purpose.  In this work, we use a different
formulation of zones by making use of $+\infty$ and $-\infty$.
Instead of using $x=\bot$ (resp.\ $x\neq\bot$) to state that a clock is undefined
(resp.\ defined) as in~\cite{GeeraertsRS11,GeeraertsRS14}, we write $+\infty\leq x$
or $x\leq-\infty$ or (resp.\ $x<+\infty$ or $-\infty<x$) depending on whether $x$ is a
history clock or a prophecy clock.  This distinction between being undefined for history
and prophecy clocks plays an important role.
\section{Event zones and simulation based reachability}\label{sec:event-zones}
The most widely used approach for checking reachability in a timed
automaton is based on reachability in a graph called the \emph{zone
  graph} of a timed automaton~\cite{Daws}. Roughly, \emph{zones}~\cite{Bengtsson:LCPN:2003} are sets of
valuations that can be represented efficiently using difference
constraints between clocks.  In this section, we introduce an
analogous notion for event-clock automata. We consider \emph{event
  zones}, which are sets of valuations of event-clock automata. 
  

\begin{definition}[\textbf{Event zones}]\label{defn:event-zones}
  An event zone is a set of valuations satisfying a conjunction of
  constraints of the form $c\mathrel{\triangleleft} x$, $x \mathrel{\triangleleft} c$ or $x - y \mathrel{\triangleleft} c$, where
  $x,y \in X$ and $c\in\overline{\mathbb{Z}}=\mathbb{Z}\cup\{-\infty,+\infty\}$.
  Constraints of the form $x-y\mathrel{\triangleleft} c$ are called diagonal constraints.
  To evaluate such constraints, we extend addition on real
  numbers with the convention that $(+\infty)+\alpha = +\infty$ for all
  $\alpha\in\overline{\mathbb{R}}$ and $(-\infty)+\beta = -\infty$, as long as
  $\beta\neq+\infty$.  We simply write $v(x - y)$ for $v(x) - v(y)$.
\end{definition}

Let $W$ be a set of valuations and $q$ a state. For transition
$t:= (q, a, g, q_1)$, we write $(q, W) \xra{t} (q_1, W_1)$ if
$W_1 = \{ v_1 \mid (q, v) \xra{t} \xra{\delta} (q_1, v_1) \text{ for
some } \delta \in \mathbb{R}_{\geq0} \}$. As is usual with timed automata,
zones are closed under the time elapse operation. We will show in the
next section that starting from an event zone $Z$, the successors
are also event zones: $(q, Z) \xra{t} (q_1, Z_1)$ implies $Z_1$ is an
event zone too. We use this feature to define an event zone graph.

\begin{definition}[\textbf{Event zone graph}]
  Nodes are of the form $(q, Z)$ where $q$ is a
  state and $Z$
  is an event zone. The initial node is $(q_0, Z_0)$ where $q_0$ is the
  initial state and $Z_0$ is given by
  $\bigwedge_{a \in \Sigma} (\infty\leq\ola{a}) \wedge (\ora{a} \leq
  0)$. 
  This is the set of all initial valuations, 
  which is already closed under time elapse. For every node $(q, Z)$ and every
  transition $t := (q, a, g, q_1)$ there is a transition
  $(q, Z) \xra{t} (q_1, Z_1)$ in the event zone graph.
  A node $(q,Z)$ is accepting if $q\in F$ and $Z\cap Z_{f}$ is non-empty where the final 
  zone $Z_{f}$ is defined by $\bigwedge_{a\in\Sigma} \ora{a}\leq-\infty$.
\end{definition}

Two examples of ECA and their event zone graphs are given in
Figure~\ref{fig:eca-zone-graph-ex-1} and Figure~\ref{fig:eca-zone-graph-ex-2} 
below.
\begin{figure}[!h]
  \centering	
	\scalebox{0.8}{
    \begin{subfigure}[b]{\textwidth}
      \centering	
      \begin{tikzpicture}
      [state/.style={draw, thick, circle, inner sep=4pt}]
      \begin{scope}[xshift=4cm, 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}	
      
      \node at (6, 2) {\footnotesize $\mathcal{A}_1$}; 

      \begin{scope}[->, >=stealth, thick]
        \draw (3.25, 3) to (q0); 
        \draw (q0) to [out=120,in=60,looseness=8] (q0);
        \draw (q1) to [out=120,in=60,looseness=8] (q1);  
        \draw (q0) to (q1); 
        \draw (q1) to (q2); 
        \draw (q2) to (8.75,3); 
      \end{scope}
      
      \node at (4, 4.6) {\footnotesize $b$}; 
      \node at (6, 4.6) {\footnotesize $b$}; 
      \node at (5, 3.25) {\footnotesize $b$}; 
      \node at (5, 2.75) {\scriptsize $\ora{a}=-1$}; 

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

    \end{scope}

    \begin{scope}[xshift=-2cm, yshift=0cm]

      \begin{scope}[xshift=0cm, yshift=0cm, zone/.style={draw,rectangle,minimum width=3.2cm, minimum height=2.5cm, rounded corners}]
        \node [zone] (z0) at (0, 0) {}; 
        \node [zone] (z1) at (0, 3.5) {};
        \node [zone] (z2) at (5, 0) {}; 
        \node [zone] (z3) at (5, 3.5) {}; 
        
      \end{scope}
      
      \begin{scope}[xshift=0cm, yshift=0cm, zone/.style={draw,rectangle,minimum width=3.2cm, minimum height=2.8cm, rounded corners}]
        \node [zone] (z4) at (9.5, 0) {};
      \end{scope}

      \begin{scope}[->, >=stealth, thick]
      \draw (z0) to (z1); 
      \draw (z0) to (z2);
      \draw (z1) to (z2);
      \draw (z2) to (z3);
      \draw (z2) to (z4);
      \draw (z3) to (z4);
      \draw (z1) to [out=110,in=70,looseness=4] (z1);
      \draw (z3) to [out=110,in=70,looseness=4] (z3);
      \end{scope}

      

      \node at (0, 0.6) {\footnotesize $q_0$}; 
      \node at (0, 0) {\scriptsize $\ora{a} \leq 0~~~~\ola{a} = \infty$}; 
      \node at (0, -0.6) {\scriptsize $\ora{b} \leq 0~~~~\ola{b} = \infty$}; 

      \node at (0, 4.5) {\footnotesize $q_0$}; 
      \node at (0, 4) {\scriptsize $\ora{a} \leq 0~~~~\ola{a} = \infty$}; 
      \node at (0, 3.5) {\scriptsize $\ora{b} \leq 0~~~~0 \leq \ola{b} < \infty$}; 
      \node at (0, 3) {\scriptsize $\ora{a} - \ola{b} \leq 0$}; 
      \node at (0, 2.5) {\scriptsize $\ora{b} - \ola{b} \leq 0$}; 


      \node at (5, 1) {\footnotesize $q_1$}; 
      \node at (5, 0.5) {\scriptsize $-1 \leq \ora{a} \leq 0~~~~\ola{a} = \infty$}; 
      \node at (5, 0) {\scriptsize $~~\ora{b} \leq 0~~~~~0 \leq \ola{b} \leq 1$}; 
      \node at (5, -0.5) {\scriptsize $\ola{b} - \ora{a} = 1$}; 
      \node at (5, -1) {\scriptsize $\ora{b} - \ora{a} \leq 1~~~\ora{b} - \ola{b} \leq 0$}; 


      \node at (5, 4.5) {\footnotesize $q_1$}; 
      \node at (5, 4) {\scriptsize $-1 \leq \ora{a} \leq 0~~~~\ola{a} = \infty$}; 
      \node at (5, 3.5) {\scriptsize $~~\ora{b} \leq 0~~~~~0 \leq \ola{b} \leq 1$}; 
      \node at (5, 3) {\scriptsize $0 \leq \ola{b} - \ora{a} \leq 1$}; 
      \node at (5, 2.5) {\scriptsize $\ora{b} - \ora{a} \leq 1~~~\ora{b} - \ola{b} \leq 0$}; 

      \node at (9.5, 1) {\footnotesize $q_2$}; 
      \node at (9.5, 0.5) {\scriptsize $\ora{a} \leq 0~~~~~~0 \leq \ola{a} < \infty$}; 
      \node at (9.5, 0.1) {\scriptsize $\ora{b} \leq 0~~~~~~0 \leq \ola{b} < \infty$}; 
      \node at (9.5, -0.3) {\scriptsize $0 \leq \ola{b} - \ola{a} \leq 1$}; 
      \node at (9.5, -0.7) {\scriptsize $\ora{a} - \ola{a} \leq 0~~\ora{b} - \ola{a} \leq 0$}; 
      \node at (9.5, -1.1) {\scriptsize $\ora{a} - \ola{b} \leq 0~~\ora{b} - \ola{b} \leq 0$}; 

      \node at (-0.25, 1.75) {\footnotesize $b$}; 
      
      \node at (0, 6) {\footnotesize $b$}; 

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

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

      \node at (4.75, 1.75) {\footnotesize $b$}; 
      \node at (5, 6) {\footnotesize $b$}; 

      \node at (7.25, 1.5) {\footnotesize $a$}; 

      \node at (7.25, 0.25) {\footnotesize $a$}; 
    \end{scope}
  \end{tikzpicture} 
    \end{subfigure}
    }
  \caption[Example of event zone graph]{An event-clock automaton and its event zone 
  graph. Missing lower bounds are of the form $-\infty\leq x-y$ and missing upper bounds 
  are of the form $x-y\leq\infty$ (including $y=0$).}
  \label{fig:eca-zone-graph-ex-1}
\end{figure}

In Figure~\ref{fig:eca-zone-graph-ex-1}, we give the event zone graph of the event-clock automaton $\mathcal{A}_1$ that recognizes the language $\{b^n a \mid n \ge 1 \}$ such that there exists some $b$ which occurs exactly one time unit before $a$.

\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 $\mathcal{A}_2$}; 

      \node at (4, 4.6) {\footnotesize $b$}; 
      \node at (4, 4.25) {\scriptsize $\ora{b}=-1 \wedge \ora{a}<-1$}; 
      \node at (5, 3.25) {\footnotesize $b$}; 
      \node at (5, 2.75) {\scriptsize $\ora{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 (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=15,in=-15,looseness=4] (z3);
      \end{scope}

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


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

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

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

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

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

      \node at (6.25, 0.25) {\footnotesize $a$}; 
      \node at (10.1, 0) {\footnotesize $d$}; 
    \end{tikzpicture} 
  \end{subfigure}
  \caption[]{Event \emph{predicting} automaton for which there exists no finite time
  abstract bisimulation and its event zone graph.  Missing lower bounds are of the form
  $-\infty\leq x-y$ and missing upper bounds are of the form $x-y\leq\infty$ (including
  $y=0$).}
  \label{fig:eca-zone-graph-ex-2}
\end{figure}


Further, Geeraerts et al.~\cite{GeeraertsRS11,GeeraertsRS14} showed that there exists no
finite time abstract bisimulation relation for the event predicting automaton (EPA) $\mathcal{A}_2$
given in Figure~\ref{fig:eca-zone-graph-ex-2}.  Figure~\ref{fig:eca-zone-graph-ex-2} also
depicts the event zone graph of $\mathcal{A}_2$.  Note that, since this is an event
\emph{predicting} automaton, there are no history clocks.  It is easy to see that there
are only finitely many distinct constraints involving the prophecy clocks.

Similar to the case of timed automata, the event zone graph can be used to decide
reachability.  The next lemma follows by a straightforward adaptation of the corresponding
proof~\cite{Daws} from timed automata.

\begin{proposition}
  The event zone graph of an ECA is sound and complete for
  reachability.
\end{proposition}

However, as in the case of zone graphs for timed automata, the event zone graph for an ECA is also not guaranteed to be finite. We will now
define what a simulation is and see how it can be used to get a finite
truncation of the event zone graph, which is still sound and complete for 
reachability.

\begin{definition}[\textbf{Simulation}]
  A simulation relation on the semantics of an ECA is a reflexive,
  transitive relation $(q, v) \preceq (q, v')$ relating configurations
  with the same control state and (1) for every
  $(q, v) \xra{\delta} (q, v+\delta)$, we have
  $(q, v') \xra{\delta} (q, v'+\delta)$ and
  $(q, v+\delta) \preceq (q, v'+ \delta)$, (2) for every transition
  $t$, if $(q, v) \xra{t} (q_1, v_1)$ for some valuation $v_{1}$, then
  $(q, v') \xra{t} (q_1, v'_1)$ for some valuation $v'_{1}$ 
  with $(q_1, v_1) \preceq (q_1, v'_1)$.

  For two event zones $Z, Z'$, we say $(q, Z) \preceq (q, Z')$ if for
  every $v \in Z$ there exists $v' \in Z'$ such that
  $(q, v) \preceq (q, v')$. The simulation $\preceq$ is said to be
  finite if for every sequence $(q_{1}, Z_1), (q_{2}, Z_2), \dots$ of 
  \emph{reachable} nodes,
  there exists $j > i$ such that $(q_{j}, Z_j) \preceq (q_{i}, Z_i)$.
\end{definition}

The reachability algorithm enumerates the nodes of the event zone
graph and uses $\preceq$ to truncate nodes that are smaller with
respect to the simulation.

\begin{definition}[\textbf{Reachability algorithm.}] \label{def:reach-algo}
  Let $\mathcal{A}$ be an ECA and
  $\preceq$ a finite simulation for $\mathcal{A}$. Add the initial node of the
  event zone graph $(q_0, Z_0)$ to a Waiting list. Repeat the following
  until Waiting list is empty:
  \begin{itemize}
    \item Pop a node $(q, Z)$ from the Waiting list and add it to the
    Passed list.
    \item For every $(q, Z) \xra{t} (q_1, Z_1)$: if there exists a
    $(q_1, Z'_1)$ in the Passed or Waiting lists such that
    $(q_1, Z_1) \preceq (q_1, Z'_1)$, discard $(q_1, Z_1)$; else add
    $(q_1, Z_1)$ to the Waiting list.
  \end{itemize}
  If some accepting node is reached,
  the algorithm terminates and returns a Yes.
  Else, it continues until there are no further nodes to be explored and returns a No answer.
\end{definition}

The correctness of the reachability algorithm follows once again from
the correctness of the simulation approach in timed automata~\cite{HerbreteauSW12}. Moreover, termination is guaranteed when the simulation used is finite.

\begin{theorem}
  An ECA has an accepting run 
  iff the reachability algorithm returns Yes.
\end{theorem}

We have now presented the framework for the simulation approach in its entirety. However, to make it functional, we will need the following.
\begin{enumerate}
  \item An efficient representation for event zones and algorithms to
  compute successors.
  \item A concrete simulation relation $\preceq$ for ECA with an
  efficient simulation test $(q, Z) \preceq (q, Z')$.
  \item A proof that $\preceq$ is finite, to
  guarantee termination of the reachability algorithm.  
\end{enumerate}
In the rest of the paper, we show how these can be achieved.  To start with, for standard
timed automata, zones are represented using Difference-Bound-Matrices
(DBMs)~\cite{Dill89}.  For such a representation to work on event zones, we will need to
incorporate the fact that valuations can now take $+\infty$ and $-\infty$.  In
Section~\ref{sec:DBM}, we propose a way to merge $+\infty$ and $-\infty$ seamlessly into
the DBM technology.  In the subsequent Section~\ref{sec:simulation}, we define a
simulation for ECA based on $\mathcal{G}$-simulation, develop some technical machinery and present
an efficient simulation test.  Finally, in Section~\ref{sec:termination}, we deal with the
main problem of showing finiteness.  For this, we prove some non-trivial
invariants on the event zones that are reachable in ECA and use them to show a surprising
property regarding prophecy clocks.  More precisely, we show that constraints involving 
prophecy clocks in reachable event zones come from a finite set depending on the maximal 
constant of the ECA only.

\section{Computing with event zones and distance graphs}\label{sec:DBM}
We now show that event zones can be represented using
Difference-Bound-Matrices (DBMs) and the operations required for the reachability
algorithm can be implemented using DBMs. Each entry in a DBM encodes a
constraint of the form $x - y \mathrel{\triangleleft} c$. For timed automata analysis,
the entries are $(\mathrel{\triangleleft}, c)$ where $c \in \mathbb{R}$ 
and ${\mathrel{\triangleleft}} \in \{ <, \leq \}$, or $(\mathrel{\triangleleft}, c) = (<, \infty)$.  In our case, we will
need to deal with valuations having $+\infty$ or $-\infty$.  For this purpose, we first
extend weights to include $(\le, -\infty)$ and $(\le, \infty)$ and define an arithmetic
that admits the new entries in a natural way.


\begin{definition}[Weights]
  Let $\mathcal{C} = \{(\leq,-\infty)\} \cup \{(\mathrel{\triangleleft}, c) \mid c \in
  \mathbb{R}\cup\{\infty\} \text{ and } {\mathrel{\triangleleft}} \in \{\leq, <\}\}$,
  called the set of weights.
  \begin{itemize}
    \item \textbf{Order.} Define
    $(\mathrel{\triangleleft}_1, c_1) < (\mathrel{\triangleleft}_2, c_2)$ when either (1) $c_1 < c_2$,
    or (2) $c_1 = c_2$ and $\mathrel{\triangleleft}_1$ is $<$ while $\mathrel{\triangleleft}_2$ is
    $\leq$. 
    This is a total order, in particular
    $(\le, -\infty) < (\mathrel{\triangleleft}, c) < (<, \infty) <
    (\le, \infty)$ for all $c \in \mathbb{R}$.

    \item \textbf{Sum.} Let $\alpha, \beta, \gamma, (\mathrel{\triangleleft}_1, c_1), (\mathrel{\triangleleft}_2, c_2) \in
    \mathcal{C}$ with $\beta\neq(\leq,\infty)$,
    $\gamma\notin\{(\leq,-\infty),(\leq,\infty)\}$ and $c_1, c_2 \in \mathbb{R}$.  We
    define the operation of \emph{sum} on weights as follows. 
    
    \smallskip\hfil
    $(\leq , \infty) + \alpha = (\leq , \infty) \qquad
      (\leq , -\infty) + \beta = (\leq , -\infty) \qquad
      (< , \infty) + \gamma = (< , \infty)$
      
    \smallskip\hfil
    $(\mathrel{\triangleleft}_1, c_1) + (\mathrel{\triangleleft}_2,c_2) = (\mathrel{\triangleleft},c_1+c_2) \qquad
      \text{with } {\mathrel{\triangleleft}}={\leq} \text{ if } {\mathrel{\triangleleft}}_1 = {\mathrel{\triangleleft}}_2 = {\leq} 
      \text{ and } {\mathrel{\triangleleft}}={<} \text{ otherwise.}$
  \end{itemize}
\end{definition}

The intuition behind the above definition of order is that when $(\mathrel{\triangleleft}, c) < (\mathrel{\triangleleft}',
c')$, the set of valuations that satisfies a constraint $x - y \mathrel{\triangleleft} c$ is contained in
the solution set of $x - y \mathrel{\triangleleft}' c'$.  For the sum, we have the following lemma which
gives the idea behind our choice of definition.

\begin{restatable}{lemma}{lemSumWeights}
  Let $v$ be a valuation, $x, y, z$ be event clocks and
  $(\mathrel{\triangleleft}_1, c_1), (\mathrel{\triangleleft}_2, c_2)\in\mathcal{C}$. 
  If $v \models x - y \mathrel{\triangleleft}_1 c_1$ and $v \models y - z \mathrel{\triangleleft}_2 c_2$,
  then $v \models x - z \mathrel{\triangleleft} c$ where
  $(\mathrel{\triangleleft}, c) = (\mathrel{\triangleleft}_1, c_1) + (\mathrel{\triangleleft}_2, c_2)$.
\end{restatable}

\begin{proof}
  When $c_1, c_2 \in \mathbb{R}$, this is clear. When either
  $(\mathrel{\triangleleft}_1, c_1)$ or $(\mathrel{\triangleleft}_2, c_2)$ is $(\le, \infty)$, we have
  $(\mathrel{\triangleleft}, c) = (\le, \infty)$. Every valuation satisfies
  $x - z \le \infty$ and hence we are done. Suppose
  $(\mathrel{\triangleleft}_1, c_1) = (\le, -\infty)$ and
  $(\mathrel{\triangleleft}_2, c_2) \neq (\le, \infty)$. From $v(x - y) \le -\infty$, we
  infer that either $v(x) = -\infty$ or $v(y) = +\infty$. But,
  $v(y) = + \infty$ or $v(z) = -\infty$ would imply
  $(\mathrel{\triangleleft}_2, c_2) = (\le, +\infty)$, a contradiction. Hence we
  conclude $v(x) = -\infty$, $v(z) \neq -\infty$ and therefore
  $v \models x - z \le -\infty$. Similar argument when
  $(\mathrel{\triangleleft}_1, c_1) \neq (\le, \infty)$ and
  $(\mathrel{\triangleleft}_2, c_2) = (\le, -\infty)$. Finally, assume
  $(\mathrel{\triangleleft}_1, c_1) = (<, \infty)$ and
  $(\mathrel{\triangleleft}_2, c_2) \notin \{ (\le, -\infty), (\le, \infty) \}$. We
  want to show that $v(x - z) < +\infty$, that is, neither $v(x)$ nor
  $-v(z)$ is $+\infty$. Indeed, if $v(x) = +\infty$ then
  $v(x - y) = +\infty$ contradicting $v(x - y) < \infty$; and if
  $v(z) = -\infty$, we have $v(y - z) = +\infty$, contradicting
  $v(y - z) \mathrel{\triangleleft}_2 c_2$. This shows that
  $v(x - z) < +\infty$. Similar argument when
  $(\mathrel{\triangleleft}_1, c_1) \notin \{ (\le, -\infty), (\le, \infty)\}$ and
  $(\mathrel{\triangleleft}_2, c_2) = (<, \infty)$.
\end{proof}

Equipped with the weights and the arithmetic over it, we will work with a graph
representation of zones (as so-called distance graphs), instead of matrices (i.e., DBMs),
since this makes the analysis more convenient.  We wish to highlight that our definition
of weights, order and sum have been chosen to ensure that this notion of distance graphs
remains identical to the one for usual TA. As a consequence, we are able to adapt many of
the well-known properties about distance graphs for ECA.

\begin{definition}[Distance graphs]
  A distance graph is a weighted directed graph, with vertices being
  $X_P \cup X_H \cup \{0\}$ where $0$ is a special vertex that plays
  the role of constant $0$. Edges are labeled with weights from
  $\mathcal{C}$. An edge $x \xra{\mathrel{\triangleleft}\,c} y$ represents the
  constraint $y - x \mathrel{\triangleleft} c$. For a graph $\mathbb{G}$, we define
  $\sem{\mathbb{G}} := \{ v \mid v \models y - x \mathrel{\triangleleft} c \text{ for
  all edges } x \xra{\mathrel{\triangleleft}\,c} y \text{ in } \mathbb{G} \}$. 
  Further,
  \begin{itemize}
  \item The weight of a path in a distance graph $\mathbb{G}$ is the
    sum of the weight of its edges. A cycle in $\mathbb{G}$ is said to
    be negative if its weight is strictly less than $(\le, 0)$.

  \item A graph $\mathbb{G}$ is said to be in canonical form if it has
    no negative cycles and for each pair of vertices $x, y$, the
    weight of $x \to y$ is not greater than the weight of any
    path from $x$ to $y$.
    
  \item For two graphs $\mathbb{G}_1$, $\mathbb{G}_2$, we write
    $\min(\mathbb{G}_1, \mathbb{G}_2)$ for the distance graph obtained
    by setting the weight of each edge to the minimum
    of the corresponding weights in $\mathbb{G}_1$ and $\mathbb{G}_2$.
  \end{itemize}
  For an event zone $Z$, we write $\graph{Z}$ for the canonical
  distance graph that satisfies $\sem{\graph{Z}} = Z$.
  We denote by $Z_{xy}$ the weight of the edge $x \to y$ in $\graph{Z}$.
\end{definition}


  We will make use of an important property, 
  which has been shown when weights come from $\mathcal{C} \setminus \{ (\le, +\infty),
  (\le, -\infty)\}$, but continues to hold even with the new weights added.
  
  \begin{lemma}
  \label{lem:fixing-values-distance-graph}
  Let $\mathbb{G}$ be a canonical distance graph. Let
  $x \xra{\mathrel{\triangleleft}_{xy}~ c_{xy}} y$ and
  $y \xra{\mathrel{\triangleleft}_{yx}~ c_{yx}} x$ be edges in $\mathbb{G}$, and let
  $\alpha \in \mathbb{R} \cup \{-\infty, +\infty\}$ such that
  $(\le, 0) \le (\le, \alpha) + (\mathrel{\triangleleft}_{yx}, c_{yx})$ and
  $(\le, 0) \le (\le, -\alpha) + (\mathrel{\triangleleft}_{xy}, c_{xy})$. 
  Then, replacing the weight of $x \to y$ with $(\le, \alpha)$ and the weight of $y \to x$
  with $(\le, -\alpha)$ results in a distance graph with no negative cycles.
\end{lemma}

\begin{proof}
  We use the fact that sum of weights is monotone:
  $\alpha\leq\beta$ implies $\alpha+\gamma\leq\beta+\gamma$.  Notice that
  $(\leq,-\infty)+(\leq,\infty)=(\leq,\infty)$ and when $\alpha$ is finite we have
  $(\leq,\alpha)+(\leq,-\alpha)=(\leq,0)$ which is the neutral element for sum.

  Consider the distance graph $\mathbb{G}'$ obtained by changing the weight of $x \to y$ to
  $(\le, \alpha)$ and the weight of $y \to x$ to $(\le, -\alpha)$.  We
  will show that $\mathbb{G}'$ has no negative cycles. Let $x \to y$
  and $y \to x$ be called new edges and the rest be called old
  edges. The cycle $x \to y \to x$ formed by the new edges has
  weight $(\leq,\infty)$ or $(\le, 0)$, hence not negative. A cycle with all old edges
  cannot be negative as $\mathbb{G}$ is in canonical form (and by
  our definition, such a graph has no negative cycles). We need to
  look for cycles containing at least one old edge and one new edge:
  $x \xra{(\le, \alpha)} y \cdots x$, or $x \cdots y \xra{(\le, -\alpha)}
  x$ where the dotted part contains only old edges. We show $x
  \xra{(\le, \alpha)} y \cdots x$ is non-negative. For the other cycle,
  the argument is similar.
  
  Suppose weight of $y \cdots x$ is $(\mathrel{\triangleleft}, c)$. 
  We have $(\mathrel{\triangleleft}_{yx}, c_{yx}) \le (\mathrel{\triangleleft}, c)$ since $\mathbb{G}$ is in canonical form.
  Adding $(\le, \alpha)$ to this inequality, we get $(\le, 0) \le
  (\leq,\alpha)+(\mathrel{\triangleleft}_{yx},c_{yx}) \leq (\le, \alpha) + (\mathrel{\triangleleft}, c)$.
  Hence $x \xra{(\le, \alpha)} y \cdots x$ cannot be a negative cycle.
\end{proof}

With this we are able to show that a classical and crucial property of distance graphs for timed automata also extends to event clock automata.


\begin{restatable}{lemma}{lemEmptyNegativeCycle}
  \label{lem:empty-iff-negative-cycle}
  For every distance graph $\mathbb{G}$, we have
  $\sem{\mathbb{G}} = \emptyset$ iff $\mathbb{G}$ has a negative
  cycle.
\end{restatable}

\begin{proof}
  Suppose $\sem{\mathbb{G}}$ is non-empty. Let
  $v \in \sem{\mathbb{G}}$. Consider an arbitrary cycle
  $x_1 \to x_2 \to \cdots \to x_n \to x_{n+1}=x_1$ in $\mathbb{G}$. As
  $v \in \sem{\mathbb{G}}$, we have $v(x_{i+1} - x_i) \mathrel{\triangleleft}_i c_i$
  where $(\mathrel{\triangleleft}_i, c_i)$ is the weight of $x_i \to x_{i+1}$. That is,
  $(\le, v(x_{i+1} - x_i)) \le (\mathrel{\triangleleft}_i, c_i)$. Adding up the left
  hand sides gives $(\leq,\infty)$ or $(\le, 0)$, and as the cycle is negative, 
  adding up the right hand sides gives a weight $(\mathrel{\triangleleft}, c) < (\le, 0)$, which is a
  contradiction. This shows there is no negative cycle.

  Suppose all cycles in $\mathbb{G}$ are non-negative. Canonicalizing
  $\mathbb{G}$ does not introduce negative cycles. Hence without loss
  of generality, we can assume that $\mathbb{G}$ is canonical. We will
  construct a valuation $v$ in $\sem{\mathbb{G}}$ by fixing values for
  each clock one by one. To start, pick some clock $x$ and consider
  the edges $0 \xra{\mathrel{\triangleleft}_{0x}~c_{0x}} x$ and $x \xra{\mathrel{\triangleleft}_{x0}
    ~c_{x0}} 0$.  Since the cycle $0 \to x \to 0$ is non-negative, we
  have $0 \le c_{0x} + c_{x0}$, and if $c_{0x} + c_{x0} = 0$, then
  both $\mathrel{\triangleleft}_{0x}$ and $\mathrel{\triangleleft}_{x0}$ are $\le$. Notice that for every
  possible values for these weights, we can find a $\alpha \in \mathbb{R}
  \cup \{+\infty, -\infty\}$ such that $(\le, 0) \le (\le, \alpha) +
  (\mathrel{\triangleleft}_{x0}, c_{x0})$ and $(\le, 0) \le (\le, -\alpha) + (\mathrel{\triangleleft}_{0x},
  c_{0x})$. Then from Lemma \ref{lem:fixing-values-distance-graph}, replacing $0 \to x$ and $x \to 0$ with
  $(\le, \alpha)$ and $(\le, -\alpha)$ respectively gives a graph $\mathbb{G}'$
  with no negative cycles. For every $v \in \sem{\mathbb{G}'}$, we
  have $v(x) = \alpha$. Canonicalize $\mathbb{G}'$ and repeat the process
  with the new canonical graph to fix another variable, until all
  variables get fixed. 
\end{proof}

\subparagraph{Successor computation}
To implement the computation of transitions
$(q, Z) \xra{t} (q_1, Z_1)$ in an event zone graph, we will make use
of some operations on event zones that we define below. 
Using distance graphs, we show that these operations preserve event zones, that is, starting from an event zone and applying any of the operations leads to an event zone again. Thanks to the algebra over the new weights that we have defined, the arguments are very similar to the case of standard timed automata.


\begin{definition}[\textbf{Operations on event zones}]
  Let $g$ be a guard and $Z$ an
  event zone.
  \begin{itemize}
  \item Guard intersection:
    $Z \wedge g := \{v \mid v \in Z \text{ and } v \models g\}$

  \item Release: $[\ora{a}]Z= \bigcup_{v\in Z} [\ora{a}]v$

  \item Reset: $[\ola{a}]Z=\{[\ola{a}]v\mid v\in Z\}$

  \item Time elapse:
    $\elapse{Z} = \{v+\d \mid v\in Z, \d\in\RR_{\ge 0} \text{ s.t.\ }
    v+\d\models \bigwedge_{a\in\Sigma} \ora{a} \leq 0 \}$
  \end{itemize}
\end{definition}

A guard $g$ can be seen as yet another event zone and hence guard
intersection is just an intersection operation between two event
zones. 
By definition, for a transition $t:=(q, a, g, q')$ and a node $(q,Z)$ the
successor $(q, Z) \xra{t} (q',Z')$
can be computed in the following sequence:
\begin{align*}
  Z_1 := Z \cap (0 \le \ora{a}) \qquad Z_2 := [\ora{a}]Z_1 \qquad  Z_3 :=
  Z_2 \cap g \qquad Z_4 := [\ola{a}]Z_3 \qquad Z' := \elapse{Z_4}
\end{align*}
As an example, in Figure~\ref{fig:succ-computation}, suppose an action $b$ with
guard $\ora{a}=-1$ ($\ora{a}\leq -1 \wedge -1 \leq \ora{a}$) is fired from Zone $Z$ as
depicted, applying the above sequence in order gives $Z_1,Z_2,Z_3,Z_4$ resulting in the
successor zone $Z'$, as depicted in the figure.

We will now translate the operations from event zones to distance
graphs.

\begin{definition}[\textbf{Operations on distance graphs}]\label{defn:dist-graph-ops}
  Let $\mathbb{G}$ be a distance graph in canonical form. Let $g$ be a
  guard.
  \begin{itemize}
  \item Guard intersection: a distance graph $\mathbb{G}_g$ is
    obtained from $\mathbb{G}$ as follows,
    \begin{itemize}
    \item for each atomic constraint $x \mathrel{\triangleleft} c$ in $g$, replace
      weight of edge $0 \to x$ with the minimum of its weight in
      $\mathbb{G}$ and $(\mathrel{\triangleleft}, c)$,
    \item for each atomic constraint $d \mathrel{\triangleleft} y$ in $g$, replace
      weight of edge $y \to 0$ with the minimum of its weight in
      $\mathbb{G}$ and $(\mathrel{\triangleleft}, -d)$,
    \item canonicalize the resulting graph.
    \end{itemize}
  \item Release: a distance graph $[\ora{a}]\mathbb{G}$ is obtained
    from $\mathbb{G}$ by
    \begin{itemize}
    \item removing all edges involving $\ora{a}$ and then
    \item adding the edges $0 \xra{(\leq,0)} \ora{a}$ and
      $\ora{a} \xra{(\leq,\infty)} 0$, and then
    \item canonicalizing the resulting graph.
    \end{itemize}
  \item Reset: a distance graph $[\ola{a}]\mathbb{G}$ is obtained from
    $\mathbb{G}$ by
    \begin{itemize}
    \item removing all edges involving $\ola{a}$ and then
    \item adding the edges $0 \xra{(\leq,0)} \ola{a}$ and
      $\ola{a} \xra{(\leq, 0)} 0$, and then
    \item canonicalizing the resulting graph.
    \end{itemize}
  \item Time elapse: the distance graph $\elapse{\mathbb{G}}$ is
    obtained by the following transformation:
    \begin{itemize}
    \item if $\ola{x}$ is defined, i.e., the weight of
      $0 \xra{} \ola{x}$ is not $(\leq,\infty)$, then replace it with
      $(<,\infty)$,
      
    \item if $\ora{x}$ is defined, i.e., the weight of
      $0 \xra{} \ora{x}$ is not $(\leq,-\infty)$, then replace it with
      $(\leq,0)$,

    \item canonicalize the resulting graph.
    \end{itemize}
  \end{itemize}
\end{definition}

We prove below that the operations on distance graphs given in Definition~\ref{defn:dist-graph-ops} correspond to the operations on event zones: Lemma~\ref{lem:guard}, Lemma~\ref{lem:release}, Lemma~\ref{lem:reset} and Lemma~\ref{lem:time-elapse-prop}. 
Other than canonicalization, it can be easily checked that these operations can be computed in quadratic time. 
We discuss the canonicalization procedure in the stated lemmas.


  \begin{lemma}\label{lem:guard}
    Let $Z$ be an event zone defined by its distance graph $\graph{Z}$, and let $g$ be a
    guard.  Then 
    $\sem{\mathbb{G}_g} = Z\wedge g$.
  \end{lemma}
  \begin{proof}
    According to the definition, we first replace edges of the form $0
    \to x$ and $x \to 0$ depending on the guards present. It is easy
    to see that the set of valuations that satisfy the constraints
    given by this intermediate graph satisfy both $Z$ and
    $g$. The canonicalization process does not change the solution
    set. Since $g$ has only non-diagonal constraints and $\graph{Z}$ is canonical, we can check if
    there is a negative cycle of the form $x \to 0 \to y \to x$ in
    quadratic time. If not, one can first
    compute all shortest paths $x \to 0$ and $0 \to x$ and then taking
    $x \to y$ as the sum of the new $x \to 0$ and $0 \to y$ edges. The
    shortest path $x \to 0$ is obtained by taking
    $\min(x \to z + z \to 0)$ over all $z \to 0$ that comes from a
    guard. Similarly the shortest path $0 \to x$ is $\min(0 \to z + z
    \to x$ over all $0 \to x$ coming from a guard. 
  \end{proof}
  
  

  \begin{lemma}\label{lem:release}
    Let $Z$ be an event zone and $\mathbb{G}$ be its distance graph in canonical form. Let 
    $a\in\Sigma$.  Then, $\sem{[\ora{a}]\mathbb{G}}=[\ora{a}]Z$.
    
    Then, the weight of the edges in $[\ora{a}]\mathbb{G}$ are given by
    \begin{itemize}
      \item $x \to y$ has weight $\mathbb{G}_{xy}$, if $x,y \neq \ora{a}$,
      \item $\ora{a} \to x$ has weight $(\leq,\infty)$ and
      $x \to \ora{a}$ has weight $\mathbb{G}_{x0}$ if $x\neq\ora{a}$.
    \end{itemize}
  \end{lemma}
  
  \begin{proof}
    The release of a prophecy clock $\ora{a}$ corresponds to removing all edges involving
    the node $\ora{a}$, and then setting it to unsure by adding the edges $0 \xra{(\leq,0)}
    \ora{a}$ and $\ora{a} \xra{(\leq,\infty)} 0$.
    Let $\mathbb{G}'$ be the distance graph thus obtained from $\mathbb{G}$. It is
    easy to see $[\ora{a}]Z \subseteq \sem{[\ora{a}\mathbb{G}]}$. Now, pick $v
    \in \sem{[\ora{a}]\mathbb{G}}$. We claim that there exists some $u
    \in \sem{\mathbb{G}}$ such that $u$ coincides with $v$ in all variables
    except $\ora{a}$. To see this, replace every $x \to y$ with
    $\min(\mathbb{G}_{xy}, (\le,
    v(y -
    x)))$ for all $x, y \neq \ora{a}$. But $\min(\mathbb{G}_{xy}, (\le,
    v(y -
    x))) = (\le, v(y - x)$ since the same edge is present in $\mathbb{G}'$
    and $v$ satisfies the corresponding constraint there. So, in this
    graph, every edge 
    involving $\ora{a}$ comes from $\mathbb{G}$ and the other edges come from
    $v$. Suppose there is a negative cycle in this graph. We can first
    reduce it to $\ora{a} \to x \to y \to \ora{a}$, with $\ora{a} \to
    x$ and $y \to \ora{a}$ coming from $\mathbb{G}$. This will imply that $v$
    does not satisfy the $\mathbb{G}_{yx}$ constraint, but that is a
    contradiction. 


    Then, $[\ora{a}]\mathbb{G}$ is obtained by canonicalization of $\mathbb{G}'$. Observe that the weight of no edge was decreased: $\mathbb{G}_{0\ora{a}}\leq(\leq,0)$ 
    and $\mathbb{G}_{\ora{a}0}\leq(\leq,\infty)$.
    Therefore, this transformation does not lead to shorter paths: 
    the edge $x \to y$ in $[\ora{a}]\mathbb{G}$ has weight $\mathbb{G}'_{xy}=\mathbb{G}_{xy}$ if $x\neq\ora{a}\neq y$.
    Now, non-trivial paths in $\mathbb{G}'$ starting from $\ora{a}$ start with weight 
    $(\leq,\infty)$, hence $\mathbb{G}'_{\ora{a}x}=(\leq,\infty)$ if $x\neq\ora{a}$.
    Finally, a path in $\mathbb{G}'$ from $x\neq\ora{a}$ to $\ora{a}$ consists of 
    a path from $x$ to $0$ in $\mathbb{G}$ followed by the edge $0\to\ora{a}$ in 
    $\mathbb{G}'$. We deduce that the weight of the edge $x \to \ora{a}$ in $[\ora{a}]\mathbb{G}$ is equal to $\mathbb{G}_{x0}+(\leq,0)$.  
  \end{proof}
  
  \begin{lemma}\label{lem:reset}
    Let $Z$ be an event zone and $\mathbb{G}$ be its distance graph in canonical form. Let 
    $a\in\Sigma$.  Then, $\sem{[\ola{a}]\mathbb{G}}=[\ola{a}]Z$.
    
    Then, the weight of the edges in $[\ola{a}]\mathbb{G}$ are given by
    \begin{itemize}
      \item $x \to y$ has weight $\mathbb{G}_{xy}$, if $x,y \neq \ola{a}$,
      \item $x \to \ola{a}$ has weight $\mathbb{G}_{x0}$ and
      $\ola{a} \to x$ has weight $\mathbb{G}_{0x}$ if $x\neq\ola{a}$ (including $x=0$).
    \end{itemize}
  \end{lemma}
  
  \begin{proof}
    The reset of a history clock $\ola{a}$ corresponds to removing all edges involving the
    node $\ola{a}$, and then setting its value to $0$ by adding the edges $0 \xra{(\leq,0)}
    \ola{a}$ and $\ola{a} \xra{(\leq, 0)} 0$.
    Let $\mathbb{G}'$ be the distance graph thus obtained from $\mathbb{G}$. Similar
    to timed automata it can be shown that $\sem{\mathbb{G}'} = [\ola{a}]Z$.   
    

Then, $[\ola{a}]\mathbb{G}$ is obtained by canonicalization of $\mathbb{G}'$.
Canonicalization does not affect the weight of the edges $x\to y$ if $x,y\neq\ola{a}$
    (as any path from $x$ to $y$ in $\mathbb{G}'$ using the new edges would involve a cycle
    $\ola{a}\to 0\to\ola{a}$ or $0\to\ola{a}\to 0$ of weight $0$).  
    Thus, the weight of the edge $x \to y$ in $[\ola{a}]\mathbb{G}$ is equal to $\mathbb{G}_{xy}$ if $x,y \neq \ola{a}$.
    Now, paths in $\mathbb{G}'$ from $x\neq\ola{a}$ to $\ola{a}$ ends with the edge $0\to\ola{a}$ of weight $(\leq,0)$. So, for $x\neq\ola{a}$, we deduce that the weight of  the edge $x \to \ola{a}$ in $[\ola{a}]\mathbb{G}$ is given by $\mathbb{G}'_{x\ola{a}}=\mathbb{G}_{x\ola{a}}$.  
    Similarly, we can see that the weight of  the edge $\ola{a} \to x$ in $[\ola{a}]\mathbb{G}$ is given by $\mathbb{G}'_{\ola{a}x}=\mathbb{G}_{\ola{a}x}$.
  \end{proof}
  

\begin{lemma}\label{lem:time-elapse-prop}
  Let $Z$ be a non-empty event zone and $\mathbb{G}$ be its distance graph in canonical form.
  Then, $\sem{\elapse{\mathbb{G}}}=\elapse{Z}$.
  
  Then, the weight of the edges in $\elapse{\mathbb{G}}$ are given by
  \begin{itemize}
    \item $x \to y$ has weight $\mathbb{G}_{xy}$, if $x\neq 0$,
    \item $0 \to y$ is defined as :
    \begin{align*}
      \elapse{\mathbb{G}}_{0y} & ~=~ (\leq,\infty) ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ \text{if } G_{0y} = (\leq, \infty) \\
                & ~=~ \displaystyle \min \{(<, \infty), \displaystyle \min_{\ora{x} \in X_{P}} \mathbb{G}_{\ora{x}y}\} ~~~~~~~\text{if $G_{0y} \neq (\leq, \infty)$ and $y$ is a history clock} \\
                & ~=~ \displaystyle \min \{(\leq, 0), \displaystyle \min_{\ora{x} \in X_{P}} \mathbb{G}_{\ora{x}y}\} ~~~~~~~~\text{$y$ is a prophecy clock} 
    \end{align*}
    In particular, $\mathbb{G}_{0y}\leq\elapse{\mathbb{G}}_{0y}$.
  \end{itemize}
\end{lemma}


\begin{proof}
  The time elapse operation corresponds to (1) replacing the weight of
  $0 \xra{} \ola{x}$ with $(<,\infty)$ if it is not $(\leq,\infty)$, and (2) replacing the weight of $0 \xra{} \ora{x}$ with $(\leq,0)$ if it is not $(\leq,-\infty)$
  Let $\mathbb{G}'$ be the distance graph thus obtained from $\mathbb{G}$.  Similar
  to timed automata it can be shown that $\sem{\mathbb{G}'} = \elapse{Z}$.


  Then, $\elapse{\mathbb{G}}$ is obtained by canonicalization of $\mathbb{G}'$.

  Observe that $\mathbb{G}'$ need not be canonical. 
  The transformation from $\mathbb{G}$ to $\mathbb{G}'$ does not decrease the weight of edges, 
  it may only increase the weight of edges from $0$ to $x$.
  Therefore, no shorter paths may be obtained by this transformation.  We deduce that, for
  all clocks $y$, $\elapse{\mathbb{G}}_{xy}=\mathbb{G}'_{xy}=\mathbb{G}_{xy}$ if $x\neq0$ and
  $\mathbb{G}_{0y}\leq\elapse{\mathbb{G}}_{0y}\leq\mathbb{G}'_{0y}$.

  Let $\ora{x}$ be a prophecy clock s.t.\ the weight $\mathbb{G}_{\ora{x}y}$ is minimum. 
  We show that weight of the edge $0 \to y$ in $\elapse{\mathbb{G}}$, given by the new shortest path in $\mathbb{G}'$ from $0$ to $y$ is $0 \xra{(\leq,0)} \ora{x} \xra{\mathbb{G}_{\ora{x}y}} y$. 
  
  Suppose that there was a (shorter) path in $\mathbb{G}'$ of the form $0 \xra{(\leq,0)} \ora{z} \xra{(\triangleleft,d')} \ora{w} \xra{(\triangleleft,d)} y$. 
  This implies that $(\triangleleft,d') + (\triangleleft,d) < \mathbb{G}_{\ora{x}y}$.
  However, since $\mathbb{G}$ is canonical, we have
  $\mathbb{G}_{\ora{z}x} \leq (\triangleleft,d') + (\triangleleft,d)< \mathbb{G}_{\ora{x}y}$.
  This contradicts our assumption that $\ora{x}$ was the prophecy clock s.t.\ the weight $G_{\ora{x}y}$ is minimum. 
\end{proof}

We are now ready to state Theorem~\ref{thm:distance-graph-operations} that says that the operations on event zones translate easily to operations on distance graphs and that the successor of an event zone is an event zone. 
Note that, except for the release operation $[\ola{a}]$, the rest of the operations are standard in timed automata, but they do not use $(\le, +\infty), (\le, -\infty)$. 
We show that we can perform all these operations in the new algebra
with quadratic complexity, as in timed automata
without diagonal constraints~\cite{DBLP:journals/ipl/ZhaoLZ05}.


\begin{restatable}{theorem}{thmDistanceGraphOperations}  
  \label{thm:distance-graph-operations}
  Let $Z$ be an event zone and $\mathbb{G}$ be its canonical distance graph. 
  Let $g$ be a guard.  We can compute, in $\mathcal{O}(|X_P \cup X_H|^2)$ time, distance graphs 
  $\mathbb{G}_g$, $[\ora a]\mathbb{G}$, $[\ola a]\mathbb{G}$ and $\elapse{\mathbb{G}}$ in canonical form, such that
  $Z \land g = \sem{\mathbb{G}_g}$,
  $[\ora a]Z = \sem{[\ora a]\mathbb{G}}$,
  $[\ola a]Z = \sem{[\ola a]\mathbb{G}}$, and
  $\elapse{Z} = \sem{\elapse{\mathbb{G}}}$.
\end{restatable}

\begin{figure}
  \centering	
	\scalebox{0.8}{
      \begin{tikzpicture}
      [state/.style={draw, thick, circle, inner sep=4pt}]
      \begin{scope}[xshift=-1cm, yshift=0cm]      
      \begin{scope}[xshift=0cm, yshift=0cm, zone/.style={draw,rectangle,minimum width=2.1cm, minimum height=2.4cm, rounded corners}]
        \node [zone] (z0) at (0, 0) {}; 
        \node [zone] (z1) at (3, 0) {};
        \node [zone] (z2) at (6, 0) {}; 
        \node [zone] (z3) at (9, 0) {};
        \node [zone] (z4) at (12, 0) {};
        \node [zone] (z5) at (15, 0) {};
      \end{scope}
  
      \begin{scope}[->, >=stealth, thick]
      \draw (z0) to (z1); 
      \draw (z1) to (z2);
      \draw (z2) to (z3);
      \draw (z3) to (z4);
      \draw (z4) to (z5);
      \end{scope}

      \node at (0, -1.6) {$Z$}; 
      \node at (3, -1.6) {$Z_1$}; 
      \node at (6, -1.6) {$Z_2$}; 
      \node at (9, -1.6) {$Z_3$}; 
      \node at (12, -1.6) {$Z_4$}; 
      \node at (15, -1.6) {$Z'$}; 

      \node at (0, 0.25) {\scriptsize $\ora{a} \leq 0~~\ola{a} = \infty$}; 
      \node at (0, -0.25) {\scriptsize $\ora{b} \leq 0~~\ola{b} = \infty$}; 


      \node at (3, 0.5) {\scriptsize $\ora{a} \leq 0~~\ola{a} = \infty$}; 
      \node at (3, 0) {\scriptsize $\ora{b} = 0~~\ola{b} = \infty$}; 
      \node at (3, -0.5) {\scriptsize $\ora{a} - \ora{b} \leq 0$}; 

      \node at (6, 0.25) {\scriptsize $\ora{a} \leq 0~~\ola{a} = \infty$}; 
      \node at (6, -0.25) {\scriptsize $\ora{b} \leq 0~~\ola{b} = \infty$}; 


      \node at (9, 0.5) {\scriptsize $\ora{a}=-1~~\ola{a} = \infty$}; 
      \node at (9, 0) {\scriptsize $\ora{b} \leq 0~~\ola{b} = \infty$}; 
      \node at (9, -0.5) {\scriptsize $\ora{b} - \ora{a} \leq 1$}; 


      \node at (12, 0.8) {\scriptsize $\ora{a}=-1~~\ola{a} = \infty$}; 
      \node at (12, 0.4) {\scriptsize $\ora{b} \leq 0~~\ola{b} = 0$}; 
      \node at (12, 0) {\scriptsize $\ora{b} - \ora{a} \leq 1$}; 
      \node at (12, -0.4) {\scriptsize $\ola{b} - \ora{a} = 1$}; 
      \node at (12, -0.8) {\scriptsize $\ora{b} - \ola{b} \leq 0$}; 

      \node at (15, 1) {\scriptsize $-1 \leq \ora{a} \leq 0$}; 
      \node at (15, 0.6) {\scriptsize $0 \leq \ola{b} \leq 1$}; 
      \node at (15, 0.2) {\scriptsize $\ora{b} \leq 0~~\ola{a} = \infty$}; 
      \node at (15, -0.2) {\scriptsize $\ora{b} - \ora{a} \leq 1$}; 
      \node at (15, -0.6) {\scriptsize $\ola{b} - \ora{a} = 1$}; 
      \node at (15, -1) {\scriptsize $\ora{b} - \ola{b} \leq 0$}; 
    \end{scope}

    \end{tikzpicture} 
  }
  \caption[]{Successor computation from event zone $Z$ on an action $b$ with guard $\ora{a}=-1$}
  \label{fig:succ-computation}
\end{figure}

\section{A concrete simulation relation for ECAs}\label{sec:simulation}
We fix an event-clock automaton $\mathcal{A}=(Q,\Sigma,X,T,q_0,F)$ for this section. We will define a simulation relation $\preceq_{\mathcal{A}}$ on the configurations of the ECA.
We first define a map $\mathcal{G}$ from $Q$  to sets of atomic constraints.
The map $\mathcal{G}$ is obtained as the least fixpoint of the set of equations:
$$
\mathcal{G}(q) = \{\ora{b}\leq0, 0\leq\ora{b} \mid b\in\Sigma\} \cup
\bigcup_{(q,a,g,q')\in T} \mathsf{split}(g) \cup \pre{a}{\mathcal{G}(q')}
$$
where $\mathsf{split}(g)$ is the set of atomic constraints occurring in $g$ and, for a set of 
atomic constraints $G$, $\pre{a}{G}$ is defined as the set of constraints 
in $G$ except those on $\ora{a}$ or $\ola{a}$.
Notice that constraints in $\mathcal{G}(q)$ use the constant $0$ and constants used in constraints of $\mathcal{A}$.

Let $G$ be a set of atomic constraints. The preorder $\preceq_{G}$ is 
defined on valuations by
$$
v\preceq_{G}v' \qquad \text { if }
\forall\varphi\in G,~\forall\delta\geq0,\qquad v+\delta\models\varphi
\implies v'+\delta\models\varphi \,.
$$
Notice that in the condition above, we \emph{do not} restrict $\delta$ to those such that 
$v+\delta$ is a valuation: we may have $v(\ora{a})+\delta>0$ for some
$a\in\Sigma$.
This is crucial for the proof of Theorem~\ref{thm:simulation} below.
It also allows to get a clean characterizations of the simulation
(Lemma~\ref{lem:simulation-properties}) which in turn is useful for deriving the
simulation test and in showing finiteness.
Based on $\preceq_G$ and the $\mathcal{G}(q)$ computation, we can define a preorder $\preceq_{\mathcal{A}}$
between configurations of ECA $\mathcal{A}$ as $(q,v)\preceq_{\mathcal{A}}(q',v')$ if $q=q'$ and
$v\preceq_{\mathcal{G}(q)}v'$.

\begin{restatable}{theorem}{thmSimulation}
  \label{thm:simulation}
  The relation $\preceq_{\mathcal{A}}$ is a simulation on the transition system $S_{\mathcal{A}}$ of
  ECA $\mathcal{A}$.
\end{restatable}


\begin{proof}
  Assume that $(q,v_{1})\preceq_{\mathcal{A}}(q,v_{2})$, i.e., $v_{1}\preceq_{\mathcal{G}(q)}v_{2}$.
  \begin{description}
    \item[Delay transition]  Assume that $(q,v_{1})\xra{\delta}(q,v_{1}+\delta)$ is a 
    transition of $S_{\mathcal{A}}$. Then, $v_{1}+\delta\models\bigwedge_{x\in\Sigma}\ora{x}\leq0$.
    Since $\mathcal{G}(q)$ contains $\ora{x}\leq0$ for all $x\in\Sigma$ and 
    $v_{1}\preceq_{\mathcal{G}(q)}v_{2}$, we deduce that 
    $v_{2}+\delta\models\bigwedge_{x\in\Sigma}\ora{x}\leq0$.
    Therefore, $(q,v_{2})\xra{\delta}(q,v_{2}+\delta)$ is a transition in $S_{\mathcal{A}}$.
    It is easy to see that $v_{1}+\delta\preceq_{\mathcal{G}(q)}v_{2}+\delta$.
  
    \item[Action transition]  
    Let $t=(q,g,a,q')$ be a transition in $\mathcal{A}$ and assume that 
    $(q,v_{1})\xra{t}(q',v'_{1})$ is a transition in $S_{\mathcal{A}}$, i.e.,
    $v_{1}\models 0\leq\ora{a}$ and for some $v''_{1}\in[\ora{a}]v_{1}$ we have 
    $v''_{1}\models g$ and $v'_{1}=[\ola{a}]v''_{1}$. 
    Since $\mathcal{G}(q)$ contains $0\leq\ora{a}$ and $v_{1}\preceq_{\mathcal{G}(q)}v_{2}$, we deduce that
    $v_{2}\models 0\leq\ora{a}$.
   
    We have $v''_{1}=v_{1}[\ora{a}\mapsto\alpha]$ for some $\alpha\in[-\infty,0]$
    and
    $v'_{1}=v''_{1}[\ola{a}\mapsto 0]=v_{1}[\ola{a}\mapsto 0,\ora{a}\mapsto\alpha]$.
    Define $v''_{2}=v_{2}[\ora{a}\mapsto\alpha]\in[\ora{a}]v_{2}$ and
    $v'_{2}=v''_{2}[\ola{a}\mapsto 0]=v_{2}[\ola{a}\mapsto 0,\ora{a}\mapsto\alpha]$.
    From $v_{1}\preceq_{\mathcal{G}(q)}v_{2}$ and the definition of $v''_{2}$, we
    deduce that $v''_{1}\preceq_{\mathcal{G}(q)}v''_{2}$.
    Since $\mathcal{G}(q)$ contains $\mathsf{split}(g)$, and 
    $v''_{1}\preceq_{\mathcal{G}(q)}v''_{2}$, we deduce that $v''_{2}\models g$.

    Therefore, $(q,v_{2})\xra{t}(q',v'_{2})$ is a transition in $S_{\mathcal{A}}$.
    Since $\mathcal{G}(q)$ contains $\pre{a}{\mathcal{G}(q')}$, we easily get from 
    $v_{1}\preceq_{\mathcal{G}(q)}v_{2}$ and the definitions of $v'_{1},v'_{2}$ that
    $v'_{1}\preceq_{\mathcal{G}(q')}v'_{2}$.
    Note that, to get this, we crucially use the fact that in the definition of the
    simulation $\preceq_{G}$ we consider \emph{all} $\delta\geq0$ and not only those such
    that $v+\delta$ is a valuation.
    \qedhere
  \end{description}
\end{proof}


When $G=\{\varphi\}$ is a singleton, we simply write $\preceq_{\varphi}$ for 
$\preceq_{\{\varphi\}}$.
The definition of the $\preceq_{G}$ simulation above in some
  sense  declares
   what is expected out of the simulation. Below, we give a constructive characterization of the simulation in terms of
the constants used and the valuations. For example, if
$v(\ola{a}) = 3$ and $\ola{a} \le 5$ is a constraint in $G$, point $2$
below says that all $v'$ with $v'(\ola{a}) \le 3$ simulate $v$. The
next lemma 
is
a generalization of Lemma 8 from
\cite{Gastin0S20} to our setting containing prophecy clocks and the
undefined values $+\infty$ and $-\infty$.

\begin{restatable}{lemma}{lemSimulationProperties} 
  \label{lem:simulation-properties}
  Let $v,v'$ be valuations and $G$ a set of atomic constraints. We have
  \begin{enumerate}
    \item  $v\preceq_{G}v'$ iff $v\preceq_{\varphi}v'$ for all $\varphi\in G$.
  
    \item  $v\preceq_{x\mathrel{\triangleleft} c}v'$ iff
    $v(x)\not\mathrel{\triangleleft} c$ or 
    $v'(x)\leq v(x)$ or
    $(\mathrel{\triangleleft},c)=(\leq,\infty)$ or
    $(\mathrel{\triangleleft},c)=(<,\infty)\wedge v'(x)<\infty$.
  
    \item  $v\preceq_{c\mathrel{\triangleleft} x}v'$ iff
    $c\mathrel{\triangleleft} v'(x)$ or 
    $v(x)\leq v'(x)$ or 
    $(c,\mathrel{\triangleleft})=(\infty,<)$ or
    $(c,\mathrel{\triangleleft})=(\infty,\leq)\wedge v(x)<\infty$.
  \end{enumerate}
\end{restatable}

\begin{proof}
  \begin{enumerate}
    \item  is clear.
  
    \item  The right to left implication is easy. Notice for instance that if 
    $(\mathrel{\triangleleft},c)=(<,\infty)$ and $v'(x)<\infty$ then for all $\delta\geq0$ we have 
    $v'+\delta\models x<\infty$. 
    
    Conversely, assume that $v\preceq_{x\mathrel{\triangleleft} c}v'$ and $v(x)\mathrel{\triangleleft} c$ and
    $(\mathrel{\triangleleft},c)\neq(\leq,\infty)$.
    If $(\mathrel{\triangleleft},c)=(<,\infty)$ then, using $\delta=0$ and $v(x)\mathrel{\triangleleft} c$, we get $v'(x)<\infty$.
    If $(\mathrel{\triangleleft},c)=(\leq,-\infty)$ then, using $\delta=0$ and $v(x)\mathrel{\triangleleft} c$,
    we get $v'(x)\leq-\infty=v(x)$.
    Otherwise, $c\in\mathbb{Z}$ and we have to show that $v'(x)\leq v(x)$.
    Assume that $v(x)<v'(x)$. Then, we find $\delta\geq0$ such that $v(x)+\delta\mathrel{\triangleleft} c 
    <v'(x)+\delta$, a contradiction.
  
    \item Again, the right to left implication is easy.  Notice that in the last two 
    cases, $(c,\mathrel{\triangleleft})=(\infty,<)$ or $(\mathrel{\triangleleft},c)=(\infty,\leq)\wedge v(x)<\infty$, then 
    for all $\delta\geq0$ we have $v+\delta\not\models c\mathrel{\triangleleft} x$.
    
    Conversely, assume that $v\preceq_{c\mathrel{\triangleleft} x}v'$ and $c\not\mathrel{\triangleleft} v'(x)$ and 
    $(c,\mathrel{\triangleleft})\neq(\infty,<)$.
    If $(c,\mathrel{\triangleleft})=(\infty,\leq)$ then, using $\delta=0$ and $c\not\mathrel{\triangleleft} v'(x)$, we get
    $c\not\mathrel{\triangleleft} v(x)$, i.e., $v(x)<\infty$.
    If $(c,\mathrel{\triangleleft})=(-\infty,<)$ then, using $\delta=0$ and $c\not\mathrel{\triangleleft} v'(x)$, we get
    $c\not\mathrel{\triangleleft} v(x)$, i.e., $v(x)=-\infty=v'(x)$.
    Otherwise, $c\in\mathbb{Z}$ and we have to show that $v(x)\leq v'(x)$.
    Assume that $v'(x)<v(x)$. Then, we find $\delta\geq0$ such that $c\mathrel{\triangleleft} v(x)+\delta$ 
    but $c\not\mathrel{\triangleleft} v'(x)+\delta$, a contradiction.
    \qedhere
  \end{enumerate}
\end{proof}

We now state some useful properties that get derived from
    Lemma~\ref{lem:simulation-properties}.
  
\begin{remark}\label{rem:simulation properties}
  Let $v,v'$ be valuations and $G$ a set of atomic constraints.
  \begin{enumerate}
    \item For all $a\in\Sigma$, if $\{0\leq\ora{a},\ora{a}\leq0\}\subseteq G$ and
    $v\preceq_{G}v'$ then $v(\ora{a})=v'(\ora{a})$.
  
    \item Let $x\mathrel{\triangleleft}_{1} c_{1}$ and $x\mathrel{\triangleleft}_{2} c_{2}$ be constraints with
    $(\mathrel{\triangleleft}_{1},c_{1})\leq(\mathrel{\triangleleft}_{2},c_{2})<(<,\infty)$ 
    (we say that $x\mathrel{\triangleleft}_{1} c_{1}$ is subsumed by $x\mathrel{\triangleleft}_{2} c_{2}$).
    If $v\preceq_{x\mathrel{\triangleleft}_{2} c_{2}}v'$ then $v\preceq_{x\mathrel{\triangleleft}_{1} c_{1}}v'$.
    
    Indeed, from $(\mathrel{\triangleleft}_{2},c_{2})<(<,\infty)$ and $v\preceq_{x\mathrel{\triangleleft}_{2} c_{2}}v'$ we
    get $v'(x)\leq v(x)$ or $v(x)\not\mathrel{\triangleleft}_{2} c_{2}$, which implies
    $v(x)\not\mathrel{\triangleleft}_{1}c_{1}$ since $(\mathrel{\triangleleft}_{1},c_{1})\leq(\mathrel{\triangleleft}_{2},c_{2})$.
  
    \item Let $c_{1}\mathrel{\triangleleft}_{1} x$ and $c_{2}\mathrel{\triangleleft}_{2} x$ be constraints with
    $(c_{1},\mathrel{\triangleleft}_{1})\leq(c_{2},\mathrel{\triangleleft}_{2})<(\infty,\leq)$
    (we say that $c_{1}\mathrel{\triangleleft}_{1} x$ is subsumed by $c_{2}\mathrel{\triangleleft}_{2} x$).
    If $v\preceq_{c_{2}\mathrel{\triangleleft}_{2} x}v'$ then $v\preceq_{c_{1}\mathrel{\triangleleft}_{1} x}v'$.

    Indeed, from $(c_{2},\mathrel{\triangleleft}_{2})<(\infty,\leq)$ and $v\preceq_{c_{2}\mathrel{\triangleleft}_{2} x}v'$ we
    get $v(x)\leq v'(x)$ or $c_{2}\mathrel{\triangleleft}_{2} v'(x)$, which implies
    $c_{1}\mathrel{\triangleleft}_{1} v'(x)$ since $(c_{1},\mathrel{\triangleleft}_{1})\leq(c_{2},\mathrel{\triangleleft}_{2})$.
    
    The ordering between \emph{lower weights} is defined by 
    $(c_{1},\mathrel{\triangleleft}_{1})<(c_{2},\mathrel{\triangleleft}_{2})$ if $c_{1}<c_{2}$ or $c_{1}=c_{2}$, 
    ${\mathrel{\triangleleft}}_{1}={\leq}$ and ${\mathrel{\triangleleft}}_{2}={<}$. We have 
    $(c_{1},\mathrel{\triangleleft}_{1})<(c_{2},\mathrel{\triangleleft}_{2})$ iff 
    $(\mathrel{\triangleleft}_{2},-c_{2})<(\mathrel{\triangleleft}_{1},-c_{1})$.
  \end{enumerate}
\end{remark}
Before lifting the simulation to event zones, we present a central
technical object that will be used from time to time in the next set
of results. 

  \subparagraph{Distance graph for valuations that simulate a valuation $v$.}\label{sec:distance graph for up G v}

For a valuation $v$, we let ${\uparrow}_{G}v=\{v'\in\mathbb{V} \mid v\preceq_{G} v'\}$, i.e., the set of valuations $v'$ which simulate $v$.  We will define a distance graph, denoted
$\graphv{G}{v}$, such that $\sem{\graphv{G}{v}}={\uparrow}_{G}v$. We remark that
$\sem{\graphv{G}{v}}$ is not really a zone since it may use constants that are not integers.

We assume that $G$ contains $\{0\leq\ora{a},\ora{a}\leq0 \mid a\in\Sigma\}$ so that 
$v\preceq_{G}v'$ implies $v(\ora{a})=v'(\ora{a})$ for all prophecy clocks $\ora{a}$ with 
$a\in\Sigma$.
We remove from $G$ constraints equivalent to true, such as $x\leq\infty$, $-3<\ola{a}$ or 
$0\leq\ola{a}$, or equivalent to false, such as $\ola{a}<0$ or $\infty<x$.
Also, by Remark~\ref{rem:simulation properties}, we may remove from $G$ constraints that 
are subsumed by other constraints in $G$, while not
changing the simulation relation. 
Hence, for history clocks, we have at most one upper-bound constraint $\ola{a}\mathrel{\triangleleft} c$ with
$(\leq,0)\leq(\mathrel{\triangleleft},c)<(<,\infty)$, and at most one lower-bound constraint $c\mathrel{\triangleleft}\ola{a}$
with $(0,\leq)<(c,\mathrel{\triangleleft})<(\infty,\leq)$.
From now on, we always assume that the sets $G$ of atomic constraints that we
consider satisfy the above conditions.

The definition of the distance graph $\graphv{G}{v}$ which
defines ${\uparrow}_{G}v$ is based on Lemma~\ref{lem:simulation-properties}.
\begin{itemize}
  \item For each prophecy clock $\ora{a}$, we have the edges $\ora{a}\xra{(\leq,-v(\ora{a}))}0$ and
  $0\xra{(\leq,v(\ora{a}))}\ora{a}$.

  \item  For each history clock $\ola{a}$, we have the edge $0\to\ola{a}$ with weight
  \begin{itemize}
    \item $(\leq,v(\ola{a}))$ if $\ola{a}\mathrel{\triangleleft} c\in G$ with $(\mathrel{\triangleleft},c)<(<,\infty)$ and
    $v(\ola{a})\mathrel{\triangleleft} c$,

  
    \item  $(<,\infty)$ if we are not in the case above and 
    $\ola{a}<\infty \in G$, $v(\ola{a})<\infty$,
  
    \item  $(\leq,\infty)$ otherwise.
  \end{itemize}

  \item  For each history clock $\ola{a}$, we have the edge $\ola{a}\to 0$ with weight
  \begin{itemize}
    \item $(\leq,-\infty)$ if $\infty\leq\ola{a} \in G$ and $v(\ola{a})=\infty$,
    and if we are not in this case:
  
    \item $(\mathrel{\triangleleft},-c)$ if $c\mathrel{\triangleleft}\ola{a}\in G$ with $(c,\mathrel{\triangleleft})<(\infty,\leq)$ and
    $c\mathrel{\triangleleft} v(\ola{a})$,

    \item $(\leq,-v(\ola{a}))$ if $c\mathrel{\triangleleft}\ola{a}\in G$ with $(c,\mathrel{\triangleleft})<(\infty,\leq)$
    and $c\not\mathrel{\triangleleft} v(\ola{a})$,

    \item $(\leq,0)$ otherwise.
  \end{itemize}
\end{itemize}
With this definition, while $\graphv{G}{v}$ is not in canonical form, it has the desired
property:

\begin{lemma}
  We have $v\preceq_{G} v'$ iff $v'$ satisfies all the constraints of $\graphv{G}{v}$.
\end{lemma}
\subparagraph{Simulation for event zones and an effective algorithmic check.}
Let $Z,Z'$ be two event zones and $G$ be a set of atomic constraints.
We say that $Z$ is $G$-simulated by $Z'$, denoted $Z\preceq_{G}Z'$, if for all $v\in Z$ 
there exists $v'\in Z'$ such that $v\preceq_{G}v'$. 
Finally, we define $(q,Z)\preceq_\mathcal{A} (q',Z')$ if $q=q'$ and $Z\preceq_{\mathcal{G}(q)} Z'$.  In the
rest of this section, we show how to check this relation efficiently.
We let ${\downarrow}_{G}Z=\{v\in\mathbb{V}\mid v\preceq_{G}v' \text{ for some } v'\in Z\}$.
Notice that $Z\preceq_{G}Z'$ iff $Z\subseteq{\downarrow}_{G}Z'$ iff ${\downarrow}_{G}Z={\downarrow}_{G}Z'$.



\begin{lemma}\label{lem:zone-non-simulation}
For event zones $Z,Z'$, we have $Z \not \preceq_{G}Z'$ iff
  $\exists v\in Z$ with ${\uparrow}_{G}v \cap Z' = \emptyset$.
\end{lemma}

To check $Z \not \preceq_G Z'$, we require a valuation $v \in Z$
  with a witness that ${\uparrow}_G{v} \cap Z'$ is empty. In the language of
  distance graphs,
  the witness will be a negative cycle in $\min({\uparrow}_G{v}, Z')$. We
  show that if ${\uparrow}_G{v} \cap Z'$ is empty, then there is a 
small witness, i.e., a negative cycle containing at most three edges, and belonging to one of three specific forms.

\begin{lemma}\label{lem:negative-cycles-v-Z}
  Let $v$ be a valuation, $Z'$ a non-empty reachable event zone
  with canonical 
  distance graph $\graph{Z'}$ and $G$ a set of atomic
  constraints. Then, ${\uparrow}_G v \cap Z'$ is empty iff there is a
  negative cycle in one of the following forms:
  \begin{enumerate}
  \item $0 \to x \to 0$ with $0\to x$ from $\graphv{G}{v}$ and
    $x \to 0$ from $\graph{Z'}$,
  \item $0 \to y \to 0$ with $0 \to y$ from $\graph{Z'}$ and $y \to 0$
    from $\graphv{G}{v}$, and
  \item $0 \to x \to y \to 0$, with weight of $x \to y$ from
    $\graph{Z'}$ and the others from $\graphv{G}{v}$. Moreover, this
    negative cycle has finite weight.
  \end{enumerate}
\end{lemma}
\begin{proof}
  Since $Z'\neq\emptyset$, the distance graph $\graph{Z'}$ has no negative cycle.  The same
  holds for $\graphv{G}{v}$ since $v\in{\uparrow}_{G}v\neq\emptyset$.  We know that ${\uparrow}_{G}v\cap
  Z'=\emptyset$ iff there is a (simple) negative cycle using edges from $\graphv{G}{v}$ and
  from $\graph{Z'}$.  Since $\graph{Z'}$ is in canonical form, we may restrict to negative
  cycles which do not use two consecutive edges from $\graph{Z'}$.  Now all edges of
  $\graphv{G}{v}$ are adjacent to node $0$.  Hence, if a simple cycle uses an edge from
  $\graph{Z'}$ which is adjacent to $0$, it consists of only two edges $0\to x\to 0$, one
  from $\graph{Z'}$ and one from $\graphv{G}{v}$. Otherwise, the simple cycle is of the 
  form $0\to x\to y\to 0$ where the edge $x\to y$ is from $\graph{Z'}$ and the other two 
  edges are from $\graphv{G}{v}$.
  It remains to show that the two clock negative cycle $0 \to x \to y \to 0$ can be
  considered to have finite weight, i.e., weight is not $(\le, -\infty)$.

  For the cycle to have weight $(\le, -\infty)$, one of the edges
  should have weight $(\le, -\infty)$ and the others should have a
  weight different from $(\le, \infty)$. We will show that for every
  such combination, there is a smaller negative cycle with a single
  clock and $0$. Hence we can ignore negative cycles of the form
  $0 \to x \to y \to 0$ with weight $(\le, -\infty)$.

  Suppose $Z'_{xy} = (\le, -\infty)$. Then, for every valuation
    in $u\in Z'$, we have $u(y) - u(x) \le -\infty$, which implies
    $u(y) = -\infty$ or $u(x) = +\infty$. If $u(x) = +\infty$ for some
    valuation $u \in Z'$, then the value of $x$ is $+\infty$ for every
    valuation in $Z'$. This follows from
    the successor computation: initially, history clocks are undefined, and
    then an action $a$ defines $\ola{a}$, and from that point onwards,
    $\ola{a}$ is always $< \infty$. Now, if $x$ is not an undefined
    history clock in $Z'$, then 
    we need to have $u(y) = -\infty$ for all valuations of $Z'$.
  Therefore, either
  $x$ is a history clock that is undefined in $Z'$ or $y$ is a
  prophecy clock that is undefined in $Z'$. In the former case,
  $Z'_{x0} = (\le, -\infty)$ and in the latter case
  $Z'_{0y} = (\le, -\infty)$. This gives a smaller negative cycle
  $0 \to x \xra{Z'_{x0}} 0$ or $0 \xra{Z'_{0y}} y \to 0$ with the
  remaining edge $0 \to x$ or $y \to 0$ coming from $\graphv{G}{v}$,
  since by our hypothesis of a negative cycle, these edges have
  weight different from $(\le, \infty)$.

  Suppose the weight of $0 \to x$ is $(\le, -\infty)$. This can
  happen only when $x$ is a prophecy clock, $v(x) = -\infty$ and
  weight of $0 \to x$ is $(\le, v(x))$. Since
  $Z'_{xy} \neq (\le, \infty)$, we infer  $Z'_{x0} \neq (\le, \infty)$ by
  $\dagger_1$ of Lemma~\ref{lem:dagger}.
  Hence
  $0 \xra{(\le, v(x))} x \xra{Z'_{x0}} 0$ is also a negative cycle.

  Suppose $y \to 0$ has weight $(\le, -\infty)$. This can happen only
  when $y$ is a history clock and $v(y)=+\infty$. Since $Z'_{xy} \neq (\le, \infty)$,
  we obtain $Z'_{0y} \neq (\le, \infty)$
  and hence $0 \xra{Z'_{0y}} y \xra{(\le, -v(y))} 0$ is a negative
  cycle.
\end{proof}
We now have all the results required to state our inclusion test.  Using the above
lemma, and relying on a careful analysis 
we obtain the following theorem.

\begin{restatable}{theorem}{thmSimulationCheck}
    \label{thm:simulation-check}
  Let $Z, Z'$ be non-empty reachable zones, and $G$ a set of atomic constraints
  containing $\ora{a} \le 0$ and $0 \le \ora{a}$ for every prophecy
  clock $\ora{a}$. Then, $Z \not \preceq_G Z'$ iff one of the
  following conditions holds:
  \begin{enumerate}
  \item $Z'_{x0} < Z_{x0}$ for some prophecy clock $x$, or for some
    history clock $x$ with
    \begin{itemize}
    \item $(x < \infty) \in G$ and $Z'_{x0} = (\le, -\infty)$, or
    \item $(x \mathrel{\triangleleft}_1 c) \in G$ for $c \in \mathbb{N}$ and
      $(\le, 0) \le Z_{x0} + (\mathrel{\triangleleft}_1, c)$.
    \end{itemize}
  \item $Z'_{0y} < Z_{0y}$ for some prophecy clock $y$, or for some
    history clock $y$ with
    \begin{itemize}
    \item $(\infty \le y) \in G$ and $Z_{0y} = (\le, \infty)$, or
    \item $(d \mathrel{\triangleleft}_2 y) \in G$ for $d \in \mathbb{N}$ and
      $Z'_{0y} + (\mathrel{\triangleleft}_2, -d) < (\le, 0)$
    \end{itemize}
    

  \item $Z'_{xy} < Z_{xy}$ and $Z'_{xy}$ is finite for two distinct (prophecy or
  history) clocks $x, y$ with $(x \mathrel{\triangleleft}_1 c), (d \mathrel{\triangleleft}_2 y) \in G$ for $c, d \in \mathbb{N}$
  and $(\le, 0) \le Z_{x0} + (\mathrel{\triangleleft}_1, c)$ and $Z'_{xy} + (\mathrel{\triangleleft}_2, -d) < Z_{x0}$.
  \end{enumerate}
\end{restatable}

\begin{proof}
  From Lemma~\ref{lem:zone-non-simulation}, $Z \not \preceq_G Z'$ iff
  there is a $v \in Z$ such that ${\uparrow}_G v \cap Z' =
  \emptyset$. Lemma~\ref{lem:negative-cycles-v-Z} gives three kinds of
  negative cycles that witness ${\uparrow}_G v \cap Z' = \emptyset$. We will
  show that the three conditions in the theorem respectively
  characterize the presence of the three kinds of negative cycles.
  
  \textbf{Case 1.} There is a negative cycle $0 \to x \to 0$ with
  $0 \to x$ from $\graphv{G}{v}$ and $x \to 0$ from $\graph{Z'}$ iff
  Item 1 above is true.

  ($\Rightarrow$).  Suppose there is such a negative cycle
  $0 \to x \to 0$. Weight of $0 \to x$ is either $(\le, v(x))$ or
  $(<, \infty)$.

  \textit{When weight of $0\to x$ is $(\le,v(x))$}: We have
  $(\le, v(x)) + Z'_{x0} < (\le, 0)$. Now, since $v \in Z$, it
  satisfies all constraints of $Z$. Substituting $(\le, v(x))$ instead
  of $Z_{0x}$ in $\graph{Z}$ keeps all cycles positive: hence
  $(\le, 0) \le (\le, v(x)) + Z_{x0}$. Adding the two inequalities
  gives $Z'_{x0} < Z_{x0}$. Notice that the weight of $0 \to x$ is
  $(\le, v(x))$ when either $x$ is a prophecy clock or $x$ is a
  history clock with $(x \mathrel{\triangleleft}_1 c) \in G$ for $c \in \mathbb{N}$ and
  $v(x) \mathrel{\triangleleft}_1 c$. We can rewrite $v(x) \mathrel{\triangleleft}_1 c$ as
  $(\le, v(x)) \le (\mathrel{\triangleleft}_1, c)$. Putting this in
  $(\le, 0) \le (\le, v(x)) + Z_{x0}$ gives
  $(\le, 0) \le (\mathrel{\triangleleft}_1, c) + Z_{x0}$. 

  \textit{When weight of $0 \to x$ is $(<, \infty)$}: This happens when $x$ is a history
  clock, $(x < \infty) \in G$ and $v(x) < \infty$ 
    (and we are not in the case above).
    For the cycle to be negative, we require $Z'_{x0} = (\le, -\infty)$.  
  From $v \in Z$ and
  $v(x) < \infty$, we get $Z_{x0} \neq (\le,-\infty)$. Hence
  $Z'_{x0} < Z_{x0}$.

  ($\Leftarrow$). Assume Item 1 is true.

  Consider the case when $x$ is a prophecy clock or a history clock
  with $x \mathrel{\triangleleft}_1 c$ in $G$ for $c \in \mathbb{N}$. Suppose
  $Z_{x0} = (\le, e)$. There is a valuation $v \in Z$ with
  $v(x) = -e$. Suppose $Z_{x0} = (<, e)$. There is a valuation
  $v \in Z$ with $v(x) = -e + \varepsilon$ for some $0 < \varepsilon <
  1$. From $Z'_{x0} < Z_{x0}$, we can infer
  $(\le, v(x)) + Z'_{x0} < (\le, 0)$: to see this, suppose
  $Z'_{x0} = (\mathrel{\triangleleft}, f)$; either ($f < e$) or ($e = f$,
  $Z'_{x0} = (<, f)$, and $Z_{x0}= (\le, e)$). Both cases give
  $(\le, v(x)) + Z'_{x0} < (\le, 0)$. When $x$ is a prophecy clock,
  this gives the required negative cycle. When $x$ is a history
  clock we need to additionally show that $v(x) \mathrel{\triangleleft}_1 c$. From
  the condition 
  $(\le, 0) \le Z_{x0} + (\mathrel{\triangleleft}_1, c)$, we get that $e + c \ge 0$,
  and when $e + c = 0$, we have ${\mathrel{\triangleleft}}_1 = {\le}$ and $Z_{x0} = (\le,
  e)$. This shows that our choice of valuation
  $v$ satisfies $v(x) \mathrel{\triangleleft}_1 c$.
  
  Now, suppose there is a history clock $x$ with $(x < \infty)  \in
  G$,  $Z'_{x0} < Z_{x0}$ and $Z'_{x0} = (\le,
  -\infty)$. This first implies that $Z_{x0} \neq (\leq,-\infty)$. Hence,
  there is a valuation $v \in Z$ with $v(x) < \infty$. For this $v$,
  the weight of $0 \to x$ in ${\uparrow}_G v$ will be at most $(<, \infty)$. 
  As $Z'_{x0} = (\le, -\infty)$, we get a negative cycle
  $0 \to x \to 0$ with $0 \to x$ from $\graphv{G}{v}$ and $x \to 0$
  from $\graph{Z'}$.
  
 

  \textbf{Case 2.} There is a negative cycle $0 \to y \to 0$ with
  $0 \to y$ from $\graph{Z'}$ and $y \to 0$ from $\graphv{G}{v}$ iff
  the item 2 in the theorem statement is true.

  ($\Rightarrow$). Suppose there is such a negative cycle.

  \textit{When weight of $y \to 0$ is $(\le, -v(y))$.} This happens
  when $y$ is a prophecy clock or $y$ is a history clock with $(d
  \mathrel{\triangleleft}_2 y) \in G$ with $d \in \mathbb{N}$ and $d \not \mathrel{\triangleleft}_2 v(y)$. From
  the negative cycle, we have $Z'_{0y} + (\le, -v(y)) < (\le, 0)$. Since
  $v \in Z$, we have $(\le, 0) \le Z_{0y} + (\le, -v(y))$. Summing
  the two gives $Z'_{0y} < Z_{0y}$. In the case when $y$ is a
  history clock, we have $d \not \mathrel{\triangleleft}_2 v(y)$. Therefore, either
  $v(y) < d$ or $v(y) = d$ and ${\mathrel{\triangleleft}}_2 = {<}$. In both 
  cases, $(\mathrel{\triangleleft}_2, -d) \le (\le, -v(y))$. Hence $Z'_{0y} +
  (\mathrel{\triangleleft}_2, -d) < (\le, 0)$.
  
  \textit{When weight of $y \to 0$ is $(\le, -\infty)$}. This occurs
  when $y$ is a history clock, $\infty \le y$ is in $G$ and $v(y) =
  \infty$. As the cycle is negative we get
  $Z'_{0y} \neq (\le, \infty)$. Since $v \in Z$, we get
  $Z_{0y} = (\le, \infty)$. This gives $Z'_{0y} < Z_{0y}$.
  
  \textit{When weight of $y \to 0$ is $(\mathrel{\triangleleft}_2, -d)$}. This is
    when $y$ is a history clock, we are not in the subcase above and
  there is $d \mathrel{\triangleleft}_2 y$ in $G$ with $d \in \mathbb{N}$ and $d
  \mathrel{\triangleleft}_2 v(y)$. The negative cycle gives $Z'_{0y} + (\mathrel{\triangleleft}_2, -d)
  < (\le, 0)$. From $d \mathrel{\triangleleft}_2 v(y)$, we can infer that $(\le,
  -v(y)) \le (\mathrel{\triangleleft}_2, -d)$. Therefore we also have $Z'_{0y} +
  (\le, -v(y)) < (\le, 0)$. As in the first subcase above, we get
  $Z'_{0y} < Z_{0y}$.
  
  The remaining case is when $y$ is a history clock and there is
  no lower bound constraint on $y$ in $G$. Then the weight of $y \to 0$
  is $(\le, 0)$. However, we have $(\le, 0) \le Z'_{0y}$. Hence $0
  \to y \to 0$ cannot be a negative cycle. So we can ignore this
  case. 
  
  
  ($\Leftarrow$). Assume Item 2 is true.
    
  Let us start with the case when $y$ is a prophecy clock.  We have $Z'_{0y} < Z_{0y}$.
  Take $v \in Z$ with $v(y) = e$ when $Z_{0y} = (\le, e)$ or $v(y) = e - \varepsilon$ with
  $0<\varepsilon<1$ when $Z_{0y} = (<, e)$.  For this $v$ the weight of $y \to 0$ is
  $(\le, -v(y))$.  As in the ($\Leftarrow$) proof of Case 1, we get
  $Z'_{0y}+(\leq,-v(y))<(\leq,0)$.


  Suppose $y$ is a history clock with $\infty \le y$ in $G$, and $Z_{0y} = (\le, \infty)$.
    For reachable zones, this implies that $Z_{y0}=(\leq,-\infty)$.
  Hence every valuation in $Z$ has $y$-value to be $\infty$.  Pick an arbitrary
  $v \in Z$.  We have $v(y) = \infty$.  For this $v$, the value of $y \to 0$ in
  $\graphv{G}{v}$ is $(\le, -\infty)$.  Now, since $Z'_{0y} < Z_{0y}$, the cycle $Z'_{0y}
  + (\le, -\infty)$ is negative.

  Finally, let $y$ be a history clock with $d \mathrel{\triangleleft}_2 y$ in $G$ for $d \in \mathbb{N}$ and
  $Z'_{0y} + (\mathrel{\triangleleft}_2, -d) < (\le, 0)$.  Pick $v\in Z$ with $v(y) = e$ when $Z_{0y} =
  (\le, e)$ and $v(y) = e - \varepsilon$ with $0<\varepsilon<1$ when $Z_{0y} = (<, e)$.
  If $v(y) \not \mathrel{\triangleleft}_2 d$, then the weight of $y \to 0$ is at most $(\le,
  -v(y))$.  Using $Z'_{0y} < Z_{0y}$ gives $0 \to y \to 0$ to be negative cycle.  Suppose
  $d \mathrel{\triangleleft}_2 y$.  Then weight of $y \to 0$ is at most $(\mathrel{\triangleleft}_2, -d)$.  But we
  already have $Z'_{0y} + (\mathrel{\triangleleft}_2, -d) < (\le, 0)$ in our hypothesis, which gives the
  required negative cycle.
  
  \textbf{Case 3.} There is a \emph{finite weight} negative cycle
  $0 \to x \to y \to 0$ with $0 \to x$ and $y \to 0$ from
  $\graphv{G}{v}$ and $x \to y$ from $\graph{Z'}$ iff the third
  condition of the theorem is true.


  ($\Rightarrow$).  Suppose there is such a negative cycle.  
  Since the weight of the cycle is finite, the weight of each edge is also finite.
  Hence, the weight of the edge $0\to x$ is $(\leq,v(x))$.  We find $x\mathrel{\triangleleft}_{1} c$ in $G$
  with $c\in\mathbb{N}$ and $v(x)\mathrel{\triangleleft}_1 c$ (if $x$ is a prophecy clock then
  $(\mathrel{\triangleleft}_{1},c)=(\leq,0)$).  As in case 1 above, from $v\in Z$ we deduce that
  $(\leq,0)\leq Z_{x0}+(\leq,v(x))$ and from $v(x)\mathrel{\triangleleft}_{1}c$ we get
  $(\leq,v(x))\leq(\mathrel{\triangleleft}_{1},c)$.
  We obtain $(\le,0) \le Z_{x0}+(\mathrel{\triangleleft}_1,c)$.
  
  Now, since the weight of $y\to 0$ is finite, we find $d\mathrel{\triangleleft}_{2}y$ in $G$ (if 
  $y$ is a prophecy clock we take $(d,\mathrel{\triangleleft}_{2})=(0,\leq)$).
  The weight of $y \to 0$ is
  $\max( (\le, -v(y)), (\mathrel{\triangleleft}_2, -d) )$. Therefore:
  $Z'_{xy} + (\le, v(x) - v(y)) < (\le, 0)$ and
  $(\le, v(x)) + Z'_{xy} + (\mathrel{\triangleleft}_2, -d) < (\le, 0)$. Since
  $v \in Z$, we have $(\le, 0) \le (\le, v(x) - v(y)) +
  Z_{xy}$. Using $Z'_{xy} + (\le, v(x) - v(y)) < (\le, 0)$
  we get $Z'_{xy} < Z_{xy}$. Again, as $v \in Z$, we have
  $(\le, 0) \le (\le, v(x)) + Z_{x0}$. Adding this to
  $(\le, v(x)) + Z'_{xy} + (\mathrel{\triangleleft}_2, -d) < (\le, 0)$ gives
  $Z'_{xy} + (\mathrel{\triangleleft}_2, -d) < Z_{x0}$.
  

  ($\Leftarrow$). Suppose the third condition is true. Instead of
  explicitly constructing a $v$ as in the previous two cases, we will simply prove that there exists a valuation that forms the required negative
  cycle.  We start by defining some new weights and observe some
  properties that will be used later. Define 
  $w_1 = (<, -e')$ if $Z'_{xy} = (\le, e')$ and $w_1 = (\le, -e')$ if
  $Z'_{xy} = (<, e')$, and $w_2 = (\le, -e' + d)$ if either $Z'_{xy}$
  or $(\mathrel{\triangleleft}_2,-d)$ has a strict inequality, and $w_2 = (<, -e' + d)$
  otherwise. Notice that $w_1 + Z'_{xy} = (<, 0)$ and 
  $w_2 + Z'_{xy} + (\mathrel{\triangleleft}_2, -d) = (<, 0)$ are negative.
    Using $Z'_{xy} + (\mathrel{\triangleleft}_2, -d) < Z_{x0}$, we get 
  $(<,0)=w_{2}+Z'_{xy}+(\mathrel{\triangleleft}_{2},-d)<w_{2}+Z_{x0}$ and we obtain
  $(\leq,0)\leq w_{2}+Z_{x0}$. Similarly, using $Z'_{xy}<Z_{xy}$ we get
  $(<,0)=w_{1}+Z'_{xy}<w_{1}+Z_{xy}$ and $(\leq,0)\leq w_{1}+Z_{xy}$.  


  Consider a distance graph $\mathbb{G}$ formed by taking $\graph{Z}$
  and modifying two of its edges as follows: change $0 \to x$ to
  $\min(Z_{0x}, (\mathrel{\triangleleft}_1, c), w_2)$; change $y \to x$ to
  $\min(Z_{yx}, w_1)$. We first claim that $\mathbb{G}$ has only
  non-negative cycles. It is sufficient to show that $0 \to x \to 0$
  and $y \to x \to y$ are non-negative. From
  $(\le, 0) \le Z_{x0} + (\mathrel{\triangleleft}_1, c)$, $(\le, 0) \le w_2 + Z_{x0}$
  and the fact that $\graph{Z}$ does not have negative cycles, we
  infer that $0 \to x \to 0$ is non-negative in $\mathbb{G}$.  The
  weight of $y \to x \to y$ is either $Z_{yx} + Z_{xy}$ or
  $w_1 + Z_{xy}$. The former is non-negative as $Z$ is non-empty. We
  have shown above that $w_1 + Z_{xy}$ is non-negative. Hence
  $\mathbb{G}$ has no negative cycles, and its solution set is
  non-empty.  
  

  Now, pick a $v$ that satisfies constraints of
  $\mathbb{G}$. Valuation $v$ is in $Z$, and additionally satisfies
  $v(x) \mathrel{\triangleleft}_1 c$, $(\le, v(x)) \le w_2$ and
  $(\le, v(x - y)) \le w_1$. Recall that $w_1 + Z'_{xy}=(<,0)$. 
  Adding this to $(\le, v(x - y)) \le w_1$ gives
  $(\le, v(x - y)) + Z'_{xy} < (\le, 0)$. If $d \not \mathrel{\triangleleft}_2 v(y)$,
  then this corresponds to the weight of the cycle
  $0 \to x \to y \to 0$ which we have now shown to be
  negative. Otherwise, we have $d \mathrel{\triangleleft}_2 v(y)$ and the weight of
  edge $y \to 0$ is $(\mathrel{\triangleleft}_2, -d)$. The weight of the cycle would
  be: $(\le, v(x)) + Z'_{xy} + (\mathrel{\triangleleft}_2, -d)$. But, $(\le, v(x)) \le
  w_2$ and 
  $w_2 + Z'_{xy} + (\mathrel{\triangleleft}_2, -d) = (<,0)$. Hence the required cycle is negative.
\end{proof}

From Theorem~\ref{thm:simulation-check}, we can see that the inclusion test requires iteration over clocks $x, y$ and checking if the conditions are satisfied by the respective weights. 

\begin{corollary}
  Checking if $(q,Z) \preceq_\mathcal{A} (q',Z')$ can be done in time $\mathcal{O}(|X|^2)$ = $\mathcal{O}(|\Sigma|^2)$.
\end{corollary}
\section{Finiteness of the simulation relation}\label{sec:termination}
In this section, we will show that the simulation relation $\preceq_{\mathcal{A}}$ defined in
Section~\ref{sec:simulation} is finite, 
which
implies that the reachability algorithm of Definition~\ref{def:reach-algo} terminates.
Recall that given an event clock automaton $\mathcal{A}$,
we have an associated map $\mathcal{G}$ from
states of $\mathcal{A}$ to sets of atomic constraints.
Let $M=\max\{|c| \mid c\in\mathbb{Z} \text{ is used in some constraint of } \mathcal{A}\}$, the maximal constant of $\mathcal{A}$.  We have $M\in\mathbb{N}$ and constraints in the sets
$\mathcal{G}(q)$ use constants in $\{-\infty,\infty\}\cup\{c\in\mathbb{Z}\mid|c|\leq M\}$.

Recall that the simulation relation $\preceq_{\mathcal{A}}$ was
defined on nodes of the event zone graph
$\ensuremath{\mathsf{EZG}}(\mathcal{A})$  by $(q,Z)\preceq_{\mathcal{A}}(q',Z')$ if $q=q'$ and
$Z\preceq_{\mathcal{G}(q)}Z'$.
This simulation relation $\preceq_{\mathcal{A}}$
is \emph{finite} if for any
infinite sequence $(q,Z_{0}),(q,Z_{1}),(q,Z_{2}),\ldots$ of
\emph{reachable} nodes in $\ensuremath{\mathsf{EZG}}(\mathcal{A})$ we find $i<j$ with
$(q,Z_{j})\preceq_{\mathcal{A}}(q,Z_{i})$, i.e., $Z_{j}\preceq_{\mathcal{G}(q)}Z_{i}$.
Notice that we restrict to \emph{reachable} zones in the definition
above.  Our goal now is to prove that the relation $\preceq_{\mathcal{A}}$ is
finite.  The structure of the proof is as follows.  
\begin{enumerate}
  \item We prove in Lemma~\ref{lem:dagger} that for any \emph{reachable} node $(q,Z)$ of
  $\ensuremath{\mathsf{EZG}}(\mathcal{A})$, the distance graph $\graph{Z}$ in canonical form satisfies a set of
  $(\dagger)$ conditions which depend only on the maximal constant $M$ of $\mathcal{A}$.

  \item We introduce an equivalence relation $\sim_{M}$ of \emph{finite index} on
  valuations (depending on 
  $M$ only) and show in
  Lemma~\ref{lem:sim_M main property} that, if $G$ is a set of atomic constraints using
  constants in $\{c\in\mathbb{Z}\mid|c|\leq M\}\cup \{-\infty,\infty\}$ and if $Z$ is a
  zone such that its distance graph $\graph{Z}$ in canonical form satisfies $(\dagger)$
  conditions, then ${\downarrow}_{G}Z$ is a union of $\sim_{M}$ equivalence classes.
\end{enumerate}

We start with a lemma which highlights an important property of \emph{prophecy} clocks in
reachable event zones.  This property is essential for the proof of the $(\dagger)$
conditions.  The proof follows from the observation that the property is true in the
initial zone, and is invariant under the zone operations, namely, guard intersection,
reset, release and time elapse.

\begin{restatable}{lemma}{lemProphecyClocks}
  \label{lem:reachable-zones-prophecy-clocks}
  Let $Z$ be a reachable event zone.  For every valuation $v \in Z$,
  and for every prophecy clock $\ora{x}$, if
  $-\infty < v(\ora{x}) < -M$, then $v[\ora{x}\mapsto\alpha] \in Z$
  for every $-\infty < \alpha < -M$.
\end{restatable}

\begin{proof}
  The initial zone is
  $(\bigwedge_{\ola{x}} \ola{x} = \infty) \land (\bigwedge_{\ora{x}}
  -\infty \le \ora{x} \le 0)$. The property is true in this zone. We
  now show that the property is invariant under guard intersection,
  reset, release and time elapse.
  Assume $Z$ is a zone that satisfies the property.  Let $v$ be an
  arbitrary valuation with $-\infty < v(\ora{x}) < -M$. For
  $-\infty<\alpha<-M$, we simply write
  $v_\alpha=v[\ora{x}\mapsto\alpha]$.
  \begin{description}
  \item[Guard intersection.] Let $g$ be a guard, which is in general a
    conjunction of atomic constraints. Suppose $g$ contains an atomic
    constraint on $\ora{x}$, either $c \mathrel{\triangleleft} \ora{x}$ or
    $\ora{x} \mathrel{\triangleleft} c$. The constant $c$ is either $-\infty$, or
    $-M \le c \le 0$. Therefore if $v$ satisfies the constraint, every
    $v_\alpha$ will satisfy the atomic constraint. Now, suppose $g$
    contains $d \mathrel{\triangleleft} y$ or $y \mathrel{\triangleleft} d$ for some $y \neq
    \ora{x}$. Once again, notice that if $v$ satisfies this guard,
    every $v_\alpha$ will satisfy the guard since
    $v(y) = v_\alpha(y)$. Hence, if $v$ satisfies the guard,
    $v_\alpha$ satisfies the guard. The property is true in the zone
    $Z \land g$.
    
  \item[Release.]  The release operation on $\ora{y}$ takes a
    valuation $u$ and adds a valuation $u[\ora{y}\mapsto\beta]$ for
    each $-\infty \le \beta \le 0$.
    Let $v \in [\ora{y}]Z$. Then, there is some valuation $u \in Z$
    such that $v=u[\ora{y}\mapsto\beta]$ for some $-\infty \le \beta \le 0$.
    When $\ora{y} = \ora{x}$, associating $\alpha$ to $\ora{x}$ in the
    release operation starting from $u$ gives $v_\alpha$.  When
    $\ora{y} \neq \ora{x}$, we use the induction hypothesis: valuation
    $u_\alpha \in Z$. 
    Setting $\ora{y}$ to $\beta$ in the release operation starting
    from $u_\alpha$ gives $v_\alpha$.

  \item[Reset.] The reset operation takes every valuation in $Z$ and
    makes some history clock to $0$. This does not perturb the
    required property.

  \item[Time elapse.]  Suppose $v + \delta \in \elapse{Z}$ for some
    $v \in Z$ and $\delta\geq0$.  This means
    $(v+\delta)(\ora{y}) \le 0$ for every prophecy clock $\ora{y}$.
    We have to show that if $-\infty < (v + \delta)(\ora{x}) < -M$,
    then $(v + \delta)_\alpha \in \elapse{Z}$ for all
    $-\infty < \alpha < -M$. Since
    $-\infty < (v + \delta)(\ora{x}) < -M$, we also have
    $-\infty < v(\ora{x}) < -M$. For some given $\alpha$, let
    $\beta = \alpha - \delta$. We have $v_\beta \in Z$ by
    hypothesis. Notice that $(v+\delta)_{\alpha}=v_\beta + \delta $.
    Moreover, $v_\beta + \delta \in \elapse{Z}$: for each clock
    $\ora{y} \neq \ora{x}$,
    $(v_\beta + \delta)(\ora{y}) = (v + \delta)(\ora{y}) \le 0$ and
    $(v_\beta + \delta)(\ora{x}) = \alpha < -M \le 0$.  \qedhere
  \end{description}
\end{proof}


There is no similar version of the above lemma for history clocks.  A reset of a history
clock makes its value exactly equal to $0$ in every valuation and creates non-trivial
diagonal constraints with other clocks.  Moreover repeated resets can generate arbitrarily
large diagonal constraints, for e.g., a loop with guard $x = 1$ and reset $x$.  This is
why simulations are particularly needed to control history clocks.  Notice that in our
simulation $v \preceq_G v'$, we have $v(\ora{a}) = v'(\ora{a})$: there is no abstraction
of the value of prophecy clocks and the simulation relation by itself does not have any
means to show finiteness.  However, as we show below, the reachable zones themselves take
care of finiteness with respect to prophecy clocks.  The challenge is then to combine this
observation on prophecy clocks along with the non-trivial simulation happening for history
clocks to prove that we still get a finite simulation.  This is the purpose of the above
mentioned item 2.

Now, we give the $(\dagger)$ conditions and prove that they are satisfied by distance
graphs of reachable zones.  In particular, the $(\dagger)$ conditions imply that the
weight of edges of the form $0 \to \ora{x}$, $\ora{x} \to 0$ and $\ora{x} \to \ora{y}$
belong to the finite set $\{(\leq,-\infty),(<,\infty),(\leq,\infty)\}\cup \{(\mathrel{\triangleleft},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 EPA, we do
not even need simulation to obtain finiteness.

\begin{restatable}{lemma}{lemDagger}
  \label{lem:dagger}
  Let $(q,Z)$ be a \emph{reachable} node in $\ensuremath{\mathsf{EZG}}(\mathcal{A})$ with $Z\neq\emptyset$.  Then, the
  distance graph $\graph{Z}$ in canonical form satisfies the $(\dagger)$ conditions:
  \begin{enumerate}
    \item[$\dagger_{1}$] If $Z_{\ora{x}0}=(\leq,\infty)$ then
    $Z_{\ora{x}y}=(\leq,\infty)$ for all $y\neq\ora{x}$.
    
    \item[$\dagger_{2}$] If $Z_{\ora{x}0}=(<,\infty)$ then
    for all $y\neq\ora{x}$, either $y$ is a prophecy clock which is undefined in $Z$ and
    $Z_{\ora{x}y}=Z_{0y}=(\leq,-\infty)$ or $Z_{\ora{x}y}\in\{(<,\infty),(\leq,\infty)\}$.
    
    \item[$\dagger_{3}$] If $Z_{\ora{x}0}<(<,\infty)$ then
    $(\leq,0)\leq Z_{\ora{x}0}\leq(\leq,M)$.
    
    \item[$\dagger_{4}$] If $Z_{\ora{x}\ola{y}}<(<,\infty)$ then
    $(\leq,0)\leq Z_{\ora{x}0}\leq(\leq,M)$.
    
    \item[$\dagger_{5}$] Either $Z_{0\ora{y}}=(\leq,-\infty)$ ($\ora{y}$
    is undefined in $Z$), or $Z_{x0} + (<,-M) \leq Z_{x\ora{y}}$ for all
    $x\neq\ora{y}$ (including $x=0$).
    
    \item[$\dagger_{6}$] Either $Z_{0\ora{x}}=(\leq,-\infty)$ or
    $(<,-M)\leq Z_{0\ora{x}}\leq(\leq,0)$.
    
    \item[$\dagger_{7}$] Either
    $Z_{\ora{x}\ora{y}}\in\{(\leq,-\infty),(<,\infty),(\leq,\infty)\}$
    or
    $(<,-M) \leq Z_{\ora{x}\ora{y}} \leq (\leq,M)$.
  \end{enumerate}
\end{restatable}
\begin{proof}
    \begin{enumerate}
      \item[$\dagger_1$] Since $Z_{\ora{x}0} = (\le, \infty)$, there is a
      valuation $v \in Z$ with $v(\ora{x}) = -\infty$. Therefore, for
      every clock $y\neq\ora{x}$, we have $v(y - \ora{x}) =
      +\infty$. Since $v \in Z$, it satisfies the constraint on
      $y - \ora{x}$ given by $Z_{\ora{x}y}$.  This is possible only when
      $Z_{\ora{x}y} = (\le, \infty)$.
      \item[$\dagger_2$] Assume that $Z_{\ora{x}0}=(<,\infty)$ and let $y\neq\ora{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 canonical form, we have
      $Z_{\ora{x}y}\leq Z_{\ora{x}0}+Z_{0y}=(<,\infty)+(\leq,-\infty)=(\leq-\infty)$.
      
      The second case is when $Z_{0y}\neq(\leq,-\infty)$.  
      This implies $Z_{\ora{x}y}\neq(\leq,-\infty)$ since otherwise we would get $Z_{0y}\leq
      Z_{0\ora{x}}+Z_{\ora{x}y}=(\leq,-\infty)$.
      We claim that there is a valuation $v\in Z$ with $-\infty<v(y)$ and
      $-\infty<v(\ora{x})<-M$.
       
      Consider the distance graph $\mathbb{G}'$ obtained from $\graph{Z}$ by setting the weight of
      edge $y\to 0$ to $\min(Z_{y0},(<,\infty))$ and of edge $0\to\ora{x}$ to
      $\min(Z_{0\ora{x}},(<,-M))$.  We show that there are no negative cycles in this graph.
      Since $Z\neq\emptyset$, the candidates for being negative must use the new weight 
      $(<,-M)$ of $0\to\ora{x}$ or the new weight $(<,\infty)$ of $y\to 0$ or both. This 
      gives the cycle $0\to\ora{x}\to 0$ with weight $(<,-M)+Z_{\ora{x}0}=(<,\infty)$ 
      since $Z_{\ora{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 \ora{x} \to y$ with weight $(<,\infty)+(<,-M)+Z_{\ora{x}y}$
      which is not negative since $Z_{\ora{x}y}\neq(\le,-\infty)$.
      Since $\mathbb{G}'$ has no negative cycle, Lemma~\ref{lem:empty-iff-negative-cycle} implies
      $\sem{\mathbb{G}'}\neq\emptyset$.  Note that $\sem{\mathbb{G}'}\subseteq\sem{\graph{Z}}=Z$.
      Finally, for all $v\in\mathbb{G}'$, we have $-\infty<v(y)$ and $-\infty<v(\ora{x})<-M$, which
      proves the claim.
      
      By Lemma~\ref{lem:reachable-zones-prophecy-clocks},
      $v_{\alpha}=v[\ora{x}\mapsto\alpha]\in Z$ for all $-\infty<\alpha<-M$.  Now,
      $v_{\alpha}(y-\ora{x})=v(y)-\alpha$ satisfies the constraint $Z_{\ora{x}y}$.  We
      deduce that $Z_{\ora{x}y}$ is either $(<,\infty)$ or $(\le,\infty)$.
      
      \item[$\dagger_3$] Suppose $Z_{\ora{x}0} = (\mathrel{\triangleleft}, c)$ for some
      integer $c>M$.  Then, there exists a valuation $v\in Z$ with
      $v(\ora{x})=-c$ or $v(\ora{x})=-c+\frac{1}{2}$ depending on
      whether $\mathrel{\triangleleft}$ is $\le$ or $<$.  Since $c,M$ are integers, we
      get $-\infty<v(\ora{x})<-M$.  By
      Lemma~\ref{lem:reachable-zones-prophecy-clocks},
      $v[\ora{x}\mapsto\alpha]\in Z$ for all $-\infty < \alpha < -M$.
      In particular, $v'=v[\ora{x}\mapsto-c-1]\in Z$.  For this
      valuation, we have $v'(\ora{x}) = -c - 1$. This violates
      $Z_{\ora{x}0}$ which says $0 - v'(\ora{x}) \mathrel{\triangleleft} c$, or seen
      differently, $-c \mathrel{\triangleleft} v'(\ora{x})$.
  
  
      \item[$\dagger_4$] Directly follows from
      $\dagger_{1},\dagger_{2},\dagger_{3}$.  
      
      \item[$\dagger_5$] If $Z_{x0} = (\le, -\infty)$ the condition
      is trivially true. If
      $Z_{x0} \in \{(<, \infty), (\le, \infty) \}$ then $x$ is a
      prophecy clock and $\dagger_5$ follows from
      $\dagger_1, \dagger_2$. Therefore, we assume
      $Z_{x0} = (\mathrel{\triangleleft}, c)$ for $c \in \mathbb{Z}$.  
      The left hand side of the
      condition is $Z_{x0} + (<, -M)=(<, c - M)$, with $c - M \in \mathbb{Z}$.
      Let $Z_{x \ora{y}} = (\mathrel{\triangleleft}', e)$
      with $e \in \mathbb{Z} \cup \{-\infty, +\infty\}$. To show
      $\dagger_5$ it is now sufficient to show $c - M \le e$.
      
      Furthermore, if $Z_{0 \ora{y}} = (\le, -\infty)$ or $e=\infty$
      the $\dagger_5$ condition is true. We assume the contrary below:
      $Z_{0\ora{y}}\neq(\leq,-\infty)$ and $e\neq\infty$.
      Note that $Z_{0x} \neq (\le, \infty)$ and $Z_{x\ora{y}} \neq (\le, -\infty)$.
      Indeed, in a reachable zone, we may have $Z_{0x}=(\leq,\infty)$ only when $x$ is
      a history clock which has not yet been reset.  In this case we have
      $Z_{x0}=(\leq,-\infty)$. This contradicts our assumption $c\in\mathbb{Z}$.
      Next, if $Z_{x\ora{y}} = (\le, -\infty)$, then
      $Z_{0\ora{y}} \le Z_{0 x} + Z_{x \ora{y}}$ which is
      $(\le, -\infty)$ since $Z_{0x} \neq (\le, \infty)$. This again
      contradicts our assumption about $Z_{0\ora{y}}$.
      \begin{itemize}
        \item Suppose $Z_{x0} = (\le, c)$. We claim that we can pick a
        valuation $v$ in $Z$ with $v(x) = -c$ and $-\infty<v(\ora{y})$. 
        Consider the distance graph $\mathbb{G}'$ obtained
        from the canonical graph $\graph{Z}$ by setting the weight of $0 \to x$ to
        $\min(Z_{0x}, (\le,-c))$,
        and the weight of $\ora{y}\to 0$ to $\min(Z_{\ora{y}0}, (<,\infty))$. 
        We have $\sem{\mathbb{G}'}\subseteq\sem{\graph{Z}}=Z$.
        As in the proof of $\dagger_{2}$, we can show mutatis mutandis that the graph 
        $\mathbb{G}'$ has no negative cycle. Hence, $\sem{\mathbb{G}'}\neq\emptyset$. For all 
        valuations $v\in\sem{\mathbb{G}'}\subseteq Z$, we have $v(x)=-c$ and $-\infty<v(\ora{y})$, 
        which proves the claim.
  
        Let $v\in\sem{\mathbb{G}'}$. Suppose $-M \le v(\ora{y})$. Then
        $c - M \le v(\ora{y} - x) \mathrel{\triangleleft}' e$. This shows $c - M \le e$.
        Suppose $-\infty < v(\ora{y}) < -M$. Then, from
        Lemma~\ref{lem:reachable-zones-prophecy-clocks}, we get
        $v_{\varepsilon}=v[\ora{y}\mapsto(-M-\varepsilon)]\in Z$ for all
        $\varepsilon>0$. We have
        $v_{\varepsilon}(\ora{y} - x) = -M - \varepsilon + c$.  If
        $e < c - M$, we can find an $\varepsilon$ such that
        $v_{\varepsilon}$ does not satisfy the $Z_{x \ora{y}}$
        constraint. This is a contradiction. Hence $c - M \le e$.
  
  
        \item Next, suppose $Z_{x0} = (<, c)$.  Since $\graph{Z}$ has no negative cycles we
        get $(\leq,-c)<Z_{0x}$.  Since $Z$ is a zone with integral or infinity weights, we
        infer we have $(<, -c + 1) \le Z_{0x}$.
        We proceed as above by considering a graph $\mathbb{G}'$ obtained from $\graph{Z}$ by
        setting the weight of $\ora{y}\to 0$ to $\min(Z_{\ora{y}0},(<,\infty))$ and the
        weight of $0\to x$ to $(<,-c+1)$.  As before, we prove that $\mathbb{G}'$ has no negative
        cycle.  We get $\emptyset\neq\sem{\mathbb{G}'}\subseteq Z$.  Let $v\in\sem{\mathbb{G}'}\subseteq
        Z$.  We have $-\infty<v(\ora{y})$ and $-c<v(x)<-c+1$.  Again, we proceed as in the
        previous case.  If $-M\leq v(\ora{y})$ we get $c-M-1\leq
        v(\ora{y})+c-1<v(\ora{y}-x)\mathrel{\triangleleft}' e$ which implies $c-M\leq e$ since
        $e\in\mathbb{Z}\cup\{-\infty\}$.  If $v(\ora{y})<-M$ we have
        $v_{\varepsilon}=v[\ora{y}\mapsto(-M-\varepsilon)]\in Z$ for all $\varepsilon>0$.
        Since $c-1<-v(x)$ we can choose $\varepsilon>0$ such that
        $c-M-1<v_{\varepsilon}(\ora{y}-x)$ and we conclude as before.
      \end{itemize}
      
      \item[$\dagger_{6}$] Follows from $\dagger_5$ applied to clocks $0$
      and $\ora{x}$. Indeed, either $Z_{0\ora{x}}=(\leq,-\infty)$ or
      $Z_{00}+(<,-M)\leq Z_{0\ora{x}}$, where $Z_{00} = (\le, 0)$. This
      implies $\dagger_{6}$.
    
      \item[$\dagger_{7}$] Assume that
      $Z_{\ora{x}\ora{y}}\notin\{(\leq,-\infty),(<,\infty),(\leq,\infty)\}$.
      
      Note that, by $\dagger_{1}$, $Z_{0 \ora{y}}=(\leq,-\infty)$ implies
      either $Z_{\ora{x}\ora{y}}=(\leq,\infty)$ (when $Z_{\ora{x}0}=(\leq,\infty)$) or 
      $Z_{\ora{x}\ora{y}}\leq Z_{\ora{x}0}+(\leq,-\infty)=(\leq,-\infty)$
      (when $Z_{\ora{x}0}\neq(\leq,\infty)$).
      Hence, $Z_{0 \ora{y}}\neq(\leq,-\infty)$.
  
      Applying $\dagger_5$, we deduce that
      $(<,-M)\leq Z_{\ora{x}0}+(<,-M)\leq Z_{\ora{x}\ora{y}}$.
      
      Also, since $Z_{0 \ora{y}}\neq(\leq,-\infty)$ and
      $Z_{\ora{x} \ora{y}}\notin\{(<,\infty),(\leq,\infty)\}$, by
      $\dagger_1, \dagger_2$ we deduce that
      $Z_{\ora{x} 0}\notin\{(<,\infty),(\leq,\infty)\}$.  From
      $\dagger_{3}$ we get $Z_{\ora{x}0} \leq (\leq,M)$.
      
      Finally,
      $Z_{\ora{x} \ora{y}} \leq Z_{\ora{x} 0}+Z_{0 \ora{y}} \leq
      Z_{\ora{x} 0} \leq (\leq,M)$. \qedhere
     
    \end{enumerate}
  \end{proof}

We turn to the second step of the proof and define an equivalence relation of finite index
$\sim_{M}$ on valuations.
First, we define $\sim_{M}$ on 
$\alpha,\beta\in\overline{\mathbb{R}}=\mathbb{R}\cup\{-\infty,\infty\}$
by $\alpha\sim_{M}\beta$ if
$(\alpha\mathrel{\triangleleft} c \Longleftrightarrow \beta\mathrel{\triangleleft} c)$ for all
$(\mathrel{\triangleleft},c)$ with ${\mathrel{\triangleleft}}\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\mathbb{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
valuations.

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 ${\uparrow}_{G}v$.

\begin{restatable}{lemma}{lemSimM}
  \label{lem:sim_M and graphv}
  Let $v_{1},v_{2}\in\mathbb{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{restatable}
    
\begin{proof}
  This is clear by definition for edges $\ora{x}\to 0$ and
  $0\to\ora{x}$ adjacent to a prophecy clock. We consider now edges
  adjacent to history clocks $\ola{x}$.
  \begin{itemize}
  \item Consider the edge $0\to\ola{x}$.
    \begin{itemize}
    \item If its weight is $(\leq,v_{1}(\ola{x}))$ in
      $\graphv{G}{v_{1}}$ then there is some $\ola{x}\mathrel{\triangleleft} c\in G$
      with $(\mathrel{\triangleleft},c)<(<,\infty)$ and $v_{1}(\ola{x})\mathrel{\triangleleft} c$.
      Since $v_{1}\sim_{M}v_{2}$ we deduce that
      $v_{2}(\ola{x})\mathrel{\triangleleft} c$ and the edge $0\to\ola{x}$ has weight
      $(\leq,v_{2}(\ola{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 $\ola{x}<\infty \in G$,
      $v_{1}(\ola{x})<\infty$.  Since $v_{1}\sim_{M}v_{2}$ we deduce
      that $v_{2}(\ola{x})<\infty$ and the edge $0\to\ola{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 $\ola{x}\to 0$.
    \begin{itemize}
    \item If its weight is $(\leq,-\infty)$ in $\graphv{G}{v_{1}}$
      then $\infty\leq\ola{x} \in G$ and $v_{1}(\ola{x})=\infty$.
      Since $v_{1}\sim_{M}v_{2}$ we deduce that
      $v_{2}(\ola{x})=\infty$ and the edge $\ola{x}\to0$ has weight
      $(\leq,-\infty)$ in $\graphv{G}{v_{2}}$.
            
    \item If its weight is $(\mathrel{\triangleleft},-c)$ in $\graphv{G}{v_{1}}$ then
      we are not in the case above and there is some
      $c\mathrel{\triangleleft}\ola{x}\in G$ with $(c,\mathrel{\triangleleft})<(\infty,\leq)$ and
      $c\mathrel{\triangleleft} v_{1}(\ola{x})$.  Since $v_{1}\sim_{M}v_{2}$ we deduce
      that $c\mathrel{\triangleleft} v_{2}(\ola{x})$ and the edge $\ola{x}\to0$ has
      weight $(\mathrel{\triangleleft},-c)$ in $\graphv{G}{v_{2}}$.
      
    \item If its weight is $(\leq,-v_{1}(\ola{x}))$ in
      $\graphv{G}{v_{1}}$ then we are not in the cases above and there
      is some $c\mathrel{\triangleleft}\ola{x}\in G$ with $(c,\mathrel{\triangleleft})<(\infty,\leq)$
      and $c\not\mathrel{\triangleleft} v(\ola{x})$, Since $v_{1}\sim_{M}v_{2}$ we
      deduce that $c\not\mathrel{\triangleleft} v_{2}(\ola{x})$ and the edge
      $\ola{x}\to0$ has weight $(\leq,-v_{2}(\ola{x}))$ in
      $\graphv{G}{v_{2}}$.
      
    \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 ${\downarrow}_{G}Z$ is a union of $\sim_{M}$ equivalence classes.


\begin{restatable}{lemma}{lemSimMMain}
  \label{lem:sim_M main property}
  Let $v_{1},v_{2}\in\mathbb{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{\downarrow}_{G}Z$ iff $v_{2}\in{\downarrow}_{G}Z$.
\end{restatable}

\begin{proof}
  Notice that $v\in{\downarrow}_{G}Z$ iff ${\uparrow}_{G}v\cap Z\neq\emptyset$.
  The proof is by contradiction.
  We assume that ${\uparrow}_{G}v_{1}\cap Z\neq\emptyset$ and
  ${\uparrow}_{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 ${\uparrow}_{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
  cases.
  \begin{enumerate}
  \item Cycle
    $C_{2}=0 \xra{(\leq,v_{2}(\ola{y}))} \ola{y} \xra{Z_{\ola{y}0}}
    0$.  We have
    $C_{1}=0 \xra{(\leq,v_{1}(\ola{y}))} \ola{y} \xra{Z_{\ola{y}0}}
    0$.

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

    Let $Z_{\ola{y}0}=(\mathrel{\triangleleft},c)$.
    Since $C_{1}$ is not a negative cycle, we get
    $(\leq,0)\leq(\mathrel{\triangleleft},c+v_{1}(\ola{y}))$, which is equivalent to
    $-c\leq v_{1}(\ola{y})$. Using $0\leq v_{1}(\ola{y})\leq M$ and
    $v_{1}\sim_{M}v_{2}$ we deduce that $-c\leq v_{2}(\ola{y})$.  This
    is equivalent to $(\leq,0)\leq(\mathrel{\triangleleft},c+v_{2}(\ola{y}))$, a
    contradiction with $C_{2}$ being a negative cycle.
    
  \item Cycle
    $C_{2}=0 \xra{Z_{0\ola{y}}} \ola{y} \xra{(\leq,-v_{2}(\ola{y}))}
    0$.  We have
    $C_{1}=0 \xra{Z_{0\ola{y}}} \ola{y} \xra{(\leq,-v_{1}(\ola{y}))}
    0$.
    
    Since we have the edge $\ola{y} \xra{(\leq,-v_{1}(\ola{y}))} 0$ in
    $\graphv{G}{v_{1}}$, there is a constraint $c'\mathrel{\triangleleft}'\ola{y}$ in
    $G$ with $(c',\mathrel{\triangleleft}')<(\infty,\leq)$ and
    $c'\not\mathrel{\triangleleft}' v_{1}(\ola{y})$.  We deduce that
    $0\leq v_{1}(\ola{y})\leq M$.

    Let $Z_{0\ola{y}}=(\mathrel{\triangleleft},c)$.
    Since $C_{1}$ is not a negative cycle, we get
    $(\leq,0)\leq(\mathrel{\triangleleft},c-v_{1}(\ola{y}))$, which is equivalent to
    $v_{1}(\ola{y})\leq c$.  Using $v_{1}\sim_{M}v_{2}$ and
    $0\leq v_{1}(\ola{y})\leq M$, we deduce that
    $v_{2}(\ola{y})\leq c$.  This is equivalent to
    $(\leq,0)\leq(\mathrel{\triangleleft},c-v_{2}(\ola{y}))$, a contradiction with
    $C_{2}$ being a negative cycle.
    
  \item Cycle
    $C_{2}=0 \xra{(\leq,v_{2}(\ora{x}))} \ora{x} \xra{Z_{\ora{x}0}}
    0$.  We have
    $C_{1}=0 \xra{(\leq,v_{1}(\ora{x}))} \ora{x} \xra{Z_{\ora{x}0}}
    0$.
    
    Let $Z_{\ora{x}0}=(\mathrel{\triangleleft},c)$.  Since $C_{2}$ is negative, we
    deduce that $c\neq\infty$.  From
    $(\dagger_{3})$, we infer
    $Z_{\ora{x}0}\leq(\leq,M)$ and $0\leq c\leq M$.
    
    Since $C_{1}$ is not negative, we get
    $(\leq,0)\leq(\mathrel{\triangleleft},c+v_{1}(\ora{x}))$, which is equivalent to
    $-c\leq v_{1}(\ora{x})$.  Using $v_{1}\sim_{M}v_{2}$ and
    $0\leq c\leq M$ we deduce that $-c\leq v_{2}(\ora{x})$.  This is
    equivalent to $(\leq,0)\leq(\mathrel{\triangleleft},c+v_{2}(\ora{x}))$, a
    contradiction with $C_{2}$ being a negative cycle.
    
  \item Cycle
    $C_{2}=0 \xra{Z_{0\ora{x}}} \ora{x} \xra{(\leq,-v_{2}(\ora{x}))}
    0$.  We have
    $C_{1}=0 \xra{Z_{0\ora{x}}} \ora{x} \xra{(\leq,-v_{1}(\ora{x}))}
    0$.
    
    Let $Z_{0\ora{x}}=(\mathrel{\triangleleft},c)$.  Since $C_{2}$ is negative, we
    deduce that $-v_{2}(\ora{x})\neq\infty$.  Using
    $v_{1}\sim_{M}v_{2}$, we infer $-v_{1}(\ora{x})\neq\infty$.  Since
    $C_{1}$ is not negative, we get $Z_{0\ora{x}}\neq(\leq,-\infty)$.
    From
    $(\dagger_{6})$, we infer
    $(<,-M)\leq Z_{0\ora{x}}$ and $-M\leq c\leq 0$.
    
    Since $C_{1}$ is not a negative cycle, we get
    $(\leq,0)\leq(\mathrel{\triangleleft},c-v_{1}(\ora{x}))$, which is equivalent to
    $v_{1}(\ora{x})\leq c$.
    Using $v_{1}\sim_{M}v_{2}$ and $-M\leq c\leq 0$, we deduce that
    $v_{2}(\ora{x})\leq c$.  This is equivalent to
    $(\leq,0)\leq(\mathrel{\triangleleft},c-v_{2}(\ora{x}))$, a contradiction with
    $C_{2}$ being a negative cycle.
  
  \item Cycle
    $C_{2}=0 \xra{(\leq,v_{2}(\ola{y}))} \ola{y}
    \xra{Z_{\ola{y}\ora{x}}} \ora{x} \xra{(\leq,-v_{2}(\ora{x}))} 0$.
        
    We have
    $C_{1}=0 \xra{(\leq,v_{1}(\ola{y}))} \ola{y}
    \xra{Z_{\ola{y}\ora{x}}} \ora{x} \xra{(\leq,-v_{1}(\ora{x}))} 0$.

    Let $Z_{\ola{y}\ora{x}}=(\mathrel{\triangleleft},c)$.  As in case 1 above, we get
    $0 \leq v_{1}(\ola{y}) \leq M$.  From the fact that the cycle
    $0 \xra{(\leq,v_{1}(\ola{y}))} \ola{y} \xra{Z_{\ola{y}0}} 0$ is
    not negative, we get $(\leq,-M)\leq Z_{\ola{y}0}$.  Since $C_{2}$
    is negative, we get $-v_{2}(\ora{x})\neq\infty$.  Using
    $v_{1}\sim_{M}v_{2}$, we infer $-v_{1}(\ora{x})\neq\infty$.  From
    the fact that the cycle
    $0 \xra{Z_{0\ora{x}}} \ora{x} \xra{(\leq,-v_{1}(\ora{x}))} 0$ is
    not negative, we deduce $Z_{0\ora{x}}\neq(\leq,-\infty)$.  Using
    $(\dagger_{5})$
    we obtain
    $$
    (\leq,-M)+(<,-M)\leq Z_{\ola{y}0}+(<,-M) \leq Z_{\ola{y}\ora{x}}
    =(\mathrel{\triangleleft},c)
    $$
    and we deduce that $-2M\leq c\leq 0$.
    
    Since $C_{1}$ is not a negative cycle, we get
    $(\leq,0)\leq(\mathrel{\triangleleft},c+v_{1}(\ola{y})-v_{1}(\ora{x}))$, which is
    equivalent to $v_{1}(\ora{x})-v_{1}(\ola{y})\leq c$.  Using
    $v_{1}\sim_{M}v_{2}$ and $-2M\leq c\leq 0$ we deduce that
    $v_{2}(\ora{x})-v_{2}(\ola{y})\leq c$.  We conclude as in the
    previous cases.
    
  \item Cycle
    $C_{2}=0 \xra{(\leq,v_{2}(\ora{x}))} \ora{x}
    \xra{Z_{\ora{x}\ola{y}}} \ola{y} \xra{(\leq,-v_{2}(\ola{y}))} 0$.

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

    Let $Z_{\ora{x}\ola{y}}=(\mathrel{\triangleleft},c)$.  Since $C_{2}$ is a negative
    cycle, we deduce that $c\neq\infty$.  From
    $(\dagger_{4})$ we deduce that
    $Z_{\ora{x}0}\leq(\leq,M)$.
    Since
    $0 \xra{(\leq,v_{1}(\ora{x}))} \ora{x} \xra{Z_{\ora{x}0}} 0$ is
    not a negative cycle, we get $-M\leq v_{1}(\ora{x})$.
    As in case 2 above, we get $0\leq v_{1}(\ola{y})\leq M$.  Finally,
    we obtain $0\leq v_{1}(\ola{y})-v_{1}(\ora{x})\leq 2M$.

    Since $C_{1}$ is not a negative cycle, we get
    $(\leq,0)\leq(\mathrel{\triangleleft},c+v_{1}(\ora{x})-v_{1}(\ola{y}))$, which is
    equivalent to $v_{1}(\ola{y})-v_{1}(\ora{x})\leq c$.  Using
    $v_{1}\sim_{M}v_{2}$ and
    $0\leq v_{1}(\ola{y})-v_{1}(\ora{x})\leq 2M$, we deduce that
    $v_{2}(\ola{y})-v_{2}(\ora{x})\leq c$.  We conclude as in the
    previous cases.
        
  \item Cycle
    $C_{2}=0 \xra{(\leq,v_{2}(\ora{x}))} \ora{x}
    \xra{Z_{\ora{x}\ola{y}}} \ola{y} \xra{(\mathrel{\triangleleft}',-c')} 0$.

    We have
    $C_{1}=0 \xra{(\leq,v_{1}(\ora{x}))} \ora{x}
    \xra{Z_{\ora{x}\ola{y}}} \ola{y} \xra{(\mathrel{\triangleleft}',-c')} 0$.

    Let $Z_{\ora{x}\ola{y}}=(\mathrel{\triangleleft},c)$.  Since $C_{2}$ is a negative
    cycle, we deduce that $c\neq\infty$.
    From
    $(\dagger_{4})$ we deduce that
    $Z_{\ora{x}0}\leq(\leq,M)$.  As in case 6 above, we deduce that
    $-M\leq v_{1}(\ora{x})\leq 0$.

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

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

    Let $Z_{\ora{x}\ora{y}}=(\mathrel{\triangleleft},c)$.  Since $C_{2}$ is a negative
    cycle, we deduce that $c\neq\infty$ and
    $v_{2}(\ora{y})\neq-\infty$.  Using $v_{1}\sim_{M}v_{2}$ we deduce
    that $v_{1}(\ora{y})\neq-\infty$.  Since $C_{1}$ is not negative,
    we get $c\neq-\infty$.
    
    From
    $(\dagger_{7})$ and
    $c\notin\{-\infty,\infty\}$, we deduce that $-M\leq c \leq M$.

    Since $C_{1}$ is not a negative cycle, we get
    $(\leq,0)\leq(\mathrel{\triangleleft},c+v_{1}(\ora{x})-v_{1}(\ora{y}))$, which is
    equivalent to $v_{1}(\ora{y})-v_{1}(\ora{x})\leq c$.  Using
    $v_{1}\sim_{M}v_{2}$ and $-M\leq c \leq M$, we deduce that
    $v_{2}(\ora{y})-v_{2}(\ora{x})\leq c$.  We conclude as in the
    previous cases.
    
  \item Cycle
    $C_{2}=0 \xra{(\leq,v_{2}(\ola{x}))} \ola{x}
    \xra{Z_{\ola{x}\ola{y}}} \ola{y} \xra{(\leq,-v_{2}(\ola{y}))} 0$
    with $x\neq y$.

    We have
    $C_{1}=0 \xra{(\leq,v_{1}(\ola{x}))} \ola{x}
    \xra{Z_{\ola{x}\ola{y}}} \ola{y} \xra{(\leq,-v_{1}(\ola{y}))} 0$.
    
    As in case 1 above, we get $0\leq v_{1}(\ola{x})\leq M$.  As in
    case 2 above, we get $0\leq v_{1}(\ola{y})\leq M$.  We obtain
    $-M\leq v_{1}(\ola{y})-v_{1}(\ola{x}) \leq M$.

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

    We have
    $C_{1}=0 \xra{(\leq,v_{1}(\ola{x}))} \ola{x}
    \xra{Z_{\ola{x}\ola{y}}} \ola{y} \xra{(\mathrel{\triangleleft}',-c')} 0$.
    
    As in case 1 above, we get $0\leq v_{1}(\ola{x})\leq M$.

    Let $Z_{\ola{x}\ola{y}}=(\mathrel{\triangleleft},c)$.  Since $C_{1}$ is not
    negative, we get $0\leq c+v_{1}(\ola{x})-c'$, which is equivalent
    to $c'-c\leq v_{1}(\ola{x})$.  Using $v_{1}\sim_{M}v_{2}$ and
    $0\leq v_{1}(\ola{x})\leq M$, we deduce that
    $c'-c\leq v_{2}(\ola{x})$, which is equivalent to
    $0\leq c+v_{2}(\ola{x})-c'$, a contradiction with $C_{2}$ being a
    negative cycle.  \qedhere
  \end{enumerate}
\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_{\mathcal{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 $\ensuremath{\mathsf{EZG}}(\mathcal{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=\mathcal{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$, 
  ${\downarrow}_{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
  ${\downarrow}_{G}Z_{i}={\downarrow}_{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 regions.
This is similar to the exponential blow up that happens in normal timed automata. 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
$\mathcal{G}$-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 $\mathcal{G}$-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}. 

