[GHI+18] Ruben Giaquinta, Ruth Hoffmann, Murray Ireland, Alice Miller and Gethin Norman. Strategy Synthesis for Autonomous Agents using PRISM. In Proc. 10th NASA Formal Methods Symposium (NFM 2018), volume 10811 of LNCS, pages 220-236, Springer. March 2018. [pdf] [bib] [Synthesises controllers for unmanned aerial vehicles using probabilistic model checking and PRISM.]
Downloads:  pdf pdf (2.8 MB)  bib bib
Notes: The original publication is available at link.springer.com.
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.