<p>An important step of developing the theory of timed automata is to reduce the question of reachability in the timed automata, which has infinitely-many states, to the question of reachability in an associated finite-state automaton constructed by grouping together clock valuations into so-called <strong>clock regions</strong>. To recall, we have a finite set <span class="math-container">$C$</span> whose elements we call <strong>clocks</strong>, and a <strong>clock valuation</strong> is then a function <span class="math-container">$\nu : C \to [0, \infty)$</span> which assigns every clock the elapsed amount of time that has progressed.</p>
<p>Note: We will write <span class="math-container">$\{r\}$</span> for the fractional part of a real number, so that <span class="math-container">$\{r\} = r - \lfloor r \rfloor$</span>.</p>
<p>We start by choosing a constant <span class="math-container">$M$</span> which is larger than any constant appearing on a guard or invariant condition in the timed automaton we are studying, then we introduce an equivalence relation by stating <span class="math-container">$\nu_1 \approx \nu_2$</span> if and only if the following conditions are satisfied:</p>
<ol>
<li><span class="math-container">$\nu_1(x) &gt; M$</span> if and only if <span class="math-container">$\nu_2(x) &gt; M$</span> for all <span class="math-container">$x \in C$</span></li>
<li>If <span class="math-container">$\nu_1(x) \le M$</span> then <span class="math-container">$\lfloor \nu_1(x) \rfloor = \lfloor \nu_2(x) \rfloor$</span></li>
<li>If <span class="math-container">$\nu_1(x) \le M$</span> then <span class="math-container">$\{\nu_1(x)\} = 0$</span> iff <span class="math-container">$\{\nu_2(x)\} = 0$</span>.</li>
<li>If <span class="math-container">$\nu_1(x) \le M$</span> and <span class="math-container">$\nu_1(y) \le M$</span> then <span class="math-container">$\{\nu_1(x)\} \le \{\nu_1(y)\}$</span> if and only if <span class="math-container">$\{\nu_2(x)\} \le \{\nu_2(y)\}$</span>.</li>
</ol>
<p>The idea is then to consider the equivalence classes <span class="math-container">$[\nu]$</span> of clock valuations under this equivalence relation, which are called <strong>regions</strong>.</p>
<p>In order for the theory to work, we need to show that clock equivalence induces a time-abstracted bisimulation on the timed automaton. The difficult step in establishing this, is to show the following Lemma.</p>
<p>Aside: Given a clock valuation <span class="math-container">$\nu$</span> alongside a number <span class="math-container">$c \in [0, \infty)$</span> define the clock valuation <span class="math-container">$\nu + c$</span> by setting <span class="math-container">$(\nu + c)(x) = \nu(x) + c$</span> for every <span class="math-container">$x \in C$</span>.</p>
<p><strong>Lemma:</strong> If <span class="math-container">$\nu_1 \approx \nu_2$</span> then for every <span class="math-container">$c_1 \in [0,\infty)$</span> there exists <span class="math-container">$c_2 \in [0,\infty)$</span> such that <span class="math-container">$\nu_1 + c_1 \approx \nu_2 + c_2$</span>.</p>
<p>My question is how to prove this lemma.</p>
<p>All chains of citations in the literature seem to take me back to page 17 of the paper &quot;Model-Checking in Dense Real-Time&quot; by Rajeev Alur and Costas Courcoubetis. However, I do not find the proof provided there to be clear at all.</p>
<p>It is easy to prove</p>
<p><strong>Lemma:</strong> If <span class="math-container">$\nu_1 \approx \nu_2$</span> then for every <span class="math-container">$c \in \mathbb{N}$</span> it follows that <span class="math-container">$\nu_1 + c \approx \nu_2 + c$</span>.</p>
<p>which allows us to reduce to the slightly more constrained problem</p>
<p><strong>Lemma:</strong> If <span class="math-container">$\nu_1 \approx \nu_2$</span> then for every <span class="math-container">$c_1 \in (0, 1)$</span> there exists <span class="math-container">$c_2 \in [0, \infty)$</span> such that <span class="math-container">$\nu_1 + c_1 \approx \nu_2 + c_2$</span>.</p>
<p>One can also show that whatever the choice of <span class="math-container">$c_2$</span>, it has to be in <span class="math-container">$[0, 1)$</span> in order to be correct.</p>
<p>I'm personally being led to the conjecture that the solution is to set
<span class="math-container">$$ \tau(\nu) := \sup \{ \epsilon \ge 0 \mid \nu + \epsilon \approx \nu \} $$</span>
and choose <span class="math-container">$c_2 = c_1 - \tau(\nu_1) + \tau(\nu_2)$</span>.</p>
<p>Edit: Shaull points out that this conjecture is false.</p>

