Collaborative models for autonomous systems controller synthesis

Douglas Fraser, Ruben Giaquinta, Ruth Hoffmann, Murray Ireland, Alice Miller, Gethin Norman

Research output: Contribution to journalArticlepeer-review

2 Citations (Scopus)
3 Downloads (Pure)


We show how detailed simulation models and abstract Markov models can be developed collaboratively to generate and implement effective controllers for autonomous agent search and retrieve missions. We introduce a concrete simulation model of an Unmanned Aerial Vehicle (UAV). We then show how the probabilistic model checker PRISM is used for optimal strategy synthesis for a sequence of scenarios relevant to UAVs and potentially other autonomous agent systems. For each scenario we demonstrate how it can be modelled using PRISM, give model checking statistics and present the synthesised optimal strategies. We then show how our strategies can be returned to the controller for the simulation model and provide experimental results to demonstrate the effectiveness of one such strategy. Finally we explain how our models can be adapted, using symmetry, for use on larger search areas, and demonstrate the feasibility of this approach.
Original languageEnglish
Pages (from-to)157–186
Number of pages30
JournalFormal Aspects of Computing
Issue number2-3
Early online date16 Apr 2020
Publication statusPublished - Jul 2020


  • Autonomous systems
  • Formal verification
  • Probabilistic model checking
  • Strategy synthesis


Dive into the research topics of 'Collaborative models for autonomous systems controller synthesis'. Together they form a unique fingerprint.

Cite this