Strategy synthesis for autonomous agents using PRISM

Ruben Giaquinta, Ruth Hoffmann, Murray Ireland, Alice Miller, Gethin Norman*

*Corresponding author for this work

Research output: Chapter in Book/Report/Conference proceedingConference contribution

10 Citations (Scopus)


We present probabilistic models for autonomous agent search and retrieve missions derived from Simulink models for an Unmanned Aerial Vehicle (UAV) and show how probabilistic model checking and the probabilistic model checker PRISM can be used for optimal controller generation. We introduce a sequence of scenarios relevant to UAVs and other autonomous agents such as underwater and ground vehicles. For each scenario we demonstrate how it can be modelled using the PRISM language, give model checking statistics and present the synthesised optimal controllers. We conclude with a discussion of the limitations when using probabilistic model checking and PRISM in this context and what steps can be taken to overcome them. In addition, we consider how the controllers can be returned to the UAV and adapted for use on larger search areas.

Original languageEnglish
Title of host publicationNASA Formal Methods
Subtitle of host publication10th International Symposium, NFM 2018, Newport News, VA, USA, April 17-19, 2018, Proceedings
EditorsAaron Dutle, César Muñoz, Anthony Narkawicz
Place of PublicationCham
Number of pages17
ISBN (Electronic)9783319779355
ISBN (Print)9783319779348
Publication statusPublished - 2018
Event10th International Symposium on NASA Formal Methods, NFM 2018 - Newport News, United States
Duration: 17 Apr 201819 Apr 2018
Conference number: 10

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349


Conference10th International Symposium on NASA Formal Methods, NFM 2018
Abbreviated titleNFM
Country/TerritoryUnited States
CityNewport News
Internet address


Dive into the research topics of 'Strategy synthesis for autonomous agents using PRISM'. Together they form a unique fingerprint.

Cite this