and

$$t_1 = \min_{x \in X} \{\frac{\mathrm{frac}(w'(x))}{\mathrm{frac}(w'(x_j))} + v(d_{0,x})\}.$$

We want to prove that $t_0 = t_1 > 0$. For this purpose, let us first show that for all $i, j$ we have $\frac{\mathrm{frac}(w'(x_j))}{\mathrm{frac}(w'(x_j))} - v(d'_{j,0}) \le \frac{\mathrm{frac}(w'(x_i))}{\mathrm{frac}(w'(x_i))} + v(d'_{0,i})$, which is $t_0 \le t_1$.

First note that for all $i, j$

$$\frac{\mathrm{frac}(w'(x_j))}{\mathrm{frac}(w'(x_j))} - \frac{\mathrm{frac}(w'(x_i))}{\mathrm{frac}(w'(x_i))} \triangleq \langle \langle \rangle_{ji'} \langle \rangle_{j,i}.$$

By applying $TE_<(\mathrm{Algorithm~2})$ to $(E, D)$, we have that $D'_{j,i} = D_{j,i}$, i. e., $(d_{i,j}, \triangleq \langle \rangle_{ij}) = (d'_{i,j}, \triangleq \langle \rangle_{ij'})$, and from Definition 3.6 (2) we have that $D_{j,i} \le D_{j,0} + D_{0,i}$ is valid for $R_p$.

Hence, we have from Definition 3.3 (2b) that either $v(d_{j,i}) < v(d_{j,0}) + v(d_{0,i})$ or $v(d_{j,i}) \le v(d_{j,0}) + v(d_{0,i})$ and $\triangleq \langle \rangle_{ji} = \triangleq \langle \rangle_{j0} \oplus \triangleq \langle \rangle_{0i}$ or $\triangleq \langle \rangle_{ji} = \langle \rangle_{0i}$ and $\triangleq \langle \rangle_{j0} \oplus \triangleq \langle \rangle_{0i} = \le$.

We can then write that

$$\frac{\mathrm{frac}(w'(x_j))}{\mathrm{frac}(w'(x_j))} - \frac{\mathrm{frac}(w'(x_i))}{\mathrm{frac}(w'(x_i))} (\triangleq \langle \rangle_{j0} \oplus \triangleq \langle \rangle_{0i}) v(d_{j,0}) + v(d_{0,i})$$

which is equivalent to

$$\frac{\mathrm{frac}(w'(x_j))}{\mathrm{frac}(w'(x_j))} - v(d_{j,0}) (\triangleq \langle \rangle_{j0} \oplus \triangleq \langle \rangle_{0i}) \frac{\mathrm{frac}(w'(x_i))}{\mathrm{frac}(w'(x_i))} + v(d_{0,i})$$

so we obtain our result, as $(\triangleq \langle \rangle_{j0} \oplus \triangleq \langle \rangle_{0i})$ is either $\le$ or $<$.

Now, recall that in $(E, D)$ for all $x$ we have $d_{0,x} = -d_{x,0}$ and $\triangleq \langle \rangle_{0x} = \triangleq \langle \rangle_{0x}$.

For any clock $x$ we have that $\frac{\mathrm{frac}(w'(x))}{\mathrm{frac}(w'(x))} - v(d_{x,0}) \le t_0$ and that $t_1 \le \frac{\mathrm{frac}(w'(x))}{\mathrm{frac}(w'(x))} + v(d_{0,x}) = \frac{\mathrm{frac}(w'(x))}{\mathrm{frac}(w'(x))} - v(d_{x,0})$.

Hence $t_0 = t_1$.

As for all $x, \triangleq \langle \rangle_{x0} = \le$, we have for all $i, j$ that $(\triangleq \langle \rangle_{x0} \oplus \triangleq \langle \rangle_{0i}) = \triangleq \langle \rangle_{0i}$ and $(\triangleq \langle \rangle_{j0} \oplus \triangleq \langle \rangle_{0x}) = \triangleq \langle \rangle_{j0}$, which gives

$$t_1 \triangleq \langle \rangle_{0i} \frac{\mathrm{frac}(w'(x_i))}{\mathrm{frac}(w'(x_i))} + v(d_{0,i})$$

and

$$\frac{\mathrm{frac}(w'(x_j))}{\mathrm{frac}(w'(x_j))} - v(d_{j,0}) \triangleq \langle \rangle_{j0} t_0.$$

Moreover in $(E', D')$ we have that $\frac{\mathrm{frac}(w'(x))}{\mathrm{frac}(w'(x))} \triangleq \langle \rangle_{0x'} v(d'_{0,x})$. From Claim H.1, $(E', D')$ is obtained after applying Algorithm 2 and therefore $\triangleq \langle \rangle_{0x'} = <$. Hence $0 < \frac{\mathrm{frac}(w'(x))}{\mathrm{frac}(w'(x))}$ and

$$0 < t_0 = t_1.$$

Let $\delta = t_0 = t_1$. More intuitively $\delta$ is the value right in the middle of the least and the largest amount of time s.t. we can go backward in time from $w'$ and respect all constraints defined in $(E, v(D))$.

First we have

$$-\frac{\mathrm{frac}(w'(x_j))}{\mathrm{frac}(w'(x_j))} + \delta \le -\frac{\mathrm{frac}(w'(x_j))}{\mathrm{frac}(w'(x_j))} + t_1 \triangleq \langle \rangle_{j0} - \frac{\mathrm{frac}(w'(x_j))}{\mathrm{frac}(w'(x_j))} + \frac{\mathrm{frac}(w'(x_j))}{\mathrm{frac}(w'(x_j))} + v(d_{0,j}) = v(d_{0,j})$$

Secondary we have

$$\frac{\mathrm{frac}(w'(x_j))}{\mathrm{frac}(w'(x_j))} - \delta \le \frac{\mathrm{frac}(w'(x_j))}{\mathrm{frac}(w'(x_j))} - t_0 \triangleq \langle \rangle_{0j} \frac{\mathrm{frac}(w'(x_j))}{\mathrm{frac}(w'(x_j))} - \frac{\mathrm{frac}(w'(x_j))}{\mathrm{frac}(w'(x_j))} + v(d_{j,0}) = v(d_{j,0})$$

which is $\frac{\mathrm{frac}(w'(x_j))}{\mathrm{frac}(w'(x_j))} - \delta \triangleq \langle \rangle_{0j} v(d_{j,0})$.

Now we prove that constraints defined in $(E, D)$ on differences of clocks are also satisfied by going back of $\delta$ units of time from $w'$

$$D'_{j,i} = D_{j,i} \quad \text{and} \quad D'_{i,j} = D_{i,j}.$$
Since we already treated the case whether $i$ or $j$ are 0, now suppose $i, j$ are both different from 0. We have that $\text{frac}(w'(x_j)) - \text{frac}(w'(x_i)) \triangleleft_{ji'} v(d'_{j,i}) = v(d_{j,i})$, and therefore as $\triangleleft_{ji'} = \triangleleft_{ji}$,

$$ \text{frac}(w'(x_j)) - \delta - \text{frac}(w'(x_i)) + \delta \triangleleft_{ji} v(d_{j,i}). $$

We also have that $\text{frac}(w'(x_i)) - \text{frac}(w'(x_j)) \triangleleft_{ij'} v(d'_{i,j}) = v(d_{i,j})$, therefore as $\triangleleft_{ij'} = \triangleleft_{ij}$,

$$ \text{frac}(w'(x_i)) - \delta - \text{frac}(w'(x_j)) + \delta \triangleleft_{ij} v(d_{i,j}). $$

To conclude, we define for all $x_j$

$$ w(x_j) = w'(x_j) - \delta $$

and clearly, $w \in (E, v(D))$.

(⇒) **for point-p-PDBMs**

Assume in $(E, D) \in \mathcal{P}\mathcal{DB}\mathcal{M}_{\odot}(R_p)$. Let $v \in R_p$, and $x_i \in \text{LFP}_{R_p}(D)$.

Now consider $(E', D') = TE((E, D))$. We need to find a value $\delta$ s.t. $w + \delta \in (E', v(D'))$. which is equivalent to prove for all $x_i, x_j$

$$ \text{frac}(w(x_j)) + \delta - \text{frac}(w(x_i)) - \delta \triangleleft_{ji'} v(d'_{j,i}) $$

and

$$ \text{frac}(w(x_i)) + \delta - \text{frac}(w(x_j)) - \delta \triangleleft_{ij'} v(d'_{i,j}) $$

and

$$ -\text{frac}(w(x_j)) - \delta \triangleleft_{0j'} v(d'_{0,j}) \quad \text{and} \quad \text{frac}(w(x_i)) + \delta \triangleleft_{0j'} v(d'_{0,j}) $$

As done previously we are going to define a $\delta$ which is different from 0, and show that constraints in $(E, D)$ are satisfied while going forward of $\delta$ units of time from $w$.

Let

$$ t_0 = \max_{x \in \mathcal{X}} \{0, -\text{frac}(w(x)) - \text{frac}(v(d'_{0,x}))\} $$

and

$$ t_1 = \min_{x \in \mathcal{X}} \{\text{frac}(v(d'_{x,0})) - \text{frac}(w(x))\}. $$

We prove that $t_1 \le t_0$.

for any clock $i$ we have that $D_{i,0} = (\text{frac}(p), \le)$ and $D_{i,0} = (-\text{frac}(p), \le)$ i. e., $d_{0,i} = -d_{i,0}$ for some $p$, hence $-\text{frac}(w(x_i)) - v(d_{0,i}) = -\text{frac}(w(x_i)) + v(d_{i,0})$.

By definition of $TE_<$ applied to $(E, D)$, we have that $D'_{0,i} = D_{0,i} + (0, <)$. In order to respect the constraint $-\text{frac}(w(x_i)) - \delta \triangleleft_{0i'} v(d'_{0,i})$ which is, as $\triangleleft_{0i'} = <$, $-\text{frac}(w(x_i)) - \delta < v(d'_{0,i})$, we have to find a $\delta > 0$.

In order to find an upper bound for $\delta$, we are going to prove that $t_1 > 0$. From Definition 3.6 (2) we have in $(E, D)$ that for any clocks $i, j$ $D_{j,0} \le D_{j,i} + D_{i,0}$. Let $x_i \in \text{LFP}_{R_p}(D)$. From Definition 3.6 (1), we have that $D_{i,0} \le (1, <)$. This gives that $D_{j,i} + D_{i,0} \le D_{j,i} + (1, <)$.

By definition of $TE_<$ applied to $(E, D)$, we have that $D'_{j,0} = D_{j,i} + (1, <)$. Hence we have $D_{j,0} \le D'_{j,0}$.

Now as $\text{frac}(w(x_i)) \triangleleft_{i0} v(d_{i,0})$ we can write $\text{frac}(w(x_i)) \triangleleft_{i0'} v(d'_{i,0})$ and then $0 \triangleleft_{i0'} v(d'_{i,0}) - \text{frac}(w(x_i))$ where $\triangleleft_{i0'} = <$, which prove our result.

We define $\delta = \frac{t_1}{2}$, therefore $t_0 < \delta < t_1$. Now for all clock $x_j$, we obtain two results. First we have

$$ -\text{frac}(w(x_j)) - \delta < -\text{frac}(w(x_i)) - t_1 \triangleleft_{0j'} -\text{frac}(w(x_j)) + \text{frac}(w(x_i)) + v(d'_{0,j}) = v(d'_{0,j}) $$
which is $-v(d'_{0,j}) \triangleleft_0 j \frac{\mathrm{frac}(w(x_j))}{\mathrm{frac}(w(x_j))} + \delta$ as $\triangleleft_0 j' = <$.

Secondary we have

$$ \frac{\mathrm{frac}(w(x_j))}{\mathrm{frac}(w(x_j))} + \delta < \frac{\mathrm{frac}(w(x_j))}{\mathrm{frac}(w(x_j))} + t_0 \triangleleft_{j_0'} \frac{\mathrm{frac}(w(x_j))}{\mathrm{frac}(w(x_j))} - \frac{\mathrm{frac}(w(x_j))}{\mathrm{frac}(w(x_j))} + v(d'_{j,0}) = v(d'_{j,0}) $$

which is $\frac{\mathrm{frac}(w(x_j))}{\mathrm{frac}(w(x_j))} + \delta \triangleleft_0 j_0 v(d'_{j,0})$ as $\triangleleft_0 j' = <$.

Now we prove that constraints defined in $(E', D')$ on differences of clocks are also satisfied by going forward of $\delta$ units of time from $w$

Recall that in $(E', D')$ from the definition of Algorithm 2 we have for all clock $x_j$,

$$ D'_{j,i} = D_{j,i} \quad \text{and} \quad D'_{i,j} = D_{i,j}. $$

Since we already treated the case whether $i$ or $j$ are 0, now suppose $i, j$ are both different from 0. We have that $\frac{\mathrm{frac}(w(x_j))}{\mathrm{frac}(w(x_j))} - \frac{\mathrm{frac}(w(x_i))}{\mathrm{frac}(w(x_i))} \triangleleft_{ji} v(d_{j,i}) = v(d'_{j,i})$, and therefore as $\triangleleft_{ji'} = \triangleleft_{ji}$,

$$ \frac{\mathrm{frac}(w(x_j))}{\mathrm{frac}(w(x_j))} + \delta - \frac{\mathrm{frac}(w(x_i))}{\mathrm{frac}(w(x_i))} - \delta \triangleleft_{ji'} v(d'_{j,i}). $$

We also have that $\frac{\mathrm{frac}(w(x_i))}{\mathrm{frac}(w(x_i))} - \frac{\mathrm{frac}(w(x_j))}{\mathrm{frac}(w(x_j))} \triangleleft_{ij} v(d_{i,j}) = v(d'_{i,j})$, therefore as $\triangleleft_{ij'} = \triangleleft_{ij}$,

$$ \frac{\mathrm{frac}(w(x_i))}{\mathrm{frac}(w(x_i))} + \delta - \frac{\mathrm{frac}(w(x_j))}{\mathrm{frac}(w(x_j))} - \delta \triangleleft_{ij'} v(d'_{i,j}). $$

Finally, we define $w' = w + \delta$ and $w' \in (E', v(D'))$.

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

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

## APPENDIX I. PROOF OF LEMMA 4.12

**Lemma 4.12 (recalled).** Let $(E, D)$ be a p-PDBM for $R_p$ and $v \in R_p$. Let $g$ be a non-parametric guard. If $v \in \mathrm{guard}_\forall(g, E, D)$, then for all $v' \in R_p$, $v' \in \mathrm{guard}_\forall(g, E, D)$.

*Proof.* Our idea is to define a clock region “larger” than our p-PDBM (following Definition 2.3) and show that, even for this (larger) clock region, either all clock valuations satisfy the guard—or none does.

**Definition 1.1.** Let $R_p$ be a parameter region, $v \in R_p$. Let $(E, D)$ be a p-PDBM for $R_p$. We define the clock region containing $(E, v(D))$, denoted by $[(E, v(D))]_{R_p}$, as follows: for all $w \in [(E, v(D))]_{R_p}$, for all clocks $x_i, x_j$,

* if $E_{x_i} < K, \lfloor w(x_i) \rfloor = E_{x_i}$, else if $E_{x_i} = \infty, w(x_i) \ge K$;

* if $(0, \le) < D_{i,j}$ is valid for $R_p$ and $E_{x_i} < K, \frac{\mathrm{frac}(w(x_j))}{\mathrm{frac}(w(x_j))} < \frac{\mathrm{frac}(w(x_i))}{\mathrm{frac}(w(x_i))}$;

* if $(0, \le) = D_{i,j}$ is valid for $R_p$ and $E_{x_i} < K, \frac{\mathrm{frac}(w(x_j))}{\mathrm{frac}(w(x_j))} = \frac{\mathrm{frac}(w(x_i))}{\mathrm{frac}(w(x_i))}$;

* if $D_{i,0} = D_{0,i} = (0, \le)$ and $E_{x_i} < K, \frac{\mathrm{frac}(w(x_i))}{\mathrm{frac}(w(x_i))} = 0$;

* if $D_{i,0} \ne (0, \le), D_{0,i} \ne (0, \le)$ and $E_{x_i} < K, \frac{\mathrm{frac}(w(x_i))}{\mathrm{frac}(w(x_i))} \ne 0$.

**Claim 1.2.** Let $(E, D)$ be a p-PDBM for $R_p$ and $v \in R_p$. We have $(E, v(D)) \subseteq [(E, v(D))]_{R_p}$.

*Proof.* Clock regions of Definition 2.3 define constraints on clocks of the form $0 = \frac{\mathrm{frac}(x)}{\mathrm{frac}(x)}$, $0 < \frac{\mathrm{frac}(x)}{\mathrm{frac}(x)} < 1$, $0 = \frac{\mathrm{frac}(x)}{\mathrm{frac}(x)} - \frac{\mathrm{frac}(y)}{\mathrm{frac}(y)}$ and $0 < \frac{\mathrm{frac}(x)}{\mathrm{frac}(x)} - \frac{\mathrm{frac}(y)}{\mathrm{frac}(y)} < 1$ for some $x, y$, and $\lfloor x \rfloor = k$ for some integer $k$. Let $(E, D)$ be a p-PDBM for $R_p$ and $v \in R_p$. It defines constraints

$$ \bigwedge_{i,j \in [0,H]^2} \frac{\mathrm{frac}(x_i) - \mathrm{frac}(x_j)}{\mathrm{frac}(x_j) - \mathrm{frac}(x_i)} \triangleleft_{i,j} v(d_{i,j}) \quad \wedge \quad \bigwedge_{i \in [1,H]} \lfloor x_i \rfloor = E_i. $$
Clearly, if $w \in (E, v(D))$ satisfies $\lfloor x_i \rfloor = E_i$ then it satisfies the same constraint defined in $[(E, v(D))]_{R_c}$.

Consider the constraints $frac(x_i) - frac(x_j) <_{i,j} v(d_{i,j})$ and $frac(x_j) - frac(x_i) <_{j,i} v(d_{j,i})$.

* Suppose $i, j$ are both different from 0. From Definition 3.5 (3) and Definition 3.6, either $d_{i,j} = d_{j,i}$ and then $<_{i,j} = \le = <_{j,i}$, then if $d_{i,j} = d_{j,i} = 0$ it satisfies the same constraint defined in $[(E, v(D))]_{R_c}$, or $d_{i,j}$ and $d_{j,i}$ are different from 0, as they are elements of $\mathcal{PLT}$ which are strictly smaller than 1, it satisfies either $0 < frac(x_i) - frac(x_j) < 1$ or $0 = frac(x_i) - frac(x_j)$ in $[(E, v(D))]_{R_c}$. Finally if $d_{i,j} \neq d_{j,i}$, then $<_{i,j} = \le = <_{j,i}$ and it satisfies $0 < frac(x_i) - frac(x_j) < 1$ in $[(E, v(D))]_{R_c}$.

* Suppose $i$ is different from 0 and $j = 0$. From Definition 3.5 (3) and Definition 3.6, either $d_{i,0} = d_{0,i}$ and then $<_{i,0} = \le = <_{0,i}$, then if $d_{i,0} = d_{0,i} = 0$ it satisfies the same constraint defined in $[(E, v(D))]_{R_c}$, or $d_{i,0}$ and $d_{0,i}$ are different from 0, as they are elements of $\mathcal{PLT}$ which are strictly smaller than 1, it satisfies either $0 < frac(x_i) < 1$ or $0 = frac(x_i)$ in $[(E, v(D))]_{R_c}$. Finally if $d_{i,0} \neq d_{0,i}$, then $<_{i,0} = \le = <_{0,i}$ and it satisfies $0 < frac(x_i) < 1$ in $[(E, v(D))]_{R_c}$.

* The case $j$ is different from 0 and $i = 0$ is similar.

* Suppose both $i, j$ are 0, the constraint is not taken into account as we have no $x_0$ in $[(E, v(D))]_{R_c}$.

Finally, we have that if $w \in (E, v(D))$ then $w \in [(E, v(D))]_{R_c}$. $\square$

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

Now we come back to the proof of the main lemma:

Let $(E, D)$ be a p-PDBM for $R_p$ and $v \in R_p$. It defines constraints

$$ \bigwedge_{i,j \in [0,H]^2} \frac{frac(x_i) - frac(x_j)}{<_{i,j}} v(d_{i,j}) \wedge \bigwedge_{i \in [1,H]} \lfloor x_i \rfloor = E_i. $$

Moreover, let $g$ be a non-parametric guard. It defines constraints for a finite number of integer constants $k_i$ with $i \in I \subseteq [1, H]$

$$ \bigwedge_{i \in I} \frac{frac(x_i)}{\le 0} \wedge \bigwedge_{i \in I} -frac(x_i) \le 0 \wedge \bigwedge_{i \in I} \lfloor x_i \rfloor \succ k_i. $$

The intersection between the two is given by the conjunction of those constraints. We project this intersection on parameter variables (by elimination of clock variables) and we prove that the intersection does not create new constraints on parameters different from those we already have in $(E, v(D))$ (and therefore in $R_p$). For some set of clocks $I \subseteq [1, H]$ and $i \in I$, suppose we have the constraints $frac(x_i) \le 0$ and $-frac(x_i) \le 0$ in $g$. When eliminating $x_i$ in any constraint of the form $frac(x_i) - frac(x_j) <_{i,j} v(d_{i,j})$, it is clear that we proceed on $\mathcal{PLT}$ to the operation $(0, \le) + (d_{i,j}, <_{i,j}) = (0 + d_{i,j}, \le \oplus <_{i,j}) = (d_{i,j}, <_{i,j})$. The same way on any constraint of the form $frac(x_i) <_{i,0} v(d_{i,0})$, eliminating $x_i$ gives the constraint $(0, \le) + (d_{i,0}, <_{i,0}) = (d_{i,0}, <_{i,0})$. Hence it does not create new inequalities not belonging to $R_p$.

Now suppose $v \in \text{guard}_\forall(g, E, D)$. We have that all $w \in (E, v(D))$ satisfy $g$.

As no new constraints not in $\mathcal{PLT}$ have been created, all $v' \in R_p$ respect the same constraints on their fractional part and integer part as $v$ and therefore, $(E, v'(D))$ is contained in the same clock region as $(E, v(D))$ is, i. e., $[(E, v(D))]_{R_c} = [(E, v'(D))]_{R_c}$. Finally, $v' \in \text{guard}_\forall(g, E, D)$. $\square$

<figure><img src="image_26.png" /></figure>
## APPENDIX J. PROOF OF LEMMA 4.13

**Lemma 4.13 (recalled).** Let $(E, D)$ be a p-PDBM for $R_p$ and $v \in R_p$. Let $g$ be a parametric guard. If $v \in p-guard_\exists(g, E, D)$, then for all $v' \in R_p$, $v' \in p-guard_\exists(g, E, D)$.

*Proof.* Let $(E, D)$ be a p-PDBM for $R_p$ and $v \in R_p$. Let $g$ be a parametric guard and suppose $v \in p-guard_\exists(g, E, D)$. After applying a projection on parameters, we obtain constraints on elements of $\mathcal{PLT}$. By hypothesis, all these constraints are satisfied by $v$. Suppose $v' \in R_p$. By definition of our parameter regions, and since $v$ and $v'$ both belong to $R_p$, $v'$ satisfies the same constraints on elements of $\mathcal{PLT}$. Therefore, the same constraints is satisfied by $v'$ and $v' \in p-guard_\exists(g, E, D)$. $\square$

## APPENDIX K. PROOF OF PROPOSITION 6.1

**Proposition 6.1 (recalled).** Let $R_p$ be a parameter region. Let $\mathcal{A}$ be an R-U2P-PTA and $\mathcal{R}(\mathcal{A})$ its parametric region automaton over $R_p$. There is a run $\sigma : (\ell_0, (E_0, D_0)) \xrightarrow{e_0} (\ell_1, (E_1, D_1)) \xrightarrow{e_1} \dots (\ell_{f-1}, (E_{f-1}, D_{f-1})) \xrightarrow{e_{f-1}} (\ell_f, (E_f, D_f))$ in $\mathcal{R}(\mathcal{A})$ iff for all $v \in R_p$ there is a run $\rho : (\ell_0, w_0) \xrightarrow{e_0} (\ell_1, w_1) \xrightarrow{e_1} \dots (\ell_{f-1}, w_{f-1}) \xrightarrow{e_{f-1}} (\ell_f, w_f)$ in $v(\mathcal{A})$ s.t. for all $0 \le i \le f$, $w_i \in (E_i, v(D_i))$.

*Proof.* ⇌ By induction on the length of the run.

Let $v \in R_p$. As the basis for the induction, in the initial location $(\ell_0, \{0\}^H)$ the only valuation is reachable by an empty run of $v(\mathcal{A})$. Moreover $\{0\}^H \in (E_0, v(D_0))$ the initial p-PDBM containing only 0. Therefore the initial location $(\ell_0, (E_0, v(D_0)))$ is reachable by an empty run of $\mathcal{R}(\mathcal{A})$.

For the induction step, suppose for all $v$, there is run in $v(\mathcal{A})$ of length $f-1$ we have our result.

Let $v \in R_p$ and $\rho = (\ell_0, w_0) \xrightarrow{e_0} \dots \xrightarrow{e_{f-2}} (\ell_{f-1}, w_{f-1}) \xrightarrow{e_{f-1}} (\ell_f, w_f)$ be a run of $v(\mathcal{A})$ of length $f$. By induction hypothesis, there is a run $\sigma = (\ell_0, (E_0, D_0)) \xrightarrow{e_0} \dots \xrightarrow{e_{f-2}} (\ell_{f-1}, (E_{f-1}, D_{f-1}))$ in $\mathcal{R}(\mathcal{A})$ and for all $0 \le i \le f-1$, $w_i \in (E_i, v(D_i))$.

Consider $e_{f-1}$. By Definition 5.1 of the parametric region automaton, it is also in its set of edges $\zeta'$. Three cases show up:

- If $e_{f-1} = (\ell_{f-1}, a, g, u_{np}, \ell_f)$ contains no parametric guard nor parametric update. Using Definition 2.2 there is a delay $\delta$ (possibly 0) s.t. $(\ell_{f-1}, w_{f-1}) \xrightarrow{\delta} (\ell_{f-1}w'_{f-1}) \xrightarrow{e_{f-1}} (\ell_f, w_f)$ where $w'_{f-1} \models g$ and $w_f = [w'_{f-1}]_{u_{np}}$. As $w_{f-1} \in (E_{f-1}, v(D_{f-1}))$ there is $(E'_{f-1}, D'_{f-1}) \in \text{Succ}((E_{f-1}, D_{f-1}))$ s.t. from Proposition 4.11 we have $w'_{f-1} \in (E'_{f-1}, v(D'_{f-1}))$. As $w'_{f-1} \models g$ by construction of our p-PDBMs (see Section 4.4) any other clock valuation belonging to $(E'_{f-1}, v(D'_{f-1}))$ satisfies $g$. Therefore $v \in \text{guard}_\forall(g, E'_{f-1}, D'_{f-1})$ and from Lemma 4.12, $R_p \subseteq \text{guard}_\forall(g, E'_{f-1}, D'_{f-1})$. Now, as $w_f = [w'_{f-1}]_{u_{np}}$ consider the open-p-PDBM $(E_f, D_f) = \text{update}((E'_{f-1}, D'_{f-1}), u_{np})$; from Lemma 4.4 we have $w_f \in (E_f, v(D_f))$. Finally there is an edge

$$ (\ell_{f-1}, (E_{f-1}, D_{f-1})) \xrightarrow{e_{f-1}} (\ell_f, (E_f, D_f)). $$
- If $e_{f-1} = \langle \ell_{f-1}, a, g, u, \ell_f \rangle$ contains a parametric guard and a parametric update. Using Definition 2.2 there is a delay $\delta$ (possibly 0) s.t. $(\ell_{f-1}, w_{f-1}) \stackrel{\delta}{\mapsto} (\ell_{f-1}, w'_{f-1}) \stackrel{e_{f-1}}{\mapsto} (\ell_f, w_f)$ where $w'_{f-1} \models v(g)$ and $w_f = [w'_{f-1}]_{v(u)}$. As $w_{f-1} \in (E_{f-1}, v(D_{f-1}))$ there is $(E'_{f-1}, D'_{f-1}) \in \text{Succ}((E_{f-1}, D_{f-1}))$ s.t. from Proposition 4.11 we have $w'_{f-1} \in (E'_{f-1}, v(D'_{f-1}))$. As $w'_{f-1} \models v(g)$, $v \in \text{p-guard}_\exists(g, E'_{f-1}, D'_{f-1})$ and from Lemma 4.13, $R_p \subseteq \text{p-guard}_\exists(g, E'_{f-1}, D'_{f-1})$. Now, as $w_f = [w'_{f-1}]_{v(u)}$ consider the **point-p-PDBM** $(E_f, D_f) = \overline{\text{update}}((E'_{f-1}, D'_{f-1}), u)$; $(E_f, v(D_f))$ contains only one clock valuation, precisely defined by the fully parametric update $v(u)$ so we have $w_f \in (E_f, v(D_f))$. Finally there is an edge $(\ell_{f-1}, (E_{f-1}, D_{f-1})) \stackrel{e_{f-1}}{\mapsto} (\ell_f, (E_f, D_f))$.

- The case where $e_{f-1}$ contains a non parametric guard and a parametric update is similar to the previous one.

Finally, there is a run $\sigma' = \sigma \stackrel{e_{f-1}}{\mapsto} (\ell_f, (E_f, D_f))$ of length $f$ in $\mathcal{R}(\mathcal{A})$ s.t. for all $0 \le i \le f$, $w_i \in (E_i, v(D_i))$.

⇒ By induction on the length of the run.

Let $v \in R_p$. As the basis for the induction, the initial location $(\ell_0, (E_0, v(D_0)))$ is reachable by an empty run of $\mathcal{R}(\mathcal{A})$. Moreover, as $\{0\}^H \in (E_0, v(D_0))$, the initial location $(\ell_0, \{0\}^H)$ is reachable by an empty run of $v(\mathcal{A})$.

For the induction step, suppose it is true for all run in $\mathcal{R}(\mathcal{A})$ of length $f-1$.

Let $v \in R_p$ and $\sigma = (\ell_0, (E_0, D_0)) \stackrel{e_0}{\longrightarrow} \dots \stackrel{e_{f-2}}{\longrightarrow} (\ell_{f-1}, (E_{f-1}, D_{f-1})) \stackrel{e_{f-1}}{\longrightarrow} (\ell_f, (E_f, D_f))$ be a run of $\mathcal{R}(\mathcal{A})$ of length $f$. Consider $e_{f-1}$. By Definition 5.1 of the parametric region automaton, it is also in the set of edges $\zeta$ of $\mathcal{A}$. Two cases show up:

- If $e_{f-1} = \langle \ell_{f-1}, a, g, u_{np}, \ell_f \rangle$ contains no parametric guard nor parametric update. By induction hypothesis, there is a run $\rho = (\ell_0, w_0) \stackrel{e_0}{\longrightarrow} \dots \stackrel{e_{f-2}}{\longrightarrow} (\ell_{f-1}, w_{f-1})$ of $v(\mathcal{A})$ of length $f-1$ s.t. for all $0 \le i \le f-1$, $w_i \in (E_i, v(D_i))$. Using Definition 5.1 there is $(E'_{f-1}, D'_{f-1}) \in \text{Succ}((E_{f-1}, D_{f-1})), R_p \subseteq \text{guard}_\forall(g, E'_{f-1}, D'_{f-1})$ and $(E_f, D_f) = \text{update}((E'_{f-1}, D'_{f-1}), u_{np})$. From Proposition 4.11 we have $w'_{f-1} \in (E'_{f-1}, v(D'_{f-1}))$ and a delay $\delta$ s.t. $w'_{f-1} = w_{f-1} + \delta$. As $R_p \subseteq \text{guard}_\forall(g, E'_{f-1}, D'_{f-1})$ from Lemma 4.12 we have $v \in \text{guard}_\forall(g, E'_{f-1}, D'_{f-1})$ and $w'_{f-1} \models g$. Moreover, since $(E_f, D_f) = \text{update}((E'_{f-1}, D'_{f-1}), u_{np})$, we define $w_f = [w'_{f-1}]_{u_{np}}$ and therefore from Lemma 4.4, $w_f \in (E_f, v(D_f))$. Finally there is an edge $(\ell_{f-1}, w_{f-1}) \stackrel{e_{f-1}}{\longrightarrow} (\ell_f, w_f)$ and a run $\rho' = \rho \stackrel{e_{f-1}}{\longrightarrow} (\ell_f, w_f)$ in $v(\mathcal{A})$ of length $f$ s.t. for all $0 \le i \le f$, $w_i \in (E_i, v(D_i))$.

- If $e_{f-1} = \langle \ell_{f-1}, a, g, u, \ell_f \rangle$ contains a parametric guard and a parametric update. Using Definition 5.1 there is $(E'_{f-1}, D'_{f-1}) \in \text{Succ}((E_{f-1}, D_{f-1})), R_p \subseteq \text{p-guard}_\exists(g, E'_{f-1}, D'_{f-1})$ and $(E_f, D_f) = \overline{\text{update}}((E'_{f-1}, D'_{f-1}), u)$. From Lemma 4.13 we can take $w'_{f-1} \in (E'_{f-1}, v(D'_{f-1}))$ s.t. $w'_{f-1} \models v(g)$. Let $w_f = [w'_{f-1}]_{v(u)}$. Clearly, $(E_f, D_f) = \overline{\text{update}}((E'_{f-1}, D'_{f-1}), u)$ is a **point-p-PDBM**; as $(E_f, v(D_f))$ contains only one clock valuation precisely defined by the fully parametric update $v(u)$, we have $w_f \in (E_f, v(D_f))$. From Proposition 4.11 as $w'_{f-1} \in (E'_{f-1}, v(D'_{f-1}))$ there is a delay $\delta$ and a $w_{f-1} \in (E_{f-1}, v(D_{f-1}))$ s.t. $w'_{f-1} = w_{f-1} + \delta$. Using the induction hypothesis, there is a run $\rho = (\ell_0, w_0) \stackrel{e_0}{\longrightarrow} \dots \stackrel{e_{f-2}}{\longrightarrow} (\ell_{f-1}, w_{f-1})$ of $v(\mathcal{A})$ of length $f-1$ s.t. for all $0 \le i \le f-1$,
$w_i \in (E_i, v(D_i))$. Finally there is an edge $(\ell_{f-1}, w_{f-1}) \xrightarrow{e_{f-1}} (\ell_f, w_f)$ and a run $\rho' = \rho \xrightarrow{e_{f-1}} (\ell_f, w_f)$ in $v(\mathcal{A})$ of length $f$ s.t. for all $0 \le i \le f$, $w_i \in (E_i, v(D_i))$.

- The case where $e_{f-1}$ contains a non parametric guard and a parametric update is similar to the previous one. $\square$