Marta Kwiatkowska, Feb 2012

Marta Kwiatkowska from the University of Oxford will be visiting on 21 Feb (Tue).

Schedule

• 10:30 am - meet with Richard Murray in 109 Steele
• 11:00 am - seminar
• 12:00 pm - Lunchtime seminar: Gabor Orosz
• 1:00-3:00 pm - Meeting with NCS group, 110 Steele
• 3:30-4:15 pm - Mihai Florian
• 4:15 pm - Ufuk

Abstract

Quantitative Multi-Objective Verification for Probabilistic Systems

Marta Kwiatkowska, University of Oxford (joint work with V. Forejt, G. Norman, D. Parker and H. Qu)

Abstract. We present a verification framework for analysing multiple quantitative objectives of systems that exhibit both nondeterministic and stochastic behaviour. These systems are modelled as probabilistic automata, enriched with cost or reward structures that capture, for example, energy usage or performance metrics. Quantitative properties of these models are expressed in a specification language that incorporates probabilistic safety and liveness properties, expected total cost or reward, and supports multiple objectives of these types. We propose and implement an efficient verification framework for such properties and then present two distinct applications of it: firstly, controller synthesis subject to multiple quantitative objectives; and, secondly, quantitative compositional verification. The practical applicability of both approaches is illustrated with experimental results from several large case studies.

Bio

Marta Kwiatkowska is Professor of Computing Systems and Fellow of Trinity College, University of Oxford. She was elected to Academia Europea and received a prestigious ERC Advanced Grant VERIWARE "From software verification to everyware verification", 2010-15.

Kwiatkowska's research is concerned with modelling and verification techniques for probabilistic systems, with application to engineered and biological systems. She spearheaded the development of probabilistic and quantitative methods in verification on the international scene. Her work on the theory to practice transfer of probabilistic model checking was recognised by invitations to speak at the LICS 2003 and ESEC/FSE 2007 conferences. She led the development of the PRISM model checker (www.prismmodelchecker.org), the leading software tool in the area and widely used for research and teaching. Applications of probabilistic model checking have spanned communication and security protocols, nanotechnology designs, power management and systems biology. Her research is currently supported by £3.7m of grant funding from EPSRC, EU, DARPA, Oxford Martin School and Microsoft Research.

Kwiatkowska serves on editorial board of IEEE Transactions on Software Engineering, Philosophical Transactions of the Royal Society A and Science of Computer Programming, and has lectured at several summer schools, including ESSLLI and the Marktoberdorf Summer School.