Academic
Publications
Compositional Verification of Probabilistic Systems Using Learning

Compositional Verification of Probabilistic Systems Using Learning,10.1109/QEST.2010.24,Lu Feng,Marta Z. Kwiatkowska,David Parker

Compositional Verification of Probabilistic Systems Using Learning   (Citations: 5)
BibTex | RIS | RefWorks Download
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.
Conference: Quantitative Evaluation of Systems - QEST , pp. 133-142, 2010
Cumulative Annual
View Publication
The following links allow you to view full publications. These links are maintained by other sources not affiliated with Microsoft Academic Search.
    • ...Possible directions for future work include extending our compositional verification approach with learning-based assumption generation, as [17] does for the simpler framework of [21], and investigation of continuous-time models...

    Vojtech Forejtet al. Quantitative Multi-objective Verification for Probabilistic Systems

    • ...In recent work [20], we showed how learning could also be successfully used to generate the probabilistic assumptions needed for the compositional verification of probabilistic systems...
    • ...This approach was proposed in [20] and shown to be applicable on several large case studies...
    • ...In this section, we give a high-level overview of the approach and describe the key underlying ideas; for the technical details, the reader is referred to [20]...
    • ...upper bound can also be generated (see [20] for details)...
    • ...Fig. 3. Overview of probabilistic assumption generation [20], using an adaption of L*: generates assumption � A� pA for verification of M1 � M2 |= � G� pG using rule (ASym)...
    • ...Firstly, a counterexample may constitute multiple traces; this is because the results of the model checking queries executed by the teacher yield probabilistic counterexamples [24], which comprise multiple paths (again, see [20] for precise details)...
    • ...The approach outlined in the previous section was successfully used in [20] to automatically generate probabilistic assumptions for several large case studies...
    • ...We added NL* to our existing implementation from [20], which is based on an extension of PRISM [26] and the libalf [6] learning library...
    • ...The first four are taken from [20]: client-server benchmark models from [32] incorporating failures in one or all clients (client-server1 and client-serverN ), Aspnes & Herlihy’s randomised consensus algorithm (consensus )a nd as ensor network exhibiting message losses (sensor network ). The fifth example is the MER model from above (mer ). Experiments were run on a 1.86GHz PC with 2GB RAM and we imposed a time-out of 24 hours...

    Lu Fenget al. Automated Learning of Probabilistic Assumptions for Compositional Reas...

    • ...In subsequent work [33], the process of generating an appropriate assumption hAi pA is also automated, using algorithmic learning techniques based on the L* algorithm...

    Marta Kwiatkowskaet al. Advances and challenges of probabilistic model checking

    • ...In particular, we would like to exploit the assume-guarantee reasoning method [15,9] implemented in PRISM to analyse large models...

    Felicita Di Giandomenicoet al. Dependability Analysis and Verification for Connected Systems

    • ...Other promising directions include: partial order reduction [49,31], symmetry reduction [66,39], algorithms for simulation and bisimulation relations [25,86] and compositional probabilistic verification techniques [69,43,38]...

    Vojtěch Forejtet al. Automated Verification Techniques for Probabilistic Systems

Sort by: