{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,12]],"date-time":"2026-02-12T17:43:39Z","timestamp":1770918219208,"version":"3.50.1"},"reference-count":128,"publisher":"Annual Reviews","issue":"1","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Annu. Rev. Control Robot. Auton. Syst."],"published-print":{"date-parts":[[2022,5,3]]},"abstract":"<jats:p> The design and control of autonomous systems that operate in uncertain or adversarial environments can be facilitated by formal modeling 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 synthesize an optimal strategy for its control. This method has recently been extended to multiagent systems that exhibit competitive or cooperative behavior modeled via stochastic games and synthesis of equilibria strategies. In this article, we provide an overview of probabilistic model checking, focusing on models supported by the PRISM and PRISM-games model checkers. This overview 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. <\/jats:p>","DOI":"10.1146\/annurev-control-042820-010947","type":"journal-article","created":{"date-parts":[[2021,12,6]],"date-time":"2021-12-06T20:31:18Z","timestamp":1638822678000},"page":"385-410","source":"Crossref","is-referenced-by-count":32,"title":["Probabilistic Model Checking and Autonomy"],"prefix":"10.1146","volume":"5","author":[{"given":"Marta","family":"Kwiatkowska","sequence":"first","affiliation":[{"name":"Department of Computer Science, University of Oxford, Oxford, United Kingdom;"}]},{"given":"Gethin","family":"Norman","sequence":"additional","affiliation":[{"name":"School of Computing Science, University of Glasgow, Glasgow, United Kingdom;"}]},{"given":"David","family":"Parker","sequence":"additional","affiliation":[{"name":"School of Computer Science, University of Birmingham, Birmingham, United Kingdom;"}]}],"member":"22","reference":[{"key":"B1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-22110-1_47"},{"key":"B2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-53291-8_25"},{"key":"B3","doi-asserted-by":"publisher","DOI":"10.1002\/9780470316887"},{"key":"B4","doi-asserted-by":"publisher","DOI":"10.1109\/IROS.2014.6942756"},{"key":"B5","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4684-9455-6"},{"key":"B6","doi-asserted-by":"publisher","DOI":"10.1007\/BF01211866"},{"key":"B7","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(81)90110-9"},{"key":"B8","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-21455-4_3"},{"key":"B9","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2016.12.003"},{"key":"B10","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-11936-6_8"},{"issue":"4","key":"B11","first-page":"3","volume":"16","author":"K\u0159et\u00ednsk\u00fd J","year":"2020","journal-title":"Log. Methods Comput. Sci."},{"key":"B12","volume-title":"Principles of Model Checking","author":"Baier C","year":"2008"},{"key":"B13","volume-title":"Formal verification of probabilistic systems","author":"de Alfaro L.","year":"1997"},{"key":"B14","volume-title":"Dynamic Programming","author":"Bellman R.","year":"1957"},{"key":"B15","doi-asserted-by":"publisher","DOI":"10.2168\/LMCS-4(4:8)2008"},{"key":"B16","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-19835-9_11"},{"key":"B17","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-33386-6_25"},{"key":"B18","doi-asserted-by":"publisher","DOI":"10.1109\/LRA.2018.2803814"},{"key":"B19","first-page":"280","volume-title":"Theoretical Aspects of Computing \u2013 ICTAC 2004: First International Colloquium","author":"Daws C","year":"2004"},{"key":"B20","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-010-0146-x"},{"key":"B21","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-10696-0_31"},{"key":"B22","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-20398-5_12"},{"key":"B23","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-46520-3_4"},{"key":"B24","doi-asserted-by":"publisher","DOI":"10.1016\/S0004-3702(00)00047-3"},{"key":"B25","doi-asserted-by":"publisher","DOI":"10.1109\/CDC.2012.6426174"},{"key":"B26","first-page":"527","volume-title":"Computer Aided Verification: 25th International Conference, CAV 2013","author":"Puggelli A","year":"2015"},{"key":"B27","doi-asserted-by":"publisher","DOI":"10.1145\/3309683"},{"key":"B28","doi-asserted-by":"publisher","DOI":"10.1023\/A:1008739929481"},{"key":"B29","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-63390-9_31"},{"key":"B30","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-54580-5_9"},{"key":"B31","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-54862-8_51"},{"key":"B32","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-06410-9_22"},{"key":"B33","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-14295-6_56"},{"key":"B34","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-21690-4_13"},{"key":"B35","doi-asserted-by":"publisher","DOI":"10.1109\/TRO.2011.2172150"},{"key":"B36","doi-asserted-by":"publisher","DOI":"10.1109\/TAC.2015.2398883"},{"key":"B37","doi-asserted-by":"publisher","DOI":"10.1007\/s00165-020-00508-1"},{"key":"B38","doi-asserted-by":"publisher","DOI":"10.1109\/MetroAeroSpace.2016.7573276"},{"key":"B39","doi-asserted-by":"publisher","DOI":"10.1177\/0278364919856695"},{"key":"B40","doi-asserted-by":"publisher","DOI":"10.1609\/aaai.v33i01.33018066"},{"key":"B41","doi-asserted-by":"publisher","DOI":"10.1145\/3387939.3391592"},{"key":"B42","doi-asserted-by":"publisher","DOI":"10.1109\/ECMR.2019.8870951"},{"key":"B43","doi-asserted-by":"publisher","DOI":"10.1145\/2330667.2330686"},{"key":"B44","first-page":"100","volume":"52","author":"Luckcuck M","year":"2019","journal-title":"ACM Comput. Surv."},{"key":"B45","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-78499-9_21"},{"key":"B46","first-page":"165","volume-title":"Computer Science Logic 2013","author":"Chatterjee K","year":"2013"},{"key":"B47","doi-asserted-by":"publisher","DOI":"10.1016\/j.artint.2016.01.007"},{"key":"B48","doi-asserted-by":"publisher","DOI":"10.1016\/S0004-3702(02)00378-8"},{"key":"B49","volume-title":"Exploiting structure to efficiently solve large scale partially observable Markov decision processes","author":"Poupart P.","year":"2005"},{"key":"B50","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-22975-1_16"},{"key":"B51","doi-asserted-by":"publisher","DOI":"10.1287\/opre.39.1.162"},{"key":"B52","first-page":"619","volume-title":"UAI '04: Proceedings of the 20th Conference on Uncertainty in Artificial Intelligence","author":"Yu H","year":"2004"},{"key":"B53","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-59152-6_16"},{"key":"B54","doi-asserted-by":"publisher","DOI":"10.1609\/aaai.v34i06.6563"},{"key":"B55","doi-asserted-by":"publisher","DOI":"10.1109\/ICRA.2015.7139019"},{"key":"B56","first-page":"519","volume-title":"UAI '18: Proceedings of the Thirty-Fourth Conference on Uncertainty in Artificial Intelligence","author":"Junges S","year":"2018"},{"key":"B57","doi-asserted-by":"publisher","DOI":"10.1109\/TAC.2020.2990140"},{"key":"B58","doi-asserted-by":"publisher","DOI":"10.24963\/ijcai.2020\/570"},{"key":"B59","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-33386-6_26"},{"key":"B60","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-22110-1_20"},{"key":"B61","doi-asserted-by":"publisher","DOI":"10.24963\/ijcai.2020\/569"},{"key":"B62","doi-asserted-by":"publisher","DOI":"10.23919\/ACC.2018.8431911"},{"key":"B63","doi-asserted-by":"publisher","DOI":"10.1109\/TASE.2016.2530623"},{"key":"B64","doi-asserted-by":"publisher","DOI":"10.1145\/585265.585270"},{"key":"B65","doi-asserted-by":"publisher","DOI":"10.1007\/s10703-013-0183-7"},{"key":"B66","volume-title":"Theory of Games and Economic Behavior","author":"von Neumann J","year":"1944"},{"key":"B67","doi-asserted-by":"publisher","DOI":"10.2307\/2586667"},{"key":"B68","doi-asserted-by":"publisher","DOI":"10.1090\/dimacs\/013\/04"},{"key":"B69","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-96145-3_36"},{"key":"B70","doi-asserted-by":"publisher","DOI":"10.1007\/11672142_42"},{"key":"B71","doi-asserted-by":"publisher","DOI":"10.1016\/j.jcss.2011.05.002"},{"key":"B72","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-40196-1_28"},{"key":"B73","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2017.09.010"},{"key":"B74","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-46681-0_22"},{"key":"B75","doi-asserted-by":"publisher","DOI":"10.1145\/2735960.2735973"},{"key":"B76","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-99154-2_13"},{"key":"B77","doi-asserted-by":"publisher","DOI":"10.1109\/SASOW.2015.14"},{"key":"B78","doi-asserted-by":"publisher","DOI":"10.1109\/ACSOS49614.2020.00029"},{"key":"B79","doi-asserted-by":"publisher","DOI":"10.1145\/2695664.2695680"},{"key":"B80","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-14295-6_57"},{"key":"B81","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-19835-9_22"},{"key":"B82","doi-asserted-by":"publisher","DOI":"10.1073\/pnas.36.1.48"},{"key":"B83","doi-asserted-by":"publisher","DOI":"10.1007\/s10703-020-00356-y"},{"key":"B84","volume-title":"An Introduction to Game Theory","author":"Osborne M","year":"2004"},{"key":"B85","first-page":"351","volume-title":"34th International Conference on Foundations of Software Technology and Theoretical Computer Science","author":"Bouyer P","year":"2014"},{"key":"B86","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2007.07.008"},{"key":"B87","doi-asserted-by":"publisher","DOI":"10.1016\/j.jcss.2012.12.001"},{"key":"B88","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-40313-2_25"},{"key":"B89","doi-asserted-by":"publisher","DOI":"10.1007\/BF02579150"},{"key":"B90","doi-asserted-by":"publisher","DOI":"10.1016\/S0022-0000(05)80063-7"},{"key":"B91","doi-asserted-by":"publisher","DOI":"10.1007\/s00224-013-9524-6"},{"key":"B92","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-59854-9_7"},{"key":"B93","doi-asserted-by":"publisher","DOI":"10.1145\/1461928.1461951"},{"key":"B94","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-30124-0_6"},{"key":"B95","doi-asserted-by":"publisher","DOI":"10.5117\/9789085550402"},{"key":"B96","first-page":"1","volume-title":"30th International Conference on Concurrency Theory","author":"Brihaye T","year":"2019"},{"key":"B97","first-page":"1","volume-title":"30th International Conference on Concurrency Theory","author":"Gutierrez J","year":"2019"},{"key":"B98","doi-asserted-by":"publisher","DOI":"10.4204\/EPTCS.226.5"},{"key":"B99","first-page":"247","volume-title":"Proceedings of the 7th Nordic Workshop on Programming Theory","author":"Jensen H.","year":"1996"},{"key":"B100","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(01)00046-9"},{"key":"B101","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(01)00215-8"},{"key":"B102","doi-asserted-by":"publisher","DOI":"10.1007\/s10703-006-0005-2"},{"key":"B103","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-31175-9_22"},{"key":"B104","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2016.04.021"},{"key":"B105","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-04081-8_28"},{"key":"B106","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2007.01.004"},{"key":"B107","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2017.01.015"},{"key":"B108","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-04368-0_17"},{"key":"B109","doi-asserted-by":"publisher","DOI":"10.1145\/2461328.2461372"},{"key":"B110","doi-asserted-by":"publisher","DOI":"10.1016\/j.ifacol.2018.08.013"},{"key":"B111","doi-asserted-by":"publisher","DOI":"10.1007\/10722167_15"},{"key":"B112","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-44804-7_3"},{"key":"B113","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45605-8_5"},{"key":"B114","first-page":"250","volume":"2","author":"Segala R","year":"1995","journal-title":"Nordic J. Comput."},{"key":"B115","doi-asserted-by":"publisher","DOI":"10.1109\/QEST.2007.10"},{"key":"B116","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-70545-1_16"},{"key":"B117","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-63166-6_10"},{"key":"B118","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.2009.5"},{"key":"B119","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-12002-2_30"},{"key":"B120","doi-asserted-by":"publisher","DOI":"10.1007\/s10703-010-0097-6"},{"key":"B121","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2013.10.001"},{"key":"B122","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-44584-6_13"},{"key":"B123","doi-asserted-by":"publisher","DOI":"10.1145\/2579821"},{"key":"B124","doi-asserted-by":"publisher","DOI":"10.1007\/BF00935665"},{"key":"B125","doi-asserted-by":"publisher","DOI":"10.1016\/0304-4068(74)90037-8"},{"key":"B126","first-page":"67","volume":"244","author":"Battigalli P","year":"2009","journal-title":"J. Econ. Theory"},{"key":"B127","doi-asserted-by":"publisher","DOI":"10.1613\/jair.301"},{"key":"B128","volume-title":"Neural-Symbolic Cognitive Reasoning","author":"d'Avila Garcez A","year":"2009"}],"container-title":["Annual Review of Control, Robotics, and Autonomous Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.annualreviews.org\/doi\/pdf\/10.1146\/annurev-control-042820-010947","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,5,3]],"date-time":"2022-05-03T16:14:19Z","timestamp":1651594459000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.annualreviews.org\/doi\/10.1146\/annurev-control-042820-010947"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022,5,3]]},"references-count":128,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2022,5,3]]}},"alternative-id":["10.1146\/annurev-control-042820-010947"],"URL":"https:\/\/doi.org\/10.1146\/annurev-control-042820-010947","relation":{},"ISSN":["2573-5144","2573-5144"],"issn-type":[{"value":"2573-5144","type":"print"},{"value":"2573-5144","type":"electronic"}],"subject":[],"published":{"date-parts":[[2022,5,3]]}}}