Compositional Verification of Probabilistic Systems using Learning - Inria - Institut national de recherche en sciences et technologies du numérique Accéder directement au contenu
Communication Dans Un Congrès Année : 2010

Compositional Verification of Probabilistic Systems using Learning

Lu Feng
  • Fonction : Auteur
Marta Kwiatkowska
  • Fonction : Auteur
  • PersonId : 861066

Résumé

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.
Fichier principal
Vignette du fichier
qest10learn.pdf (535.85 Ko) Télécharger le fichier
Origine : Fichiers produits par l'(les) auteur(s)
Loading...

Dates et versions

inria-00531203 , version 1 (02-11-2010)

Identifiants

  • HAL Id : inria-00531203 , version 1

Citer

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. ⟨inria-00531203⟩

Collections

CONNECT
109 Consultations
133 Téléchargements

Partager

Gmail Facebook X LinkedIn More