%O Report 
%F rr7381
%A Bertrand, N.
%A Stainer, A.
%A Jéron, T.
%A Krichen, M.
%T A game approach to determinize timed automata
%N 7381
%I INRIA
%X Timed automata are frequently used to model real-time systems. Their determinization is a key issue for several validation problems. However, not all timed automata can be determinized, and determinizability itself is undecidable. In this paper, we propose a game-based algorithm which, given a timed automaton, tries to produce a language-equivalent deterministic timed automaton, otherwise a deterministic over-approximation. Our method subsumes two recent contributions: it is at once more general than the existing determinization procedure and more precise than the approximation algorithm. Moreover, we explain how to extend our method to deal with invariants and $\varepsilon$-transitions, and also consider other useful approximations: under-approximation, and combination of under- and over-approximations
%U http://hal.inria.fr/docs/00/52/48/30/PDF/RR-7381.pdf
%8 October
%D 2010