Assume-Guarantee Verification for Probabilistic Systems

Abstract : We present a compositional verification technique for systems that exhibit both probabilistic and nondeterministic behaviour. We adopt an assume-guarantee approach to verification, where both the assumptions made about system components and the guarantees that they provide are regular safety properties, represented by finite automata. Unlike previous proposals for assume-guarantee reasoning about probabilistic systems, our approach does not require that components interact in a fully synchronous fashion. In addition, the compositional verification method is efficient and fully automated, based on a reduction to the problem of multi-objective probabilistic model checking. We present asymmetric and circular assume-guarantee rules, and show how they can be adapted to form quantitative queries, yielding lower and upper bounds on the actual probabilities that a property is satisfied. Our techniques have been implemented and applied to several large case studies, including instances where conventional probabilistic verification is infeasible.
Type de document :
Communication dans un congrès
TACAS 2010 : 16th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, Mar 2010, Paphos, Cyprus. Springer, 2010
Liste complète des métadonnées

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

https://hal.inria.fr/inria-00458058
Contributeur : Brigitte Briot <>
Soumis le : vendredi 19 février 2010 - 10:19:25
Dernière modification le : vendredi 26 février 2010 - 13:55:14
Document(s) archivé(s) le : jeudi 18 octobre 2012 - 15:30:17

Fichier

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

Identifiants

  • HAL Id : inria-00458058, version 1

Collections

Citation

Marta Kwiatkowska, Gethin Norman, David Parker, Hongyang Qu. Assume-Guarantee Verification for Probabilistic Systems. TACAS 2010 : 16th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, Mar 2010, Paphos, Cyprus. Springer, 2010. 〈inria-00458058〉

Partager

Métriques

Consultations de la notice

158

Téléchargements de fichiers

38