Autonomous Agent Behaviour Modelled in PRISM -- A Case Study
This work addresses safety verification for autonomous systems like robots, but it appears incremental as it builds on existing formal verification methods.
The paper tackled the problem of ensuring safety in autonomous systems by proposing an abstract definition of autonomy and using small-scale simulation models to infer quantitative data, demonstrated through building and verifying a model of an unmanned aerial vehicle in an autonomous scenario.
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.