Seminars

Automated Compositional Verification for Probabilistic Systems PDF slides
Marta Kwiatkowska, Director Graduate
Studies, Oxford University Computing Laboratory

9/27/2010, 2pm, GHC-6501

Abstract

Probabilistic automata are a natural formalism for modelling and verifying systems that exhibit both stochastic and nondeterministic behaviour. Scalability of these techniques, however, represents a major challenge. This talk describes a compositional verification framework for such systems, based on assume-guarantee reasoning. Assumptions and guarantees are captured by probabilistic safety properties, represented as finite automata. These can be verified efficiently, using a reduction to the problem of multi-objective probabilistic model checking.

Furthermore, we address the problem of automatically generating suitable assumptions, using the well-known L* algorithm for algorithmic learning of regular languages. A prototype tool implementing these techniques has been used to perform compositional probabilistic verification of several large case studies, including instances where conventional, non-compositional approaches are infeasible.

 

Biography

Marta Kwiatkowska serves on editorial boards of several journals, including Science of Computer Programming and Royal Society's Philosophical Transactions A, and is a member of the Steering Committee of the International Conference on Quantitative Evaluation of SysTems (QEST). She was lead organiser of the Royal Society Discussion Meeting "From computers to ubiquitous computing, by 2020" and guest co-editor of the associated Proceedings in Phil. Trans. R. Soc. A vol 366 no 1881.