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.
Type de document :
Rapport
[Research Report] RR-7381, INRIA. 2010
Liste complète des métadonnées

Littérature citée [14 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/inria-00524830
Contributeur : Nathalie Bertrand <>
Soumis le : lundi 25 octobre 2010 - 11:07:46
Dernière modification le : mercredi 11 avril 2018 - 01:55:52
Document(s) archivé(s) le : vendredi 2 décembre 2016 - 03:01:09

Fichier

RR-7381.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • 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〉

Partager

Métriques

Consultations de la notice

516

Téléchargements de fichiers

149