1
$\begingroup$

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?

$\endgroup$

1 Answer 1

3
$\begingroup$

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

$\endgroup$
2
  • $\begingroup$ 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 ? $\endgroup$
    – whoisit
    Sep 26, 2022 at 12:53
  • $\begingroup$ You can try the introduction talks by Patricia Bouyer: 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. $\endgroup$
    – Shaull
    Sep 26, 2022 at 13:23

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.