CC BY-SA 4.0
2024-03-20T20:13:51.700Z
I don't think your approach with $\tau(v)$ can work. Take two clocks $x,y$, and set $v_1(x)=0.3, v_1(y)=0.9$ and $v_2(x)=0.4, v_2(y)=0.5$, then $\tau(v_1)=0.1$ and $\tau(v_2)=0.5$. Now take $c_1=0.6$, then $v_1+c_1=(0.9,1.5)$ ("lower triangle"). But $c_2=0.6-0.1+0.5=1$, so you'll get $v_2+c_2=(1.4,1.5)$ ("upper triangle").
I think the reason you didn't find a proof is because it's easier to see it visually than write the technical details. I'll see if I can find a clean way to write it. If so, I'll post an answer.
Shaull
CC BY-SA 4.0
2024-03-22T15:16:44.543Z
Ah, yes, \tau(\nu) definitely doesn't work. At least with 1, 2, or 3 clocks it's visually clear. But I feel like it's important to make sure we really have a formal proof, otherwise its a bit strange to build a theory for verifying timed programs in which we don't have a formal verification of the theory itself!
generic_logician
<automata-theory><model-checking><formal-methods><program-verification><temporal-logic>
How to prove clock equivalence is a time-abstracted bisimulation
generic_logician
# How to prove clock equivalence is a time-abstracted bisimulation

(Asked by: username_0 on 2024-03-12)

An important step of developing the theory of timed automata is to reduce the question of reachability in the timed automata, which has infinitely-many states, to the question of reachability in an associated finite-state automaton constructed by grouping together clock valuations into so-called **clock regions**. To recall, we have a finite set $C$ whose elements we call **clocks**, and a **clock valuation** is then a function $\nu : C \to [0, \infty)$ which assigns every clock the elapsed amount of time that has progressed.

Note: We will write $\{r\}$ for the fractional part of a real number, so that $\{r\} = r - \lfloor r \rfloor$.

We start by choosing a constant $M$ which is larger than any constant appearing on a guard or invariant condition in the timed automaton we are studying, then we introduce an equivalence relation by stating $\nu\_1 \approx \nu\_2$ if and only if the following conditions are satisfied:

1. $\nu\_1(x) > M$ if and only if $\nu\_2(x) > M$ for all $x \in C$
2. If $\nu\_1(x) \le M$ then $\lfloor \nu\_1(x) \rfloor = \lfloor \nu\_2(x) \rfloor$
3. If $\nu\_1(x) \le M$ then $\{\nu\_1(x)\} = 0$ iff $\{\nu\_2(x)\} = 0$.
4. If $\nu\_1(x) \le M$ and $\nu\_1(y) \le M$ then $\{\nu\_1(x)\} \le \{\nu\_1(y)\}$ if and only if $\{\nu\_2(x)\} \le \{\nu\_2(y)\}$.

The idea is then to consider the equivalence classes $[\nu]$ of clock valuations under this equivalence relation, which are called **regions**.

In order for the theory to work, we need to show that clock equivalence induces a time-abstracted bisimulation on the timed automaton. The difficult step in establishing this, is to show the following Lemma.

Aside: Given a clock valuation $\nu$ alongside a number $c \in [0, \infty)$ define the clock valuation $\nu + c$ by setting $(\nu + c)(x) = \nu(x) + c$ for every $x \in C$.

**Lemma:** If $\nu\_1 \approx \nu\_2$ then for every $c\_1 \in [0,\infty)$ there exists $c\_2 \in [0,\infty)$ such that $\nu\_1 + c\_1 \approx \nu\_2 + c\_2$.

My question is how to prove this lemma.

All chains of citations in the literature seem to take me back to page 17 of the paper "Model-Checking in Dense Real-Time" by Rajeev Alur and Costas Courcoubetis. However, I do not find the proof provided there to be clear at all.

It is easy to prove

**Lemma:** If $\nu\_1 \approx \nu\_2$ then for every $c \in \mathbb{N}$ it follows that $\nu\_1 + c \approx \nu\_2 + c$.

which allows us to reduce to the slightly more constrained problem

**Lemma:** If $\nu\_1 \approx \nu\_2$ then for every $c\_1 \in (0, 1)$ there exists $c\_2 \in [0, \infty)$ such that $\nu\_1 + c\_1 \approx \nu\_2 + c\_2$.

One can also show that whatever the choice of $c\_2$, it has to be in $[0, 1)$ in order to be correct.

I'm personally being led to the conjecture that the solution is to set
$$ \tau(\nu) := \sup \{ \epsilon \ge 0 \mid \nu + \epsilon \approx \nu \} $$
and choose $c\_2 = c\_1 - \tau(\nu\_1) + \tau(\nu\_2)$.

Edit: Shaull points out that this conjecture is false.

**Tags:** automata-theory, model-checking, formal-methods, program-verification, temporal-logic
> **Comments:**
> **username_1**: I don't think your approach with $\tau(v)$ can work. Take two clocks $x,y$, and set $v_1(x)=0.3, v_1(y)=0.9$ and $v_2(x)=0.4, v_2(y)=0.5$, then $\tau(v_1)=0.1$ and $\tau(v_2)=0.5$. Now take $c_1=0.6$, then $v_1+c_1=(0.9,1.5)$ ("lower triangle"). But $c_2=0.6-0.1+0.5=1$, so you'll get $v_2+c_2=(1.4,1.5)$ ("upper triangle"). I think the reason you didn't find a proof is because it's easier to see it visually than write the technical details. I'll see if I can find a clean way to write it. If so, I'll post an answer.  
> **username_0**: Ah, yes, \tau(\nu) definitely doesn't work. At least with 1, 2, or 3 clocks it's visually clear. But I feel like it's important to make sure we really have a formal proof, otherwise its a bit strange to build a theory for verifying timed programs in which we don't have a formal verification of the theory itself!  

---

## 0 answers

