{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,25]],"date-time":"2025-11-25T06:52:18Z","timestamp":1764053538190},"publisher-location":"Cham","reference-count":37,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319779348"},{"type":"electronic","value":"9783319779355"}],"license":[{"start":{"date-parts":[[2018,1,1]],"date-time":"2018-01-01T00:00:00Z","timestamp":1514764800000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2018]]},"DOI":"10.1007\/978-3-319-77935-5_16","type":"book-chapter","created":{"date-parts":[[2018,3,10]],"date-time":"2018-03-10T15:02:34Z","timestamp":1520694154000},"page":"220-236","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":11,"title":["Strategy Synthesis for Autonomous Agents Using PRISM"],"prefix":"10.1007","author":[{"given":"Ruben","family":"Giaquinta","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Ruth","family":"Hoffmann","sequence":"additional","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"}]}],"member":"297","published-online":{"date-parts":[[2018,3,11]]},"reference":[{"key":"16_CR1","first-page":"7","volume":"15","author":"R Alur","year":"1999","unstructured":"Alur, R., Henzinger, T.: Reactive modules. FMSD 15, 7\u201348 (1999)","journal-title":"FMSD"},{"key":"16_CR2","series-title":"Lecture Notes in Economics and Mathematical Systems","doi-asserted-by":"publisher","first-page":"21","DOI":"10.1007\/978-3-540-48271-0_2","volume-title":"Cooperative Systems","author":"C Bohn","year":"2007","unstructured":"Bohn, C.: Heuristics for designing the control of a UAV fleet with model checking. In: Grundel, D., Murphey, R., Pardalos, P., Prokopyev, O. (eds.) Cooperative Systems. Lecture Notes in Economics and Mathematical Systems, vol. 588, pp. 21\u201336. Springer, Heidelberg (2007). https:\/\/doi.org\/10.1007\/978-3-540-48271-0_2"},{"key":"16_CR3","doi-asserted-by":"crossref","first-page":"16","DOI":"10.1145\/2579821","volume":"15","author":"K Chatterjee","year":"2014","unstructured":"Chatterjee, K., Doyen, L.: Partial-observation stochastic games: how to win when belief fails. ACM Trans. Comput. Log. 15, 16 (2014)","journal-title":"ACM Trans. Comput. Log."},{"key":"16_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"185","DOI":"10.1007\/978-3-642-36742-7_13","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"T Chen","year":"2013","unstructured":"Chen, T., Forejt, V., Kwiatkowska, M., Parker, D., Simaitis, A.: PRISM-games: a model checker for stochastic multi-player games. In: Piterman, N., Smolka, S.A. (eds.) TACAS 2013. LNCS, vol. 7795, pp. 185\u2013191. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-36742-7_13"},{"key":"16_CR5","doi-asserted-by":"crossref","unstructured":"Choi, J.: Model checking for decision making behaviour of heterogeneous multi-agent autonomous system. Ph.D. thesis, Cranfield University (2012)","DOI":"10.2514\/6.2011-6239"},{"issue":"3","key":"16_CR6","first-page":"305","volume":"23","author":"L Dennis","year":"2016","unstructured":"Dennis, L., Fisher, M., Lincoln, N., Lisitsa, A., Veres, S.: Practical verification of decision-making in agent-based autonomous systems. ASE 23(3), 305\u2013359 (2016)","journal-title":"ASE"},{"key":"16_CR7","doi-asserted-by":"crossref","first-page":"1244","DOI":"10.1109\/TAC.2014.2298143","volume":"59","author":"X Ding","year":"2014","unstructured":"Ding, X., Smith, S., Belta, C., Rus, D.: Optimal control of Markov decision processes with linear temporal logic constraints. IEEE Trans. Autom. Control 59, 1244\u20131257 (2014)","journal-title":"IEEE Trans. Autom. Control"},{"issue":"2","key":"16_CR8","first-page":"1","volume":"11","author":"K Draeger","year":"2015","unstructured":"Draeger, K., Forejt, V., Kwiatkowska, M., Parker, D., Ujma, M.: Permissive controller synthesis for probabilistic systems. LMCS 11(2), 1\u201334 (2015)","journal-title":"LMCS"},{"key":"16_CR9","first-page":"1","volume":"4","author":"K Etessami","year":"2008","unstructured":"Etessami, K., Kwiatkowska, M., Vardi, M., Yannakakis, M.: Multi-objective model checking of Markov decision processes. LMCS 4, 1\u201321 (2008)","journal-title":"LMCS"},{"key":"16_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"53","DOI":"10.1007\/978-3-642-21455-4_3","volume-title":"Formal Methods for Eternal Networked Software Systems","author":"V Forejt","year":"2011","unstructured":"Forejt, V., Kwiatkowska, M., Norman, G., Parker, D.: Automated verification techniques for probabilistic systems. In: Bernardo, M., Issarny, V. (eds.) SFM 2011. LNCS, vol. 6659, pp. 53\u2013113. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-21455-4_3"},{"key":"16_CR11","doi-asserted-by":"crossref","unstructured":"Fu, J., Topcu, U.: Computational methods for stochastic control with metric interval temporal logic specifications. In: Proceedings of CDC 2015 (2015)","DOI":"10.1109\/CDC.2015.7403395"},{"key":"16_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"104","DOI":"10.1007\/978-3-319-32582-8_7","volume-title":"Model Checking Software","author":"R Hoffmann","year":"2016","unstructured":"Hoffmann, R., Ireland, M., Miller, A., Norman, G., Veres, S.: Autonomous agent behaviour modelled in PRISM \u2013 a case study. In: Bo\u0161na\u010dki, D., Wijs, A. (eds.) SPIN 2016. LNCS, vol. 9641, pp. 104\u2013110. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-32582-8_7"},{"key":"16_CR13","series-title":"Lecture Notes in Control and Information Sciences","doi-asserted-by":"publisher","first-page":"69","DOI":"10.1007\/978-3-642-37694-8_4","volume-title":"Recent Advances in Research on Unmanned Aerial Vehicles","author":"L Humphrey","year":"2013","unstructured":"Humphrey, L.: Model checking for verification in UAV cooperative control applications. In: Fahroo, F., Wang, L., Yin, G. (eds.) Recent Advances in Research on Unmanned Aerial Vehicles. LNCIS, vol. 444, pp. 69\u2013117. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-37694-8_4"},{"key":"16_CR14","unstructured":"Ireland, M., Hoffmann, R., Miller, A., Norman, G., Veres, S.: A continuous-time model of an autonomous aerial vehicle to inform and validate formal verification methods. http:\/\/arxiv.org\/abs\/1609.00177v1"},{"key":"16_CR15","doi-asserted-by":"crossref","unstructured":"Kalra, N., Paddock, S.: Driving to safety: how many miles of driving would it take to demonstrate autonomous vehicle reliability? Transp. Res. Part A: Policy Pract. 94, 182\u2013193 (2016)","DOI":"10.7249\/RR1478"},{"key":"16_CR16","first-page":"246","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. FMSD 36, 246\u2013280 (2010)","journal-title":"FMSD"},{"key":"16_CR17","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4684-9455-6","volume-title":"Denumerable Markov Chains","author":"J Kemeny","year":"1976","unstructured":"Kemeny, J., Snell, J., Knapp, A.: Denumerable Markov Chains. Springer, New York (1976). https:\/\/doi.org\/10.1007\/978-1-4684-9455-6"},{"issue":"2","key":"16_CR18","doi-asserted-by":"crossref","first-page":"199","DOI":"10.1016\/j.robot.2011.10.005","volume":"60","author":"S Konur","year":"2012","unstructured":"Konur, S., Dixon, C., Fisher, M.: Analysing robot swarm behaviour via probabilistic model checking. Robot. Auton. Syst. 60(2), 199\u2013213 (2012)","journal-title":"Robot. Auton. Syst."},{"key":"16_CR19","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). https:\/\/doi.org\/10.1007\/978-3-642-22110-1_47"},{"key":"16_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"5","DOI":"10.1007\/978-3-319-02444-8_2","volume-title":"Automated Technology for Verification and Analysis","author":"M Kwiatkowska","year":"2013","unstructured":"Kwiatkowska, M., Parker, D.: Automated verification and strategy synthesis for probabilistic systems. In: Van Hung, D., Ogawa, M. (eds.) ATVA 2013. LNCS, vol. 8172, pp. 5\u201322. Springer, Cham (2013). https:\/\/doi.org\/10.1007\/978-3-319-02444-8_2"},{"key":"16_CR21","doi-asserted-by":"crossref","unstructured":"Lacerda, B., Parker, D., Hawes, N.: Multi-objective policy generation for mobile robots under probabilistic time-bounded guarantees. In: Proceedings of ICAPS 2017 (2017)","DOI":"10.1609\/icaps.v27i1.13865"},{"key":"16_CR22","doi-asserted-by":"crossref","first-page":"2031","DOI":"10.1109\/TAC.2015.2398883","volume":"60","author":"M Lahijanian","year":"2015","unstructured":"Lahijanian, M., Andersson, S., Belta, C.: Formal verification and synthesis for discrete-time stochastic systems. IEEE Trans. Autom. Control 60, 2031\u20132045 (2015)","journal-title":"IEEE Trans. Autom. Control"},{"key":"16_CR23","doi-asserted-by":"crossref","unstructured":"Lahijanian, M., Kwiatkowska, M.: Specification revision for Markov decision processes with optimal trade-off. In: Proceedings of CDC 2016. IEEE (2016)","DOI":"10.1109\/CDC.2016.7799414"},{"key":"16_CR24","unstructured":"Liu, W., Winfield, A., Sa, J.: Modelling swarm robotic systems: a case study in collective foraging. In: Proceedings of TAROS 2007 (2007)"},{"key":"16_CR25","doi-asserted-by":"crossref","first-page":"8","DOI":"10.1145\/1132960.1132962","volume":"36","author":"A Miller","year":"2006","unstructured":"Miller, A., Donaldson, A., Calder, M.: Symmetry in temporal logic model checking. Comput. Surve. 36, 8 (2006)","journal-title":"Comput. Surve."},{"key":"16_CR26","doi-asserted-by":"crossref","first-page":"354","DOI":"10.1007\/s11241-017-9269-4","volume":"53","author":"G Norman","year":"2017","unstructured":"Norman, G., Parker, D., Zou, X.: Verification and control of partially observable probabilistic systems. Real-Time Syst. 53, 354\u2013402 (2017)","journal-title":"Real-Time Syst."},{"key":"16_CR27","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"462","DOI":"10.1007\/978-3-319-11900-7_39","volume-title":"Simulation, Modeling, and Programming for Autonomous Robots","author":"M O\u2019Brien","year":"2014","unstructured":"O\u2019Brien, M., Arkin, R.C., Harrington, D., Lyons, D., Jiang, S.: Automatic verification of autonomous robot missions. In: Brugali, D., Broenink, J.F., Kroeger, T., MacDonald, B.A. (eds.) SIMPAR 2014. LNCS (LNAI), vol. 8810, pp. 462\u2013473. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-11900-7_39"},{"key":"16_CR28","doi-asserted-by":"crossref","first-page":"1095","DOI":"10.1073\/pnas.39.10.1953","volume":"39","author":"L Shapley","year":"1953","unstructured":"Shapley, L.: Stochastic games. Proc. Natl. Acad. Sci. 39, 1095\u20131100 (1953)","journal-title":"Proc. Natl. Acad. Sci."},{"key":"16_CR29","unstructured":"Sharan, R.: Formal methods for control synthesis in partially observed environments: application to autonomous robotic manipulation. Ph.D. thesis, California Institute of Technology (2014)"},{"key":"16_CR30","unstructured":"Soudjani, S., Majumdar, R.: Controller synthesis for reward collecting Markov processes in continuous space. In: Proceedings of HSCC 2017. ACM (2017)"},{"key":"16_CR31","doi-asserted-by":"crossref","unstructured":"Svore\u0148ov\u00e1, M., Chmel\u00edk, M., Leahy, K., Eniser, H., Chatterjee, K., \u010cern\u00e1, I., Belta, C.: Temporal logic motion planning using POMDPs with parity objectives: case study paper. In: Proceedings of HSCC 2015. ACM (2015)","DOI":"10.1145\/2728606.2728617"},{"key":"16_CR32","doi-asserted-by":"crossref","unstructured":"Svore\u0148ov\u00e1, M., K\u0159et\u00ednsk\u00fd, J., Chmel\u00edk, M., Chatterjee, K., Cerna, I., Belta, C.: Temporal logic control for stochastic linear systems using abstraction refinement of probabilistic games. In: Proceedings of HSCC 2015. ACM (2015)","DOI":"10.1145\/2728606.2728608"},{"key":"16_CR33","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"228","DOI":"10.1007\/978-3-642-24270-0_17","volume-title":"Computer Safety, Reliability, and Security","author":"M Webster","year":"2011","unstructured":"Webster, M., Fisher, M., Cameron, N., Jump, M.: Formal methods for the certification of autonomous unmanned aircraft systems. In: Flammini, F., Bologna, S., Vittorini, V. (eds.) SAFECOMP 2011. LNCS, vol. 6894, pp. 228\u2013242. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-24270-0_17"},{"key":"16_CR34","unstructured":"Wilson, J.: Drones hacked and crashed by research team to expose design flaws. Engineering and Technology (2016)"},{"key":"16_CR35","doi-asserted-by":"crossref","unstructured":"Wolff, E., Topcu, U., Murray, R.: Robust control of uncertain Markov decision processes with temporal logic specifications. In: Proceedings of CSC 2012. IEEE (2012)","DOI":"10.1109\/CDC.2012.6426174"},{"key":"16_CR36","doi-asserted-by":"crossref","unstructured":"Yoo, C., Finch, R., Sukkarieh, S.: Provably-correct stochastic motion planning with safety constraints. In: Proceedings of ICRA 2013. IEEE (2013)","DOI":"10.1109\/ICRA.2013.6630692"},{"key":"16_CR37","unstructured":"http:\/\/www.prismmodelchecker.org\/files\/nfm18\/"}],"container-title":["Lecture Notes in Computer Science","NASA Formal Methods"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-77935-5_16","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,9,1]],"date-time":"2023-09-01T15:06:52Z","timestamp":1693580812000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-77935-5_16"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018]]},"ISBN":["9783319779348","9783319779355"],"references-count":37,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-77935-5_16","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2018]]}}}