Skip to Main content Skip to Navigation
New interface
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
Contributor : Emmanuelle Grousset Connect in order to contact the contributor
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


Files produced by the author(s)


  • HAL Id : inria-00531203, version 1



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⟩



Record views


Files downloads