is not clear to us whether this problem is decidable in general, but for a (perhaps) restricted version of it we construct an algorithm that solves it.

Timed Automaton {#sec:ta}
===============

A timed automaton is an abstract model of temporal behavior of real-time systems. It is a finite automaton with *locations* and *transitions* between them, extended with a finite set of (continuous) clocks defined over ${\mathbb{R}_{\geq 0}}$. A transition at time $t$ can occur only if the condition expressed as a *transition guard* is satisfied at $t$. A transition guard is a conjunction of constraints of the form ${c}\sim n$, where ${c}$ is a clock, $\sim \ \in \{<,\leq, =,\geq, >\}$ and $n \in {\mathbb{N}_0}= {\mathbb{N}}\cup \{0\}$. Each transition is labeled by some *action* $a \in {\Sigma}$ and some of the clocks may be reset to zero. In ${\mathrm{NTA}}$, the class of non-deterministic timed automata, and unlike deterministic TAs, it may occur that two transitions from the same location $q$ can be taken at the same time and with the same action but to two different locations $q'$ and $q''$.

\[def:ntaeps\] A *non-deterministic timed automaton* $A \in {\mathrm{NTA}}$ is a tuple $({\mathcal{Q}}, q_0, {\mathcal{F}}, {\Sigma}, {\mathcal{C}},
{\mathcal{T}})$, where:

1.  ${\mathcal{Q}}$ 