BCS Lovelace lecture: Probabilistic model checking for the data-rich world

Probabilistic model checking for the data-rich world

Professor Marta Kwiatkowska FRS MAE leads this year’s BCS Lovelace lecture.

She was awarded the 2019 BCS Lovelace Medal for her research in probabilistic and quantitative verification. Since 2001 she has led the development of the highly influential probabilistic model checker: PRISM.

Computing systems have become indispensable in our society, supporting us in almost all tasks, from social interactions and online banking to robotic assistants and implantable medical devices. Since software faults in such systems can have disastrous consequences, methods based on mathematical logic, such as proof assistants or model checking, have been developed to ensure their correctness. However, many computing systems employ probability, for example as a randomisation technique in distributed protocols, or to quantify uncertainty in the environment for AI and robotics applications.

Systems with machine learning components that make decisions based on observed data also have a natural, Bayesian probabilistic interpretation. In such cases logic no longer suffices, and we must reason with probability.

Probabilistic model checking techniques aim to verify the correctness of probabilistic models against quantitative properties, such as the probability or expectation of a critical event. Exemplified through the software tool PRISM (prismmodelchecker.org), they have been successfully applied in a variety of domains, finding and fixing flaws in real-world systems.

As today’s computing systems evolve to increasingly rely on automated, strategic decisions learnt from rich sources of data, probabilistic model checking has the potential to provide probabilistic robustness guarantees for machine learning.

Using illustrative examples from mobile communications, robotics, security, autonomous driving and affective computing, this lecture will give an overview of recent progress in probabilistic model checking and highlight challenges and opportunities for the future.

Speaker biographies

Headline Speaker: Professor Marta Kwiatkowska

Marta Kwiatkowska is Professor of Computing Systems and Fellow of Trinity College, University of Oxford. She is known for fundamental contributions to the theory and practice of model checking for probabilistic systems. She led the development of the PRISM model checker (www.prismmodelchecker.org), the leading software tool in the area. Probabilistic model checking has been adopted in diverse fields, including distributed computing, wireless networks, security, robotics, healthcare, systems biology, DNA computing and nanotechnology, with genuine flaws found and corrected in real-world protocols.

Kwiatkowska was awarded two ERC Advanced Grants, VERIWARE and FUN2MODEL, and is a coinvestigator of the EPSRC Programme Grant on Mobile Autonomy. She was honoured with the Royal Society Milner Award in 2018 and the Lovelace Medal in 2019, and is a Fellow of the Royal Society, ACM and BCS, and Member of Academia Europea.

Introductory Speaker: Professor Muffy Calder OBE

Professor Calder is the Professor of Formal Methods, Head of the College of Science and Engineering, and Vice Principal of the University of Glasgow.

Her research is in modelling and reasoning about the behaviour of complex software and biochemical systems using computer science, mathematics and automated-reasoning techniques.

She is one of twelve holders of the Suffrage Science Award in Maths and Computing, presented to celebrate her scientific achievement and her ability to inspire others.

Vote of thanks: Professor Tony Cohn, University of Leeds

Tony Cohn is Professor of Automated Reasoning at the University of Leeds. He is also a Turing Fellow at the Alan Turing Institute, and is the recipient of the 2015 IJCAI Donald E Walker Distinguished Service Award and the 2012 AAAI Distinguished Service Award. He is a Fellow of the Royal Academy of Engineering, AAAI, AISB, EurAI, the BCS, and the IET. His research is broadly based in AI and robotics, including machine learning, and knowledge representation and reasoning, with a particular focus on spatial reasoning.

The Lovelace lecture is brought to you by BCS, The Chartered Institute for IT, and is sponsored by the Ada Lovelace Institute.