be ’closed under digitization’ and the specification should be ’closed under inverse digitization’ in order to be able to reduce the language inclusion problem from the continuous world to the discretized one. In [@irta] the authors construct TAs with reset only on integral time and demonstrate the decidability of the language inclusion problem ${\mathfrak{L}}(A) \subseteq {\mathfrak{L}}(B)$ in case $B$ is an integer reset TA. In this paper we go further with this approach. The idea is to work in the setting of discretized time, but without restricting or modifying the definition of a TA. The discretization is over intervals which are smaller than 1 time unit so that although we work in the discretized setting we are able to check for exact occurrence of events also outside integral time. For this matter we construct discretized TAs that enable effective comparison of the languages of the original TAs. The discretized TA stays within a distance of $\frac{1}{6}$ time units from the original TA (the distance can, in fact, be as small as we like, in the cost of complexity, but that won’t improve our knowledge about the inclusion of the languages of the original automata), a goal that is achieved through 