Simulations for Event-Clock Automata

S Akshay, Paul Gastin, R Govind, B Srivathsan

► To cite this version:

S Akshay, Paul Gastin, R Govind, B Srivathsan. Simulations for Event-Clock Automata. Logical Methods in Computer Science, 2024, 23 (3), pp.2. 10.46298/LMCS-20(3:2)2024 . hal-05052201

HAL Id: hal-05052201

https://hal.science/hal-05052201v1

Submitted on 30 Apr 2025

**HAL** is a multi-disciplinary open access
archive for the deposit and dissemination of sci-
entific research documents, whether they are pub-
lished or not. The documents may come from
teaching and research institutions in France or
abroad, or from public or private research centers.

L'archive ouverte pluridisciplinaire HAL, est
destinée au dépôt et à la diffusion de documents
scientifiques de niveau recherche, publiés ou non,
émanant des établissements d'enseignement et de
recherche français ou étrangers, des laboratoires
publics ou privés.

<figure><img src="image_1.png" /></figure>

Distributed under a Creative Commons Attribution 4.0 International License
# SIMULATIONS FOR EVENT-CLOCK AUTOMATA

S. AKSHAY ⚪<sup>a</sup>, PAUL GASTIN ⚪<sup>b,d</sup>, R. GOVIND ⚪<sup>a,e</sup>, AND B. SRIVATHSAN ⚪<sup>c,d</sup>

<sup>a</sup> Department of Computer Science and Engineering, Indian Institute of Technology Bombay, Mumbai, India

e-mail address: akshayss@cse.iitb.ac.in

<sup>b</sup> Université Paris-Saclay, ENS Paris-Saclay, CNRS, LMF, 91190, Gif-sur-Yvette, France

e-mail address: paul.gastin@ens-paris-saclay.fr

<sup>c</sup> Chennai Mathematical Institute, India

e-mail address: sri@cmi.ac.in

<sup>d</sup> CNRS, ReLaX, IRL 2000, Siruseri, India

<sup>e</sup> Uppsala University, Sweden

e-mail address: govind.rajanbabu@it.uu.se

**ABSTRACT.** Event-clock automata (ECA) are a well-known semantic subclass of timed automata (TA) which enjoy admirable theoretical properties, e.g., determinizability, and are practically useful to capture timed specifications. However, unlike for timed automata, there exist no implementations for checking non-emptiness of event-clock automata. As ECAs contain special prophecy clocks that guess and maintain the time to the next occurrence of specific events, they cannot be seen as a syntactic subclass of TA. Therefore, implementations for TA cannot be directly used for ECAs, and moreover the translation of an ECA to a semantically equivalent TA is expensive. Another reason for the lack of ECA implementations is the difficulty in adapting zone-based algorithms, critical in the timed automata setting, to the event-clock automata setting. This difficulty was studied by Geeraerts et al. in 2011, where the authors proposed a zone enumeration procedure that uses zone extrapolations for finiteness.

In this article, we propose a different zone-based algorithm to solve the reachability problem for event-clock automata, using simulations for finiteness. A surprising consequence of our result is that for event-predicting automata, the subclass of event-clock automata that only use prophecy clocks, we obtain finiteness even without any simulations. For general event-clock automata, our new algorithm exploits the *G*-simulation framework, which is the coarsest known simulation relation in timed automata literature, and has been recently used for advances in other extensions of timed automata.

**Key words and phrases:** Event-clock automata, verification, zones, simulations, reachability.
A preliminary version of this paper appeared in [AGGS22].

This work was supported by DST/CEFIPRA/INRIA Project EQuaVE. S. Akshay was partially supported by DST/SERB Matrics Grant MTR/2018/000744. Paul Gastin was partially supported by ANR project Ticktac (ANR-18-CE40-0015). The bulk of this work was carried out while R. Govind was a postdoctoral fellow at Indian Institute of Technology Bombay.

<figure><img src="image_2.png" /></figure>

<figure><img src="image_3.png" /></figure>
# 1. INTRODUCTION

Timed automata (TA) [AD94] 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 [AD94]. 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 [LPY97, BDL+06], KRONOS [BDM+98], PAT [SLDP09], RED [Wan06], TChecker [HP19], Theta [THV+17], LTS-Min [KLM+15], Symrob [RSM19], MCTA [KWNP08], etc. Most of these tools have a common underlying algorithm which is an explicit enumeration of reachable configurations stored as *zones* [BY03]. 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 asks whether the system represented by a TA $\mathcal{A}$ satisfies the specification given by a TA $\mathcal{B}$. This problem reduces to checking language inclusion $\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, is often less than ideal for modeling timed specifications. This has led to the introduction of event-clocks and the corresponding model of *event-clock automata (ECA)* [AFH99]. 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 [DT04, ABG13, RS99], which are often used as specification languages and can be converted into ECA. On the other hand, ECAs can be determinized and hence complemented. So, model-checking event-clock specifications over TA models can be reduced to the emptiness problem on the product of the TA with an ECA (for the complement of the specification). 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.

Note that ECAs are a semantic (and not syntactic) subclass of TAs., i.e., while the class of languages recognized by ECA are a subclass of the class of languages recognized by TA, syntactically ECAs are not a subclass of TAs. Thus, even though there are several efficient zone-based algorithms based on time-abstract simulations for timed automata, these cannot be directly applied to event-clock automata. In the work that first introduced ECA [AFH99], a translation from an event-clock automaton to an equivalent timed automaton was also proposed. One could, in principle, first translate a given ECA into a timed automaton using the translation proposed in [AFH99], and then run the state-of-the-art reachability algorithm of [GMS18, GMS19, GMS20] on this timed automaton. However, the translation from ECA to TA is not efficient: in the worst case, this translation incurs a blowup that is linear in the number of clocks and exponential in the number of clocks [GRS14].
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 ECAs with recent approaches for TAs 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ïve enumeration does not terminate. One approach to guarantee termination is to make use of an *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 *simulation* approach to zone enumeration has been designed, where enumerated zones are left unchanged (i.e., no extrapolation). 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 [HSW12] which is based on maximum constants appearing in lower and upper bounded constraints in the TA, or the *G*-simulation [GMS20], which is based on a carefully-chosen set of constraints from the TA. Coarser simulations lead to fewer zones being enumerated. The *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 [HSW13], (2) the simulation approach has been extended to richer models like timed automata with diagonal constraints [GMS19, GMS18], updatable timed automata [GMS20], weighted timed automata [BCM16] and pushdown timed automata [AGP21]. In these richer models, extrapolation has either been shown to be impossible [Bou04] 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 [GRS11, GRS14]. 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.

**Our contributions.** Given the advantages of using simulations with respect to extrapolations in the TA setting described above, we extend the *G*-simulation approach to ECA. Here are the technical contributions leading to the result.

* 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 event-zones. This simplifies the reasoning and allows us to adapt many ideas for simulation developed in the TA setting directly to the ECA setting.
* The $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.

* 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.

* Finally, we show that the reachability algorithm using the $G$-simulation terminates for ECA: for every sequence $Z_0, Z_1, \dots$ of event-zones that are *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 event-zones which are incomparable with respect to the new $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.

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 *reachable* event-zones, the constraints involving *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. This observation is similar in spirit to an early work on automata with timers [Dil89], whose symbolic analysis was shown to terminate without additional constructions.

A preliminary version of this paper appeared in the conference proceedings [AGGS22]. The current version includes cleaner proofs and additional intuitions. Most importantly, we identify a mistake in the conference version and fix it here. Event-clocks can sometimes take *undefined values* – for instance, before seeing the first *a*, the history clock recording the time since the previous *a* is undefined, and similarly after seeing the last *a*, the prophecy clock predicting the next occurrence to *a* is undefined. One of the key contributions of this work is the novel mechanism to represent these undefined values using $+\infty$ and $-\infty$ and seamlessly integrating the manipulation of these quantities along with the finite (real) values. This required the definition of a new algebra to handle weights in the graph representation of event-zones. In the conference version, we had wrongly claimed that an event-zone is empty iff its graph representation has a negative cycle. We explain in Section 4 that this is not true as it is stated, due to the subtle interplay between finite and infinity weights. We fix this by introducing a *standard form* for the graph representation, and a *normal form* that is obtained from graphs in standard form. These changes have a significant impact on many of the proofs in the later sections and lead to a clearer presentation. As a result we are able to avoid certain cases, while in other places we use our new lemmas to get more succinct proofs.

As a follow-up to [AGGS22], an extended model of *Generalized Timed Automata* has been proposed, implemented in the open source tool TChecker, and is publicly available [AGG+23]. This model subsumes event-clock automata, and also contains diagonal constraints. Reachability is undecidable for this model, and a decidable fragment has been identified. The decidable fragment strongly subsumes event-clock automata, and requires further sophisticated analysis of the objects that we develop in this document.
**Organization of the paper.** Section 2 recalls ECA and describes a slightly modified presentation of the ECA semantics. Section 3 introduces event-zones, event zone graph and the simulation-based reachability framework. Section 4 introduces the new algebra for representing event-zones and describes some operations needed to build the zone graph. Section 5 introduces the *G*-simulation for event-clock automata and gives the simulation test. Section 6 proves finiteness of the simulation when restricted to reachable zones.

## 2. EVENT-CLOCK AUTOMATA AND VALUATIONS

Let $X$ be a finite set of real-valued variables called *clocks*. Let $\bar{\mathbb{R}} = \mathbb{R} \cup \{-\infty, +\infty\}$ denote the set of all real numbers along with $-\infty$ and $+\infty$. The usual $<$ order on reals is extended to deal with $\{-\infty, +\infty\}$ as: $-\infty < c, c < +\infty$ for all $c \in \mathbb{R}$ and $-\infty < +\infty$. Similarly, $\bar{\mathbb{Z}} = \mathbb{Z} \cup \{-\infty, +\infty\}$ denotes the set of all integers along with $-\infty$ and $+\infty$. Let $\mathbb{R}_{\ge 0}$ (resp. $\mathbb{R}_{< 0}$) be the set of non-negative (resp. non-positive) reals. Let $\Phi(X)$ denote a set of clock constraints generated by the following grammar: $\varphi ::= x \triangleleft c \mid c \triangleleft x \mid \varphi \land \varphi$ where $x \in X$, $c \in \bar{\mathbb{Z}}$ and $\triangleleft \in \{\langle, \le\}$. The base constraints of the form $x \triangleleft c$ and $c \triangleleft x$ will be called *atomic constraints*. Constraints $x < -\infty$ and $+\infty < x$ are equivalent to *false* and constraints $-\infty \le x$ and $x \le +\infty$ are equivalent to *true*.

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

**Definition 2.1 (Valuation).** A valuation of event-clocks is a function $v: X \mapsto \bar{\mathbb{R}}$ which maps history clocks to $\mathbb{R}_{\ge 0} \cup \{+\infty\}$ and prophecy clocks to $\mathbb{R}_{< 0} \cup \{-\infty\}$. We say a history clock $\overleftarrow{a}$, for some $a \in \Sigma$ is *undefined* (resp. *defined*) when $v(\overleftarrow{a}) = +\infty$ (resp. $v(\overleftarrow{a}) < +\infty$) and a prophecy clock $\overrightarrow{a}$ is undefined (resp. defined) when $v(\overrightarrow{a}) = -\infty$ (resp. $-\infty < v(\overrightarrow{a})$). We denote by $V(X)$ or simply by $V$ the set of valuations over $X$.

