Autonomous agent behaviour modelled in PRISM: a case study