David Parker
Professor of Computer Science, University of Birmingham
[KNP22] Marta Kwiatkowska, Gethin Norman and David Parker. Probabilistic Model Checking and Autonomy. Annual Review of Control, Robotics, and Autonomous Systems, 5, Annual Reviews. To appear. 2022. [pdf] [bib] [Gives an overview of probabilistic model checking as applied to the context of robotics and autonomous systems.]
Downloads:  pdf pdf (2.25 MB)  bib bib
Notes: Posted with permission from the Annual Review of Control, Robotics, and Autonomous Systems, Volume 5; copyright 2022 Annual Reviews, https://www.annualreviews.org/.
Abstract. Design and control of autonomous systems that operate in uncertain or adversarial environments can be facilitated by formal modelling and analysis. Probabilistic model checking is a technique to automatically verify, for a given temporal logic specification, that a system model satisfies the specification, as well as to synthesise an optimal strategy for its control. This method has recently been extended to multi-agent systems that exhibit competitive or cooperative behaviour modelled via stochastic games and synthesis of equilibria strategies. In this paper, we provide an overview of probabilistic model checking, focusing on models supported by the PRISM and PRISM-games model checkers. This includes fully observable and partially observable Markov decision processes, as well as turn-based and concurrent stochastic games, together with associated probabilistic temporal logics. We demonstrate the applicability of the framework through illustrative examples from autonomous systems. Finally, we highlight research challenges and suggest directions for future work in this area.