We remark that the history clock and the
prophecy clock of an event *a* are symmetric no-
tions, as illustrated in Figure 2. In the semantics
that we introduce in this paper, history clock $\overleftarrow{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, $\overleftarrow{a}$ is set to $+\infty$. The prophecy clock $\overrightarrow{a}$ stores the negative of the amount of time that needs to be elapsed before seeing the next *a*. In other words, $-\overrightarrow{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., $\overrightarrow{a} = -\infty$.

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

**Remark 2.2.** In the earlier works on ECA [AFH99, GRS14], 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., $\overrightarrow{a} \le 5$ means that the next *a* occurs in at most 5

<figure><img src="image_4.png" /><figcaption>Figure 1: Valuation of event-clocks.</figcaption></figure>
time units. In our convention, this would be written as $-5 \le \vec{a}$. Secondly, an undefined clock (history or prophecy) was assigned a special symbol $\perp$ 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.

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

We write $[\overleftarrow{a}]v$ to denote the valuation $v'$ obtained from $v$ by resetting the history clock $\overleftarrow{a}$ to 0, keeping the value of other clocks unchanged. We denote by $[\vec{a}]v$ the set of valuations $v'$ obtained from $v$ by setting the prophecy clock $\vec{a}$ non-deterministically to some value in $[-\infty, 0]$, keeping the value of other clocks unchanged. We see $[\vec{a}]v$ as the result of an operation $[\vec{a}]$ on valuation $v$, which we call the *release* of $a$ from $v$. The idea is that $v$ maintains an exact value for the next occurrence of $a$. On releasing $a$ from $v$, this value is forgotten and a fresh guess is made for the next $a$. This fresh guess has no constraints and can take any value between $-\infty$ and 0. As an example, consider a valuation $v$ over two events $a$ and $b$, with $v(\vec{a}) = 0, v(\overleftarrow{b}) = -2$, and some arbitrary values for the history clocks $v(\overleftarrow{a})$ and $v(\vec{b})$. This valuation $v$ predicts that the next $a$ will occur immediately, whereas $b$ will occur in two time units from now. By releasing $a$ from $v$, we get a set $[\vec{a}]v$ with valuations containing the different possible orders between the next occurrences of $a$ and $b$: for instance, pick $v_1, v_2 \in [\vec{a}]v$ with $v_1(\vec{a}) = -3, v_2(\vec{a}) = -0.5$. In both the valuations, the value of $\vec{b}$ retains the value $-2$ from $v$. Therefore, valuation $v_1$ predicts that $a$ will occur after $b$, whereas $v_2$ predicts that $a$ will occur before $b$. There is also a valuation $v_3 \in [\vec{a}]v$ with $v_3(\vec{a}) = -\infty$. This valuation says that $a$ will never occur from hereon.

The next operation on valuations is that of a *time elapse*. We denote by $v + \delta$ the valuation obtained by increasing the value of all clocks from the valuation $v$ by $\delta \in \mathbb{R}_{\ge 0}$. The time elapse operation is illustrated in Figure 2. 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(\vec{a}) = -3$ and $v(\overleftarrow{b}) = -2$ can elapse at most 2 time units.

**Definition 2.3 (Event-clock automata [AFH99])**. An *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 = X_H \cup X_P$ 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. 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 *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$. A configuration $(q, v)$ is accepting if $q \in F$, and $v(x) = -\infty$ for all $x \in X_P$. Transitions of $S_{\mathcal{A}}$ are of two forms:

* **Delay transition**: $(q, v) \xrightarrow{\delta} (q, v + \delta)$, if $(v + \delta)(x) \le 0$ for all $x \in X_P$.

* **Action transition**: $(q, v) \xrightarrow{t} (q', [\overleftarrow{a}]v')$ if $t = (q, a, g, q')$ is a transition in $\mathcal{A}$, $v(\vec{a}) = 0$, $v' \in [\vec{a}]v$ and $v' \models g$.

A transition with action $a$ can be taken when the value of the prophecy clock $\vec{a}$ is 0, then a new value in $[-\infty, 0]$ for $\vec{a}$ is non-deterministically guessed so that the resulting valuation $v'$ satisfies the guard $g$, and finally, the history clock $\overleftarrow{a}$ is reset to 0.
<figure><img src="image_5.png" /><figcaption>Figure 2: Representation of valuations in event-clock automata. Here, $v' = v + \delta$.</figcaption></figure>

**Remark 2.4.** In the semantics for ECA defined above, we say that a configuration is accepting only if $v(x) = -\infty$ for all prophecy clocks. Analogously, for initial configurations, we ask that all the history clocks are set to $+\infty$.

Here is an example to illustrate the transition semantics. A transition $t = (q, a, g, q')$ with guard $g := (\overleftarrow{a} \le 5) \land (-3 \le \overrightarrow{a}) \land (\overrightarrow{b} \le -\infty)$ can be taken if the previous $a$ was seen within 5 units, the next $a$ will be seen within 3 units and there will be no $b$ anymore. A valuation $v$ can take this transition provided $v(\overleftarrow{a}) \le 5$, $v(\overrightarrow{b}) = -\infty$ and $v(\overrightarrow{a}) = 0$. At this point, the guard $-3 \le \overrightarrow{a}$ is not used. This constraint plays a role in the value to which $\overrightarrow{a}$ is released to: the only possible values of $\overrightarrow{a}$ after taking the transition lie in the interval $[-3, 0]$. More precisely, if $(q, v) \xrightarrow{t} (q', [\overleftarrow{a}]v')$, then $v'(\overrightarrow{a}) \in [-3, 0]$. Notice that in $[\overleftarrow{a}]v'$, the value of the history clock $\overleftarrow{a}$ is set to 0 to record the information that $a$ was just seen. Figure 3 gives an example of an ECA. Intuitively, this ECA recognizes sequences of the form $b^+a$ where there exists a $b$ (not necessarily the last one) at time 1 before the final letter $a$.

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 *run* of an event-clock automaton is a finite sequence of transitions from an initial configuration of $S_A$. A run is said to be *accepting* if its last configuration is accepting. We are interested in the *reachability problem* of an event-clock automaton. Formally,

**Definition 2.5** (Reachability problem for ECA). The reachability problem for an event-clock automaton $\mathcal{A}$ is to decide whether $\mathcal{A}$ has an accepting run.

Different solutions based on regions and zones have been proposed in [AFH99, GRS11, GRS14]. 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, [GRS11] show that the standard region abstraction is not possible, as there exists no finite bisimulation due to the behavior of prophecy clocks. We provide an intuitive reasoning for this fact. Pick some $\alpha \ge 0$. From a valuation $v_\alpha$ with $v_\alpha(\overrightarrow{a}) = -\alpha$ and $v_\alpha(\overleftarrow{b}) = 0$, we can see $[\alpha]$ (the greatest integer smaller than or equal to $\alpha$) occurrences of $b$, if we assume that the time between consecutive $b$'s is 1 (see Figure 3 of [GRS14] or Figure 11 for a detailed example).
This creates a difference between $v_α$, and say $v_{α+1}$, since there is an extra occurrence of $b$ possible from $v_{α+1}$. Therefore, there is no constant $M \ge 0$ such that we can put all valuations $v_α$ with $\alpha < -M$ into one “equivalence class”. In other words, there is no $M$ for which we can forget the actual value of $\overrightarrow{d}$ as long as it is less than $-M$. This is in sharp contrast with history clocks (and classical timed automata) where once a clock goes beyond a maximum constant $M$, its actual value can be forgotten. In some sense, time elapse moves history clocks above some $M$ only further away from $M$, whereas for prophecy clocks time elapse brings clocks which are $< -M$ closer to $-M$ and at some point they cross $-M$ and are no longer $< -M$. This creates a fundamental issue causing the impossibility of finite bisimulations. Also, the standard definition of zones used for timed automata is not sufficient to handle valuations with undefined clocks. The papers [GRS11, GRS14] make use of special symbols $\perp$ 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 = \perp$ (resp. $x \neq \perp$) to state that a clock is undefined (resp. defined) as in [GRS11, GRS14], we write $+\infty \le x \le$ or $x \le -\infty$ (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.

### 3. EVENT-ZONES AND SIMULATION-BASED REACHABILITY

The most widely used approach for checking reachability in a timed automaton is based on reachability in a graph called the *zone graph* of a timed automaton [DT98]. Roughly, *zones* [BY03] are sets of valuations that can be represented efficiently using constraints between differences of clocks. In this section, we introduce an analogous notion for event-clock automata. We consider *event zones*, which are special sets of valuations of event-clock automata.

**Definition 3.1 (Weights).** Let $\mathcal{C} = \{(\triangleleft, c) \mid c \in \overline{\mathbb{R}} \text{ and } \triangleleft \in \{\leq, <\}\},$ called the set of weights.

We will use constraints of the form $y - x \triangleleft c$ with $(\triangleleft, c) \in \mathcal{C}$ and $x, y \in X \cup \{0\}$ (event-clocks are extended with the special constant clock 0, meaning that $v(0) = 0$ for all valuations $v \in \mathcal{V}$). Such constraints, between two clocks are sometimes called diagonal constraints. The introduction of the special constant clock allows us to treat constraints with just a single clock (sometimes referred to as non-diagonal constraints) as special cases. Indeed, for all weights $(\triangleleft, c) \in \mathcal{C}$, the constraint $x \triangleleft c$ is equivalent to $x - 0 \triangleleft c$ and the constraint $c \triangleleft x$ is equivalent to $0 - x \triangleleft -c$.

To evaluate such constraints, we extend addition on real numbers with the convention that $(+\infty) + \alpha = \alpha + (+\infty) = +\infty$ for all $\alpha \in \overline{\mathbb{R}}$ and $(-\infty) + \beta = \beta + (-\infty) = -\infty$, as long as $\beta \neq +\infty$. We also extend the unary minus operation from real numbers to $\overline{\mathbb{R}}$ by setting $-(+\infty) = -\infty$ and $-(-\infty) = +\infty$. Abusing notation, we write $\beta - \alpha$ for $\beta + (-\alpha)$. Notice that with this definition of extended addition, the minus operation does not distribute over addition.<fnref n="1" /> We now highlight a few more important features of this definition.

**Remark 3.2.** This extended addition has the following properties that are easy to check: (1) $(\overline{\mathbb{R}}, +, 0)$ is a monoid with 0 as neutral element. In particular, the extended addition is associative.

<footnote n="1">¹Notice that $-(a+b) = (-a) + (-b)$ when $a$ or $b$ is finite or when $a = b$. But, when $a = +\infty$ and $b = -\infty$ then $-(a+b) = -\infty$ whereas $(-a) + (-b) = +\infty$.</footnote>
(2) $(\overline{\mathbb{R}}, +, 0)$ is not a group, since $-\infty$ and $+\infty$ have no opposite values. Note that, $\alpha + (-\alpha) = 0$ when $\alpha \in \mathbb{R}$ is finite but $\alpha + (-\alpha) = +\infty$ when $\alpha \in \{-\infty, +\infty\}$. As a consequence, in an equation $\alpha + \beta = \alpha + \gamma$, we can cancel $\alpha$ and deduce $\beta = \gamma$ when $\alpha$ is finite, but not when $\alpha$ is infinite.

(3) The order $\leq$ is monotone on $\overline{\mathbb{R}}$: $b \leq c$ implies $a+b \leq a+c$, but the converse implication only holds when $a$ is finite.

(4) The strict order $<$ is only monotone with respect to finite values: when $a$ is finite, $b < c$ iff $a+b < a+c$.

(5) For all $a, b \in \overline{\mathbb{R}}$ and $(\triangleleft, c) \in \mathcal{C}$, we have $a \triangleleft b$ iff $-b \triangleleft -a$. Further, $a - b \triangleleft c$ implies $a \triangleleft b + c$. The converse of the latter statement holds when $b$ is finite, but may be false when $b$ is infinite.<fnref n="2" />

**Definition 3.3.** Let $x, y \in X \cup \{0\}$ be event-clocks (including 0) and $(\triangleleft, c) \in \mathcal{C}$ be a weight. For valuations $v \in \mathbb{V}$, define $v \models y - x \triangleleft c$ as $v(y) - v(x) \triangleleft c$.

**Remark 3.4.** From Definition 3.3, we easily check that the constraint $y - x \triangleleft c$ is equivalent to true (resp. false) when $(\triangleleft, c) = (\leq, +\infty)$ (resp. $(\triangleleft, c) = (\langle, -\infty))$: for all valuations $v \in \mathbb{V}$, $v \models y - x \leq +\infty$ and $v \not\models y - x < -\infty$. Constraints that are equivalent to true or false will be called trivial, whereas all others are non-trivial constraints.

If $(\triangleleft, c) \neq (\leq, +\infty)$ then $v \models y - x \triangleleft c$ never holds when $v(x) = -\infty$.

Also, if $v(x) = v(y) \in \{-\infty, +\infty\}$ then $v \models y - x \triangleleft c$ only holds for $(\triangleleft, c) = (\leq, +\infty)$.

Consider now a non-trivial constraint $y - x \triangleleft c$ with weight $(\triangleleft, c) \in \mathcal{C} \setminus \{\langle, -\infty\}, (\leq, +\infty)\}$. We have $v \models y - x \triangleleft c$ iff $v(y) < +\infty = v(x)$ or $(v(x)$ is finite and $v(y) \triangleleft v(x) + c)$.
Let us consider special cases of Definition 3.3.

* $v \models y - x \leq -\infty$ iff $v(y) < +\infty = v(x)$ or $v(y) = -\infty < v(x)$.

* $v \models y - x < +\infty$ iff $v(x) \neq -\infty$ and $v(y) \neq +\infty$.

<figure><img src="image_6.png" /></figure>

**Definition 3.5 (Event-zones).** An event-zone is a set of valuations satisfying a conjunction of constraints of the form $y - x \triangleleft c$, where $x, y \in X \cup \{0\}$, $c \in \overline{\mathbb{Z}} = \mathbb{Z} \cup \{-\infty, +\infty\}$ and $\triangleleft \in \{\leq, <\}$.

Let $W$ be an arbitrary set of valuations (not necessarily an event-zone) and $q$ be a state. For transition $t := (q, a, g, q_1)$, we write $(q, W) \xrightarrow{t} (q_1, W_t)$ if $W_t = \{v_1 \mid v_1$ is a valuation and $(q, v) \xrightarrow{t} (q_1, v_1)$ for some $v \in W$ and $\delta \in \mathbb{R}_{\geq 0}\}$. Notice that we have action $\xrightarrow{t}$ followed by delay $\xrightarrow{\delta}$ in this definition, a common convention adopted in the timed automata literature. This results in the set $W_t$ being closed under time-successors. We will show in the next section that starting from an event-zone $Z$, the successors are also event-zones: $(q, Z) \xrightarrow{t} (q_1, Z_t)$ implies $Z_t$ is an event-zone too. We use this feature to define an event-zone graph.

**Definition 3.6 (Event-zone graph).** Given an ECA $\mathcal{A}$, its *event-zone graph*, denoted $EZG(\mathcal{A})$, is defined as follows: 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 \overleftarrow{a}) \wedge (\overrightarrow{a} \leq 0))$. This is the set of all initial valuations, which is already closed under time elapse<fnref n="3" />. For every node $(q, Z)$ and every transition $t := (q, a, g, q_1)$ there

<footnote n="2">²For instance, if $a < +\infty = b$ then $a < b + (-\infty)$, but $a - b = -\infty \not< -\infty$.</footnote>

<footnote>If $a < +\infty$ and $b = -\infty$ then $a < b + \infty$, but $a - b = +\infty \not< +\infty$.</footnote>

<footnote>If $a = b \in \{-\infty, +\infty\}$ and $c$ is finite then $a \leq b + c$, but $a - b = +\infty \not\leq c$.</footnote>

<footnote n="3">³By definition, the time elapse operation only permits delays that keep prophecy clocks non-positive.</footnote>
is a transition $(q, Z) \stackrel{t}{\to} (q_1, Z_t)$ 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} \overrightarrow{a} \le -\infty$.

An example of ECA with its event-zone graph is given in Figure 3. We use some shorthands when writing some constraints. For instance, we write $\overrightarrow{b} - \overrightarrow{a} = 1$ for the conjunction of $\overrightarrow{b} - \overrightarrow{a} \le 1$ and $\overrightarrow{a} - \overrightarrow{b} \le -1$.<fnref n="4" /> Another example is $0 \le \overrightarrow{b} - \overrightarrow{a} \le 1$ which stands for the conjunction of $\overrightarrow{b} - \overrightarrow{a} \le 1$ and $\overrightarrow{a} - \overrightarrow{b} \le 0$.

<figure><img src="image_7.png" /><figcaption>Figure 3: The event-clock automaton $A_1$ recognizes the language $\{b^n a \mid n \ge 1\}$ such that there exists some $b$ which occurs exactly one time unit before $a$. Its event-zone graph is on the left.</figcaption></figure>

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 [DT98] from timed automata.

**Proposition 3.7.** The event-zone graph of an ECA is sound and complete for reachability.

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. In fact, in Geeraerts et al. [GRS11, GRS14], it was shown that there are ECAs for which there is no finite time-abstract bisimulation relation on valuations, e.g., the ECA $A_2$ in Figure 11.

In the rest of this section, we will define what a simulation is and see how it can be used to get a finite truncation of the event-zone graph for ECAs, which is still sound and complete for reachability.

**Definition 3.8 (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

<footnote n="4">⁴Notice that for $a, b, c \in \mathbb{R}$ and $\triangleleft \in \{\le, <\}$, if $a - b \triangleleft c$ then $-c \triangleleft b - a$. The converse is true when $a, b, c$ are finite, but not in general. For instance, when $a = b \in \{-\infty, +\infty\}$ and the weight $(\triangleleft, c) \in C \setminus \{(\le, -\infty), (\le, +\infty)\}$ is non-trivial, then $-c \triangleleft b - a = +\infty$ but $a - b = +\infty \nleq c$.</footnote>
and (1) for every $(q, v) \xrightarrow{\delta} (q, v + \delta)$, we have $(q, v') \xrightarrow{\delta} (q, v' + \delta)$ and $(q, v + \delta) \preceq (q, v' + \delta)$,
(2) for every transition $t$, if $(q, v) \xrightarrow{t} (q_1, v_1)$ for some valuation $v_1$, then $(q, v') \xrightarrow{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')$. Adopting the terminology from [GMS18, GMS19, GMS20], we say that the simulation $\preceq$ is *finite* if for every sequence $(q_1, Z_1), (q_2, Z_2), \dots$ of *reachable* nodes (i.e., those having a path from initial node), there exists $j > i$ such that $(q_j, Z_j) \preceq (q_i, Z_i)$. That is, the converse or transpose of $\preceq$ is a well-quasi order over reachable nodes, and thus the set of downward closed sets is finite.

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.

**Definition 3.9 (Reachability algorithm).** 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:

* Pop a node $(q, Z)$ from the Waiting list and add it to the Passed list.

* For every $(q, Z) \xrightarrow{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.

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.

The correctness of the reachability algorithm follows from the fact that $\preceq$ is a simulation relation. Moreover, termination is guaranteed when the simulation used is finite.

**Theorem 3.10.** An ECA has an accepting run iff the reachability algorithm returns Yes.

We have now presented the framework for the simulation approach in its entirety. However, to make it functional, we will need the following.

(1) An efficient representation for event-zones and algorithms to compute successors.

(2) A concrete simulation relation $\preceq$ for ECA with an efficient simulation test $(q, Z) \preceq (q, Z')$.

(3) A proof that $\preceq$ is finite, to guarantee termination of the reachability algorithm.

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) [Dil89]. 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 4, we propose a way to merge $+\infty$ and $-\infty$ seamlessly into the DBM technology. In the subsequent Section 5, we define a simulation for ECA based on $\mathcal{G}$-simulation, develop some technical machinery and present an efficient simulation test. Finally, in Section 6, 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.

## 4. COMPUTING WITH EVENT-ZONES AND DISTANCE GRAPHS

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 \triangleleft c$. For timed automata analysis, the entries could be $(<, +\infty)$ or $(\triangleleft, c)$ with $c \in \mathbb{R}$ and $\triangleleft \in \{<, \leq\}$. For ECA, we need to deal with valuations $+\infty$ or $-\infty$. For this purpose, we use more general weights as introduced in Definition 3.1 and we extend the algebra of weights to the new entries in a natural way. However, we need to rework the basic results on DBMs in our extended setting, since as we have seen in Remark 3.2, some seemingly obvious properties that hold for finite weights do not carry over to the extended weights. It turns out that even with the restricted versions of the properties that continue to hold, as listed in Remark 3.2, we can achieve the same results in the extended DBMs. This is the subject of this section.

## 4.1. Extending the algebra on weights.

**Definition 4.1 (Order and sum of weights).** Let $(\triangleleft, c), (\triangleleft', c') \in \mathcal{C}$ be weights.

**Order.** Define $(\triangleleft, c) < (\triangleleft', c')$ when either (1) $c < c'$, or (2) $c = c'$ and $\triangleleft$ is $< $ while $\triangleleft'$ is $\leq$. This is a total order with $(<, -\infty) < (\leq, -\infty) < (\triangleleft, c) < (<, +\infty) < (\leq, +\infty)$ for all $c \in \mathbb{R}$.

**Sum.** We define the commutative sum operation as follows.

$$ (<, -\infty) + \alpha = (<, -\infty) \quad \text{if } \alpha \in \mathcal{C} $$

$$ (\leq, +\infty) + \alpha = (\leq, +\infty) \quad \text{if } \alpha \in \mathcal{C} \setminus \{(<, -\infty)\} $$

$$ (\leq, -\infty) + \alpha = (\leq, -\infty) \quad \text{if } \alpha \in \mathcal{C} \setminus \{(<, -\infty), (\leq, +\infty)\} $$

$$ (<, +\infty) + \alpha = (<, +\infty) \quad \text{if } \alpha \in \mathcal{C} \setminus \{(<, -\infty), (\leq, -\infty), (\leq, +\infty)\} $$

$$ (\triangleleft, c) + (\triangleleft', c') = (\triangleleft'', c + c') \quad \text{if } c, c' \in \mathbb{R} \text{ and } \triangleleft'' = \leq \text{ if } \triangleleft = \triangleleft' = \leq \text{ and } \triangleleft'' = < \text{ otherwise.} $$

Notice that the sum of weights is an associative operation and $\alpha + (\leq, 0) = \alpha$ for all $\alpha \in \mathcal{C}$.

**Remark 4.2.** Note that our set of weights $\mathcal{C}$ has a sequence of partially absorbant elements with decreasing strength - $(<, -\infty)$ is an absorbant for $\mathcal{C}$, $(\leq, +\infty)$ is an absorbant for $\mathcal{C} \setminus \{(<, -\infty)\}$, $(\leq, -\infty)$ is an absorbant for $\mathcal{C} \setminus \{(<, -\infty), (\leq, +\infty)\}$, and $(<, +\infty)$ is an absorbant for $\mathcal{C} \setminus \{(<, -\infty), (\leq, +\infty), (\leq, -\infty)\}$. This implies that all the sums are well-defined.

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

**Lemma 4.3.** Let $x, y, z \in X \cup \{0\}$ be event-clocks, $(\triangleleft_1, c_1), (\triangleleft_2, c_2) \in \mathcal{C}$ be weights and $(\triangleleft, c) = (\triangleleft_1, c_1) + (\triangleleft_2, c_2)$. For all valuations $v \in V$, if $v \models y - x \triangleleft_1 c_1$ and $v \models z - y \triangleleft_2 c_2$, then $v \models z - x \triangleleft c$.

*Proof.* When $(\triangleleft, c) \in \{(<, -\infty), (\leq, +\infty)\}$, this is clear. We assume for the rest of the proof that $(\triangleleft, c) \in \mathcal{C} \setminus \{(<, -\infty), (\leq, +\infty)\}$ is non-trivial. Consider a valuation $v \in V$ such that $v \models y - x \triangleleft_1 c_1$ and $v \models z - y \triangleleft_2 c_2$.

From $v(y) - v(x) \triangleleft_1 c_1$ and $(\triangleleft_1, c_1) \neq (\leq, +\infty)$ we deduce that $v(y) \neq +\infty$ and $v(x) \neq -\infty$. Similarly, from $v(z) - v(y) \triangleleft_2 c_2$ and $(\triangleleft_2, c_2) \neq (\leq, +\infty)$ we deduce that $v(z) \neq +\infty$ and $v(y) \neq -\infty$. Hence, $v(y)$ is finite. If $v(x) = +\infty$, or $v(x) < +\infty$ and $v(z) = -\infty$ then $v(z) - v(x) = -\infty$, hence $v \models z - x \triangleleft c$.

The remaining case is when $v(x), v(y), v(z)$ are all finite. This rules out $(\triangleleft, c) = (\leq, -\infty)$. If $(\triangleleft, c) = (<, +\infty)$ then $v \models z - x \triangleleft c$. Otherwise, $c = c_1 + c_2$ is finite and $v(z) - v(x) = v(z) - v(y) + v(y) - v(x) \triangleleft c_2 + c_1$. This completes the proof. $\square$
The following technical lemma will be useful in many proofs.

**Lemma 4.4.**

(1) Let $\langle \triangleleft, c \rangle$ be a weight and $\alpha \in \overline{\mathbb{R}}$. Then,

• $\alpha \triangleleft c \text{ iff } (\leq, \alpha) \leq (\triangleleft, c) \text{ iff } (\leq, 0) \leq (\leq, -\alpha) + (\triangleleft, c),$

• $\alpha \nparallel c \text{ iff } (\triangleleft, c) < (\leq, \alpha) \text{ iff } (\leq, -\alpha) + (\triangleleft, c) < (\leq, 0) \text{ iff } (\leq, -\alpha) + (\triangleleft, c) \leq (<, 0).$

(2) Let $(\triangleleft, c), (\triangleleft', c'), (\triangleleft'', c'')$ be weights with $(\leq, 0) \leq (\triangleleft, c) + (\triangleleft', c')$.

Then, there exists $\alpha \in \overline{\mathbb{R}}$ such that $\alpha \triangleleft c$ and $-\alpha \triangleleft c'$.

If in addition we have $(\triangleleft'', c'') < (\triangleleft, c)$ then there exists such an $\alpha$ with $\alpha \nparallel c''$.

*Proof.*

(1) The first item is easy to prove, checking separately the cases where $\alpha$ or $c$ is infinite. The second item follows from the first one using the fact that $\leq$ is a total order on weights.

(2) Assume first that $\triangleleft = \leq$. Take $\alpha = c$. Using 1, we easily check that $\alpha$ satisfies the desired properties.

Next, assume that $\triangleleft = <$. From $(\leq, 0) \leq (\triangleleft, c) + (\triangleleft', c')$ we deduce that $c \neq -\infty \neq c'$. Next, we see that $-c' < c$ (consider separately the cases $c = +\infty$ or $c' = +\infty$). Take $\alpha$ such that $-c' < \alpha < c$. We obtain $\alpha \triangleleft c$ and $-\alpha < c'$. The latter inequality implies $-\alpha \triangleleft c'$.

If in addition we have $(\triangleleft'', c'') < (<, c)$, then $c'' < c$ and we take $\alpha$ such that $\max(-c', c'') < \alpha < c$. As above, we have $\alpha \triangleleft c$ and $-\alpha \triangleleft c'$. We also get $\alpha \nparallel c''$. $\square$

Equipped with the weights and the arithmetic over it, we will work with a graph representation of zones (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.

## 4.2. Distance graphs over the extended algebra.

**Definition 4.5 (Distance graphs).** A distance graph $\mathcal{G}$ is a weighted directed graph without self-loops, with vertex set being $X \cup \{0\} = X_P \cup X_H \cup \{0\}$, edges being labeled with weights from $C \setminus \{(\leq, -\infty)\}$.<fnref n="5" /> We define $[\mathcal{G}] := \{v \in V \mid v \models y - x \triangleleft c \text{ for all edges } x \stackrel{\triangleleft c}{\longrightarrow} y \text{ in } \mathcal{G}\}$. The weight of edge $x \to y$ is denoted $G_{xy}$ and we set $G_{xy} = (\leq, +\infty)$ if there is no edge $x \to y$.

We say that $\mathcal{G}$ is in standard form if it satisfies the following conditions;

(1) $G_{0x} \leq (\leq, 0)$ for all $x \in X_P$ and $G_{x0} \leq (\leq, 0)$ for all $x \in X_H$.

(2) For all $x, y \in X$, if $G_{xy} \neq (\leq, +\infty)$ then $G_{x0} \neq (\leq, +\infty)$ and $G_{0y} \neq (\leq, +\infty)$.

We extend the order on weights to distance graphs pointwise: Let $\mathcal{G}$, $\mathcal{G}'$ be distance graphs, we write $\mathcal{G} \leq \mathcal{G}'$ when $G_{xy} \leq G'_{xy}$ for all edges $x \to y$. Notice that this implies $[\mathcal{G}] \subseteq [\mathcal{G}']$.

Here is an example to illustrate the need for a standard form. Suppose that valuations are finite and that we have constraints: $y - x \leq 1$ and $-y \leq 2$. The distance graph representing these constraints is depicted with black edges in Figure 4. From these constraints, we can

<footnote n="5">⁵If we allowed an edge with weight $G_{xy} = (<, -\infty)$ then we would get $[\mathcal{G}] = \emptyset$ since the constraint $y - x < -\infty$ is equivalent to false.</footnote>
<figure><img src="image_8.png" /><figcaption>Figure 4: An example of a distance graph for timed automata with clocks $x, y$. The dotted edge in black denotes that the edge is obtained by canonicalization, and the dotted edge in red depicts an edge introduced by a guard.</figcaption></figure>

<figure><img src="image_9.png" /><figcaption>Figure 5: Distance graph with standardization using the extended algebra. Note that the green edges are the edges induced by standardization.</figcaption></figure>

infer $-x \le 3$ just by adding the inequalities - this corresponds to the edge depicted by dotted lines from $x$ to 0. If there was another constraint $x \le -4$ (denoted by the red dotted edge from 0 to $x$), we will get unsatisfiability, witnessed by a negative cycle $0 \stackrel{\le-4}{\longrightarrow} x \stackrel{\le3}{\longrightarrow} 0$, as depicted by the dotted edges in Figure 4. Basically, adding the weights of $x \to y$ and $y \to 0$, we get the strongest possible constraint about $x \to 0$.

This holds no more in the extended algebra, due to the fundamental difference while adding weight $(\le, +\infty)$. Consider the constraint $y - x \le 1$ corresponding to the edge $x \stackrel{\le1}{\longrightarrow} y$ in the distance graph. Recall that missing edges correspond to the constraint $(\le, +\infty)$ which is equivalent to true, hence we have implicit edges $x \stackrel{\le\infty}{\longrightarrow} 0$ and $0 \stackrel{\le\infty}{\longrightarrow} y$. These are not the strongest possible constraints on $x$ and $y$ induced by $y - x \le 1$. Indeed, any valuation $v$ satisfying $y - x \le 1$ should have $v(y) \ne \infty$ and $v(x) \ne -\infty$. Now, if we also had a constraint $x - 0 \le -\infty$, corresponding to edge $0 \stackrel{\le-\infty}{\longrightarrow} x$, we have no negative cycle in the corresponding distance graph, as can be seen by considering the part of the graph without green edges in Figure 5. But, as explained above, the set of constraints $y - x \le 1$ and $x - 0 \le -\infty$ is not satisfiable.

In order to get a correspondence between negative cycles and empty solution sets, we propose the standard form. The standard form equips the graph with the additional information that when $y - x$ is bounded by a finite value, that is, edge $x \to y$ does not have weight $(\le, +\infty)$, the constraints $0 - x$ and $y - 0$ are at most $(<, +\infty)$ - the edges induced
by standardization are depicted in green in Figure 5. With this information, we get negative cycles whenever there is a contradiction.

Now, each distance graph $\mathcal{G}$ can be transformed into an equivalent distance graph $\mathcal{G}'$ which is in standard form. By equivalent, we mean $[\mathcal{G}] = [\mathcal{G}']$. First, we set $\mathcal{G}'_{0x} = \min(\mathcal{G}_{0x}, (\le, 0))$ for $x \in X_P$ and $\mathcal{G}'_{x0} = \min(\mathcal{G}_{x0}, (\le, 0))$ for $x \in X_H$. Moreover, if $x \in X_P$ then we set $\mathcal{G}'_{x0} = \min(\mathcal{G}_{x0}, (<, +\infty))$ if $\mathcal{G}_{xy} \neq (\le, +\infty)$ for some $y \neq x$, otherwise we keep $\mathcal{G}'_{x0} = \mathcal{G}_{x0}$. Similarly, if $y \in X_H$ then we set $\mathcal{G}'_{0y} = \min(\mathcal{G}_{0y}, (<, +\infty))$ if $\mathcal{G}_{xy} \neq (\le, +\infty)$ for some $x \neq y$, otherwise we keep $\mathcal{G}'_{0y} = \mathcal{G}_{0y}$. Finally, for $x, y \in X$ with $x \neq y$ we set $\mathcal{G}'_{xy} = \mathcal{G}_{xy}$. The graph $\mathcal{G}'$ constructed above is called the standardization of $\mathcal{G}$.

**Lemma 4.6.** The standardization $\mathcal{G}'$ of a distance graph $\mathcal{G}$ is in standard form and $[\mathcal{G}'] = [\mathcal{G}]$.

*Proof.* The graph $\mathcal{G}'$ is in standard form by construction. Clearly, $\mathcal{G}' \le \mathcal{G}$, hence $[\mathcal{G}'] \subseteq [\mathcal{G}]$. Now, let $v \in [\mathcal{G}]$. We show that $v$ satisfies all constraints in $\mathcal{G}'$. Let $x \in X_P$ be a prophecy clock. We have $v(x) \le 0$. Hence $v$ satisfies the constraint $\mathcal{G}'_{0x} = \min(\mathcal{G}_{0x}, (\le, 0))$. Assume now that $\mathcal{G}_{xy} = (\triangleleft, c) < (\le, +\infty)$ for some $y \ne x$. Since $v \in [\mathcal{G}]$, we have $v(y) - v(x) \triangleleft c$, which implies $v(x) \ne -\infty$. Hence $v$ satisfies the constraint $\mathcal{G}'_{x0} = \min(\mathcal{G}_{x0}, (<, +\infty))$. We proceed similarly for the new constraints when $x \in X_H$ is a history clock. $\square$

**Definition 4.7.** The weight of a path in a distance graph $\mathcal{G}$ is the sum of the weights of its edges. A cycle in $\mathcal{G}$ is said to be negative if its weight is strictly less than $(\le, 0)$.

A distance graph $\mathcal{G}$ is in *normal form* if it is in standard form, has no negative cycles, and the weight of each edge $x \to y$ is not greater than the weight of any path from $x$ to $y$.

A standard distance graph with no negative cycles can be normalized. Let $\mathcal{G}$ be a standard distance graph with no negative cycles. Let $\mathcal{G}'$ be the graph where the weight of an edge $x \to y$ is set to the minimum of the weights of the paths from $x$ to $y$ in $\mathcal{G}$.<fnref n="6" /> The graph $\mathcal{G}'$ constructed above is called the *normalization* of $\mathcal{G}$.

**Lemma 4.8 (Normalization).** Let $\mathcal{G}$ be a standard distance graph with no negative cycles. The normalization $\mathcal{G}'$ of $\mathcal{G}$ is in normal form and $[\mathcal{G}] = [\mathcal{G}']$.

*Proof.* First, we check that $\mathcal{G}'$ is in standard form. Let $x \in X_P$. We have $\mathcal{G}'_{0x} \le \mathcal{G}_{0x} \le (\le, 0)$. Now assume that $\mathcal{G}'_{x0} = (\le, +\infty)$. Then $\mathcal{G}'_{x0} \le \mathcal{G}_{x0} = (\le, +\infty)$ and $\mathcal{G}_{xy} = (\le, +\infty)$ for all $y \ne x$. Since all paths in $\mathcal{G}$ from $x$ to some $y \ne x$ start with some edge $x \to z$ of weight $(\le, +\infty)$, we obtain $\mathcal{G}'_{xy} = (\le, +\infty)$ for all $y \ne x$. The condition for history clocks is proved similarly.

It is easy to see that $\mathcal{G}'$ is in normal form. We have $\mathcal{G}' \le \mathcal{G}$ by construction, hence $[\mathcal{G}'] \subseteq [\mathcal{G}]$. Conversely, let $v \in [\mathcal{G}]$ and let $x_1 \to x_2 \to \dots \to x_n$ be an arbitrary path in $\mathcal{G}$ with weight $(\triangleleft, c)$. As $v \in [\mathcal{G}]$, we have $v \models x_{i+1} - x_i \triangleleft c_i$ with $\mathcal{G}_{x_ix_{i+1}} = (\triangleleft_i, c_i)$. By Lemma 4.3, we get $v \models x_n - x_1 \triangleleft c$. We deduce that $v \in [\mathcal{G}']$. $\square$

Given two distance graphs $\mathcal{G}', \mathcal{G}'',$ we define $\mathcal{G} = \min(\mathcal{G}', \mathcal{G}'')$ as the distance graph obtained by setting $\mathcal{G}_{xy} = \min(\mathcal{G}'_{xy}, \mathcal{G}''_{xy})$ for all $x \ne y$. Notice that $[\mathcal{G}] = [\mathcal{G}'] \cap [\mathcal{G}'']$. Moreover, if both $\mathcal{G}'$ and $\mathcal{G}''$ are in standard form, then so is $\min(\mathcal{G}', \mathcal{G}'')$. On the other hand, even when $\mathcal{G}'$ and $\mathcal{G}''$ are in normal form, $\min(\mathcal{G}', \mathcal{G}'')$ need not be in normal form.

<footnote n="6">⁶When $\mathcal{G}$ has no negative cycles, the weight of a non-simple path $x \cdots z \cdots z \cdots y$ is at least the weight of the subpath $x \cdots z \cdots y$. Hence, we may restrict to simple paths when taking the minimum.</footnote>
We will make use of important properties, which have been shown when weights come from $C \setminus \{(-\infty, -\infty), (\leq, -\infty), (\leq, +\infty)\}$, and continue to hold even with the new weights. First, we show that a classical and crucial property of distance graphs for timed automata extends to the *standard* distance graphs over the extended algebra that we have defined above for event-clock automata.

**Lemma 4.9.** Let $\mathcal{G}$ be a standard distance graph. Then, $[\mathcal{G}] \neq \emptyset$ iff $\mathcal{G}$ has no negative cycles.

*Proof.* Suppose $[\mathcal{G}]$ is non-empty. Let $v \in [\mathcal{G}]$. Let $x_1 \to x_2 \to \dots \to x_n \to x_{n+1} = x_1$ be an arbitrary cycle in $\mathcal{G}$ and let $(\triangleleft, c)$ be the weight of the cycle. As $v \in [\mathcal{G}]$, we have $v \models x_{i+1} - x_i \triangleleft c_i$ with $(\triangleleft, c_i)$ the weight of $x_i \to x_{i+1}$ in $\mathcal{G}$. By Lemma 4.3, we deduce that $v \models x_{n+1} - x_1 \triangleleft c$. Since $x_{n+1} = x_1$, we get $v(x_{n+1}) - v(x_1) \in \{0, +\infty\}$. Hence, the cycle is not negative.

Conversely, let $\mathcal{G}$ be a standard distance graph with no negative cycles. We will tighten the distance graph, progressively fixing the value of each clock, while preserving a standard graph with no negative cycles. By Lemma 4.8, we assume w.l.o.g. that $\mathcal{G}$ is in normal form.

Let $x \in X$ be a clock. Considering the cycle $0 \to x \to 0$, we get $(\leq, 0) \leq \mathbb{G}_{0x} + \mathbb{G}_{x0}$. By Lemma 4.4, we find $\alpha \in \mathbb{R}$ with $(\leq, \alpha) \leq \mathbb{G}_{0x}$ and $(\leq, -\alpha) \leq \mathbb{G}_{x0}$. Notice that $0 \leq \alpha$ if $x$ is a history clock and $\alpha \leq 0$ if $x$ is a prophecy clock.

Define the graph $\mathcal{G}'$ obtained from $\mathcal{G}$ by setting $\mathbb{G}'_{0x} = (\leq, \alpha)$, $\mathbb{G}'_{x0} = (\leq, -\alpha)$ and keeping the other weights unchanged. We can easily check that $\mathcal{G}'$ is in standard form. We claim that $\mathcal{G}'$ has no negative cycles. Cycles using only weights from $\mathcal{G}$ are non-negative since $\mathcal{G}$ has no negative cycles. Consider now a cycle $0 \to x \dots 0$. If $x \to \dots \to 0$ consists of a single edge, then the weight of the cycle in $\mathcal{G}'$ is $(\leq, \alpha) + (\leq, -\alpha)$ which is either $(\leq, 0)$ or $(\leq, +\infty)$ and hence non-negative. Otherwise, the path $x \dots 0$ only uses weights from $\mathcal{G}$. Let $(\triangleleft, c)$ be its weight. We have $\mathbb{G}_{x0} \leq (\triangleleft, c)$ since $\mathcal{G}$ is in normal form. Now, using $(\leq, -\alpha) \leq \mathbb{G}_{x0}$ and Lemma 4.4, we get $(\leq, 0) \leq (\leq, \alpha) + (\triangleleft, c)$ showing that the cycle is not negative. We proceed similarly for cycles of the form $0 \to \dots x \to 0$.

The graph $\mathcal{G}'$, denoted $\mathbb{G}[x = \alpha]$, is obtained from $\mathcal{G}$ by fixing the value of $x$ to $\alpha$. By construction we have $\mathbb{G}' \leq \mathcal{G}$, hence $[\mathbb{G}'] \subseteq [\mathcal{G}]$. Moreover, $v(x) = \alpha$ for all $v \in [\mathbb{G}']$.

Since $\mathcal{G}'$ is standard and has no negative cycles, we can repeat the process, fixing the value of each clock in $X$ one after the other. At the end of the process, we obtain a standard distance graph $\mathbb{G}''$ with no negative cycles and where the value of each clock $x \in X$ has been fixed to some $\alpha_x \in \mathbb{R}$. We still have $[\mathbb{G}''] \subseteq [\mathcal{G}]$.

Let $v \in V$ be defined by $v(x) = \alpha_x$ for all $x \in X$. We show that $v \in [\mathbb{G}'']$. Clearly, $v$ satisfies all the constraints $\mathbb{G}''_{0x} = (\leq, \alpha_x)$ and $\mathbb{G}''_{x0} = (\leq, -\alpha_x)$. Now, consider an edge $x \to y$ with weight $\mathbb{G}''_{xy} = (\triangleleft, c)$. If $\alpha_y = +\infty$ then $y$ is a history clock and $\mathbb{G}''_{0y} = (\leq, +\infty)$. Since $\mathbb{G}''$ is standard, we deduce that $\mathbb{G}''_{xy} = (\leq, +\infty)$. Similarly, if $\alpha_x = -\infty$ then $x$ is a prophecy clock, $\mathbb{G}''_{x0} = (\leq, +\infty)$ and $\mathbb{G}''_{xy} = (\leq, +\infty)$. In both cases we get $v \models y - x \triangleleft c$. We assume below that $\alpha_y \neq +\infty$ and $\alpha_x \neq -\infty$. The cycle $x \to y \to 0 \to x$ is non-negative and has weight $(\triangleleft, c) + (\leq, -\alpha_y) + (\leq, \alpha_x) = (\triangleleft, c) + (\leq, \alpha_x - \alpha_y)$. We deduce that $(\leq, -(\alpha_x - \alpha_y)) \leq (\triangleleft, c)$. Recall that $-(b-a) = a-b$ unless $a=b \in \{-\infty, +\infty\}$. Since $\alpha_y \neq +\infty$ and $\alpha_x \neq -\infty$ we obtain $(\leq, \alpha_y - \alpha_x) \leq (\triangleleft, c)$, which implies $v \models y - x \triangleleft c$. This concludes the proof. $\square$

We will now establish a stronger result, which will be used in several proofs, which will also show that a distance graph in normal form is *canonical*, in a sense that we explain below. The result (which generalizes the one from timed automata) intuitively says that if a distance
graph is in normal form, then for every pair of clocks $x, y \in X \cup \{0\}$, there is a valuation $v$ in its semantics which assigns time-stamps to $x$ and $y$ such that their difference (in the extended algebra) is a value arbitrarily close to the weight of the edge $x \to y$. Formally,

**Lemma 4.10.** Let $\mathcal{G}$ be a distance graph in normal form, $x, y \in X \cup \{0\}$ be a pair of distinct clocks and $\alpha \in \mathbb{R}$. There is a valuation $v \in [\mathcal{G}]$ with $v(y) - v(x) = \alpha$ if and only if

(1) $(\leq, \alpha) \leq \mathcal{G}_{xy}$ and $(\leq, -\alpha) \leq \mathcal{G}_{yx}$, and

(2) if $x, y \in X$ and $\alpha \in \mathbb{R}$ is finite then the weights $\mathcal{G}_{x0}, \mathcal{G}_{0x}, \mathcal{G}_{y0}, \mathcal{G}_{0y}$ are all different from $(\leq, -\infty)$, and

(3) if $x, y \in X$ and $\alpha = -\infty$ then $\mathcal{G}_{0x} \neq (\leq, -\infty) \neq \mathcal{G}_{y0}$.

*Proof.* We first show that the conditions are necessary. Let $v \in [\mathcal{G}]$ be a valuation with $v(y) - v(x) = \alpha$.

(1) Let $\mathcal{G}_{xy} = (\triangleleft, c)$. We know that $v \models y - x \triangleleft c$ and we deduce that $\alpha \triangleleft c$, which is equivalent to $(\leq, \alpha) \leq \mathcal{G}_{xy}$. Let $\mathcal{G}_{yx} = (\triangleleft', c')$. We know that $v \models x - y \triangleleft' c'$ and we deduce that $v(x) - v(y) \triangleleft' c'$. Recall that $-(b-a) = a-b$ unless $a=b \in \{-\infty, +\infty\}$, in which case $a-b = b-a = +\infty$. We deduce that $-\alpha \leq v(x) - v(y) \triangleleft' c'$, which implies $(\leq, -\alpha) \leq \mathcal{G}_{yx}$.

(2) Assume that $\alpha \in \mathbb{R}$ is finite, then $v(x), v(y) \in \mathbb{R}$ are both finite. Assume that $\mathcal{G}_{x0} = (\leq, -\infty)$ (resp. $\mathcal{G}_{0x} = (\leq, -\infty)$). Then $v \in [\mathcal{G}]$ implies $v(x) = +\infty$ (resp. $v(x) = -\infty$), a contradiction. Similarly, $\mathcal{G}_{y0}, \mathcal{G}_{0y}$ are not $(\leq, -\infty)$.

(3) Assume that $\alpha = -\infty$. Then, $v(y) = -\infty \neq v(x)$ or $v(x) = +\infty \neq v(y)$. Now, if $\mathcal{G}_{0x} = (\leq, -\infty)$ then $v(x) = -\infty$, a contradiction. Similarly, we must have $\mathcal{G}_{y0} \neq (\leq, -\infty)$.

Before proving the other direction, we give a short comparison with the timed automata setting. For distance graphs arising in classical timed automata, Condition 1 is already sufficient to get the right-to-left direction: if we replace the edges $x \to y$ and $y \to x$ with $(\leq, \alpha)$ and $(\leq, -\alpha)$ respectively, we can deduce that the resulting graph has no negative cycles, and hence the semantics of this graph is non-empty. Any valuation $v$ in the semantics of the resulting graph has $v(y) - v(x) = \alpha$, which gives us the converse direction of the lemma. On the other hand, in the current setting with infinity weights, doing this same replacement might not result in a graph in standard form. As we have seen earlier, for graphs not in standard form, the absence of negative cycles does not imply a non-empty solution set. This is why we need the second and third conditions which indirectly allow to reason on a standard form for the resulting graph, depending on the $\alpha$ that is chosen. Let us now prove this direction.

Assume that the three conditions are satisfied. We consider different cases.

Assume first that $x = 0$. We fix the value of $y$ to $\alpha$ by considering the graph $\mathcal{G}' = \mathcal{G}[y = \alpha]$ defined in the proof of Lemma 4.9. We have seen that $\mathcal{G}'$ is standard with no negative cycles. By Lemma 4.9 we find $v \in [\mathcal{G}'] \subseteq [\mathcal{G}]$ and we have $v(y) = \alpha$. The case $y = 0$ is handled similarly by considering $\mathcal{G}' = \mathcal{G}[x = -\alpha]$ which fixes the value of $x$ to $-\alpha$. For the rest of the proof, we assume that $x, y \in X$ and we distinguish three cases depending on $\alpha$.

• The first case is when $\alpha = +\infty$. Since $\mathcal{G}$ is in normal form, we have $(\leq, +\infty) \leq \mathcal{G}_{xy} \leq \mathcal{G}_{x0} + \mathcal{G}_{0y}$. Hence, $\mathcal{G}_{x0} = (\leq, +\infty)$ or $\mathcal{G}_{0y} = (\leq, +\infty)$. Assume that $\mathcal{G}_{x0} = (\leq, +\infty)$. We have $(\leq, -\infty) \leq \mathcal{G}_{0x}$. Hence we may fix the value of $x$ to $-\infty$ by taking $\mathcal{G}' = \mathcal{G}[x = -\infty]$. Applying Lemma 4.9 we find a valuation $v \in [\mathcal{G}'] \subseteq [\mathcal{G}]$. We have $v(x) = -\infty$. We deduce that $v(y) - v(x) = +\infty = \alpha$. We proceed similarly when $\mathcal{G}_{0y} = (\leq, +\infty)$, fixing the value of $y$ to $+\infty$.
• The next case is when $\alpha \in \mathbb{R}$ is finite. To fix the value of $y-x$ to $\alpha$ we define the graph $G'$ by setting $G'_{xy} = (\le, \alpha)$, $G'_{yx} = (\le, -\alpha)$, $G'_{x0} = \min(G_{x0}, (<, +\infty))$, $G'_{0x} = \min(G_{0x}, (<, +\infty))$, $G'_{y0} = \min(G_{y0}, (<, +\infty))$, $G'_{0y} = \min(G_{0y}, (<, +\infty))$, and the weight of other edges $z \to z'$ are kept unchanged: $G'_{zz'} = G_{zz'}$. This graph $G'$ is denoted $\mathbb{G}[y-x=\alpha]$. It is easy to see that $G'$ is in standard form. Since $G' \le \mathbb{G}$ we have $[G'] \subseteq [\mathbb{G}]$. Moreover, $v(y) - v(x) = \alpha$ for all $v \in [G']$. It remains to show that $[G'] \ne \emptyset$, i.e., that $G'$ has no negative cycles. Since $\mathbb{G}$ is in normal form, we may restrict to cycles not using two consecutive weights from $\mathbb{G}$. In particular, cycles using only weights from $\mathbb{G}$ are non-negative. It remains to consider the following cycles.

• Cycle $x \to y \to x$ has weight $(\le, \alpha) + (\le, -\alpha) = (\le, 0)$ which is non-negative.

• Cycle $0 \to x \to 0$ with $G'_{0x} = (<, +\infty)$ or $G'_{x0} = (<, +\infty)$ is not negative since we have $G_{x0} \ne (\le, -\infty) \ne G_{0x}$. We argue similarly for cycle $0 \to y \to 0$.

• Cycle $0 \to x \to y \to 0$ with $G'_{0x} = (<, +\infty)$ or $G'_{y0} = (<, +\infty)$ is not negative since $G_{y0} \ne (\le, -\infty) \ne G_{0x}$. We argue similarly for cycle $0 \to y \to x \to 0$.

Therefore, $G'$ has no negative cycles and we are done with the case $\alpha \in \mathbb{R}$ finite.

• The last case is $\alpha = -\infty$. From $(\le, -\alpha) \le G_{yx}$ we get $G_{yx} = (\le, +\infty)$. Since $\mathbb{G}$ is in normal form, $G_{yx} \le G_{y0} + G_{0x}$ and we deduce that $G_{y0} = (\le, +\infty)$ or $G_{0x} = (\le, +\infty)$.

Assume that $G_{0x} = (\le, +\infty)$. We define a graph $G'$ which fixes $x$ to $+\infty$ and forces $y$ to be different from $+\infty$. We set $G'_{x0} = (\le, -\infty)$, $G'_{0y} = \min(G_{0y}, (<, +\infty))$ and $G'_{zz'} = G_{zz'}$ otherwise. The graph $G'$ is denoted $\mathbb{G}[x = +\infty, y < +\infty]$. It is easy to check that $G'$ is in standard form. Moreover, $G' \le \mathbb{G}$ and for all $v \in [G']$ we have $v(x) = +\infty$ and $v(y) < +\infty$, so we get $v(y) - v(x) = -\infty$ as desired. It remains to show that $[G'] \ne \emptyset$, i.e., that $G'$ has no negative cycles. Since $\mathbb{G}$ is in normal form, we may restrict to cycles not using two consecutive weights from $\mathbb{G}$. In particular, cycles using only weights from $\mathbb{G}$ are non-negative. It remains to consider the following cycles.

• Cycle $0 \to x \to 0$ has weight $(\le, +\infty)$ since $G_{0x} = (\le, +\infty)$.

• Cycle $0 \to y \to 0$ with $G'_{0y} = (<, +\infty)$ is not negative since $G_{y0} \ne (\le, -\infty)$.

• Cycle $0 \to y \to x \to 0$ with $G'_{0y} = (<, +\infty)$ has weight $(\le, +\infty)$ since $G_{yx} = (\le, +\infty)$.

Therefore, $G'$ has no negative cycles.

We proceed similarly when $G_{y0} = (\le, +\infty)$ by defining a graph $G' = \mathbb{G}[x \ne -\infty, y = -\infty]$ fixing $y$ to $-\infty$ and forcing $x$ to be different from $-\infty$. This concludes the proof. $\square$

To conclude, we show that a distance graph in normal form is canonical, in the sense that if two distance graphs in normal form have the same semantics, then they must be identical.

**Lemma 4.11.** Let $\mathbb{G}, G'$ be two distance graphs with $\mathbb{G}$ in normal form. If $[\mathbb{G}] \subseteq [G']$ then $\mathbb{G} \le G'$. In particular, if both $\mathbb{G}, G'$ are in normal form and if $[\mathbb{G}] = [G']$ then $\mathbb{G} = G'$.

*Proof.* Assume that $\mathbb{G} \not\le \mathbb{G}'$. Let $x, y \in X \cup \{0\}$ such that $G'_{xy} < G_{xy}$. Since the cycle $x \to y \to x$ is not negative in $\mathbb{G}$, by Lemma 4.4(2) we find $\alpha \in \mathbb{R}$ such that $(\le, \alpha) \le G_{xy}$, $(\le, -\alpha) \le G_{yx}$, and $G'_{xy} < (\le, \alpha)$.

We will apply Lemma 4.10. We have chosen $\alpha$ so that Condition 1 is satisfied. Notice that $\alpha \ne -\infty$ since $G'_{xy} < (\le, \alpha)$ (recall that weight $(<, -\infty)$ is not allowed in distance graphs). Assume that $x, y \in X$ and $\alpha$ finite. From the choice of $\alpha$ in the proof of Lemma 4.4, we see that if $G_{xy} = (\le, +\infty)$ then $\alpha = +\infty$. Hence, $G_{xy} \ne (\le, +\infty)$. Since $\mathbb{G}$ is standard, this implies $G_{x0} \ne (\le, +\infty) \ne G_{0y}$. Since $\mathbb{G}$ has no negative cycles, we deduce that
$G_{0x} \neq (\leq, -\infty) \neq G_{y0}$. Using $(\leq, -\infty) \neq G_{xy} \leq G_{x0} + G_{0y}$ and $G_{x0} \neq (\leq, +\infty) \neq G_{0y}$, we deduce that $G_{x0} \neq (\leq, -\infty) \neq G_{0y}$. Therefore, Condition 2 is also satisfied. We apply Lemma 4.10 and get a valuation $v \in G$ with $v(y) - v(x) = \alpha$. From $G'_{xy} < (\leq, \alpha)$, we deduce that $v \notin [[G']]$. Therefore, $[[G] \not\subseteq [[G']]]$. □

This lemma finally allows us to define the canonical distance graph of a non-empty event-zone $Z$, that can be computed from a distance graph defining the zone $Z$ (extending the result from usual zones in timed automata).

**Definition 4.12.** For a non-empty event-zone $Z$, we denote by $G(Z)$ the unique distance graph in normal form satisfying $[[G(Z)]] = Z$. $G(Z)$ is called the canonical distance graph of $Z$. We denote by $Z_{xy}$ the weight of the edge $x \to y$ in $G(Z)$.

**4.3. Successor computation.** To implement the computation of transitions $(q, Z) \xrightarrow{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 will show in Lemmas 4.16, 4.18, 4.17 and 4.19 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.

**Definition 4.13 (Operations on event-zones).** Let $g$ be a guard and $Z$ an event-zone.

* Guard intersection: $Z \wedge g := \{v \mid v \in Z \text{ and } v \models g\}$

* Release: $[\vec{a}]Z = \bigcup_{v \in Z} [\vec{a}]v$

* Reset: $[\overleftarrow{a}]Z = \{[\overleftarrow{a}]v \mid v \in Z\}$

* Time elapse: $\vec{Z} = \{v + \delta \mid v \in Z, \delta \in \mathbb{R}_{\geq 0} \text{ s.t. } v + \delta \models \bigwedge_{a \in \Sigma} \vec{a} \leq 0\}$

Let $M \in \mathcal{N}$. We say that an event-zone $Z$ is $M$-reachable if it can be obtained starting from the initial zone $Z_0$ and applying the above operations, where guards $g$ use $M$-bounded finite constants, i.e., the constants allowed in a guard are from $\{-\infty, -M, \dots, -1, 0, 1, \dots, M, +\infty\}$. Recall that the initial zone $Z_0$ is given by $\bigwedge_{a \in \Sigma} ((+\infty \leq \overleftarrow{a}) \wedge (\vec{a} \leq 0))$.

When $M$ is clear from context, we will sometimes abuse notation and just say reachable zone instead of $M$-reachable zone. 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) \xrightarrow{t} (q', Z')$ can be computed in the following sequence:

$$Z_1 := Z \cap (0 \leq \vec{a}) \quad Z_2 := [\vec{a}]Z_1 \quad Z_3 := Z_2 \cap g \quad Z_4 := [\overleftarrow{a}]Z_3 \quad Z' := \vec{Z}_4$$

As an example, in Figure 6, suppose an action $b$ with guard $(\vec{a} = -1) = (\vec{a} \leq -1) \wedge (-1 \leq \overleftarrow{a})$ is fired from Zone $Z$ as depicted, applying the above sequence in order gives $Z_1 := Z \cap (0 \leq \vec{b})$, $Z_2 := [\vec{b}]Z_1$, $Z_3 := Z_2 \cap (\vec{a} = -1)$, $Z_4 := [\overleftarrow{b}]Z_3$ resulting in the successor zone $Z' := \vec{Z}_4$, as depicted in the figure.

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

**Definition 4.14 (Operations on distance graphs).** Let $G$ be a distance graph in normal form. Let $g$ be a guard.

* Guard intersection: a distance graph $G_g$ is obtained from $G$ as follows,
<figure><img src="image_10.png" /><figcaption>Figure 6: Successor computation from event-zone Z on an action b with guard $\vec{a} = -1$</figcaption></figure>

- for each constraint $x \triangleleft c$ in $g$, replace weight of edge $0 \to x$ with $\min(\mathbb{G}_{0x}, (\triangleleft, c))$,

- for each constraint $d \triangleleft y$ in $g$, replace weight of edge $y \to 0$ with $\min(\mathbb{G}_{y0}, (\triangleleft, -d))$,

- normalize the resulting graph if it has no negative cycles.

* Release: a distance graph $[\vec{a}]\mathbb{G}$ is obtained from $\mathbb{G}$ by

- removing all edges involving $\vec{a}$ and then

- adding the edges $0 \xrightarrow{(\le, 0)} \vec{a}$ and $\vec{a} \xrightarrow{(\le, +\infty)} 0$, and then

- normalizing the resulting graph.

* Reset: a distance graph $[\overleftarrow{a}]\mathbb{G}$ is obtained from $\mathbb{G}$ by

- removing all edges involving $\overleftarrow{a}$ and then

- adding the edges $0 \xrightarrow{(\le, 0)} \overleftarrow{a}$ and $\overleftarrow{a} \xrightarrow{(\le, 0)} 0$, and then

- normalizing the resulting graph.

* Time elapse: the distance graph $\vec{G}$ is obtained by the following transformation:

- if $\mathbb{G}_{0\vec{a}} \neq (\le, +\infty)$ then replace it with $(<, +\infty)$,

- if $\mathbb{G}_{0\overleftarrow{a}} \neq (\le, -\infty)$ then replace it with $(\le, 0)$,

- normalize the resulting graph.

The theorem below 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 $[\vec{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 [ZLZ05].

**Theorem 4.15.** Let $\mathbb{G}$ be a distance graph in normal form, $a \in \Sigma$, and $g$ be a guard. We can compute, in $O(|X_P \cup X_H|^2)$ time, distance graphs $\mathbb{G}_g$, $[\vec{a}]\mathbb{G}$, $[\overleftarrow{a}]\mathbb{G}$ and $\vec{G}$ in normal form, such that $[\mathbb{G}] \wedge g = [\mathbb{G}_g]$, $[\vec{a}][\mathbb{G}] = [[\vec{a}]\mathbb{G}]$, $[\overleftarrow{a}][\mathbb{G}] = [[\overleftarrow{a}]\mathbb{G}]$, and $[\vec{G}] = [\vec{G}]$.

This theorem follows from Lemmas 4.16, 4.17, 4.18 and 4.19 which handle respectively the operations on distance graphs given in Definition 4.14. Other than normalization, it can be easily checked that these operations can be computed in quadratic time. We discuss the normalization procedure in the stated lemmas.

In general, the normal form of a distance graph cannot always be computed in quadratic time. However, starting from an event zone in normal form, and applying the operations of Definition 4.14 gives us special event-zones whose normal forms can be computed in quadratic time. This is explained in Lemmas 4.16, 4.17, 4.18 and 4.19.

**Lemma 4.16.** Let $\mathbb{G}$ be a distance graph in normal form and let $g$ be a guard. Then $[\mathbb{G}_g] = [\mathbb{G}] \wedge g$, and $\mathbb{G}_g$ can be computed in time $O(|X|^2)$.
**Proof.** According to the definition, we first construct an intermediate graph $\mathcal{G}'$ by replacing weights of edges of the form $0 \to x$ and $y \to 0$ depending on the guards present. It is easy to see that $[[\mathcal{G}']] = [[\mathcal{G}]] \wedge g$. The normalization process does not change the solution set.

Since $g$ has only non-diagonal guards (as $g$ is from an ECA, and our ECAs do not have diagonal guards) and $\mathcal{G}$ is in normal form, we can check if there is a negative cycle in $\mathcal{G}'$ in quadratic time (relevant cycles use one or two modified edges and are of the form $x \to 0 \to x$ or $x \to 0 \to y \to x$). If not, one first computes in quadratic time all shortest paths $x \to 0$ and $0 \to x$. The shortest path $x \to 0$ is obtained as $\mathcal{G}'_{x0} = \min(\mathcal{G}'_{x0}, \mathcal{G}_{xz} + \mathcal{G}'_{z0})$ over all $z \to 0$ that comes from guard $g$. Similarly the shortest path $0 \to x$ is $\mathcal{G}''_{0x} = \min(\mathcal{G}'_{0x}, \mathcal{G}'_{0z} + \mathcal{G}_{zx})$ over all $0 \to z$ coming from guard $g$. Finally, the shortest path $x \to y$ has weight $\min(\mathcal{G}'_{xy}, \mathcal{G}''_{x0} + \mathcal{G}''_{0y})$. $\square$

**Lemma 4.17.** Let $\mathcal{G}$ be a distance graph in normal form and $a \in \Sigma$. Then, $[[\vec{a}]\mathcal{G}] = [\vec{a}][\mathcal{G}]$, and $[\vec{a}]\mathcal{G}$ can be computed in time $O(|X|^2)$.

Moreover, the weights of edges in $[\vec{a}]\mathcal{G}$ are given by

* $x \to y$ has weight $\mathcal{G}_{xy}$, if $x, y \neq \vec{a}$,

* $\vec{a} \to x$ has weight $(\leq, +\infty)$ and $x \to \vec{a}$ has weight $\mathcal{G}_{x0}$ if $x \neq \vec{a}$.

**Proof.** The release of a prophecy clock $\vec{a}$ corresponds to removing all edges involving the node $\vec{a}$, and then adding the edges $0 \xrightarrow{(\leq,0)} \vec{a}$ and $\vec{a} \xrightarrow{(\leq,+\infty)} 0$. Let $\mathcal{G}'$ be the distance graph thus obtained from $\mathcal{G}$. It is easy to see $[\vec{a}][\mathcal{G}] \subseteq [[\mathcal{G}']]$. For the converse inclusion, we pick $v \in [[\mathcal{G}']]$ and show that there exists some $u \in [[\mathcal{G}]]$ such that $u$ coincides with $v$ in all variables except $\vec{a}$. To see this, we construct a distance graph $\mathcal{G}''$ by setting $\mathcal{G}''_{0x} = (\leq, v(x))$ and $\mathcal{G}''_{x0} = (\leq, -v(x))$ for all $x \in X \setminus \{\vec{a}\}$; and $\mathcal{G}''_{xy} = \mathcal{G}_{xy}$ for all other edges $x \to y$. We show below that (a) $\mathcal{G}'' \leq \mathcal{G}$, (b) $\mathcal{G}''$ is in standard form, and (c) $\mathcal{G}''$ has no negative cycles. We deduce that $\emptyset \neq [[\mathcal{G}』] \subseteq [[\mathcal{G}]]$ and $v \in [\vec{a}]u$ for all $u \in [[\mathcal{G}』]]$.

(a) Let $x \in X \setminus \{\vec{a}\}$. Since $v \in [[\mathcal{G}']]$, we have $\mathcal{G}''_{0x} = (\leq, v(x)) \leq \mathcal{G}'_{0x} = \mathcal{G}_{0x}$ and similarly $\mathcal{G}''_{x0} = (\leq, -v(x)) \leq \mathcal{G}'_{x0} = \mathcal{G}_{x0}$.

(b) Let $x \in X_H$. We have $\mathcal{G}''_{x0} = (\leq, -v(x)) \leq (\leq, 0)$. Assume that $\mathcal{G}''_{0x} = (\leq, +\infty)$. From (a) we get $\mathcal{G}_{0x} = (\leq, +\infty)$. Since $\mathcal{G}$ is standard, this implies $\mathcal{G}''_{yx} = \mathcal{G}_{yx} = (\leq, +\infty)$ for all $y \neq x$. We proceed similarly when $x \in X_P \setminus \{\vec{a}\}$.

(c) Since $\mathcal{G}$ is in normal form, cycles of $\mathcal{G}$ that are possibly negative are of the form $0 \to x \to 0$ or $0 \to x \to y \to 0$ with $x, y \neq \vec{a}$. The weight of $0 \to x \to 0$ in $\mathcal{G}''$ is $(\leq, 0)$ or $(\leq, +\infty)$, hence not negative. For the other cycle, notice first that since $v \in [[\mathcal{G}']]$ we have $(\leq, v(y) - v(x)) \leq \mathcal{G}'_{xy} = \mathcal{G}_{xy}$, which is equivalent to $(\leq, 0) \leq \mathcal{G}_{xy} + (\leq, -(v(y) - v(x)))$. Recall that $-(b-a) \leq a-b$. Therefore, $(\leq, 0) \leq \mathcal{G}_{xy} + (\leq, v(x) - v(y))$, which is the weight of the cycle $0 \to x \to y \to 0$.

Then, $[\vec{a}]\mathcal{G}$ is obtained by normalization of $\mathcal{G}'$. Observe that the weight of no edge was decreased: $\mathcal{G}_{0\vec{a}} \leq (\leq, 0)$ and $\mathcal{G}_{\vec{a}0} \leq (\leq, +\infty)$. Therefore, this transformation does not lead to shorter paths: the edge $x \to y$ in $[\vec{a}]\mathcal{G}$ has weight $\mathcal{G}'_{xy} = \mathcal{G}_{xy}$ if $x \neq \vec{a} \neq y$. Now, non-trivial paths in $\mathcal{G}'$ starting from $\vec{a}$ start with weight $(\leq, +\infty)$, hence the weight of edge $\vec{a} \to x$ in $[\vec{a}]\mathcal{G}$ is $(\leq, +\infty)$. Finally, the shortest path in $\mathcal{G}'$ from $x$ to $\vec{a}$ is $x \to 0 \to \vec{a}$, which is of weight $\mathcal{G}_{x0} + (\leq, 0) = \mathcal{G}_{x0}$. Hence, the weight of $x \to \vec{a}$ in $[\vec{a}]\mathcal{G}$ is $\mathcal{G}_{x0}$. $\square$

**Lemma 4.18.** Let $\mathcal{G}$ be a distance graph in normal form and $a \in \Sigma$. Then, $[[\vec{a}]\mathcal{G}] = [\vec{a}][\mathcal{G}]$, and $[\vec{a}]\mathcal{G}$ can be computed in time $O(|X|^2)$.

Moreover, the weights of edges in $[\vec{a}]\mathcal{G}$ are given by
• $x \to y$ has weight $G_{xy}$, if $x, y \neq \overleftarrow{a}$,

• $x \to \overleftarrow{a}$ has weight $G_{x0}$ and $\overleftarrow{a} \to x$ has weight $G_{0x}$ if $x \neq \overleftarrow{a}$ (including $x = 0$ assuming $G_{00} = (\le, 0)$).

*Proof.* The reset of a history clock $\overleftarrow{a}$ corresponds to removing all edges involving node $\overleftarrow{a}$, and then setting its value to 0 by adding the edges $0 \xrightarrow{(\le, 0)} \overleftarrow{a}$ and $\overleftarrow{a} \xrightarrow{(\le, 0)} 0$. Let $\mathcal{G}'$ be the distance graph thus obtained from $\mathcal{G}$. Similar to timed automata it can be shown that $[\mathcal{G}'] = [\overleftarrow{a}][\mathcal{G}]$.

Then, $[\overleftarrow{a}]\mathcal{G}$ is obtained by normalization of $\mathcal{G}'$. Normalization does not affect the weight of the edges $x \to y$ if $x, y \neq \overleftarrow{a}$ (as any path from $x$ to $y$ in $\mathcal{G}'$ using the new edges would involve a cycle $\overleftarrow{a} \to 0 \to \overleftarrow{a}$ or $0 \to \overleftarrow{a} \to 0$ of weight $(\le, 0)$). Thus, the weight of edge $x \to y$ in $[\overleftarrow{a}]\mathcal{G}$ is equal to $G_{xy}$ if $x, y \neq \overleftarrow{a}$. Now, paths in $\mathcal{G}'$ from $x \neq \overleftarrow{a}$ to $\overleftarrow{a}$ ends with the edge $0 \to \overleftarrow{a}$ of weight $(\le, 0)$. Since $\mathcal{G}$ is in normal form, we deduce that the weight of edge $x \to \overleftarrow{a}$ in $[\overleftarrow{a}]\mathcal{G}$ is $G'_{x0} = G_{x0}$. Similarly, the weight of edge $\overleftarrow{a} \to x$ in $[\overleftarrow{a}]\mathcal{G}$ is $G'_{0x} = G_{0x}$. $\square$

**Lemma 4.19.** Let $\mathcal{G}$ be a distance graph in normal form. Then, $[\overrightarrow{\mathcal{G}}] = [\overleftarrow{\mathcal{G}}]$, and $\overrightarrow{\mathcal{G}}$ can be computed in time $O(|X|^2)$.

*Proof.* The time elapse operation corresponds to (1) replacing the weight of $0 \to \overleftarrow{a}$ with $(<, +\infty)$ if it is not $(\le, +\infty)$, and (2) replacing the weight of $0 \to \overrightarrow{a}$ with $(\le, 0)$ if it is not $(\le, -\infty)$. Let $\mathcal{G}'$ be the distance graph thus obtained from $\mathcal{G}$. Similar to timed automata it can be shown that $[\mathcal{G}'] = [\overrightarrow{\mathcal{G}}]$.

Then, $\overrightarrow{\mathcal{G}}$ is obtained by normalization of $\mathcal{G}'$. The transformation from $\mathcal{G}$ to $\mathcal{G}'$ does not decrease the weights of edges, it may only increase the weights of edges from $0$ to $x \in X$. Therefore, no shorter paths may be obtained by this transformation. We deduce that, for all edges $0 \neq x \to y$ we have $\overrightarrow{G}_{xy} = G'_{xy} = G_{xy}$, and $G_{0y} \leq \overrightarrow{G}_{0y} \leq G'_{0y}$ for all $y \in X$.

Since $\mathcal{G}$ is in normal form, the shortest path in $\mathcal{G}'$ from $0$ to $y \in X$ is either the edge $0 \to y$ with weight $G'_{0y}$ or of the form $0 \to x \to y$ which is of weight $G'_{0x} + G_{xy}$. We show below that, if $G'_{0x} + G_{xy} < G'_{0y}$ then $x \in X_P$ is a prophecy clock and $G'_{0x} = (\le, 0)$. We deduce that $\overrightarrow{G}_{0y} = \min(\{G'_{xy}\} \cup \{G_{xy} | x \in X_P\}) = \min(\{G'_{xy} | x \in X_P \cup \{0\}\})$.

Assume that $G'_{0x} + G_{xy} < G'_{0y}$. Then, $G'_{0x} \neq (\le, +\infty) \neq G_{xy}$ and $G'_{0y} \neq (\le, -\infty)$. Hence, $G_{0x} \neq (\le, +\infty)$ and $G_{0y} \neq (\le, -\infty)$. Since $\mathcal{G}$ is in normal form, we have $G_{0y} \leq G_{0x} + G_{xy}$ and we deduce that $G_{0x} \neq (\le, -\infty) \neq G_{xy}$. If $x \in X_P$, we get $G'_{0x} = (<, +\infty) = G'_{0x} + G_{xy} < G'_{0y}$. This implies $G_{0y} = G'_{0y} = (\le, +\infty)$, a contradiction with $G_{xy} \neq (\le, +\infty)$ since $\mathcal{G}$ is in standard form. Hence, $x \in X_H$ is a history clock and $G_{0x} \neq (\le, -\infty)$ implies $G'_{0x} = (\le, 0)$.

Finally, from $\overrightarrow{G}_{0y} = \min(\{G'_{0y}\} \cup \{G_{xy} | x \in X_P\})$ and the definition of $G'_{0y}$, we get

$$ \overrightarrow{G}_{0y} = \begin{cases} (\le, +\infty) & \text{if } G_{0y} = (\le, +\infty) \\ (\le, -\infty) & \text{if } G_{0y} = (\le, -\infty) \\ \min((<, +\infty), (\triangleleft, c)) & \text{if } y \text{ is a history clock and } G_{0y} \neq (\le, +\infty) \\ \min((\le, 0), (\triangleleft, c)) & \text{if } y \text{ is a prophecy clock and } G_{0y} \neq (\le, -\infty) \end{cases} $$

where $(\triangleleft, c) = \min\{G_{xy} | x \in X_P\}$.

<figure><img src="image_11.png" /></figure>

We conclude this section by showing some properties of reachable zones that will be useful in the sequel.
**Lemma 4.20.** Let Z be a non-empty reachable zone and let $\mathcal{G}$ be its canonical distance graph.

(1) For all $x \in X_H$, we have $\mathcal{G}_{x0} = (\leq, -\infty)$ or $\mathcal{G}_{0x} \leq (<, +\infty)$.

(2) For all $x, y \in X$, if $\mathcal{G}_{xy} = (\leq, -\infty)$ then $\mathcal{G}_{x0} = (\leq, -\infty)$ or $\mathcal{G}_{0y} = (\leq, -\infty)$.

*Proof.* Let $\overleftarrow{a} \in X_H$ be a history clock. The weight of $\overleftarrow{a} \to 0$ in the initial distance graph $Z_0$ is $(\leq, -\infty)$, which is the least possible weight. It stays unchanged until we first apply the reset operation on $\overleftarrow{a}$, resulting in the weighted edges $0 \xrightarrow{(\leq,0)} \overleftarrow{a}$ and $\overleftarrow{a} \xrightarrow{(\leq,0)} 0$. Then, the weight of edge $0 \to \overleftarrow{a}$ may only be increased by the time elapse operation, which sets it to $(<, +\infty)$. This proves the first property.

For the second property, let $x, y \in X$ with $\mathcal{G}_{xy} = (\leq, -\infty)$ and $\mathcal{G}_{x0} \neq (\leq, -\infty)$. We have to show that $\mathcal{G}_{0y} = (\leq, -\infty)$. If $x \in X_H$ then we get $\mathcal{G}_{0x} \leq (<, +\infty)$ by the first property. If $x \in X_P$ then we have $\mathcal{G}_{0x} \leq (\leq, 0)$. In both cases, since $\mathcal{G}$ is normal, we obtain $\mathcal{G}_{0y} \leq \mathcal{G}_{0x} + \mathcal{G}_{xy} = (\leq, -\infty)$ and we are done. $\square$

We have so far seen the computation of the event-zone graph. As discussed in Section 3, we require a simulation to truncate the event-zone graph to a finite prefix that is sound and complete for reachability. We discuss a new simulation relation for ECAs in the next section.

## 5. A CONCRETE SIMULATION RELATION FOR ECAS

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) = \{ \overrightarrow{b} \leq 0, 0 \leq \overrightarrow{b} \mid b \in \Sigma \} \cup \bigcup_{(q,a,g,q') \in T} \mathbf{split}(g) \cup \mathbf{pre}(a, \mathcal{G}(q')) $$

where $\mathbf{split}(g)$ is the set of atomic constraints on history clocks occurring in $g$ and, for a set of atomic constraints $G$, $\mathbf{pre}(a, G)$ is defined as the set of constraints on history clocks in $G$ except those on $\overleftarrow{a}$. Notice that constraints in $\mathcal{G}(q)$ use the constant 0 and constants used in constraints of $\mathcal{A}$. As a consequence, it is easy to see that the least fixpoint computation terminates and results in a finite set. Intuitively, $\mathcal{G}(q)$ contains an atomic constraint $\varphi$ of the form $\overleftarrow{a} \triangleleft c$ or $c \triangleleft \overleftarrow{a}$ if $\varphi$ appears in a transition out of some state $q'$, and there is a path $q \to \dots \to q'$ from $q$ to $q'$ over transitions that do not read $a$. This makes the value of $\overleftarrow{a}$ at $q$ important for the verification of the constraint $\varphi$ at $q'$. Transitions on letter $a$ reset the history clock $\overleftarrow{a}$ to 0, and so, the actual value of $\overleftarrow{a}$ at $q$ is irrelevant for constraints on $\overleftarrow{a}$ that are witnessed after a “reset”. This is why such constraints are ignored in $\mathcal{G}(q)$. Figure 7 illustrates the computation of the $\mathcal{G}$-sets associated with each state of a given event-clock automaton.

Let $G$ be a set of atomic constraints. The preorder $\preceq_G$ is defined on valuations by

$$ v \preceq_G v' \quad \text{if } \forall \varphi \in G, \forall \delta \geq 0, \quad v + \delta \models \varphi \implies v' + \delta \models \varphi. $$

Notice that in the condition above, we do not restrict $\delta$ to those such that $v + \delta$ is a valuation: we may have $v(\overleftarrow{a}) + \delta > 0$ for some $a \in \Sigma^7$. In usual timed automata, this question does not arise, as elapsing any $\delta$ from any given valuation always results in a

<footnote n="7">⁷We highlight the distinction between time elapse operation in general, and the time elapse operation allowed by the semantics of ECA. In a general time elapse, there is no restriction on the amount of time</footnote>
<figure><img src="image_12.png" /><figcaption>Figure 7: An event-clock automaton $\mathcal{A}$ and illustration of the computation of the $\mathcal{G}$-map. Note that the set $P$ is used to denote the set of constraints involving prophecy clocks, i.e., $P = \{\vec{a} \le 0, 0 \le \overleftarrow{a}, \vec{b} \le 0, 0 \le \overleftarrow{b}\}$ - this set is part of the $\mathcal{G}$-set of each state. Further, observe that the constraints involving $\overleftarrow{a}$ do not get propagated to state $q_0$ as the transition $q_0 \to q_1$ is on the action $a$, and therefore resets $\overleftarrow{a}$.</figcaption></figure>

valuation. But this is crucial for the proof of Theorem 5.4 below. We illustrate this using Example 5.1. It also allows us to get a clean characterization of the simulation (Lemma 5.5) which in turn is useful for deriving the simulation test and in showing finiteness.

**Example 5.1.** Consider two valuations $v$ and $v'$ defined as follows: $v(\vec{a}) = -4$, $v(\overleftarrow{b}) = -1$ and $v'(\vec{a}) = -3$ and $v'(\overleftarrow{b}) = -1$. Let $G = \{\vec{a} \le 0, 0 \le \overleftarrow{a}, \vec{b} \le 0, 0 \le \overleftarrow{b}\}$. Firstly, notice that $v \not\subseteq_G v'$: if we take $\delta = 3.5$, we have $v + \delta \models \vec{a} \le 0$, whereas $v' + \delta \not\models \vec{a} \le 0$. Notice that in $v + \delta$ and $v' + \delta$, the value of $\overleftarrow{b}$ is +2.5, which is not a legal valuation reachable in an ECA. This means that if $v, v'$ were valuations at a certain state of an ECA, they cannot elapse $\delta$ units staying at that state.

Now, suppose in the definition of $\leq_G$, we restrict to $\delta$ such that $v + \delta$ of all prophecy clocks is at most 0. Then, $v \leq_G v'$: firstly $\delta \le 1$ due to the value of $\overleftarrow{b}$, and further, for all $\delta \le 1$, whenever $v + \delta$ satisfies a constraint in $G$, the valuation $v' + \delta$ satisfies the same constraint. However, this way of relating $v$ and $v'$ does not guarantee a simulation, especially after a transition that updates the value of $\overleftarrow{b}$ to a fresh value. In particular, we can come up with a sequence of transitions that is feasible from $v$, but not from $v'$. This is illustrated in Figure 8.

**Remark 5.2.** Let $v, v'$ be valuations and $a \in \Sigma$. If $v \leq_{\{0 \le \overleftarrow{a}, \overleftarrow{a} \le 0\}} v'$ then $v(\vec{a}) = v'(\vec{a})$.

The proof is easy. First, if $v(\vec{a}) = -\infty$ then $v + \delta \models \vec{a} \le 0$ for all $\delta \ge 0$. Since $v'$ simulates $v$ we deduce that $v' + \delta \models \vec{a} \le 0$ for all $\delta \ge 0$. This implies $v'(\vec{a}) = -\infty$. Next, if $-\infty < v(\vec{a}) \ne v'(\vec{a}) \le 0$. Then, for $\delta = -v(\vec{a}) \ge 0$ we have $v(\vec{a}) + \delta = 0 \ne v'(\vec{a}) + \delta$, a contradiction with $v \leq_{\{0 \le \overleftarrow{a}, \overleftarrow{a} \le 0\}} v'$.

Based on $\leq_G$ and the $\mathcal{G}(q)$ computation, we can define a preorder $\leq_A$ between configurations of ECA $\mathcal{A}$.

<footnote>that can be elapsed from a valuation. But for the semantics of ECA, we restrict to time elapses such that
prophecy clocks stay at most 0.</footnote>
<figure><img src="image_13.png" /><figcaption>Figure 8: An example to explain why it is not sufficient to only look at time-elapse restricted to ECA valuations in the definition of $\mathcal{G}$-simulation. The $*$ symbol for the value of $\vec{b}$ denotes that $\vec{b}$ may take any legal value in this valuation.</figcaption></figure>

**Definition 5.3.** $(q, v) \preceq_A (q', v')$ if $q = q'$ and $v \preceq_{\mathcal{G}(q)} v'$.

With this definition in place, we can now show the following theorem.

**Theorem 5.4.** *The relation $\preceq_A$ is a simulation on the transition system $S_A$ of ECA $\mathcal{A}$.*

*Proof.* Assume that $(q, v_1) \preceq_A (q, v_2)$, i.e., $v_1 \preceq_{\mathcal{G}(q)} v_2$.

**Delay transition:** Assume that $(q, v_1) \xrightarrow{\delta} (q, v_1 + \delta)$ is a transition of $S_A$. Then, $v_1 + \delta \models \bigwedge_{x \in \Sigma} \vec{x} \le 0$. Since $\mathcal{G}(q)$ contains $\vec{x} \le 0$ 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} \vec{x} \le 0$. Therefore, $(q, v_2) \xrightarrow{\delta} (q, v_2 + \delta)$ is a transition in $S_A$. It is easy to see that $v_1 + \delta \preceq_{\mathcal{G}(q)} v_2 + \delta$.

**Action transition:** Let $t = (q, g, a, q')$ be a transition in $\mathcal{A}$ and assume that $(q, v_1) \xrightarrow{t} (q', v'_1)$ is a transition in $S_A$, i.e., $v_1 \models 0 \le \vec{a}$ and for some $v''_1 \in [\vec{a}]v_1$ we have $v''_1 \models g$ and $v'_1 = [\vec{a}]v''_1$. Since $\mathcal{G}(q)$ contains $0 \le \vec{a}$ and $v_1 \preceq_{\mathcal{G}(q)} v_2$, we deduce that $v_2 \models 0 \le \vec{a}$.

We have $v''_1 = v_1[\vec{a} \mapsto \alpha]$ for some $\alpha \in [-\infty, 0]$ and $v'_1 = v''_1[\vec{a} \mapsto 0] = v_1[\vec{a} \mapsto 0, \vec{a} \mapsto \alpha]$. Define $v''_2 = v_2[\vec{a} \mapsto \alpha] \in [\vec{a}]v_2$ and $v'_2 = v''_2[\vec{a} \mapsto 0] = v_2[\vec{a} \mapsto 0, \vec{a} \mapsto \alpha]$. Notice that, $v'_1(x) = v''_1(x) = v''_2(x) = v'_2(x)$ for all prophecy clocks $x \in X_P$ (follows from $v_1 \preceq_{\mathcal{G}(q)} v_2$ and $\{x \le 0, 0 \le x\} \subseteq \mathcal{G}(q)$). 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 split($g$), and $v''_1 \preceq_{\mathcal{G}(q)} v''_2$, we deduce that $v''_2 \models g$.

Therefore, $(q, v_2) \xrightarrow{t} (q', v'_2)$ is a transition in $S_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 all $\delta \ge 0$ and not only those such that $v + \delta$ is a valuation. To see why, notice that the $\alpha$ that is picked to make $v'_1(\vec{a}) = \alpha$ could be any value in $[-\infty, 0]$, in particular, it could be smaller than all values in $v_1$. This potentially allows $\delta$ such that $v'_1 + \delta$ is a valuation whereas $v_1 + \delta$ is not. $\square$

When $G = \{\varphi\}$ is a singleton, we simply write $\preceq_{\varphi}$ for $\preceq_{\{\varphi\}}$. The definition of the $\preceq_A$ 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(\vec{a}) = 3$ and $\vec{a} \le 5$ is a constraint in $G$, point 2 below
says that all $v'$ with $v'(\bar{a}) \le 3$ simulate $v$. The next lemma is a generalization of [GMS20, Lemma 8] to our setting containing prophecy clocks and the undefined values $+\infty$ and $-\infty$.

**Lemma 5.5.** Let $v, v'$ be valuations and $G$ a set of atomic constraints. We have

(1) $v \preceq_G v'$ iff $v \preceq_{\varphi} v'$ for all $\varphi \in G$.

(2) $v \preceq_{x \triangleleft c} v'$ iff $v(x) \not\le c$ or $v'(x) \le v(x)$ or $(\triangleleft, c) = (\le, +\infty)$ or $(\triangleleft, c) = (<, +\infty) \wedge v'(x) < +\infty$.

(3) $v \preceq_{c \triangleleft x} v'$ iff $c \triangleleft v'(x)$ or $v(x) \le v'(x)$ or $(\triangleleft, c) = (<, +\infty)$ or $(\triangleleft, c) = (\le, +\infty) \wedge v(x) < +\infty$.

*Proof.*

(1) is clear.

(2) The right to left implication is easy. Notice for instance that if $(\triangleleft, c) = (<, +\infty)$ and $v'(x) < +\infty$ then for all $\delta \ge 0$ we have $v' + \delta = v < +\infty$. Conversely, assume that $v \preceq_{x \triangleleft c} v'$ and $v(x) \triangleleft c$ and $(\triangleleft, c) \ne (\le, +\infty)$. If $(\triangleleft, c) = (<, +\infty)$ then, using $\delta = 0$ and $v(x) \triangleleft c$, we get $v'(x) < +\infty$. If $(\triangleleft, c) = (\le, -\infty)$ then, using $\delta = 0$ and $v(x) = -\infty = v'(x)$. Otherwise, $c \in \mathbb{Z}$ and we have to show that $v'(x) \le v(x)$. Assume that $v(x) < v'(x)$. Then, we find $\delta \ge 0$ such that $v(x) + \delta \triangleleft c < v'(x) + \delta$, a contradiction.

(3) Again, the implication from right to left is easy. Notice that in the last two cases, $(\triangleleft, c) = (<, +\infty)$ or $(\triangleleft, c) = (\le, +\infty) \wedge v(x) < +\infty$, then for all $\delta \ge 0$ we have $v + \delta \not= c \triangleleft x$. Conversely, assume that $v \preceq_{c \triangleleft x} v'$ and $c \not\preceq v'(x)$ and $(\triangleleft, c) \ne (<, +\infty)$. If $(\triangleleft, c) = (\le, +\infty)$ then, using $\delta = 0$ and $c \not\preceq v'(x)$, we get $c \not\preceq v(x)$, i.e., $v(x) < +\infty$. If $(\triangleleft, c) = (<, -\infty)$ then, using $\delta = 0$ and $c \not\preceq v'(x)$, we get $c \not\preceq v(x)$, i.e., $v(x) = -\infty = v'(x)$. Otherwise, $c \in \mathbb{Z}$ and we have to show that $v(x) \le v'(x)$. Assume that $v'(x) < v(x)$. Then, we find $\delta \ge 0$ such that $c \triangleleft v(x) + \delta$ but $c \not\preceq v'(x) + \delta$, a contradiction. $\square$

We now state some useful properties that get derived from Lemma 5.5.

**Remark 5.6.** Let $v, v'$ be valuations and $G$ a set of atomic constraints.

(1) Let $x \triangleleft_1 c_1$ and $x \triangleleft_2 c_2$ be constraints with $(\triangleleft_1, c_1) \le (\triangleleft_2, c_2) < (<, +\infty)$ (we say that $x \triangleleft_1 c_1$ is subsumed by $x \triangleleft_2 c_2$). If $v \preceq_{x \triangleleft_2 c_2} v'$ then $v \preceq_{x \triangleleft_1 c_1} v'$. Indeed, from $(\triangleleft_2, c_2) < (<, +\infty)$ and $v \preceq_{x \triangleleft_2 c_2} v'$ we get either (1) $v'(x) \le v(x)$ or (2) $v(x) \not\le_2 c_2$ which implies $v(x) \not\le_1 c_1$ since $(\triangleleft_1, c_1) \le (\triangleleft_2, c_2)$.

(2) Let $c_1 \triangleleft_1 x$ and $c_2 \triangleleft_2 x$ be constraints with $(c_1, \triangleleft_1) \le (c_2, \triangleleft_2) < (+\infty, \le)$ (we say that $c_1 \triangleleft_1 x$ is subsumed by $c_2 \triangleleft_2 x$). If $v \preceq_{c_2 \triangleleft_2 x} v'$ then $v \preceq_{c_1 \triangleleft_1 x} v'$. Indeed, from $(c_2, \triangleleft_2) < (+\infty, \le)$ and $v \preceq_{c_2 \triangleleft_2 x} v'$ we get either (1) $v(x) \le v'(x)$ or (2) $c_2 \triangleleft_2 v'(x)$ which implies $c_1 \triangleleft_1 v'(x)$ since $(c_1, \triangleleft_1) \le (c_2, \triangleleft_2)$.

The ordering between lower weights is defined by $(c_1, \triangleleft_1) < (c_2, \triangleleft_2)$ if $c_1 < c_2$ or $c_1 = c_2, \triangleleft_1 = \le$ and $\triangleleft_2 = <$. We have $(c_1, \triangleleft_1) < (c_2, \triangleleft_2)$ iff $(\triangleleft_2, -c_2) < (\triangleleft_1, -c_1)$.

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.

## 5.1. Distance graph for valuations that simulate a given valuation.

For a valuation $v$ and a set of constraints $G$, 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 $\mathbb{G}_G(v)$, such that $[\mathbb{G}_G(v)] = \uparrow_G v$. We remark that $[\mathbb{G}_G(v)]$ is not really a zone since it may use constants that are not integers.
<figure><img src="image_14.png" /><figcaption>Figure 9: The distance graph $\uparrow_G v$ when $v$ is such that $v(\overrightarrow{a}) = 2, v(\overrightarrow{d}) = -7, v(\overrightarrow{b}) = 3, v(\overrightarrow{b}) = -5$ and $G = P \cup \{\overleftarrow{a} \le 3, \overleftarrow{a} > 1, \overrightarrow{b} \le 2, \overrightarrow{b} \ge 5\}$. Here, the set $P = \{\overrightarrow{d} \le 0, \overrightarrow{d} \ge 0, \overrightarrow{b} \le 0, \overrightarrow{b} \ge 0\}$ denotes the set of constraints involving prophecy clocks.</figcaption></figure>

We assume that $G$ contains $\{0 \le \overrightarrow{d}, \overrightarrow{d} \le 0 \mid a \in \Sigma\}$ so that $v \preceq_G v'$ implies $v(\overrightarrow{d}) = v'(\overrightarrow{d})$ for all prophecy clocks $\overrightarrow{d}$ with $a \in \Sigma$ (see Remark 5.2). We remove from $G$ constraints equivalent to true, such as $x \le +\infty, -3 < \overleftarrow{a}$ or $0 \le \overleftarrow{a}$, or equivalent to false, such as $\overleftarrow{a} < 0$ or $+\infty < x$. Also, by Remark 5.6, 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 $\overleftarrow{a} \triangleleft c$ with $(\le, 0) \le (\triangleleft, c) < (\triangleleft, +\infty)$, and at most one lower-bound constraint $c \triangleleft \overleftarrow{a}$ with $(0, \le) < (c, \triangleleft) < (+\infty, \le)$. 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 $G_G(v)$ which defines $\uparrow_G v$ is based on Lemma 5.5.

* For each prophecy clock $\overrightarrow{d}$, we have the edges $\overrightarrow{d} \xrightarrow{(\le, -v(\overrightarrow{d}))} 0$ and $0 \xrightarrow{(\le, v(\overrightarrow{d}))} \overrightarrow{d}$.

* For each history clock $\overleftarrow{a}$, we have the edge $0 \to \overleftarrow{a}$ with weight

- $(\le, v(\overleftarrow{a}))$ if $\overleftarrow{a} \triangleleft c \in G$ with $(\triangleleft, c) < (\triangleleft, +\infty)$ and $v(\overleftarrow{a}) \triangleleft c$,

- $(<, +\infty)$ if we are not in the case above and $\overleftarrow{a} < +\infty \in G$, $v(\overleftarrow{a}) < +\infty$,

- $(\le, +\infty)$ otherwise.

* For each history clock $\overleftarrow{a}$, we have the edge $\overleftarrow{a} \to 0$ with weight

- $(\le, -\infty)$ if $+\infty \le \overleftarrow{a} \in G$ and $v(\overleftarrow{a}) = +\infty$, and if we are not in this case:

- $(\triangleleft, -c)$ if $c \triangleleft \overleftarrow{a} \in G$ with $(c, \triangleleft) < (+\infty, \le)$ and $c \triangleleft v(\overleftarrow{a})$,

- $(\le, -v(\overleftarrow{a}))$ if $c \triangleleft \overleftarrow{a} \in G$ with $(c, \triangleleft) < (+\infty, \le)$ and $c \nleq v(\overleftarrow{a})$,

- $(\le, 0)$ otherwise.

An example of $\uparrow_G v$ is given in Figure 9.

With this definition, the distance graph $G_G(v)$ is in standard form, but not in normal form. Using Lemma 5.5, we easily see that it has the desired property:

**Lemma 5.7.** We have $v \preceq_G v'$ iff $v'$ satisfies all the constraints of $G_G(v)$.

5.2. **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_A (q', Z')$ if $q = q'$ and $Z \preceq_{G(q)} Z'$. In the rest of this section, we show how to
check this relation efficiently. We let $\downarrow_G Z = \{v \in 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 \subseteq \downarrow_G Z'$.

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. Let $G'$ be a distance graph in standard form with $Z' = [[G']]$. Since $G_G(v)$ is also in standard form, so is the distance graph $\min(G_G(v), G')$ which defines $\uparrow_G v \cap Z'$. So we may apply Lemma 4.9 and the witness will be a negative cycle in $\min(G_G(v), G')$. We show that if $\uparrow_G v \cap Z'$ is empty and $G'$ is in normal form, then there is a small witness, i.e., a negative cycle in $\min(G_G(v), G')$ containing at most three edges, and belonging to one of three specific forms.

**Lemma 5.8.** Let $v$ be a valuation, $Z'$ a non-empty reachable event-zone with canonical distance graph $G'$ 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:

(1) $0 \to x \to 0$ with $0 \to x$ from $G_G(v)$ and $x \to 0$ from $G'$,

(2) $0 \to y \to 0$ with $0 \to y$ from $G'$ and $y \to 0$ from $G_G(v)$, and

(3) $0 \to x \to y \to 0$, with weight of $x \to y$ from $G'$ and the others from $G_G(v)$. Moreover, this negative cycle has finite weight.

*Proof.* Since the distance graph $G'$ is in normal form, it has no negative cycle. Similarly, $G_G(v)$ has no negative cycle since $v \in \uparrow_G v \neq \emptyset$. We know that $\uparrow_G v \cap Z' = \emptyset$ iff there is a (simple) negative cycle in $\min(G_G(v), G')$. Since $G'$ is in normal form, we may restrict to negative cycles which do not use two consecutive edges from $G'$. Now all edges of $G_G(v)$ are adjacent to node 0. Hence, if a simple cycle uses an edge from $G'$ which is adjacent to 0, it consists of only two edges $0 \to x \to 0$, one from $G'$ and one from $G_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 $G'$ and the other two edges are from $G_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 $G'_{xy} = (\le, -\infty)$. Since $Z'$ (the zone corresponding to the distance graph $G'$) is a reachable zone, using Lemma 4.20 we get $G'_{x0} = (\le, -\infty)$ or $G'_{0y} = (\le, -\infty)$. This gives a smaller negative cycle $0 \to x \xrightarrow{(\le, -\infty)} 0$ or $0 \to y \xrightarrow{(\le, -\infty)} 0$ with the other edge $0 \to x$ or $y \to 0$ coming from $G_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)$ in $G_G(v)$. This can happen only when $x$ is a prophecy clock and $v(x) = -\infty$. Since $G'_{xy} \neq (\le, +\infty)$ and $G'$ is in standard form, we infer $G'_{x0} \neq (\le, +\infty)$. Hence $0 \xrightarrow{(\le, v(x))} x \xrightarrow{G'_{x0}} 0$ is also a negative cycle.

Suppose $y \to 0$ has weight $(\le, -\infty)$ in $G_G(v)$. This can happen only when $y$ is a history clock and $v(y) = +\infty$. Since $G'_{xy} \neq (\le, +\infty)$ and $G'$ is in standard form, we obtain $G'_{0y} \neq (\le, +\infty)$. Hence, $0 \xrightarrow{G'_{0y}} y \xrightarrow{(\le, -v(y))} 0$ is a negative cycle. $\square$

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.
**Theorem 5.9.** Let $Z, Z'$ be non-empty reachable zones, and $G$ a set of atomic constraints containing $\vec{d} \le 0$ and $0 \le \vec{d}$ for every prophecy clock $\vec{d}$. Then, $Z \not\subseteq_G Z'$ iff one of the following conditions holds:<fnref n="8" />

(1) $Z'_{x0} < Z_{x0}$ for some prophecy clock $x$, or for some history clock $x$ with

• $(x < +\infty) \in G$ and $Z'_{x0} = (\le, -\infty)$, or

• $(x \triangleleft_1 c) \in G$ for $c \in \mathbb{N}$ and $(\le, 0) \le Z_{x0} + (\triangleleft_1 c)$.

(2) $Z'_{0y} < Z_{0y}$ for some prophecy clock $y$, or for some history clock $y$ with

• $(+\infty \le y) \in G$ and $Z_{0y} = (\le, +\infty)$, or

• $(d \triangleleft_2 y) \in G$ for $d \in \mathbb{N}$ and $Z'_{0y} + (\triangleleft_2, -d) < (\le, 0)$.

(3) $Z'_{xy} < Z_{xy}$ and $Z'_{xy}$ is finite for two distinct (prophecy or history) clocks $x, y$ with $(x \triangleleft_1 c), (d \triangleleft_2 y) \in G$ for $c, d \in \mathbb{N}$ and $(\le, 0) \le Z_{x0} + (\triangleleft_1 c)$ and $Z'_{xy} + (\triangleleft_2, -d) < Z_{x0}$.

*Proof.* By definition, $Z \not\subseteq_G Z'$ iff there is a $v \in Z$ such that $\uparrow_G v \cap Z' = \emptyset$. Lemma 5.8 gives three kinds of negative cycles that witness $\uparrow_G v \cap Z' = \emptyset$. We show that the three conditions in the theorem respectively characterize the presence of the three kinds of negative cycles.

**Case 1.** There is a negative cycle $0 \to x \to 0$ with $0 \to x$ from $\mathbb{G}_G(v)$ and $x \to 0$ from $\mathbb{G}(Z')$ iff Item 1 above is true.

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

When weight of $0 \to x$ is $(\le, v(x))$: We have $(\le, v(x)) + Z'_{x0} < (\le, 0)$. Lemma 4.4 implies $Z'_{x0} < (\le, -v(x))$. Now, since $v \in Z$, it satisfies all constraints of $\mathbb{G}(Z)$. In particular, $(\le, -v(x)) \le Z_{x0}$. We obtain $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 \triangleleft_1 c) \in G$ for $c \in \mathbb{N}$ and $v(x) \triangleleft_1 c$. We can rewrite $v(x) \triangleleft_1 c$ as $(\le, v(x)) \le (\triangleleft_1 c)$. Hence, we get $(\le, 0) \le (\triangleleft_1 c) + (\le, -v(x)) \le (\triangleleft_1 c) + Z_{x0}$.

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 must have $Z'_{x0} = (\le, -\infty)$. From $v \in Z$ and $v(x) < +\infty$, we get $Z_{x0} \ne (\le, -\infty)$. Hence $Z'_{x0} < Z_{x0}$.

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

Suppose first that $x$ is a prophecy clock. Since $Z'_{x0} < Z_{x0}$, using Lemma 4.4 we find $\alpha$ satisfying both $Z'_{x0} < (\le, -\alpha) \le Z_{x0}$ and $(\le, \alpha) \le Z_{0x}$. By Lemma 4.10 we find $v \in Z$ with $v(x) = \alpha$. This gives the negative cycle $0 \xrightarrow{(\le, v(x))} x \xrightarrow{Z'_{x0}} 0$.

Next, suppose that $x$ is a history clock with $x \triangleleft_1 c$ in $G$ for $c \in \mathbb{N}$ and $(\le, 0) \le Z_{x0} + (\triangleleft_1 c)$. Since $Z'_{x0} < Z_{x0}$, using Lemma 4.4, we can find $\alpha$ with $Z'_{x0} < (\le, -\alpha) \le Z_{x0}$ and $(\le, \alpha) \le \min(Z_{0x}, (\triangleleft_1 c))$. As above, by Lemma 4.10 we find $v \in Z$ with $v(x) = \alpha$, resulting in the negative cycle $0 \xrightarrow{(\le, v(x))} x \xrightarrow{Z'_{x0}} 0$.

Now, suppose there is a history clock $x$ with $(x < +\infty) \in G$ and $(\le, -\infty) = Z'_{x0} < Z_{x0}$. This implies $Z_{x0} \ne (\le, -\infty)$ and by Lemma 4.20 we obtain $Z_{0x} \le (< +\infty)$. Let $v \in Z$. We have $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 $\mathbb{G}_G(v)$ and $x \to 0$ from $\mathbb{G}(Z')$.

<footnote n="8">⁸Recall that for a non-empty zone $Z$, we simply write $Z_{xy}$ for the weight of the edge $x \to y$ in the canonical distance graph of $Z$.</footnote>
**Case 2.** There is a negative cycle $0 \to y \to 0$ with $0 \to y$ from $\mathbb{G}(Z')$ and $y \to 0$ from $\mathbb{G}_G(v)$ iff Item 2 in the theorem statement is true.

(⇒). Suppose there is such a negative cycle.

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 \triangleleft_2 y) \in G$ with $d \in \mathbb{N}$ and $d \not\triangleleft_2 v(y)$. From the negative cycle, we have $Z'_{0y} + (\le, -v(y)) < (\le, 0)$, i.e., $Z'_{0y} < (\le, v(y))$. Since $v \in Z$, we have $(\le, v(y)) \le Z_{0y}$. We deduce that $Z'_{0y} < Z_{0y}$. In the case when $y$ is a history clock, we have $d \not\triangleleft_2 v(y)$. Therefore, either $v(y) < d$ or $v(y) = d$ and $\triangleleft_2 = <$. In both cases, $(\triangleleft_2, -d) \le (\le, -v(y))$. Hence $Z'_{0y} + (\triangleleft_2, -d) < (\le, 0)$.

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}$.

When weight of $y \to 0$ is $(\triangleleft_2, -d)$. This is when $y$ is a history clock, we are not in the subcase above and there is $d \triangleleft_2 y$ in $G$ with $d \in \mathbb{N}$ and $d \triangleleft_2 v(y)$. The negative cycle gives $Z'_{0y} + (\triangleleft_2, -d) < (\le, 0)$. From $d \triangleleft_2 v(y)$, we can infer that $(\le, -v(y)) \le (\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 the weight of $y \to 0$ is $(\le, 0)$. Since $(\le, 0) \le Z'_{0y}$, the cycle $0 \to y \to 0$ cannot be negative and 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}$. By Lemma 4.4, we can find $\alpha$ with both $Z'_{0y} < (\le, \alpha) \le Z_{0y}$ and $(\le, -\alpha) \le Z_{0y}$. By Lemma 4.10 we find $v \in Z$ with $v(y) = \alpha$. This gives the negative cycle $0 \xrightarrow{Z'_{0y}} y \xrightarrow{(\le, -v(y))} 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} = (\le, -\infty)$ (Lemma 4.20). 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 $\mathbb{G}_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 \triangleleft_2 y$ in $G$ for $d \in \mathbb{N}$ and $Z'_{0y} + (\triangleleft_2, -d) < (\le, 0)$. Since $Z'_{0y} < Z_{0y}$, using again Lemma 4.4, we find $\alpha$ with both $Z'_{0y} < (\le, \alpha) \le Z_{0y}$ and $(\le, -\alpha) \le Z_{y0}$. By Lemma 4.10 we find $v \in Z$ with $v(y) = \alpha$. If $v(y) \not\triangleleft_2 d$, then the weight of $y \to 0$ is at most $(\le, -v(y))$. Using $Z'_{0y} < (\le, \alpha)$ gives $0 \to y \to 0$ to be negative cycle. Suppose $d \triangleleft_2 v(y)$. Then weight of $y \to 0$ is at most $(\triangleleft_2, -d)$. But we already have $Z'_{0y} + (\triangleleft_2, -d) < (\le, 0)$ in our hypothesis, which gives the required negative cycle.

**Case 3.** There is a finite weight negative cycle $0 \to x \to y \to 0$ with $0 \to x$ and $y \to 0$ from $\mathbb{G}_G(v)$ and $x \to y$ from $\mathbb{G}(Z')$ iff the third condition of the theorem is true.

(⇒). 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 $(\le, v(x))$. We find $x \triangleleft_1 c$ in $G$ with $c \in \mathbb{N}$ and $v(x) \triangleleft_1 c$ (if $x$ is a prophecy clock then $(\triangleleft_1, c) = (\le, 0)$). As in case 1 above, from $v \in Z$ we deduce that $(\le, 0) \le Z_{x0} + (\le, v(x))$ and from $v(x) \triangleleft_1 c$ we get $(\le, v(x)) \le (\triangleleft_1, c)$. We obtain $(\le, 0) \le Z_{x0} + (\triangleleft_1, c)$.

Now, since the weight of $y \to 0$ is finite, we find $d \triangleleft_2 y$ in $G$ (if $y$ is a prophecy clock we take $(d, \triangleleft_2) = (0, \le))$. The weight of $y \to 0$ is $\max((\le, -v(y)), (\triangleleft_2, -d))$. Therefore: $Z'_{xy} + (\le, v(x) - v(y)) < (\le, 0)$ and $(\le, v(x)) + Z'_{xy} + (\triangleleft_2, -d) < (\le, 0)$. Since $v \in Z$, we have $(\le, v(y) - v(x)) \le Z_{xy}$. Using $Z'_{xy} < (\le, -(v(x) - v(y))) = (\le, v(y) - v(x))$ (recall that $v(x)$ and $v(y)$ are finite in the present case), we get $Z'_{xy} < Z_{xy}$. Again, as $v \in Z$, we have $(\le, -v(x)) \le Z_{x0}$. Together with $Z'_{xy} + (\triangleleft_2, -d) < (\le, -v(x))$, we get $Z'_{xy} + (\triangleleft_2, -d) < Z_{x0}$.
(↔). 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 $(\triangle2, -d)$ has a strict inequality, and $w_2 = (<, -e' + d)$ otherwise. Notice that $w_1 + Z'_{xy} = (<, 0)$ and $w_2 + Z'_{xy} + (\triangle2, -d) = (<, 0)$ are negative. Using $Z'_{xy} + (\triangle2, -d) < Z_{x0}$, we get $(<, 0) = w_2 + Z'_{xy} + (\triangle2, -d) < w_2 + Z_{x0}$ and we obtain $(\le, 0) \le w_2 + Z_{x0}$. Similarly, using $Z'_{xy} < Z_{xy}$ we get $(<, 0) = w_1 + Z'_{xy} < w_1 + Z_{xy}$ and $(\le, 0) \le w_1 + Z_{xy}$.

Consider a distance graph $\mathcal{G}$ formed by taking $\mathcal{G}(Z)$ and modifying two of its edges as follows: change $0 \to x$ to $\min(Z_{0x}, (\triangle1, c), w_2)$; change $y \to x$ to $\min(Z_{yx}, w_1)$. Notice first that $\mathcal{G}$ is in standard form. Next, we claim that $\mathcal{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} + (\triangle1, c)$, $(\le, 0) \le w_2 + Z_{x0}$ and the fact that $\mathcal{G}(Z)$ does not have negative cycles, we infer that $0 \to x \to 0$ is non-negative in $\mathcal{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 $\mathcal{G}$ is standard with no negative cycles, and its solution set is non-empty.

Now, pick a $v$ that satisfies constraints of $\mathcal{G}$. Valuation $v$ is in $Z$, and additionally satisfies $v(x) \triangle1 c$, $(\le, v(x)) \le w_2$ and $(\le, v(x) - v(y)) \le w_1$. Recall that $w_1 + Z'_{xy} = (<, 0)$. Using $(\le, v(x) - v(y)) \le w_1$, we obtain $(\le, v(x) - v(y)) + Z'_{xy} < (\le, 0)$. If $d \triangle2 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 \triangle2 v(y)$ and the weight of edge $y \to 0$ is $(\triangle2, -d)$. The weight of the cycle would be: $(\le, v(x)) + Z'_{xy} + (\triangle2, -d)$. But, $(\le, v(x)) \le w_2$ and $w_2 + Z'_{xy} + (\triangle2, -d) = (<, 0)$. Hence the required cycle is negative. $\square$

From Theorem 5.9, we can see that the inclusion test requires iteration over clocks $x, y$ and checking if the conditions are satisfied by the respective weights.

**Corollary 5.10.** *Checking if* $(q, Z) \preceq_A (q', Z')$ *can be done in time* $O(|X|^2) = O(|\Sigma|^2)$.

## 6. FINITENESS OF THE SIMULATION RELATION

In this section, we will show that the simulation relation $\preceq_A$ defined in Section 5 is finite, which implies that the reachability algorithm of Definition 3.9 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}\}$ 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| \le M\}$.

Recall that the simulation relation $\preceq_A$ was defined on nodes of the event-zone graph $\mathrm{EZG}(\mathcal{A})$ by $(q, Z) \preceq_A (q', Z')$ if $q = q'$ and $Z \preceq_{\mathcal{G}(q)} Z'$. This simulation relation $\preceq_A$ is finite if for any infinite sequence $(q, Z_0), (q, Z_1), (q, Z_2), \dots$ of reachable nodes in $\mathrm{EZG}(\mathcal{A})$ we find $i < j$ with $(q, Z_i) \preceq_A (q, Z_j)$, i.e., $Z_j \preceq_{\mathcal{G}(q)} Z_i$. Notice that we restrict to reachable zones in the definition above. Our goal now is to prove that the relation $\preceq_A$ is finite. The structure of the proof is as follows.

(1) We prove in Lemma 6.3 of Section 6.1 that for any *reachable* node $(q, Z)$ of $\mathrm{EZG}(\mathcal{A})$, the canonical distance graph $\mathcal{G}(Z)$ satisfies a set of conditions, that we call (†) conditions below, which depend only on the maximal constant $M$ of $\mathcal{A}$.
(2) We introduce an equivalence relation $\sim_M$ of finite index on valuations (depending on $M$ only) and show in Lemma 6.6 of Section 6.2 that, if $G$ is a set of atomic constraints using constants in $\{c \in \mathbb{Z} \mid |c| \le M\} \cup \{-\infty, +\infty\}$ and if $Z$ is a zone such that its canonical distance graph $\mathbb{G}(Z)$ satisfies (†) conditions, then $\downarrow_G Z$ is a union of $\sim_M$ equivalence classes.

**6.1. Prophecy clocks and distance graphs in reachable event-zones.** We start with a lemma which highlights an important and surprising property of prophecy clocks in reachable event-zones. Namely, we show that if an $M$-reachable event-zone contains a valuation $v$ in which a prophecy clock has a finite value that is below $-M$, then it must contain all valuations obtained from $v$ by setting that prophecy clock to any finite value smaller than $-M$. The implication of this property is illustrated in Figure 10. This property is essential for the proof of the (†) 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.

**Lemma 6.1.** Let $Z$ be an $M$-reachable event-zone. For every valuation $v \in Z$, and for every prophecy clock $\vec{x}$, if $-\infty < v(\vec{x}) < -M$, then $v[\vec{x} \mapsto \alpha] \in Z$ for every $-\infty < \alpha < -M$.

*Proof.* The initial zone is $(\bigwedge_{\vec{x}} \vec{x} = +\infty) \wedge (\bigwedge_{\vec{x}} -\infty \le \vec{x} \le 0)$. The property is true in this zone. We now show that the property is invariant under guard intersection (with maximal constant $M$), reset, release and time elapse. Assume $Z$ is a zone that satisfies the property. Let $v$ be an arbitrary valuation (not necessarily in $Z$) with $-\infty < v(\vec{x}) < -M$. For $-\infty < \alpha < -M$, we simply write $v_\alpha = v[\vec{x} \mapsto \alpha]$.

**Guard intersection:** Let $g$ be a guard, which is in general a conjunction of atomic constraints. Suppose $g$ contains an atomic constraint on $\vec{x}$, either $c \triangleleft \vec{x}$ or $\vec{x} \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 \triangleleft y$ or $y \triangleleft d$ for some $y \ne \vec{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 \wedge g$.

**Release:** The release operation on $\vec{y}$ takes a valuation $u$ and adds a valuation $u[\vec{y} \mapsto \beta]$ for each $-\infty \le \beta \le 0$. Let $v \in [\vec{y}]Z$. Then, there is some valuation $u \in Z$ such that $v = u[\vec{y} \mapsto \beta]$ for some $-\infty \le \beta \le 0$. When $\vec{y} = \vec{x}$, associating $\alpha$ to $\vec{x}$ in the release operation starting from $u$ gives $v_\alpha$. When $\vec{y} \ne \vec{x}$, we use the induction hypothesis: valuation $u_\alpha \in Z$. Setting $\vec{y}$ to $\beta$ in the release operation starting from $u_\alpha$ gives $v_\alpha$.

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

**Time elapse:** Suppose $v + \delta \in \overrightarrow{Z}$ for some $v \in Z$ and $\delta \ge 0$. This means $(v + \delta)(\vec{y}) \le 0$ for every prophecy clock $\vec{y}$. We have to show that if $-\infty < (v + \delta)(\vec{x}) < -M$, then $(v + \delta)_\alpha \in \overrightarrow{Z}$ for all $-\infty < \alpha < -M$. Since $-\infty < (v + \delta)(\vec{x}) < -M$, we also have $-\infty < v(\vec{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 \overrightarrow{Z}$: for each clock $\vec{y} \ne \vec{x}$, $(v_\beta + \delta)(\vec{y}) = (v + \delta)(\vec{y}) \le 0$ and $(v_\beta + \delta)(\vec{x}) = \alpha < -M \le 0$. $\square$

**Remark 6.2.** We now make three significant observations about the above lemma.
<figure><img src="image_15.png" /><figcaption>Figure 10: A pictorial depiction of Lemma 6.1, where the shaded region depicts the zone Z.</figcaption></figure>

(1) The lemma holds for $M$-reachable event-zones but not for all event-zones.

(2) 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.

(3) In our simulation $v \le_G v'$, we have $v(\vec{a}) = v'(\vec{a})$ (Remark 5.2): 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, due to the above property, 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 what we do in Section 6.2.

Now, we give the (†) conditions and prove that they are satisfied by canonical distance graphs of reachable zones.

**Lemma 6.3.** Let $Z \neq \emptyset$ be an $M$-reachable zone. Then, the canonical distance graph $\mathcal{G}(Z)$ satisfies the (†) conditions:

†1 If $Z_{\vec{x}0} = (<, +\infty)$ then for all $y \neq \vec{x}$, either $y$ is a prophecy clock which is undefined in $Z$ and $Z_{\vec{x}y} = Z_{0y} = (\le, -\infty)$ or $Z_{\vec{x}y} \in \{(<, +\infty), (\le, +\infty)\}$.

†2 If $Z_{\vec{x}0} < (<, +\infty)$ then $(\le, 0) \le Z_{\vec{x}0} \le (\le, M)$.

†3 If $Z_{\vec{x}\vec{y}} < (<, +\infty)$ then $(\le, 0) \le Z_{\vec{x}0} \le (\le, M)$.

†4 Either $Z_{0\vec{x}} = (\le, -\infty)$ or $(<, -M) \le Z_{0\vec{x}} \le (\le, 0)$.

†5 Either $Z_{0\vec{y}} = (\le, -\infty)$ or $Z_{x0} + (<, -M) \le Z_{\vec{x}\vec{y}}$ for all $x \in X$ with $x \neq \vec{y}$.

†6 Either $Z_{\vec{x}\vec{y}} \in \{(\le, -\infty), (<, +\infty), (\le, +\infty)\}$ or $(<, -M) \le Z_{\vec{x}\vec{y}} \le (\le, M)$.

*Proof.*

†1 Assume that $Z_{\vec{x}0} = (<, +\infty)$ and let $y \neq \vec{x}$. Consider first the case $Z_{0y} = (\le, -\infty)$, i.e., $y$ is a prophecy clock which is undefined in $Z$. Then, since $\mathcal{G}(Z)$ is in normal form, we have $Z_{\vec{x}0} \le Z_{\vec{x}0} + Z_{0y} = (<, +\infty) + (\le, -\infty) = (\le, -\infty)$.

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

Consider the distance graph $\mathcal{G}'$ obtained from $\mathcal{G}(Z)$ by setting the weight of edge $y \to 0$ to $\min(Z_{y0}, (<, +\infty))$ and of edge $0 \to \vec{x}$ to $\min(Z_{0\vec{x}}, (<, -M))$. Notice that $\mathcal{G}'$ is in standard form. We show that $\mathcal{G}'$ has no negative cycles. Since $\mathcal{G}(Z)$ is in normal form, the candidates for being negative must use the new weight $(<, -M)$ of $0 \to \vec{x}$ or the new weight $(<, +\infty)$ of $y \to 0$ or both. This gives the cycle $0 \to \vec{x} \to 0$ with weight $(<, -M) + Z_{\vec{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 \vec{x} \to y$ with weight $(<, +\infty) + (<, -M) + Z_{\vec{x}y}$ which is not negative since $Z_{\vec{x}y} \neq (\leq, -\infty)$. Since $G'$ is standard and has no negative cycle, Lemma 4.9 implies $[[G']] \neq \emptyset$. Note that $[[G']] \subseteq [[G(Z)]] = Z$. Finally, $-\infty < v(y)$ and $-\infty < v(\vec{x}) < -M$ for all $v \in G'$, which proves the claim.

By Lemma 6.1, $v_\alpha = v[\vec{x} \mapsto \alpha] \in Z$ for all $-\infty < \alpha < -M$. Now, $v_\alpha(y) - v_\alpha(\vec{x}) = v(y) - \alpha$ satisfies the constraint $Z_{\vec{x}y}$. We deduce that $Z_{\vec{x}y}$ is either $(<, +\infty)$ or $(\leq, +\infty)$.

†2 Suppose $(\leq, M) < Z_{\vec{x}0} < (<, +\infty)$. By Lemma 4.4, we find $\alpha$ such that $(\leq, \alpha) \leq Z_{\vec{x}0}$, $(\leq, -\alpha) \leq Z_{0\vec{x}}$ and $\alpha \not\leq M$. Now, by Lemma 4.10, we find $v \in Z$ with $-\infty < v(\vec{x}) = -\alpha < -M$. By Lemma 6.1, $v[\vec{x} \mapsto \alpha] \in Z$ for all $-\infty < \alpha < -M$, a contradiction with $Z_{\vec{x}0}$ finite.

†3 Assume $Z_{\vec{x}\vec{y}} < (<, +\infty)$ is finite. Since $G(Z)$ is standard, we get $Z_{\vec{x}0} \neq (\leq, +\infty)$. Now, $\dagger_1$ implies $Z_{\vec{x}0} < (<, +\infty)$. We conclude with $\dagger_2$.

†4 The proof is similar to $\dagger_2$. Suppose $(\leq, -\infty) < Z_{0\vec{x}} < (<, -M)$. By Lemma 4.4, we find $\alpha$ such that $(\leq, \alpha) \leq Z_{0\vec{x}}$, $(\leq, -\alpha) \leq Z_{\vec{x}0}$ and $\alpha \neq -\infty$. Now, by Lemma 4.10, we find $v \in Z$ with $-\infty < v(\vec{x}) = -\alpha < -M$. Since $Z_{0\vec{x}} < (<, -M)$, we can find $-\infty \neq \beta < -M$ such that $Z_{0\vec{x}} < (\leq, \beta)$. Now, Lemma 6.1 implies that $v[\vec{x} \mapsto \beta] \in Z$, which is a contradiction with $Z_{0\vec{x}} < (\leq, \beta)$.

†5 Suppose $Z_{0\vec{y}} \neq (\leq, -\infty)$. If $Z_{x0} = (\leq, -\infty)$ or $Z_{x\vec{y}} = (\leq, +\infty)$, the condition is trivially true. So we also assume in the following that $Z_{x0} \neq (\leq, -\infty)$ and $Z_{x\vec{y}} \neq (\leq, +\infty)$. Since $G(Z)$ is in standard form, we get $Z_{x0} \neq (\leq, +\infty)$. By Lemma 4.20, we also have $Z_{x\vec{y}} \neq (\leq, -\infty)$.

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

We claim that for all $\varepsilon > 0$ and all $c \in \mathbb{R}$ with $(\leq, c) < Z_{x0}$ we have $(\leq, c - M - \varepsilon) < Z_{x\vec{y}}$. Indeed, if $(\leq, c) < Z_{x0} = G''_{x0}$ then by Lemma 4.4 we find $\alpha$ such that $(\leq, \alpha) \leq G''_{x0}$, $(\leq, -\alpha) \leq G''_{0x}$ and $c < \alpha$. Next, by Lemma 4.10, we find $v \in [[G'')] \subseteq Z$ such that $v(x) = -\alpha$. If $v(\vec{y}) < -M$ then by Lemma 6.1 we get $v' = v[\vec{y} \mapsto -M - \varepsilon] \in Z$. Otherwise, we let $v' = v$. We have $c - M - \varepsilon < \alpha - M - \varepsilon \leq v'(\vec{y}) - v'(x)$. We obtain $(\leq, c - M - \varepsilon) < (\leq, v'(\vec{y}) - v'(x)) \leq Z_{x\vec{y}}$ and the claim is proved.

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

†6 Assume that $Z_{\vec{x}\vec{y}} \notin \{(\leq, -\infty), (<, +\infty), (\leq, +\infty)\}$. Since $G(Z)$ is in standard form, we have $Z_{\vec{x}0} \neq (\leq, +\infty)$. Now, $(\leq, -\infty) \neq Z_{\vec{x}\vec{y}} \leq Z_{\vec{x}0} + Z_{0\vec{y}}$ implies that $Z_{0\vec{y}} \neq (\leq, -\infty)$. Next, since $Z_{0\vec{y}} \neq (\leq, -\infty)$ and $Z_{\vec{x}\vec{y}} \notin \{(<, +\infty), (\leq, +\infty)\}$, by $\dagger_1$ we deduce that $Z_{\vec{x}0} \neq (<, +\infty)$.

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

Finally, $Z_{\vec{x}\vec{y}} \leq Z_{\vec{x}0} + Z_{0\vec{y}} \leq Z_{\vec{x}0} \leq (\leq, M)$ by $\dagger_2$.

<figure><img src="image_16.png" /></figure>
We now see that the (†) conditions imply that the weights of edges of the form $0 \to \vec{x}$, $\vec{x} \to 0$ and $\vec{x} \to \vec{y}$ belong to the finite set

$$ \{(\leq, -\infty), (\leq, +\infty), (\leq, +\infty)\} \cup \{(\leq, c) \mid c \in \mathbb{Z} \wedge -M \leq c \leq M\}. $$

For an example, see Figure 11. Note that the event-zone graph is sound and complete for reachability. Thus, we obtain as a corollary that, for event-predicting automata (EPA), we do not even need simulation to obtain finiteness.

**Corollary 6.4.** Let $\mathcal{A}$ be an EPA. The zone graph $\mathrm{EZG}(\mathcal{A})$ is finite.

<figure><img src="image_17.png" /><figcaption>Figure 11: Event-predicting automaton $\mathcal{A}_2$, for which there exists no finite time-abstract bisimulation on valuations, and its (finite) event-zone graph $\mathrm{EZG}(\mathcal{A}_2)$.</figcaption></figure>

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

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

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

For general ECA, i.e., when we have both history and prophecy clocks, we need to make sure that the finiteness of the simulation that we do for handling history clocks does not get affected in the presence of prophecy clocks. We turn to this issue in the next section.
**6.2. An equivalence relation of finite index on valuations.** We define an equivalence relation of finite index $\sim_M$ on valuations. First, we define $\sim_M$ on $\alpha, \beta \in \mathbb{R} = \mathbb{R} \cup \{-\infty, +\infty\}$ by $\alpha \sim_M \beta$ if $(\alpha \triangleleft c \Longleftrightarrow \beta \triangleleft c)$ for all $(\triangleleft, c)$ with $\triangleleft \in \{\triangleleft, \le\}$ and $c \in \{-\infty, +\infty\} \cup \{d \in \mathbb{Z} \mid |d| \le 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 $\leq_G$ when the finite constants used in the constraints are bounded by $M$. Recall from Section 5.1 the definition of the distance graph $\mathbb{G}_G(v)$ for the set of valuations $\uparrow_G v$.

**Lemma 6.5.** 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| \le M\}$. By replacing the weights ($\le$, $v_1(x)$) (resp. ($\le$, $-v_1(x)$)) by ($\le$, $v_2(x)$) (resp. ($\le$, $-v_2(x)$)) in the graph $\mathbb{G}_G(v_1)$ we obtain the graph $\mathbb{G}_G(v_2)$.

*Proof.* This is clear by definition for edges $\overrightarrow{x} \to 0$ and $0 \to \overrightarrow{x}$ adjacent to a prophecy clock. We consider now edges adjacent to history clocks $\overleftarrow{x}$.

* Consider the edge $0 \to \overleftarrow{x}$.

- If its weight is ($\le$, $v_1(\overleftarrow{x})$) in $\mathbb{G}_G(v_1)$ then there is some $\overleftarrow{x} \triangleleft c \in G$ with ($\triangleleft, c) \prec (\prec, +\infty)$ and $v_1(\overleftarrow{x}) \triangleleft c$. Since $v_1 \sim_M v_2$ we deduce that $v_2(\overleftarrow{x}) \triangleleft c$ and the edge $0 \to \overleftarrow{x}$ has weight ($\le$, $v_2(\overleftarrow{x})$) in $\mathbb{G}_G(v_2)$.

- If its weight is ($\prec, +\infty$) in $\mathbb{G}_G(v_1)$ then we are not in the case above and $\overleftarrow{x} < +\infty \in G$, $v_1(\overleftarrow{x}) < +\infty$. Since $v_1 \sim_M v_2$ we deduce that $v_2(\overleftarrow{x}) < +\infty$ and the edge $0 \to \overleftarrow{x}$ has weight ($\prec, +\infty$) in $\mathbb{G}_G(v_2)$.

- Otherwise, the weight is ($\le$, $+\infty$) in both $\mathbb{G}_G(v_1)$ and $\mathbb{G}_G(v_2)$.

* Consider the edge $\overleftarrow{x} \to 0$.

- If its weight is ($\le$, $-\infty$) in $\mathbb{G}_G(v_1)$ then $+\infty \le \overleftarrow{x} \in G$ and $v_1(\overleftarrow{x}) = +\infty$. Since $v_1 \sim_M v_2$ we deduce that $v_2(\overleftarrow{x}) = +\infty$ and the edge $\overleftarrow{x} \to 0$ has weight ($\le$, $-\infty$) in $\mathbb{G}_G(v_2)$.

- If its weight is ($\triangleleft, -c$) in $\mathbb{G}_G(v_1)$ then we are not in the case above and there is some $c \triangleleft \overleftarrow{x} \in G$ with ($c, \triangleleft) \prec (+\infty, \le)$ and $c \triangleleft v_1(\overleftarrow{x})$. Since $v_1 \sim_M v_2$ we deduce that $c \triangleleft v_2(\overleftarrow{x})$ and the edge $\overleftarrow{x} \to 0$ has weight ($\triangleleft, -c$) in $\mathbb{G}_G(v_2)$.

- If its weight is ($\le$, $-v_1(\overleftarrow{x})$) in $\mathbb{G}_G(v_1)$ then we are not in the cases above and there is some $c \triangleleft \overleftarrow{x} \in G$ with ($c, \triangleleft) \prec (+\infty, \le)$ and $c \nparallel v(\overleftarrow{x})$. Since $v_1 \sim_M v_2$ we deduce that $c \nparallel v_2(\overleftarrow{x})$ and the edge $\overleftarrow{x} \to 0$ has weight ($\le$, $-v_2(\overleftarrow{x})$) in $\mathbb{G}_G(v_2)$.

- Otherwise, the weight is ($\le$, $0$) in both $\mathbb{G}_G(v_1)$ and $\mathbb{G}_G(v_2)$.

Next we state the central lemma that says that $\downarrow_G Z$ is a union of $\sim_M$ equivalence classes.

**Lemma 6.6.** 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| \le M\}$. Let $Z$ be a zone with a canonical distance graph $\mathbb{G}(Z)$ satisfying (†). Then, $v_1 \in \downarrow_G Z$ iff $v_2 \in \downarrow_G Z$.

*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 5.8 we find a negative cycle $C_2$ using one edge from $\mathbb{G}(Z)$ and one or two edges from $\mathbb{G}_G(v_2)$. By Lemma 6.5, we have a corresponding cycle $C_1$ using the same edge from $\mathbb{G}(Z)$ and the same one or two edges from $\mathbb{G}_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.

$$ (1) \text{ Cycle } C_2 = 0 \xrightarrow{\langle\leq, v_2(\bar{y})\rangle} \bar{y} \xrightarrow{Z_{\bar{y}} \xrightarrow{\langle\leq, v_1(\bar{y})\rangle}} 0. \text{ We have } C_1 = 0 \xrightarrow{\langle\leq, v_1(\bar{y})\rangle} \bar{y} \xrightarrow{Z_{\bar{y}} \xrightarrow{\langle\leq, v_1(\bar{y})\rangle}} 0. $$

Since we have the edge $0 \xrightarrow{\langle\leq, v_1(\bar{y})\rangle} \bar{y}$ in $\mathbb{G}_G(v_1)$, there is a constraint $\bar{y}' \prec c'$ in $G$ with $(\bar{y}', c') < (\langle-, +\infty\rangle)$ and $v_1(\bar{y}) \prec' c'$. We deduce that $0 \leq v_1(\bar{y}) \leq M$.

Let $Z_{\bar{y}0} = (\prec, c)$. Since $C_1$ is not a negative cycle, we get $(\leq, 0) \leq (\prec, c + v_1(\bar{y}))$, which is equivalent to $-c \leq v_1(\bar{y})$. Using $0 \leq v_1(\bar{y}) \leq M$ and $v_1 \sim_M v_2$ we deduce that $-c \leq v_2(\bar{y})$. This is equivalent to $(\leq, 0) \leq (\prec, c + v_2(\bar{y}))$, a contradiction with $C_2$ being a negative cycle.

$$ (2) \text{ Cycle } C_2 = 0 \xrightarrow{Z_{0\bar{y}}} \bar{y} \xrightarrow{\langle\leq, -v_2(\bar{y})\rangle} 0. \text{ We have } C_1 = 0 \xrightarrow{Z_{0\bar{y}}} \bar{y} \xrightarrow{\langle\leq, -v_1(\bar{y})\rangle} 0. $$

Since we have the edge $\bar{y} \xrightarrow{\langle\leq, -v_1(\bar{y})\rangle} 0$ in $\mathbb{G}_G(v_1)$, there is a constraint $c' \prec' \bar{y}$ in $G$ with $(c', \prec') < (+\infty, \leq)$ and $c' \nsim v_1(\bar{y})$. We deduce that $0 \leq v_1(\bar{y}) \leq M$.

Let $Z_{\bar{y}0} = (\prec, c)$. Since $C_1$ is not a negative cycle, we get $(\leq, 0) \leq (\prec, c - v_1(\bar{y}))$, which is equivalent to $v_1(\bar{y}) \leq c$. Using $v_1 \sim_M v_2$ and $0 \leq v_1(\bar{y}) \leq M$, we deduce that $v_2(\bar{y}) \leq c$. This is equivalent to $(\leq, 0) \leq (\prec, c + v_2(\bar{y}))$, a contradiction with $C_2$ being a negative cycle.

$$ (3) \text{ Cycle } C_2 = 0 \xrightarrow{\langle\leq, v_2(\vec{x})\rangle} \vec{x} \xrightarrow{Z_{\vec{x}} \xrightarrow{\langle\leq, v_1(\vec{x})\rangle}} 0. \text{ We have } C_1 = 0 \xrightarrow{Z_{\vec{x}} \xrightarrow{\langle\leq, v_1(\vec{x})\rangle}} \vec{x} \xrightarrow{Z_{\vec{x}} \xrightarrow{\langle\leq, v_1(\vec{x})\rangle}} 0. $$

Since $C_2$ is negative, we have $Z_{\vec{x}} \neq (\leq, +\infty)$. Also, if $Z_{\vec{x}} = (\langle-, +\infty\rangle)$ then we must have $v_2(\vec{x}) = -\infty$, which implies $v_1(\vec{x}) = -\infty$ since $v_1 \sim_M v_2$, a contradiction with $C_1$ being non-negative. Hence, $Z_{\vec{x}} = (\prec, c) < (\langle-, +\infty\rangle)$ and by $(\dagger_2)$, we infer $0 \leq c \leq M$.

Since $C_1$ is not negative, we get $(\leq, 0) \leq (\prec, c + v_1(\vec{x}))$, which is equivalent to $-c \leq v_1(\vec{x})$. Using $v_1 \sim_M v_2$ and $0 \leq c \leq M$ we deduce that $-c \leq v_2(\vec{x})$. This is equivalent to $(\leq, 0) \leq (\prec, c + v_2(\vec{x}))$, a contradiction with $C_2$ being a negative cycle.

$$ (4) \text{ Cycle } C_2 = 0 \xrightarrow{Z_{0\vec{x}}} \vec{x} \xrightarrow{\langle\leq, -v_2(\vec{x})\rangle} 0. \text{ We have } C_1 = 0 \xrightarrow{Z_{0\vec{x}}} \vec{x} \xrightarrow{\langle\leq, -v_1(\vec{x})\rangle} 0. $$

Let $Z_{0\vec{x}} = (\prec, c)$. Since $C_2$ is negative, we deduce that $v_2(\vec{x}) \neq -\infty$. Using $v_1 \sim_M v_2$, we infer $v_1(\vec{x}) \neq -\infty$. Since $C_1$ is not negative, we get $Z_{0\vec{x}} \neq (\leq, -\infty)$. From $(\dagger_4)$, we infer $(\langle-, -M\rangle) \leq Z_{0\vec{x}}$ and $-M \leq c \leq 0$.

Since $C_1$ is not a negative cycle, we get $(\leq, 0) \leq (\prec, c - v_1(\vec{x}))$, which is equivalent to $v_1(\vec{x}) \leq c$. Using $v_1 \sim_M v_2$ and $-M \leq c \leq 0$, we deduce that $v_2(\vec{x}) \leq c$. This is equivalent to $(\leq, 0) \leq (\prec, c - v_2(\vec{x}))$, a contradiction with $C_2$ being a negative cycle.

$$ (5) \text{ Cycle } C_2 = 0 \xrightarrow{\langle\leq, v_2(\bar{y})\rangle} \bar{y} \xrightarrow{Z_{\bar{y}} \xrightarrow{\langle\leq, v_1(\bar{y})\rangle}} \vec{x} \xrightarrow{Z_{\vec{x}} \xrightarrow{\langle\leq, v_1(\vec{x})\rangle}} 0. $$

$$ \text{We have } C_1 = 0 \xrightarrow{\langle\leq, v_1(\bar{y})\rangle} \bar{y} \xrightarrow{Z_{\bar{y}}} \vec{x} \xrightarrow{\langle\leq, -v_1(\vec{x})\rangle} 0. $$

Let $Z_{\bar{y}\vec{x}} = (\prec, c)$. As in case 1 above, we get $0 \leq v_1(\bar{y}) \leq M$. From the fact that the cycle $0 \xrightarrow{\langle\leq, v_1(\bar{y})\rangle} \bar{y} \xrightarrow{Z_{\bar{y}} \xrightarrow{\langle\leq, v_1(\bar{y})\rangle}} 0$ is not negative, we get $(\leq, -M) \leq Z_{\bar{y}0}$. Since $C_2$ is negative, we get $v_2(\bar{x}) \neq -\infty$. Using $v_1 \sim_M v_2$, we infer $v_1(\bar{x}) \neq -\infty$. From the fact that the cycle $0 \xrightarrow{Z_{0\vec{x}}} \vec{x} \xrightarrow{\langle\leq, -v_1(\vec{x})\rangle} 0$ is not negative, we deduce $Z_{0\vec{x}} \neq (\leq, -\infty)$. Using $(\dagger_5)$ we obtain

$$ (\leq, -M) + (\langle-, -M\rangle) \leq Z_{\bar{y}0} + (\langle-, -M\rangle) \leq Z_{\bar{y}\vec{x}} = (\prec, c) $$

and we deduce that $-2M \leq c \leq 0$.
Since $C_1$ is not a negative cycle, we get $(\le, 0) \le (\triangleleft, c + v_1(\bar{y}) - v_1(\bar{x}))$, which is equivalent to $v_1(\bar{x}) - v_1(\bar{y}) \le c$. Using $v_1 \sim_M v_2$ and $-2M \le c \le 0$ we deduce that $v_2(\bar{x}) - v_2(\bar{y}) \le c$. We conclude as in the previous cases.

$$
(6) \text{ Cycle } C_2 = 0 \xrightarrow{\langle\le, v_2(\bar{x})\rangle} \bar{x} \xrightarrow{Z_{\bar{x}}\bar{y}} \bar{y} \xrightarrow{\langle\le, -v_2(\bar{y})\rangle} 0.
$$

$$
\text{We have } C_1 = 0 \xrightarrow{\langle\le, v_1(\bar{x})\rangle} \bar{x} \xrightarrow{Z_{\bar{x}}\bar{y}} \bar{y} \xrightarrow{\langle\le, -v_1(\bar{y})\rangle} 0.
$$

Since $C_2$ is negative but not $C_1$, we get first $Z_{\bar{x}\bar{y}} \neq (\le, +\infty)$ and then $v_1(\bar{x}) \neq -\infty$. As in case 2 above, we get $0 \le v_1(\bar{y}) \le M$. We deduce that $Z_{\bar{x}\bar{y}} = (\triangleleft, c) < (\triangleleft, +\infty)$ and $c \neq +\infty$. From $(\dagger_3)$ we obtain $Z_{\bar{x}0} \le (\le, M)$. Since $0 \xrightarrow{\langle\le, v_1(\bar{x})\rangle} \bar{x} \xrightarrow{Z_{\bar{x}0}} 0$ is not a negative cycle, we get $-M \le v_1(\bar{x}) \le 0$. Finally, we obtain $0 \le v_1(\bar{y}) - v_1(\bar{x}) \le 2M$.

Since $C_1$ is not a negative cycle, we get $(\le, 0) \le (\triangleleft, c + v_1(\bar{x}) - v_1(\bar{y}))$, which is equivalent to $v_1(\bar{y}) - v_1(\bar{x}) \le c$. Using $v_1 \sim_M v_2$ and $0 \le v_1(\bar{y}) - v_1(\bar{x}) \le 2M$, we deduce that $v_2(\bar{y}) - v_2(\bar{x}) \le c$. We conclude as in the previous cases.

$$
(7) \text{ Cycle } C_2 = 0 \xrightarrow{\langle\le, v_2(\bar{x})\rangle} \bar{x} \xrightarrow{Z_{\bar{x}}\bar{y}} \bar{y} \xrightarrow{\langle\alpha', -c'\rangle} 0.
$$

$$
\text{We have } C_1 = 0 \xrightarrow{\langle\le, v_1(\bar{x})\rangle} \bar{x} \xrightarrow{Z_{\bar{x}}\bar{y}} \bar{y} \xrightarrow{\langle\alpha', -c'\rangle} 0.
$$

$$
\text{Let } Z_{\bar{x}\bar{y}} = (\triangleleft, c). \text{ As in case 6 above, we show that } c \neq +\infty \text{ and } -M \le v_1(\bar{x}) \le 0.
$$

Since $C_1$ is not a negative cycle, we get $0 \le c + v_1(\bar{x}) - c'$, which is equivalent to $c' - c \le v_1(\bar{x})$. Using $v_1 \sim_M v_2$ and $-M \le v_1(x) \le 0$, we deduce that $c' - c \le v_2(\bar{x})$, which is equivalent to $0 \le c + v_2(\bar{x}) - c'$, a contradiction with $C_2$ being a negative cycle.

$$
(8) \text{ Cycle } C_2 = 0 \xrightarrow{\langle\le, v_2(\bar{x})\rangle} \bar{x} \xrightarrow{Z_{\bar{x}}\bar{y}} \bar{y} \xrightarrow{\langle\le, -v_2(\bar{y})\rangle} 0 \text{ with } x \neq y.
$$

$$
\text{We have } C_1 = 0 \xrightarrow{\langle\le, v_1(\bar{x})\rangle} \bar{x} \xrightarrow{Z_{\bar{x}}\bar{y}} \bar{y} \xrightarrow{\langle\le, -v_1(\bar{y})\rangle} 0.
$$

Since $C_2$ is negative but not $C_1$, using $v_1 \sim_M v_2$ we get successively $Z_{\bar{x}\bar{y}} \neq (\le, +\infty)$, $v_2(\bar{y}) \neq -\infty \neq v_1(\bar{y})$, $v_1(\bar{x}) \neq -\infty \neq v_2(\bar{x})$, and finally $(\le, -\infty) < Z_{\bar{x}\bar{y}} < (\triangleleft, +\infty)$.

$$
\text{Let } Z_{\bar{x}\bar{y}} = (\triangleleft, c). \text{ From } (\dagger_6), \text{ we deduce that } -M \le c \le M.
$$

Since $C_1$ is not a negative cycle, we get $(\le, 0) \le (\triangleleft, c + v_1(\bar{x}) - v_1(\bar{y}))$, which is equivalent to $v_1(\bar{y}) - v_1(\bar{x}) \le c$. Using $v_1 \sim_M v_2$ and $-M \le c \le M$, we deduce that $v_2(\bar{y}) - v_2(\bar{x}) \le c$. We conclude as in the previous cases.

$$
(9) \text{ Cycle } C_2 = 0 \xrightarrow{\langle\le, v_2(\bar{x})\rangle} \bar{x} \xrightarrow{Z_{\bar{x}}\bar{y}} \bar{y} \xrightarrow{\langle\le, -v_2(\bar{y})\rangle} 0 \text{ with } x \neq y.
$$

$$
\text{We have } C_1 = 0 \xrightarrow{\langle\le, v_1(\bar{x})\rangle} \bar{x} \xrightarrow{Z_{\bar{x}}\bar{y}} \bar{y} \xrightarrow{\langle\le, -v_1(\bar{y})\rangle} 0.
$$

As in case 1 above, we get $0 \le v_1(\bar{x}) \le M$. As in case 2 above, we get $0 \le v_1(\bar{y}) \le M$.
We obtain $-M \le v_1(\bar{y}) - v_1(\bar{x}) \le M$.

Let $Z_{\bar{x}\bar{y}} = (\triangleleft, c)$. Since $C_1$ is not negative, we get $(\le, 0) \le (\triangleleft, c + v_1(\bar{x}) - v_1(\bar{y}))$, which is equivalent to $v_1(\bar{y}) - v_1(\bar{x}) \le c$. Using $v_1 \sim_M v_2$ and $-M \le v_1(\bar{y}) - v_1(\bar{x}) \le M$, we deduce that $v_2(\bar{y}) - v_2(\bar{x}) \le c$. We conclude as in the previous cases.

$$
(10) \text{ Cycle } C_2 = 0 \xrightarrow{\langle\le, v_2(\bar{x})\rangle} \bar{x} \xrightarrow{Z_{\bar{x}}\bar{y}} \bar{y} \xrightarrow{\langle\alpha', -c'\rangle} 0 \text{ with } x \neq y.
$$

$$
\text{We have } C_1 = 0 \xrightarrow{\langle\le, v_1(\bar{x})\rangle} \bar{x} \xrightarrow{Z_{\bar{x}}\bar{y}} \bar{y} \xrightarrow{\langle\alpha', -c'\rangle} 0.
$$

As in case 1 above, we get $0 \le v_1(\bar{x}) \le M$.

Let $Z_{\bar{x}\bar{y}} = (\triangleleft, c)$. Since $C_1$ is not negative, we get $0 \le c + v_1(\bar{x}) - c'$, which is equivalent to $c' - c \le v_1(\bar{x})$. Using $v_1 \sim_M v_2$ and $0 \le v_1(\bar{x}) \le M$, we deduce that $c' - c \le v_2(\bar{x})$, which is equivalent to $0 \le c + v_2(\bar{x}) - c'$, a contradiction with $C_2$ being a negative cycle.
Notice that we have crucially used the “2M” occurring in the definition of $v_1 \sim_M v_2$ (as $v_1(x) - v_1(y) \sim_{2M} v_2(x) - v_2(y)$) in the cases where we deal with cycles containing one prophecy clock and one history clock (Cases 5 and 6). In the rest of the cases, it was sufficient to use $v_1(x) \sim_M v_2(x)$. $\square$

Finally, from Lemmas 6.3 and 6.6, we obtain our main theorem of the section.

**Theorem 6.7.** The simulation relation $\preceq_A$ is finite.

*Proof.* Let $(q, Z_0), (q, Z_1), (q, Z_2), \dots$ be an infinite sequence of reachable nodes in $EZG(A)$. By Lemma 6.3, for all $i$, the distance graph $G(Z_i)$ in canonical form satisfies conditions (†).

The atomic constraints in $G = G(q)$ use constants in $\{-\infty, +\infty\} \cup \{c \in \mathbb{Z} \mid |c| \le M\}$. From Lemma 6.6 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$. $\square$

Note that the number of enumerated zones is bounded by $2^r$ where $r$ is the number of equivalence classes of $\sim_M$. This is similar to the known upper bound in classical timed automata, where instead of $r$, we can use the number of regions as defined in [AD94]. 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.

## 7. 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 $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. As a follow-up to this work, we have extended our reachability algorithm to a more general model, called *Generalized timed automaton (GTA)* [AGG+23] (which subsumes event-clock automata). In [AGG+23], we also developed a prototype implementation of our algorithm in `TCHECKER`, an open-source platform for timed automata analysis. To the best of our knowledge, this is the first tool that can handle event-clock automata, and it provides a way to efficiently check event-clock specifications on timed automata models.

## REFERENCES

[ABG13] S. Akshay, Benedikt Bollig, and Paul Gastin. Event clock message passing automata: a logical characterization and an emptiness checking algorithm. *Formal Methods Syst. Des.*, 42(3):262–300, 2013.

[AD94] Rajeev Alur and David L. Dill. A theory of timed automata. *Theoretical Computer Science*, 126:183–235, 1994.
[AFH99] Rajeev Alur, Limor Fix, and Thomas A. Henzinger. Event-clock automata: A determinizable class of timed automata. *Theor. Comput. Sci.*, 211(1-2):253-273, 1999.

[AGG$^{+}$23] S. Akshay, Paul Gastin, R. Govind, Aniruddha R. Joshi, and B. Srivathsan. A unified model for real-time systems: Symbolic techniques and implementation. In *CAV (1)*, volume 13964 of *Lecture Notes in Computer Science*, pages 266–288. Springer, 2023.

[AGGS22] S. Akshay, Paul Gastin, R. Govind, and B. Srivathsan. Simulations for event-clock automata. In *CONCUR*, volume 243 of *LIPIcs*, pages 13:1–13:18. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2022.

[AGP21] S. Akshay, Paul Gastin, and Karthik R. Prakash. Fast zone-based algorithms for reachability in pushdown timed automata. In *CAV (1)*, volume 12759 of *Lecture Notes in Computer Science*, pages 619–642. Springer, 2021.

[BCM16] Patricia Bouyer, Maximilien Colange, and Nicolas Markey. Symbolic optimal reachability in weighted timed automata. In *CAV (1)*, volume 9779 of *Lecture Notes in Computer Science*, pages 513–530. Springer, 2016.

[BDL$^{+}$06] Gerd Behrmann, Alexandre David, Kim Guldstrand Larsen, John Hakansson, Paul Pettersson, Wang Yi, and Martijn Hendriks. UPPAAL 4.0. In *QEST*, pages 125–126. IEEE Computer Society, 2006.

[BDM$^{+}$98] Marius Bozga, Conrado Daws, Oded Maler, Alfredo Olivero, Stavros Tripakis, and Sergio Yovine. Kronos: A model-checking tool for real-time systems. In *CAV*, volume 1427 of *Lecture Notes in Computer Science*, pages 546–550. Springer, 1998.

[Bou04] Patricia Bouyer. Forward analysis of updatable timed automata. *Formal Methods Syst. Des.*, 24(3):281–320, 2004.

[BY03] Johan Bengtsson and Wang Yi. Timed automata: Semantics, algorithms and tools. In *ACPN 2003*, volume 3098 of *Lecture Notes in Computer Science*, pages 87–124. Springer, 2003.

[Dil89] David L. Dill. Timing assumptions and verification of finite-state concurrent systems. In *Automatic Verification Methods for Finite State Systems*, volume 407 of *Lecture Notes in Computer Science*, pages 197–212. Springer, 1989.

[DT98] Conrado Daws and Stavros Tripakis. Model checking of real-time reachability properties using abstractions. In *TACAS*, volume 1384 of *Lecture Notes in Computer Science*, pages 313–329. Springer, 1998.

[DT04] Deepak D'Souza and Nicolas Tabareau. On timed automata with input-determined guards. In *FORMATS/FTRTFT*, volume 3253 of *Lecture Notes in Computer Science*, pages 68–83. Springer, 2004.

[GMS18] Paul Gastin, Sayan Mukherjee, and B. Srivathsan. Reachability in timed automata with diagonal constraints. In *CONCUR*, volume 118 of *LIPIcs*, pages 28:1–28:17. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2018.

[GMS19] Paul Gastin, Sayan Mukherjee, and B. Srivathsan. Fast algorithms for handling diagonal constraints in timed automata. In *CAV (1)*, volume 11561 of *Lecture Notes in Computer Science*, pages 41–59. Springer, 2019.

[GMS20] Paul Gastin, Sayan Mukherjee, and B. Srivathsan. Reachability for updatable timed automata made faster and more effective. In *FSTTCS*, volume 182 of *LIPIcs*, pages 47:1–47:17. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2020.

[GRS11] Gilles Geeraerts, Jean-François Raskin, and Nathalie Sznajder. Event clock automata: From theory to practice. In *FORMATS*, volume 6919 of *Lecture Notes in Computer Science*, pages 209–224. Springer, 2011.

[GRS14] Gilles Geeraerts, Jean-François Raskin, and Nathalie Sznajder. On regions and zones for event-clock automata. *Formal Methods Syst. Des.*, 45(3):330–380, 2014.

[HP19] Frédéric Herbreteau and Gerald Point. TChecker. https://github.com/fredher/tchecker, v0.2 - April 2019.

[HSW12] Frédéric Herbreteau, B. Srivathsan, and Igor Walukiewicz. Better abstractions for timed automata. In *LICS*, pages 375–384. IEEE Computer Society, 2012.

[HSW13] Frédéric Herbreteau, B. Srivathsan, and Igor Walukiewicz. Lazy abstractions for timed automata. In *CAV*, volume 8044 of *Lecture Notes in Computer Science*, pages 990–1005. Springer, 2013.
[KLM<sup>+</sup>15] Gijs Kant, Alfons Laarman, Jeroen Meijer, Jaco van de Pol, Stefan Blom, and Tom van Dijk. LTSmin: High-performance language-independent model checking. In *TACAS*, volume 9035 of *Lecture Notes in Computer Science*, pages 692–707. Springer, 2015.

[KWNP08] Sebastian Kupferschmid, Martin Wehrle, Bernhard Nebel, and Andreas Podelski. Faster than UPPAAL? In *CAV*, volume 5123 of *Lecture Notes in Computer Science*, pages 552–555. Springer, 2008.

[LPY97] Kim Guldstrand Larsen, Paul Pettersson, and Wang Yi. UPPAAL in a nutshell. *STTT*, 1(1-2):134–152, 1997.

[RS99] Jean-François Raskin and Pierre-Yves Schobbens. The logic of event clocks - decidability, complexity and expressiveness. *J. Autom. Lang. Comb.*, 4(3):247–282, 1999.

[RSM19] Victor Roussanaly, Ocan Sankur, and Nicolas Markey. Abstraction refinement algorithms for timed automata. In *CAV (1)*, volume 11561 of *Lecture Notes in Computer Science*, pages 22–40. Springer, 2019.

[SLDP09] Jun Sun, Yang Liu, Jin Song Dong, and Jun Pang. PAT: towards flexible verification under fairness. In *CAV*, volume 5643 of *Lecture Notes in Computer Science*, pages 709–714. Springer, 2009.

[THV<sup>+</sup>17] Tamás Tóth, Ákos Hajdu, András Vörös, Zoltán Micskei, and István Majzik. Theta: a framework for abstraction refinement-based model checking. In Daryl Stewart and Georg Weissenbacher, editors, *Proceedings of the 17th Conference on Formal Methods in Computer-Aided Design*, pages 176–179, 2017.

[Wan06] Farn Wang. REDLIB for the formal verification of embedded systems. In *ISoLA*, pages 341–346. IEEE Computer Society, 2006.

[ZLZ05] Jianhua Zhao, Xuandong Li, and Guoliang Zheng. A quadratic-time DBM-based successor algorithm for checking timed automata. *Inf. Process. Lett.*, 96(3):101–105, 2005.