of ${\mathfrak{R}}(A)$ are labeled by the transition actions and they correspond to the actual transitions that occur in the runs on $A$.

The *augmented region automaton*, denoted ${\mathfrak{R}^t}(A)$, is defined as in [@R19]. First, we add to $A$ a clock $t$ that measures absolute time, is never reset to $0$ and does not affect the runs and timed traced of $A$. Secondly, we want to construct ${\mathfrak{R}^t}(A)$ in a way that keeps track of absolute time and regain much of the information that is lost when passing from the timed automaton $A$ to the regular region automaton ${\mathfrak{R}}(A)$. But since $t$ does not appear in the transition guards of $A$, we need not know the exact value of the integral part of $t$ but just how much time passes between two consecutive transitions. Thus, we assign $t$ in ${\mathfrak{R}^t}(A)$ only two time-regions: $\{0\}$ and $(0,1)$. However, in order to keep track of the absolute time that passes, each edge is assigned a ’weight’, the time difference in the integral part of $t$ between the target and the source regions. The ordering among the fractional part of the clocks does, however, take that of $t$ into account. Overall, the number of 