A game approach to determinize timed automata
Résumé
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.
Les automates temporisés sont classiquement utilisés pour modéliser des systèmes temps- réel. Leur déterminisation est un problème clef pour plusieurs problèmes de validation. Pourtant certains automates temporisés ne sont pas déterminisables et la déterminisabilité elle-même est indécidable. Dans cet article, nous proposons un algorithme qui, étant donné un automate temporisé, essaie de produire un automate déterministe équivalent, ou à défaut une surapproximation déterministe. Notre méthode améliore deux contributions récentes dans le domaine : elle est à la fois plus générale que la procédure de déterminisation existante et plus précise que l'algorithme d'approximation. De plus, nous expliquons comment étendre notre méthode pour traiter les invariants et les ε-transitions, et considérons également d'autres types d'approximation utiles : les sous-approximations et les combinaisons de sous- et sur- approximations.
Origine : Fichiers produits par l'(les) auteur(s)