Stochastic Games for Verification of Probabilistic Timed Automata

Abstract : Probabilistic timed automata (PTAs) are used for formal modelling and verification of systems with probabilistic, nondeterministic and real-time behaviour. For non-probabilistic timed automata, forwards reachability is the analysis method of choice, since it can be implemented extremely efficiently. However, for PTAs, such techniques are only able to compute upper bounds on maximum reachability probabilities. In this paper, we propose a new approach to the analysis of PTAs using abstraction and stochastic games. We show how efficient forwards reachability techniques can be extended to yield both lower and upper bounds on maximum (and minimum) reachability probabilities. We also present abstraction-refinement techniques that are guaranteed to improve the precision of these probability bounds, providing a fully automatic method for computing the exact values. We have implemented these techniques and applied them to a set of large case studies. We show that, in comparison to alternative approaches to verifying PTAs, such as backwards reachability and digital clocks, our techniques exhibit superior performance and scalability.
Type de document :
Communication dans un congrès
Vaandrager, Frits W. 7th International Conference on Formal Modeling and Analysis of Timed Systems : FORMATS 2009, Sep 2009, Budapest, Hungary. Springer, 5813, pp.212-217, 2009, Lecture notes in computer science. 〈10.1007/978-3-642-04368-0_17〉
Liste complète des métadonnées

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

https://hal.inria.fr/inria-00457923
Contributeur : Brigitte Briot <>
Soumis le : jeudi 18 février 2010 - 16:51:50
Dernière modification le : vendredi 26 février 2010 - 14:09:14
Document(s) archivé(s) le : jeudi 18 octobre 2012 - 15:30:37

Fichier

formats09.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

Collections

Citation

Marta Kwiatkowska, Gethin Norman, David Parker. Stochastic Games for Verification of Probabilistic Timed Automata. Vaandrager, Frits W. 7th International Conference on Formal Modeling and Analysis of Timed Systems : FORMATS 2009, Sep 2009, Budapest, Hungary. Springer, 5813, pp.212-217, 2009, Lecture notes in computer science. 〈10.1007/978-3-642-04368-0_17〉. 〈inria-00457923〉

Partager

Métriques

Consultations de la notice

117

Téléchargements de fichiers

97