Skip to Main content Skip to Navigation
New interface
Reports (Research report)

A game approach to determinize timed automata

Abstract : 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.
Complete list of metadata

Cited literature [14 references]  Display  Hide  Download
Contributor : Nathalie Bertrand Connect in order to contact the contributor
Submitted on : Monday, October 25, 2010 - 11:07:46 AM
Last modification on : Thursday, October 27, 2022 - 4:02:37 AM
Long-term archiving on: : Friday, December 2, 2016 - 3:01:09 AM


Files produced by the author(s)


  • HAL Id : inria-00524830, version 2


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⟩



Record views


Files downloads