{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,4]],"date-time":"2025-11-04T16:21:49Z","timestamp":1762273309999,"version":"3.41.0"},"reference-count":53,"publisher":"Association for Computing Machinery (ACM)","issue":"7","license":[{"start":{"date-parts":[[2024,9,27]],"date-time":"2024-09-27T00:00:00Z","timestamp":1727395200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Softw. Eng. Methodol."],"published-print":{"date-parts":[[2024,9,30]]},"abstract":"<jats:p>Mission planning for multi-agent autonomous systems aims to generate feasible and optimal mission plans that satisfy given requirements. In this article, we propose a tool-supported mission-planning methodology that combines (i) a path-planning algorithm for synthesizing path plans that are safe in environments with complex road conditions, and (ii) a task-scheduling method for synthesizing task plans that schedule the tasks in the right and fastest order, taking into account the planned paths. The task-scheduling method is based on model checking, which provides means of automatically generating task execution orders that satisfy the requirements and ensure the correctness and efficiency of the plans by construction. We implement our approach in a tool named MALTA, which offers a user-friendly GUI for configuring mission requirements, a module for path planning, an integration with the model checker UPPAAL, and functions for automatic generation of formal models, and parsing of the execution traces of models. Experiments with the tool demonstrate its applicability and performance in various configurations of an industrial case study of an autonomous quarry. We also show the adaptability of our tool by employing it in a special case of an industrial case study.<\/jats:p>","DOI":"10.1145\/3672445","type":"journal-article","created":{"date-parts":[[2024,6,12]],"date-time":"2024-06-12T21:28:32Z","timestamp":1718227712000},"page":"1-46","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":4,"title":["Synthesis and Verification of Mission Plans for Multiple Autonomous Agents under Complex Road Conditions"],"prefix":"10.1145","volume":"33","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-0570-6005","authenticated-orcid":false,"given":"Rong","family":"Gu","sequence":"first","affiliation":[{"name":"M\u00e4lardalen University, V\u00e4ster\u00e5s, Sweden"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-7357-705X","authenticated-orcid":false,"given":"Eduard","family":"Baranov","sequence":"additional","affiliation":[{"name":"UCLouvain, Louvain-la-Neuve, Belgium"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-9437-6599","authenticated-orcid":false,"given":"Afshin","family":"Ameri","sequence":"additional","affiliation":[{"name":"M\u00e4lardalen University, V\u00e4ster\u00e5s, Sweden"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-2870-2680","authenticated-orcid":false,"given":"Cristina","family":"Seceleanu","sequence":"additional","affiliation":[{"name":"M\u00e4lardalen University, V\u00e4ster\u00e5s, Sweden"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-2416-4205","authenticated-orcid":false,"given":"Eduard Paul","family":"Enoiu","sequence":"additional","affiliation":[{"name":"M\u00e4lardalen University, V\u00e4ster\u00e5s, Sweden"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-5224-8302","authenticated-orcid":false,"given":"Baran","family":"C\u00fcr\u00fckl\u00fc","sequence":"additional","affiliation":[{"name":"M\u00e4lardalen University, V\u00e4ster\u00e5s, Sweden"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-2287-8925","authenticated-orcid":false,"given":"Axel","family":"Legay","sequence":"additional","affiliation":[{"name":"UCLouvain, Louvain-la-Neuve, Belgium"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-0904-3712","authenticated-orcid":false,"given":"Kristina","family":"Lundqvist","sequence":"additional","affiliation":[{"name":"M\u00e4lardalen University, V\u00e4ster\u00e5s, Sweden"}]}],"member":"320","published-online":{"date-parts":[[2024,9,27]]},"reference":[{"key":"e_1_3_2_2_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2005.11.018"},{"key":"e_1_3_2_3_2","first-page":"453","volume-title":"Proccedings of the 5th International Symposium on Robotics Research","author":"Alami Rachid","year":"1990","unstructured":"Rachid Alami, Thierry Simeon, and Jean-Paul Laumond. 1990. A geometrical approach to planning manipulation tasks. The case of discrete placements and grasps. In Proccedings of the 5th International Symposium on Robotics Research. MIT Press, 453\u2013463."},{"key":"e_1_3_2_4_2","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(94)90010-8"},{"key":"e_1_3_2_5_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-41540-6_14"},{"key":"e_1_3_2_6_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2018.02.021"},{"key":"e_1_3_2_7_2","doi-asserted-by":"publisher","DOI":"10.1109\/IEEECONF38699.2020.9389393"},{"key":"e_1_3_2_8_2","doi-asserted-by":"publisher","DOI":"10.1016\/0004-3702(94)90062-0"},{"key":"e_1_3_2_9_2","volume-title":"Principles of Model Checking","author":"Baier Christel","year":"2008","unstructured":"Christel Baier and Joost-Pieter Katoen. 2008. Principles of Model Checking. MIT Press."},{"key":"e_1_3_2_10_2","doi-asserted-by":"publisher","DOI":"10.23919\/ECC.2019.8795925"},{"key":"e_1_3_2_11_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-50763-7"},{"key":"e_1_3_2_12_2","first-page":"87","volume-title":"Proceedings of the Advanced Course on Petri Nets","author":"Bengtsson Johan","year":"2003","unstructured":"Johan Bengtsson and Wang Yi. 2003. Timed automata: Semantics, algorithms and tools. In Proceedings of the Advanced Course on Petri Nets. Springer, 87\u2013124."},{"key":"e_1_3_2_13_2","doi-asserted-by":"publisher","DOI":"10.1109\/ROBOT.2010.5509503"},{"key":"e_1_3_2_14_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-14295-6_31"},{"key":"e_1_3_2_15_2","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0055357"},{"key":"e_1_3_2_16_2","doi-asserted-by":"publisher","DOI":"10.1109\/TAC.2020.3006967"},{"key":"e_1_3_2_17_2","doi-asserted-by":"publisher","DOI":"10.3233\/AIS-150338"},{"key":"e_1_3_2_18_2","doi-asserted-by":"publisher","DOI":"10.1613\/jair.2994"},{"key":"e_1_3_2_19_2","doi-asserted-by":"publisher","DOI":"10.1007\/BF01386390"},{"key":"e_1_3_2_20_2","first-page":"2011","volume-title":"Proceedings of the NATO RTO Human Factors and Medicine Symp. HFM-135","author":"Eggers J. W.","year":"2006","unstructured":"J. W. Eggers and Mark H. Draper. 2006. Multi-UAV control for tactical reconnaissance and close air support missions: Operator perspectives and design challenges. In Proceedings of the NATO RTO Human Factors and Medicine Symp. HFM-135. 2011\u201306."},{"key":"e_1_3_2_21_2","doi-asserted-by":"publisher","DOI":"10.1109\/IROS.2010.5650371"},{"key":"e_1_3_2_22_2","first-page":"21","volume-title":"Proceedings of the International Workshop on Agent Theories, Architectures, and Languages","author":"Franklin Stan","year":"1996","unstructured":"Stan Franklin and Art Graesser. 1996. Is it an agent, or just a program?: A taxonomy for autonomous agents. In Proceedings of the International Workshop on Agent Theories, Architectures, and Languages. Springer, 21\u201335."},{"key":"e_1_3_2_23_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-22110-1_30"},{"key":"e_1_3_2_24_2","doi-asserted-by":"publisher","DOI":"10.1146\/annurev-control-091420-084139"},{"key":"e_1_3_2_25_2","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9781139583923"},{"key":"e_1_3_2_26_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-61362-4_20"},{"key":"e_1_3_2_27_2","first-page":"1624","article-title":"TAMAA: UPPAAL-based mission planning for autonomous agents","author":"Gu Rong","year":"2019","unstructured":"Rong Gu, Eduard P. Enoiu, and Cristina Seceleanu. 2019. TAMAA: UPPAAL-based mission planning for autonomous agents. In Proceedings of the 35th ACM\/SIGAPP Symposium On Applied Computing (SAC \u201920). 1624\u20131633.","journal-title":"Proceedings of the 35th ACM\/SIGAPP Symposium On Applied Computing (SAC \u201920)"},{"key":"e_1_3_2_28_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-58298-2_2"},{"key":"e_1_3_2_29_2","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-022-00657-z"},{"key":"e_1_3_2_30_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2022.102894"},{"key":"e_1_3_2_31_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-20652-9_12"},{"key":"e_1_3_2_32_2","doi-asserted-by":"publisher","DOI":"10.1109\/TSSC.1968.300136"},{"key":"e_1_3_2_33_2","doi-asserted-by":"publisher","DOI":"10.1177\/0278364909352098"},{"key":"e_1_3_2_34_2","doi-asserted-by":"publisher","DOI":"10.1109\/QEST.2006.59"},{"key":"e_1_3_2_35_2","volume-title":"Efficient Analysis and Synthesis of Complex Quantitative Systems","author":"Jensen Peter G.","year":"2018","unstructured":"Peter G. Jensen. 2018. Efficient Analysis and Synthesis of Complex Quantitative Systems. Aalborg Universitetsforlag."},{"key":"e_1_3_2_36_2","doi-asserted-by":"publisher","DOI":"10.1109\/70.508439"},{"key":"e_1_3_2_37_2","doi-asserted-by":"publisher","DOI":"10.1109\/ICUAS.2015.7152335"},{"key":"e_1_3_2_38_2","doi-asserted-by":"publisher","DOI":"10.1109\/TRO.2009.2030225"},{"key":"e_1_3_2_39_2","unstructured":"Steven M. LaValle. 1998. Rapidly-Exploring Random Trees: A New Tool for Path Planning. Technical Report."},{"key":"e_1_3_2_40_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-77489-8_10"},{"key":"e_1_3_2_41_2","doi-asserted-by":"publisher","DOI":"10.1109\/DASC.2016.7778109"},{"key":"e_1_3_2_42_2","doi-asserted-by":"publisher","DOI":"10.1145\/3342355"},{"key":"e_1_3_2_43_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.eswa.2013.07.033"},{"key":"e_1_3_2_44_2","doi-asserted-by":"publisher","DOI":"10.1177\/1729881416657974"},{"key":"e_1_3_2_45_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.automatica.2018.08.023"},{"key":"e_1_3_2_46_2","volume-title":"Shakey the Robot","author":"Nilsson Nils J.","year":"1984","unstructured":"Nils J. Nilsson. 1984. Shakey the Robot. Articial Intelligence Center, SRI International Menlo Park, California."},{"key":"e_1_3_2_47_2","doi-asserted-by":"publisher","DOI":"10.1007\/s10846-012-9759-5"},{"key":"e_1_3_2_48_2","doi-asserted-by":"publisher","DOI":"10.1109\/TSSC.1968.300136"},{"key":"e_1_3_2_49_2","doi-asserted-by":"publisher","DOI":"10.1051\/matecconf\/201815104011"},{"key":"e_1_3_2_50_2","doi-asserted-by":"publisher","unstructured":"Gopinadh Sirigineedi Antonios Tsourdos Brian A. White and Rafal Zbikowski. 2010. Modelling and verification of multiple UAV mission using SMV. DOI:10.4204\/EPTCS.20.3","DOI":"10.4204\/EPTCS.20.3"},{"key":"e_1_3_2_51_2","doi-asserted-by":"publisher","DOI":"10.1109\/MILCOM.2018.8599684"},{"key":"e_1_3_2_52_2","doi-asserted-by":"publisher","DOI":"10.1093\/biomet\/34.1-2.1"},{"key":"e_1_3_2_53_2","doi-asserted-by":"publisher","DOI":"10.1145\/2347583.2347592"},{"key":"e_1_3_2_54_2","author":"Woodrow Ian","year":"2005","unstructured":"Ian Woodrow, Chris Purry, Adam Mawby, and James Goodwin. 2005. Autonomous Auv Mission Planning and Replanning-Towards True Autonomy. Retrieved from https:\/\/api.semanticscholar.org\/CorpusID:14643879","journal-title":"Autonomous Auv Mission Planning and Replanning-Towards True Autonomy"}],"container-title":["ACM Transactions on Software Engineering and Methodology"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3672445","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3672445","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,19]],"date-time":"2025-06-19T00:58:01Z","timestamp":1750294681000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3672445"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,9,27]]},"references-count":53,"journal-issue":{"issue":"7","published-print":{"date-parts":[[2024,9,30]]}},"alternative-id":["10.1145\/3672445"],"URL":"https:\/\/doi.org\/10.1145\/3672445","relation":{},"ISSN":["1049-331X","1557-7392"],"issn-type":[{"type":"print","value":"1049-331X"},{"type":"electronic","value":"1557-7392"}],"subject":[],"published":{"date-parts":[[2024,9,27]]},"assertion":[{"value":"2022-04-12","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2024-05-03","order":2,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2024-09-27","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}