{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,2]],"date-time":"2025-11-02T16:44:05Z","timestamp":1762101845918,"version":"3.41.0"},"publisher-location":"Cham","reference-count":7,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319325811"},{"type":"electronic","value":"9783319325828"}],"license":[{"start":{"date-parts":[[2016,1,1]],"date-time":"2016-01-01T00:00:00Z","timestamp":1451606400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2016]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>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.<\/jats:p>","DOI":"10.1007\/978-3-319-32582-8_7","type":"book-chapter","created":{"date-parts":[[2016,4,7]],"date-time":"2016-04-07T10:04:23Z","timestamp":1460023463000},"page":"104-110","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":13,"title":["Autonomous Agent Behaviour Modelled in PRISM \u2013 A Case Study"],"prefix":"10.1007","author":[{"given":"Ruth","family":"Hoffmann","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Murray","family":"Ireland","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Alice","family":"Miller","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Gethin","family":"Norman","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Sandor","family":"Veres","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2016,4,8]]},"reference":[{"key":"7_CR1","doi-asserted-by":"crossref","unstructured":"Chaimowicz, L., Campos, M.F.M., Kumar, V.: Hybrid systems modeling of cooperative robots. In: Proceedings International Conference Robotics and Automation (ICRA 2003), pp. 4086\u20134091. IEEE Press, New York (2003)","DOI":"10.1109\/ROBOT.2003.1242225"},{"key":"7_CR2","doi-asserted-by":"crossref","unstructured":"Cook, J., Hu, G.: Experimental verification and algorithm of a multi-robot cooperative control method. In: Proceedings IEEE\/ASME International Conference Advanced Intelligent Mechatronics (AIM 2010), pp. 109\u2013114. IEEE Press, New York (2010)","DOI":"10.1109\/AIM.2010.5695917"},{"key":"7_CR3","doi-asserted-by":"crossref","unstructured":"Dennis, L., Fisher, M., Lincoln, N., Lisitsa, A., Veres, S.: Practical verification of decision-making in agent-based autonomous systems. Autom. Softw. Eng., pp. 1\u201355 (2014). http:\/\/link.springer.com\/article\/10.1007\/s10515-014-0168-9","DOI":"10.1007\/s10515-014-0168-9"},{"issue":"3","key":"7_CR4","doi-asserted-by":"publisher","first-page":"246","DOI":"10.1007\/s10703-010-0097-6","volume":"36","author":"M Kattenbelt","year":"2010","unstructured":"Kattenbelt, M., Kwiatkowska, M., Norman, G., Parker, D.: A game-based abstraction-refinement framework for Markov decision processes. Formal Methods Syst. Des. 36(3), 246\u2013280 (2010)","journal-title":"Formal Methods Syst. Des."},{"key":"7_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"585","DOI":"10.1007\/978-3-642-22110-1_47","volume-title":"Computer Aided Verification","author":"M Kwiatkowska","year":"2011","unstructured":"Kwiatkowska, M., Norman, G., Parker, D.: PRISM 4.0: verification of probabilistic real-time systems. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 585\u2013591. Springer, Heidelberg (2011)"},{"key":"7_CR6","unstructured":"PRISM model repository (2016). http:\/\/dx.doi.org\/10.5525\/gla.researchdata.274"},{"issue":"2","key":"7_CR7","first-page":"155","volume":"225","author":"S Veres","year":"2011","unstructured":"Veres, S., Molnar, L., Lincoln, N., Morice, C.: Autonomous vehicle control systems\u00a0- a review of decision making. Proc. Inst. Mech. Eng. Part I: J. Syst. Control Eng. 225(2), 155\u2013195 (2011)","journal-title":"Proc. Inst. Mech. Eng. Part I: J. Syst. Control Eng."}],"container-title":["Lecture Notes in Computer Science","Model Checking Software"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-32582-8_7","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,2]],"date-time":"2025-06-02T07:04:19Z","timestamp":1748847859000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-319-32582-8_7"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016]]},"ISBN":["9783319325811","9783319325828"],"references-count":7,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-32582-8_7","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2016]]},"assertion":[{"value":"8 April 2016","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}