A game approach to determinize timed automata

Nathalie Bertrand (1) , Amélie Stainer (1) , Thierry Jéron (1) , Moez Krichen (2)

1 VERTECS - Verification models and techniques applied to testing and control of reactive systems
2 ISIMS - Institut Supérieur d'Informatique et de Multimédia de Sfax

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 determinization procedure of [BBBB09a] and more precise than the approximation algorithm of [KT09]. 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.

Domaines: Informatique et langage [cs.CL]; Théorie et langage formel [cs.FL]

Nathalie Bertrand, Amélie Stainer, Thierry Jéron, Moez Krichen. A game approach to determinize timed automata. [Research Report] RR-7381, INRIA. 2010. ⟨inria-00524830v2⟩