Skip to Main content Skip to Navigation
Reports

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

https://hal.inria.fr/inria-00524830
Contributor : Nathalie Bertrand <>
Submitted on : Monday, October 25, 2010 - 11:07:46 AM
Last modification on : Tuesday, June 23, 2020 - 12:30:04 PM
Long-term archiving on: : Friday, December 2, 2016 - 3:01:09 AM

File

RR-7381.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : inria-00524830, version 2

Collections

Citation

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⟩

Share

Metrics

Record views

614

Files downloads

472