location invariants in the definition of timed automata since they are more of a ’syntactic sugar’: the invariants of location $q$ are composed of upper bounds to the values of the clocks while being in $q$, but these constraints can be incorporated in the transition guards to $q$ (for the clocks that are not reset at the transitions) and in those transitions that emerge from $q$, thus not affecting ${\mathfrak{L}}(A)$.

Augmented Region Automaton {#sec:ARA}
==========================

Given a (finite) timed automaton $A$, the region automaton ${\mathfrak{R}}(A)$ [@ta] is a finite *discretized* version of $A$, such that time is abstracted and both automata define the same untimed language. Instead of looking at the clocks-space as a continuous space it is partitioned into regions. Suppose that the maximal integer appearing in the transition guards of $A$ is $M$, then we denote by $\top$ a value of a clock which is greater than $M$. The regions partition the space of clock valuations into equivalent classes, where two valuations belong to the same equivalent class if and only if they agree on the clocks with $\top$ value and on the integral parts and the order among the fractional parts of the other clocks. The edges 