Compositional Verification of Probabilistic Systems using Learning

Abstract : We present a fully automated technique for compositional verification of probabilistic systems. Our approach builds upon a recently proposed assume-guarantee framework for probabilistic automata, in which assumptions and guarantees are probabilistic safety properties, represented using finite automata. A limitation of this work is that the assumptions need to be created manually. To overcome this, we propose a novel learning technique based on the L* algorithm, which automatically generates probabilistic assumptions using the results of queries executed by a probabilistic model checker. Learnt assumptions either establish satisfaction of the verification problem or are used to generate a probabilistic counterexample that refutes it. In the case where an assumption cannot be generated, lower and upper bounds on the probability of satisfaction are produced. We illustrate the applicability of the approach on a range of case studies.
Type de document :
Communication dans un congrès
7th International Conference on Quantitative Evaluation of Systems (QEST'10), Sep 2010, Williamsburg, United States. p. 133-142, 2010
Liste complète des métadonnées

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

https://hal.inria.fr/inria-00531203
Contributeur : Emmanuelle Grousset <>
Soumis le : mardi 2 novembre 2010 - 10:24:53
Dernière modification le : mardi 2 novembre 2010 - 11:37:00
Document(s) archivé(s) le : vendredi 2 décembre 2016 - 16:01:07

Fichier

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

Identifiants

  • HAL Id : inria-00531203, version 1

Collections

Citation

Lu Feng, Marta Kwiatkowska, David Parker. Compositional Verification of Probabilistic Systems using Learning. 7th International Conference on Quantitative Evaluation of Systems (QEST'10), Sep 2010, Williamsburg, United States. p. 133-142, 2010. 〈inria-00531203〉

Partager

Métriques

Consultations de la notice

176

Téléchargements de fichiers

109