Application of nominal sets to machine-independent characterization of timed languages

We introduce a variant of nominal sets that is well-suited for languages recognized by timed automata. We state and prove a machine-independent characterization of languages recognized by deterministic timed automata. Finally, in the setting of nominal sets we define a class of automata, called timed register automata, that extends timed automata and is effectively closed under minimization.