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, 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 gives an overview of recent progress in probabilistic model checking and highlight challenges and opportunities for the future.
The Lovelace lecture was brought to you by BCS and sponsored by The Ada Lovelace Institute.
About the speakers
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, 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.
Marta 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 Dame Muffy Calder DBE 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.