Probabilistic Model Checking for the Data-Rich World

Duration: 30 mins 21 secs

Share this media item:

Embed this media item:

<iframe width="_width_" height="_height_" src="https://sms.cam.ac.uk/media/3527521/embed" frameborder="0" scrolling="no" allowfullscreen></iframe>

Choose size:

About this item

Available Formats

About this item

Description:	Kwiatkowska, M Thursday 13th May 2021 - 16:00 to 16:30


Created:	2021-05-18 12:30
Collection:	Verified software: from theory to practice
Publisher:	Isaac Newton Institute for Mathematical Sciences
Copyright:	Kwiatkowska, M
Language:	eng (English)


Abstract:	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, this lecture will give an overview of recent progress in probabilistic model checking and highlight challenges and opportunities for the future.

Abstract:

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, this lecture will give an overview of recent progress in probabilistic model checking and highlight challenges and opportunities for the future.

Available Formats

Format	Quality	Bitrate	Size
MPEG-4 Video	640x360	1.24 Mbits/sec	283.02 MB	View	Download
WebM	640x360	544.34 kbits/sec	121.07 MB	View	Download
iPod Video	480x270	480.11 kbits/sec	106.73 MB	View	Download
MP3	44100 Hz	249.8 kbits/sec	55.59 MB	Listen	Download
Auto *	(Allows browser to choose a format it supports)