Computing systems have become indispensable in our society, supporting us in almost all tasks, from social interactions and online banking to robotic .. Read more 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. 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. 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.
- Share your Experience