Skip to Main content Skip to Navigation
Conference papers

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.
Document type :
Conference papers
Complete list of metadata

Cited literature [17 references]  Display  Hide  Download

https://hal.inria.fr/inria-00531203
Contributor : Emmanuelle Grousset <>
Submitted on : Tuesday, November 2, 2010 - 10:24:53 AM
Last modification on : Tuesday, September 8, 2020 - 4:58:02 PM
Long-term archiving on: : Friday, December 2, 2016 - 4:01:07 PM

File

qest10learn.pdf
Files produced by the author(s)

Identifiers

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

Share

Metrics

Record views

227

Files downloads

304