Strategy synthesis for autonomous agents using PRISM

Ruben Giaquinta; Ruth Hoffmann; Murray Ireland; Alice Miller; Gethin Norman

doi:10.1007/978-3-319-77935-5_16

Strategy synthesis for autonomous agents using PRISM

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

^*Corresponding author for this work

School of Computer Science

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

11 Citations (Scopus)

Abstract

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 language	English
Title of host publication	NASA Formal Methods
Subtitle of host publication	10th International Symposium, NFM 2018, Newport News, VA, USA, April 17-19, 2018, Proceedings
Editors	Aaron Dutle, César Muñoz, Anthony Narkawicz
Place of Publication	Cham
Publisher	Springer
Pages	220-236
Number of pages	17
ISBN (Electronic)	9783319779355
ISBN (Print)	9783319779348
DOIs	https://doi.org/10.1007/978-3-319-77935-5_16
Publication status	Published - 2018
Event	10th International Symposium on NASA Formal Methods, NFM 2018 - Newport News, United States Duration: 17 Apr 2018 → 19 Apr 2018 Conference number: 10 https://shemesh.larc.nasa.gov/NFM2018/

Publication series

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

Conference

Conference	10th International Symposium on NASA Formal Methods, NFM 2018
Abbreviated title	NFM
Country/Territory	United States
City	Newport News
Period	17/04/18 → 19/04/18
Internet address	https://shemesh.larc.nasa.gov/NFM2018/

Access to Document

10.1007/978-3-319-77935-5_16

Cite this

Giaquinta, R., Hoffmann, R., Ireland, M., Miller, A., & Norman, G. (2018). Strategy synthesis for autonomous agents using PRISM. In A. Dutle, C. Muñoz, & A. Narkawicz (Eds.), NASA Formal Methods: 10th International Symposium, NFM 2018, Newport News, VA, USA, April 17-19, 2018, Proceedings (pp. 220-236). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 10811). Springer. https://doi.org/10.1007/978-3-319-77935-5_16

Giaquinta, Ruben ; Hoffmann, Ruth ; Ireland, Murray et al. / Strategy synthesis for autonomous agents using PRISM. NASA Formal Methods: 10th International Symposium, NFM 2018, Newport News, VA, USA, April 17-19, 2018, Proceedings. editor / Aaron Dutle ; César Muñoz ; Anthony Narkawicz. Cham : Springer, 2018. pp. 220-236 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).

@inproceedings{f78f1b615e674a638058e1b4ce779943,

title = "Strategy synthesis for autonomous agents using PRISM",

abstract = "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.",

author = "Ruben Giaquinta and Ruth Hoffmann and Murray Ireland and Alice Miller and Gethin Norman",

year = "2018",

doi = "10.1007/978-3-319-77935-5_16",

language = "English",

isbn = "9783319779348",

series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

publisher = "Springer",

pages = "220--236",

editor = "Aaron Dutle and C{\'e}sar Mu{\~n}oz and Anthony Narkawicz",

booktitle = "NASA Formal Methods",

address = "Netherlands",

note = "10th International Symposium on NASA Formal Methods, NFM 2018, NFM ; Conference date: 17-04-2018 Through 19-04-2018",

url = "https://shemesh.larc.nasa.gov/NFM2018/",

}

Giaquinta, R, Hoffmann, R, Ireland, M, Miller, A & Norman, G 2018, Strategy synthesis for autonomous agents using PRISM. in A Dutle, C Muñoz & A Narkawicz (eds), NASA Formal Methods: 10th International Symposium, NFM 2018, Newport News, VA, USA, April 17-19, 2018, Proceedings. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 10811, Springer, Cham, pp. 220-236, 10th International Symposium on NASA Formal Methods, NFM 2018, Newport News, Virginia, United States, 17/04/18. https://doi.org/10.1007/978-3-319-77935-5_16

Strategy synthesis for autonomous agents using PRISM. / Giaquinta, Ruben; Hoffmann, Ruth; Ireland, Murray et al.
NASA Formal Methods: 10th International Symposium, NFM 2018, Newport News, VA, USA, April 17-19, 2018, Proceedings. ed. / Aaron Dutle; César Muñoz; Anthony Narkawicz. Cham: Springer, 2018. p. 220-236 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 10811).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

TY - GEN

T1 - Strategy synthesis for autonomous agents using PRISM

AU - Giaquinta, Ruben

AU - Hoffmann, Ruth

AU - Ireland, Murray

AU - Miller, Alice

AU - Norman, Gethin

N1 - Conference code: 10

PY - 2018

Y1 - 2018

N2 - 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.

AB - 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.

U2 - 10.1007/978-3-319-77935-5_16

DO - 10.1007/978-3-319-77935-5_16

M3 - Conference contribution

AN - SCOPUS:85045300250

SN - 9783319779348

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 220

EP - 236

BT - NASA Formal Methods

A2 - Dutle, Aaron

A2 - Muñoz, César

A2 - Narkawicz, Anthony

PB - Springer

CY - Cham

T2 - 10th International Symposium on NASA Formal Methods, NFM 2018

Y2 - 17 April 2018 through 19 April 2018

ER -

Giaquinta R, Hoffmann R, Ireland M, Miller A, Norman G. Strategy synthesis for autonomous agents using PRISM. In Dutle A, Muñoz C, Narkawicz A, editors, NASA Formal Methods: 10th International Symposium, NFM 2018, Newport News, VA, USA, April 17-19, 2018, Proceedings. Cham: Springer. 2018. p. 220-236. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). Epub 2018 Mar 11. doi: 10.1007/978-3-319-77935-5_16

Strategy synthesis for autonomous agents using PRISM

Abstract

Publication series

Conference

Access to Document

Fingerprint

Cite this