Autonomous agent behaviour modelled in PRISM -- a case study

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

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

12 Citations (Scopus)
3 Downloads (Pure)


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 languageEnglish
Title of host publicationModel Checking Software
Subtitle of host publication23rd International Symposium, SPIN 2016, Co-located with ETAPS 2016, Eindhoven, The Netherlands, April 7-8, 2016, Proceedings
EditorsDragan Bošnački, Anton Wijs
Place of PublicationCham
ISBN (Electronic)9783319325828
ISBN (Print)9783319325811
Publication statusPublished - 2016
Event23rd International SPIN Symposium on Model Checking of Software - TU/e Science park of the Eindhoven University of Technology, Eindhoven, Netherlands
Duration: 7 Apr 20168 Apr 2016
Conference number: 23

Publication series

NameLecture Notes in Computer Science
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349


Conference23rd International SPIN Symposium on Model Checking of Software
Abbreviated titleSPIN
Internet address


Dive into the research topics of 'Autonomous agent behaviour modelled in PRISM -- a case study'. Together they form a unique fingerprint.

Cite this