{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,28]],"date-time":"2025-03-28T04:15:00Z","timestamp":1743135300023,"version":"3.40.3"},"publisher-location":"Cham","reference-count":21,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783030613617"},{"type":"electronic","value":"9783030613624"}],"license":[{"start":{"date-parts":[[2020,1,1]],"date-time":"2020-01-01T00:00:00Z","timestamp":1577836800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2020,1,1]],"date-time":"2020-01-01T00:00:00Z","timestamp":1577836800000},"content-version":"vor","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":[[2020]]},"DOI":"10.1007\/978-3-030-61362-4_20","type":"book-chapter","created":{"date-parts":[[2020,10,28]],"date-time":"2020-10-28T13:02:36Z","timestamp":1603890156000},"page":"350-367","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":4,"title":["Probabilistic Mission Planning and Analysis for Multi-agent Systems"],"prefix":"10.1007","author":[{"given":"Rong","family":"Gu","sequence":"first","affiliation":[]},{"given":"Eduard","family":"Enoiu","sequence":"additional","affiliation":[]},{"given":"Cristina","family":"Seceleanu","sequence":"additional","affiliation":[]},{"given":"Kristina","family":"Lundqvist","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2020,10,29]]},"reference":[{"issue":"2","key":"20_CR1","doi-asserted-by":"publisher","first-page":"272","DOI":"10.1016\/j.tcs.2005.11.018","volume":"354","author":"Y Abdedda\u0131","year":"2006","unstructured":"Abdedda\u0131, Y., Asarin, E., Maler, O., et al.: Scheduling with timed automata. Theor. Comput. Sci. 354(2), 272\u2013300 (2006)","journal-title":"Theor. Comput. Sci."},{"key":"20_CR2","doi-asserted-by":"crossref","unstructured":"Al-Nuaimi, M., Qu, H., Veres, S.M.: A stochastically verifiable decision making framework for autonomous ground vehicles. In: 2018 IEEE International Conference on Intelligence and Safety for Robotics (ISR), pp. 26\u201333. IEEE (2018)","DOI":"10.1109\/IISR.2018.8535911"},{"key":"20_CR3","unstructured":"Ayala, A.M., Andersson, S.B., Belta, C.: Temporal logic control in dynamic environments with probabilistic satisfaction guarantees. In: 2011 IEEE\/RSJ International Conference on Intelligent Robots and Systems, pp. 3108\u20133113. IEEE (2011)"},{"key":"20_CR4","doi-asserted-by":"crossref","unstructured":"Chandler, P., Pachter, M.: Research issues in autonomous control of tactical UAVs. In: Proceedings of the 1998 American Control Conference. ACC (IEEE Cat. No. 98CH36207). IEEE (1998)","DOI":"10.1109\/ACC.1998.694698"},{"key":"20_CR5","doi-asserted-by":"publisher","first-page":"533","DOI":"10.1613\/jair.2994","volume":"39","author":"K Daniel","year":"2010","unstructured":"Daniel, K., Nash, A., Koenig, S., Felner, A.: Theta*: any-angle path planning on grids. J. Artif. Intell. Res. 39, 533\u2013579 (2010)","journal-title":"J. Artif. Intell. Res."},{"key":"20_CR6","unstructured":"David, A., et al.: Statistical model checking for stochastic hybrid systems. arXiv preprint \narXiv:1208.3856\n\n (2012)"},{"key":"20_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"206","DOI":"10.1007\/978-3-662-46681-0_16","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"A David","year":"2015","unstructured":"David, A., Jensen, P.G., Larsen, K.G., Miku\u010dionis, M., Taankvist, J.H.:  Uppaal stratego. In: Baier, C., Tinelli, C. (eds.) TACAS 2015. LNCS, vol. 9035, pp. 206\u2013211. Springer, Heidelberg (2015). \nhttps:\/\/doi.org\/10.1007\/978-3-662-46681-0_16"},{"key":"20_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"21","DOI":"10.1007\/BFb0013570","volume-title":"Intelligent Agents III Agent Theories, Architectures, and Languages","author":"S Franklin","year":"1997","unstructured":"Franklin, S., Graesser, A.: Is it an agent, or just a program?: A taxonomy for autonomous agents. In: M\u00fcller, J.P., Wooldridge, M.J., Jennings, N.R. (eds.) ATAL 1996. LNCS, vol. 1193, pp. 21\u201335. Springer, Heidelberg (1997). \nhttps:\/\/doi.org\/10.1007\/BFb0013570"},{"key":"20_CR9","doi-asserted-by":"crossref","unstructured":"Gu, R., Enoiu, E.P., Seceleanu, C.: TAMAA: UPPAAL-based mission planning for autonomous agents. In: 35th ACM\/SIGAPP Symposium on Applied Computing SAC2020. ACM (2019)","DOI":"10.1145\/3341105.3374001"},{"key":"20_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"73","DOI":"10.1007\/978-3-030-58298-2_2","volume-title":"Formal Methods for Industrial Critical Systems","author":"R Gu","year":"2020","unstructured":"Gu, R., Enoiu, E., Seceleanu, C., Lundqvist, K.: Verifiable and scalable mission-plan synthesis for autonomous agents. In: ter Beek, M.H., Ni\u010dkovi\u0107, D. (eds.) FMICS 2020. LNCS, vol. 12327, pp. 73\u201392. Springer, Cham (2020). \nhttps:\/\/doi.org\/10.1007\/978-3-030-58298-2_2"},{"key":"20_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"186","DOI":"10.1007\/978-3-030-20652-9_12","volume-title":"NASA Formal Methods","author":"R Gu","year":"2019","unstructured":"Gu, R., Marinescu, R., Seceleanu, C., Lundqvist, K.: Towards a two-layer framework for verifying autonomous vehicles. In: Badger, J.M., Rozier, K.Y. (eds.) NFM 2019. LNCS, vol. 11460, pp. 186\u2013203. Springer, Cham (2019). \nhttps:\/\/doi.org\/10.1007\/978-3-030-20652-9_12"},{"key":"20_CR12","doi-asserted-by":"publisher","first-page":"265","DOI":"10.1007\/978-3-642-59615-5_13","volume-title":"Verification of Digital and Hybrid Systems NATO ASI Series (Series F: Computer and Systems Sciences)","author":"TA Henzinger","year":"2000","unstructured":"Henzinger, T.A.: The theory of hybrid automata. In: Inan, M.K., Kurshan, R.P. (eds.) Verification of Digital and Hybrid Systems NATO ASI Series (Series F: Computer and Systems Sciences), vol. 170, pp. 265\u2013292. Springer, Heidelberg (2000). \nhttps:\/\/doi.org\/10.1007\/978-3-642-59615-5_13"},{"key":"20_CR13","doi-asserted-by":"publisher","DOI":"10.7551\/mitpress\/10187.001.0001","volume-title":"Decision Making Under Uncertainty: Theory and Application","author":"MJ Kochenderfer","year":"2015","unstructured":"Kochenderfer, M.J.: Decision Making Under Uncertainty: Theory and Application. MIT press, Cambridge (2015)"},{"issue":"1\u20132","key":"20_CR14","doi-asserted-by":"publisher","first-page":"134","DOI":"10.1007\/s100090050010","volume":"1","author":"KG Larsen","year":"1997","unstructured":"Larsen, K.G., Pettersson, P., Yi, W.: UPPAAL in a nutshell. Int. J. Softw. Tools Technol. Transf. 1(1\u20132), 134\u2013152 (1997)","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"key":"20_CR15","unstructured":"LaValle, S.M.: Rapidly-exploring random trees: a new tool for path planning. Technical report, Computer Science Department, Iowa State University, October 1998"},{"issue":"1","key":"20_CR16","doi-asserted-by":"publisher","first-page":"10766","DOI":"10.1016\/j.ifacol.2017.08.2280","volume":"50","author":"A Nikou","year":"2017","unstructured":"Nikou, A., Tumova, J., Dimarogonas, D.V.: Probabilistic plan synthesis for coupled multi-agent systems. IFAC-PapersOnLine 50(1), 10766\u201310771 (2017)","journal-title":"IFAC-PapersOnLine"},{"issue":"2","key":"20_CR17","first-page":"480","volume":"64","author":"S Sadraddini","year":"2018","unstructured":"Sadraddini, S., Belta, C.: Formal synthesis of control strategies for positive monotone systems. IEEE Trans. Autom. Control 64(2), 480\u2013495 (2018)","journal-title":"IEEE Trans. Autom. Control"},{"key":"20_CR18","doi-asserted-by":"crossref","unstructured":"Sekizawa, T., Otsuki, F., Ito, K., Okano, K.: Behavior verification of autonomous robot vehicle in consideration of errors and disturbances. In: 2015 IEEE 39th Annual Computer Software and Applications Conference, vol. 3, pp. 550\u2013555. IEEE (2015)","DOI":"10.1109\/COMPSAC.2015.268"},{"key":"20_CR19","doi-asserted-by":"publisher","first-page":"28","DOI":"10.3389\/fnbot.2018.00028","volume":"12","author":"LA Trinh","year":"2018","unstructured":"Trinh, L.A., Ekstr\u00f6m, M., C\u00fcr\u00fckl\u00fc, B.: Toward shared working space of human and robotic agents through dipole flow field for dependable path planning. Front. Neurorobot. 12, 28 (2018)","journal-title":"Front. Neurorobot."},{"key":"20_CR20","unstructured":"Wang, Y., Chaudhuri, S., Kavraki, L.E.: Bounded policy synthesis for POMDPs with safe-reachability objectives. In: International Conference on Autonomous Agents and Multi Agent Systems. IFAAMS, ACM (2018)"},{"key":"20_CR21","unstructured":"Watkins, C.J.C.H.: Learning from delayed rewards, King\u2019s College, Cambridge (1989)"}],"container-title":["Lecture Notes in Computer Science","Leveraging Applications of Formal Methods, Verification and Validation: Verification Principles"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-61362-4_20","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,10,28]],"date-time":"2020-10-28T13:07:54Z","timestamp":1603890474000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-030-61362-4_20"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020]]},"ISBN":["9783030613617","9783030613624"],"references-count":21,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-61362-4_20","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2020]]},"assertion":[{"value":"29 October 2020","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"ISoLA","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Symposium on Leveraging Applications of Formal Methods","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Rhodes","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Greece","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2020","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"20 October 2020","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"30 October 2020","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"9","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"isola2020","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"http:\/\/isola-conference.org\/isola2020\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}