<p>It's not exactly about obtaining an &quot;equivalent&quot; DFA, but rather an NFA that has an equivalent reachability problem.
The main idea is to consider what information you actually need to know about the clocks. For example, if you only have one clock <span class="math-container">$x$</span>, and guards that involve the numbers <span class="math-container">$1$</span> and <span class="math-container">$3$</span>, then any value beyond <span class="math-container">$3$</span> is clearly equivalent, in the sense that the automaton doesn't distinguish between e.g., <span class="math-container">$5$</span> and <span class="math-container">$17$</span>.
The value <span class="math-container">$2$</span>, however, may be of interest, as it can influence the run using the interaction of <span class="math-container">$3$</span> and <span class="math-container">$1$</span>.</p>
<p>So in this case, it's enough to track the value of the clock up to the nearest integer, and up to the value <span class="math-container">$3$</span>.</p>
<p>If you have multiple clocks, it seems that it is enough to track all clocks up to the nearest integer, which would give sort of &quot;cube&quot; zones.
However, it turns out that you also need to track the order of the clocks, e.g., <span class="math-container">$x&lt;y,x=y,x&gt;y$</span> are all distinct regions.</p>
<p>Splitting all the clocks according to these regions gives the &quot;region construction&quot;. I don't provide details here, but you can look in e.g.,
<a href="https://www.researchgate.net/publication/2399954_Timed_Automata" rel="nofollow noreferrer">https://www.researchgate.net/publication/2399954_Timed_Automata</a></p>

CC BY-SA 4.0
2022-09-26T12:53:39.843Z
The publication pdf is not available online and the author has not replied (and is unlikely to reply) to my mail. Is there any other *easy-to-understand* reference ?
whoisit
CC BY-SA 4.0
2022-09-26T13:23:01.687Z
You can try the introduction talks by Patricia Bouyer: http://www.lsv.fr/~bouyer/files/movep14.pdf
Also, if you're affiliated with an academic institute, you can probably get access to the book, or ask the library to purchase it.
Shaull
CC BY-SA 4.0
2022-09-25T14:10:49.633Z
2022-09-25T14:10:49.633Z
Shaull
<p>I've recently started self-learning timed automata.</p>
<p>There's this theorem in there that a timed automaton can be converted to a DFA using a &quot;region&quot; construction. I've looked up references on this, which appear on first google searches; but the construction is thoroughly confusing and everyone offers different definitions.</p>
<p>Can anyone please explain to me what this &quot;region&quot; construction is (i.e. what are the states and transitions in the resulting DFA), or some easy-to-understand reference on it, and some simple example?</p>

<automata-theory><reductions><formal-methods>
What is region construction in timed automata?
whoisit
# What is region construction in timed automata?

(Asked by: username_0 on 2022-09-25)

I've recently started self-learning timed automata.

There's this theorem in there that a timed automaton can be converted to a DFA using a "region" construction. I've looked up references on this, which appear on first google searches; but the construction is thoroughly confusing and everyone offers different definitions.

Can anyone please explain to me what this "region" construction is (i.e. what are the states and transitions in the resulting DFA), or some easy-to-understand reference on it, and some simple example?

**Tags:** automata-theory, reductions, formal-methods


---

## 1 answers

### Answer by username_1 on 2022-09-25. Score: 3 | Accepted answer

It's not exactly about obtaining an "equivalent" DFA, but rather an NFA that has an equivalent reachability problem.
The main idea is to consider what information you actually need to know about the clocks. For example, if you only have one clock $x$, and guards that involve the numbers $1$ and $3$, then any value beyond $3$ is clearly equivalent, in the sense that the automaton doesn't distinguish between e.g., $5$ and $17$.
The value $2$, however, may be of interest, as it can influence the run using the interaction of $3$ and $1$.

So in this case, it's enough to track the value of the clock up to the nearest integer, and up to the value $3$.

If you have multiple clocks, it seems that it is enough to track all clocks up to the nearest integer, which would give sort of "cube" zones.
However, it turns out that you also need to track the order of the clocks, e.g., $xy$ are all distinct regions.

Splitting all the clocks according to these regions gives the "region construction". I don't provide details here, but you can look in e.g.,
<https://www.researchgate.net/publication/2399954_Timed_Automata>

> **Comments:**
> **username_0**: The publication pdf is not available online and the author has not replied (and is unlikely to reply) to my mail. Is there any other *easy-to-understand* reference ?  
> **username_1**: You can try the introduction talks by Patricia Bouyer: http://www.lsv.fr/~bouyer/files/movep14.pdf Also, if you're affiliated with an academic institute, you can probably get access to the book, or ask the library to purchase it.  

---

