9/27/2010, 2pm, GHC-6501
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.
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.