Autonomous agent behaviour modelled in PRISM -- a case study

Ruth Hoffmann; Murray Ireland; Alice Miller; Gethin Norman; Sandor Veres

doi:10.1007/978-3-319-32582-8_7

Autonomous agent behaviour modelled in PRISM -- a case study

Ruth Hoffmann, Murray Ireland, Alice Miller, Gethin Norman, Sandor Veres

School of Computer Science

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

Abstract

Formal verification of agents representing robot behaviour is a growing area due to the demand that autonomous systems have to be proven safe. In this paper we present an abstract definition of autonomy which can be used to model autonomous scenarios and propose the use of small-scale simulation models representing abstract actions to infer quantitative data. To demonstrate the applicability of the approach we build and verify a model of an unmanned aerial vehicle (UAV) in an exemplary autonomous scenario, utilising this approach.

Original language	English
Title of host publication	Model Checking Software
Subtitle of host publication	23rd International Symposium, SPIN 2016, Co-located with ETAPS 2016, Eindhoven, The Netherlands, April 7-8, 2016, Proceedings
Editors	Dragan Bošnački, Anton Wijs
Place of Publication	Cham
Publisher	Springer
Pages	104-110
ISBN (Electronic)	9783319325828
ISBN (Print)	9783319325811
DOIs	https://doi.org/10.1007/978-3-319-32582-8_7
Publication status	Published - 2016
Event	23rd International SPIN Symposium on Model Checking of Software - TU/e Science park of the Eindhoven University of Technology, Eindhoven, Netherlands Duration: 7 Apr 2016 → 8 Apr 2016 Conference number: 23 http://www.spin2016.info/

Publication series

Name	Lecture Notes in Computer Science
Volume	9641
ISSN (Print)	0302-9743
ISSN (Electronic)	1611-3349

Conference

Conference	23rd International SPIN Symposium on Model Checking of Software
Abbreviated title	SPIN
Country/Territory	Netherlands
City	Eindhoven
Period	7/04/16 → 8/04/16
Internet address	http://www.spin2016.info/

Access to Document

10.1007/978-3-319-32582-8_7Licence: CC BY

