What is region construction in timed automata?

Question

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?

Answer 1

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., $x<y,x=y,x>y$ 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