Learning-based Compositional Verification for Synchronous Probabilistic Systems

Abstract : We present novel techniques for automated compositional verification of synchronous probabilistic systems. First, we give an assume-guarantee framework for verifying probabilistic safety properties of systems modelled as discrete-time Markov chains. Assumptions about system components are represented as probabilistic finite automata (PFAs) and the relationship between components and assumptions is captured by weak language inclusion. In order to implement this framework, we develop a semi-algorithm to check language inclusion for PFAs and a new active learning method for PFAs. The latter is then used to automatically generate assumptions for compositional verification.
Type de document :
Communication dans un congrès
9th International Symposium on Automated Technology for Verification and Analysis (ATVA'11), 2011, Taipei, Taiwan. Springer, 6996, pp.511--521, 2011, LNCS
Liste complète des métadonnées

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

https://hal.inria.fr/hal-00647061
Contributeur : Hongyang Qu <>
Soumis le : lundi 30 janvier 2012 - 12:39:42
Dernière modification le : lundi 30 janvier 2012 - 14:16:12
Document(s) archivé(s) le : mardi 13 décembre 2016 - 19:10:01

Fichier

atva11.pdf
Accord explicite pour ce dépôt

Identifiants

  • HAL Id : hal-00647061, version 1

Collections

Citation

Lu Feng, Tingting Han, Marta Kwiatkowska, David Parker. Learning-based Compositional Verification for Synchronous Probabilistic Systems. 9th International Symposium on Automated Technology for Verification and Analysis (ATVA'11), 2011, Taipei, Taiwan. Springer, 6996, pp.511--521, 2011, LNCS. 〈hal-00647061〉

Partager

Métriques

Consultations de la notice

116

Téléchargements de fichiers

109