Hoffman-2017-Autonomous-agent-behaviour-SPIN2016-104-CC
Copyright The Author(s) 2016. This chapter is distributed under the terms of the Creative Commons Attribution 4.0 International License (http://creativecommons.org/licenses/by/4.0/), which permits use, duplication, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, a link is provided to the Creative Commons license and any changes made are indicated. The images or other third party material in this chapter are included in the work’s Creative Commons license, unless indicated otherwise in the credit line; if such material is not included in the work’s Creative Commons license and the respective action is not permitted by statutory regulation, users will need to obtain permission from the license holder to duplicate, adapt or reproduce the material.
Final published version, 208 KBLicence: CC BY

Cite this

Hoffmann, R., Ireland, M., Miller, A., Norman, G., & Veres, S. (2016). Autonomous agent behaviour modelled in PRISM -- a case study. In D. Bošnački, & A. Wijs (Eds.), Model Checking Software: 23rd International Symposium, SPIN 2016, Co-located with ETAPS 2016, Eindhoven, The Netherlands, April 7-8, 2016, Proceedings (pp. 104-110). (Lecture Notes in Computer Science; Vol. 9641). Springer. https://doi.org/10.1007/978-3-319-32582-8_7

Hoffmann, Ruth ; Ireland, Murray ; Miller, Alice et al. / Autonomous agent behaviour modelled in PRISM -- a case study. Model Checking Software: 23rd International Symposium, SPIN 2016, Co-located with ETAPS 2016, Eindhoven, The Netherlands, April 7-8, 2016, Proceedings. editor / Dragan Bošnački ; Anton Wijs. Cham : Springer, 2016. pp. 104-110 (Lecture Notes in Computer Science).

@inproceedings{0a462308eb9e46908b9fc3bd355edf15,

title = "Autonomous agent behaviour modelled in PRISM -- a case study",

abstract = "Formal verification of agents representing robot behaviour is a growing area due to the demand that autonomous systems have to be proven safe. In this paper we present an abstract definition of autonomy which can be used to model autonomous scenarios and propose the use of small-scale simulation models representing abstract actions to infer quantitative data. To demonstrate the applicability of the approach we build and verify a model of an unmanned aerial vehicle (UAV) in an exemplary autonomous scenario, utilising this approach.",

author = "Ruth Hoffmann and Murray Ireland and Alice Miller and Gethin Norman and Sandor Veres",

note = "This work was supported by the Engineering and Physical Sciences Research Council [grant number EP/N508792/1].; 23rd International SPIN Symposium on Model Checking of Software, SPIN ; Conference date: 07-04-2016 Through 08-04-2016",

year = "2016",

doi = "10.1007/978-3-319-32582-8_7",

language = "English",

isbn = "9783319325811",

series = "Lecture Notes in Computer Science",

publisher = "Springer",

pages = "104--110",

editor = "Dragan Bo{\v s}na{\v c}ki and Anton Wijs",

booktitle = "Model Checking Software",

address = "Netherlands",

url = "http://www.spin2016.info/",

}

Hoffmann, R, Ireland, M, Miller, A, Norman, G & Veres, S 2016, Autonomous agent behaviour modelled in PRISM -- a case study. in D Bošnački & A Wijs (eds), Model Checking Software: 23rd International Symposium, SPIN 2016, Co-located with ETAPS 2016, Eindhoven, The Netherlands, April 7-8, 2016, Proceedings. Lecture Notes in Computer Science, vol. 9641, Springer, Cham, pp. 104-110, 23rd International SPIN Symposium on Model Checking of Software, Eindhoven, Netherlands, 7/04/16. https://doi.org/10.1007/978-3-319-32582-8_7

Autonomous agent behaviour modelled in PRISM -- a case study. / Hoffmann, Ruth; Ireland, Murray; Miller, Alice et al.
Model Checking Software: 23rd International Symposium, SPIN 2016, Co-located with ETAPS 2016, Eindhoven, The Netherlands, April 7-8, 2016, Proceedings. ed. / Dragan Bošnački; Anton Wijs. Cham: Springer, 2016. p. 104-110 (Lecture Notes in Computer Science; Vol. 9641).

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

TY - GEN

T1 - Autonomous agent behaviour modelled in PRISM -- a case study

AU - Hoffmann, Ruth

AU - Ireland, Murray

AU - Miller, Alice

AU - Norman, Gethin

AU - Veres, Sandor

N1 - Conference code: 23

PY - 2016

Y1 - 2016

N2 - Formal verification of agents representing robot behaviour is a growing area due to the demand that autonomous systems have to be proven safe. In this paper we present an abstract definition of autonomy which can be used to model autonomous scenarios and propose the use of small-scale simulation models representing abstract actions to infer quantitative data. To demonstrate the applicability of the approach we build and verify a model of an unmanned aerial vehicle (UAV) in an exemplary autonomous scenario, utilising this approach.

AB - Formal verification of agents representing robot behaviour is a growing area due to the demand that autonomous systems have to be proven safe. In this paper we present an abstract definition of autonomy which can be used to model autonomous scenarios and propose the use of small-scale simulation models representing abstract actions to infer quantitative data. To demonstrate the applicability of the approach we build and verify a model of an unmanned aerial vehicle (UAV) in an exemplary autonomous scenario, utilising this approach.

U2 - 10.1007/978-3-319-32582-8_7

DO - 10.1007/978-3-319-32582-8_7

M3 - Conference contribution

SN - 9783319325811

T3 - Lecture Notes in Computer Science

SP - 104

EP - 110

BT - Model Checking Software

A2 - Bošnački, Dragan

A2 - Wijs, Anton

PB - Springer

CY - Cham

T2 - 23rd International SPIN Symposium on Model Checking of Software

Y2 - 7 April 2016 through 8 April 2016

ER -

Hoffmann R, Ireland M, Miller A, Norman G, Veres S. Autonomous agent behaviour modelled in PRISM -- a case study. In Bošnački D, Wijs A, editors, Model Checking Software: 23rd International Symposium, SPIN 2016, Co-located with ETAPS 2016, Eindhoven, The Netherlands, April 7-8, 2016, Proceedings. Cham: Springer. 2016. p. 104-110. (Lecture Notes in Computer Science). Epub 2016 Apr 8. doi: 10.1007/978-3-319-32582-8_7

Autonomous agent behaviour modelled in PRISM -- a case study

Abstract

Publication series

Conference

Access to Document

Fingerprint

Cite this