Abstract
Multi-Robot Task Allocation (MRTA) is a problem that arises in many application domains including package delivery, warehouse robotics, and healthcare. In this work, we consider the problem of MRTA for a dynamic stream of tasks with task deadlines and capacitated agents (capacity for more than one simultaneous task). Previous work commonly focuses on the static case, uses specialized algorithms for restrictive task specifications, or lacks guarantees. We propose an approach to Dynamic MRTA for capacitated robots that is based on Satisfiability Modulo Theories (SMT) solving and addresses these concerns. We show our approach is both sound and complete, and that the SMT encoding is general, enabling extension to a broader class of task specifications. We show how to leverage the incremental solving capabilities of SMT solvers, kee** learned information when allocating new tasks arriving online, and to solve non-incrementally, which we provide runtime comparisons of. Additionally, we provide an algorithm to start with a smaller but potentially incomplete encoding that can iteratively be adjusted to the complete encoding. We evaluate our method on a parameterized set of benchmarks encoding multi-robot delivery created from a graph abstraction of a hospital-like environment. The effectiveness of our approach is demonstrated using a range of encodings, including quantifier-free theories of uninterpreted functions and linear or bitvector arithmetic across multiple solvers.
P.-W. Chen—Denotes significant contribution.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Notes
- 1.
Link to extended version: https://arxiv.org/abs/2403.11737.
- 2.
Link to implementation and benchmarks: https://github.com/victoria-tuck/SMrTa.
References
Barbosa, H., et al.: cvc5: a versatile and industrial-strength SMT solver. In: TACAS 2022. LNCS, vol. 13243, pp. 415–442. Springer, Cham (2022). https://doi.org/10.1007/978-3-030-99524-9_24
Barrett, C., Sebastiani, R., Seshia, S.A., Tinelli, C.: Satisfiability modulo theories. In: Biere, A., Heule, M., van Maaren, H., Walsh, T. (eds.), Handbook of Satisfiability, chapter 33, pp. 1267–1329. IOS Press, second edition (2021)
Chakraa, H., Guerin, F., Leclercq, E., Lefebvre, D.: Optimization techniques for multi-robot task allocation problems: review on the state-of-the-art. Robot. Auton. Syst.168, 104492
Chen, Z., Alonso-Mora, J., Bai, X., Harabor, D.D., Stuckey, P.J.: Integrated task assignment and path planning for capacitated multi-agent pickup and delivery. IEEE Robot. Autom. Lett. 6(3), 5816–5823 (2021)
Das, G.P., Mcginnity, T.M., Coleman, S.A., Behera, L.: A distributed task allocation algorithm for a multi-robot system in healthcare facilities. J. Intell. Robot. Syst. 80, 33–58 (2015)
de Moura, L., Bjørner, N.: Z3: an efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337–340. Springer, Heidelberg (2008). https://doi.org/10.1007/978-3-540-78800-3_24
Gavran, I., Majumdar, R., Saha, I.: Antlab: a multi-robot task server. ACM Trans. Embed. Comput. Syst. (TECS) 16(5s), 1–19 (2017)
Hansson, H., Jonsson, B.: A logic for reasoning about time and reliability. Form. Aspects Comput. 6, 02 (1995)
Hekmatnejad, M., Pedrielli, G., Fainekos, G.: Optimal task scheduling with nonlinear costs using SMT solvers. In: IEEE International Conference on Automation Science and Engineering (CASE) (2019)
Jeon, S., Lee, J.: Vehicle routing problem with pickup and delivery of multiple robots for hospital logistics. In: 2016 16th International Conference on Control, Automation and Systems (ICCAS), pp. 1572–1575. IEEE (2016)
Jeon, S., Lee, J., Kim, J.: Multi-robot task allocation for real-time hospital logistics. In: IEEE International Conference on Systems, Man, and Cybernetics (SMC), pp. 2465–2470 (2017)
Lopes, R.B., Ferreira, C., Santos, B.S.: A simple and effective evolutionary algorithm for the capacitated location-routing problem. Comput. Oper. Res. 70, 155–162 (2016)
Majd, K., Yaghoubi, S., Yamaguchi, T., Hoxha, B., Prokhorov, D., Fainekos, G.: Safe navigation in human occupied environments using sampling and control barrier functions. In: IEEE/RSJ International Conference on Intelligent Robots and Systems (IROS) (2021)
Niemetz, A., Preiner, M.: Bitwuzla. In: Computer Aided Verification–35th International Conference, CAV, pp. 3–17. Springer, Cham (2023). https://doi.org/10.1007/978-3-031-37703-7_1
Nunes, E., Manner, M., Mitiche, H., Gini, M.: A taxonomy for task allocation problems with temporal and ordering constraints. Robot. Auton. Syst. 90, 55–70 (2017). Special Issue on New Research Frontiers for Intelligent Autonomous Systems
Okubo, T., Takahashi, M.: Simultaneous optimization of task allocation and path planning using mixed-integer programming for time and capacity constrained multi-agent pickup and delivery. In: 2022 22nd International Conference on Control, Automation and Systems (ICCAS), pp. 1088–1093. IEEE (2022)
Parwana, H., et al.: Feasible space monitoring for multiple control barrier functions with application to large scale indoor navigation (2023). https://arxiv.org/abs/2312.07803
Rungta, N.: A billion SMT queries a day (Invited Paper). In: Shoham, S., Vizel, Y. (eds.) Computer Aided Verification. CAV 2022. LNCS, vol. 13371, pp. 3–18. Springer, Cham (2022). https://doi.org/10.1007/978-3-031-13185-1_1
Sarkar, C., Paul, H.S., Pal, A.: A scalable multi-robot task allocation algorithm. In: 2018 IEEE International Conference on Robotics and Automation (ICRA), pp. 5022–5027. IEEE (2018)
Schüle, M., Kraus, J.M., Babel, F., Reißner, N.: Patients’ trust in hospital transport robots: evaluation of the role of user dispositions, anxiety, and robot characteristics. In: 17th ACM/IEEE International Conference on Human-Robot Interaction (HRI), pp. 246–255 (2022)
Shah, N., Srivastava, S.: Using deep learning to bootstrap abstractions for hierarchical robot planning. In: 21st International Conference on Autonomous Agents and Multiagent Systems (AAMAS) (2022)
Shoukry, Y., Nuzzo, P., Sangiovanni-Vincentelli, A.L., Seshia, S.A., Pappas, G.J., Tabuada, P.: SMC: satisfiability modulo convex programming. Proc. IEEE 106(9) (2018)
Uwacu, D., Yammanuru, A., Morales, M., Amato, N.M.: Hierarchical planning with annotated skeleton guidance. IEEE Robot. Autom. Lett. (RAL) 7, 11055–11061 (2022)
Wurman, P.R., D’Andrea, R., Mountz, M.: Coordinating hundreds of cooperative, autonomous vehicles in warehouses. AI Mag. 29(1), 9 (2008)
Acknowledgements
This work was supported in part by LOGiCS: Learning-Driven Oracle-Guided Compositional Symbiotic Design for Cyber-Physical Systems, Defense Advanced Research Projects Agency award number FA8750-20-C-0156; by Provably Correct Design of Adaptive Hybrid Neuro-Symbolic Cyber Physical Systems, Defense Advanced Research Projects Agency award number FA8750-23-C-0080; by Toyota under the iCyPhy Center; and by Berkeley Deep Drive.
Author information
Authors and Affiliations
Corresponding authors
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2024 The Author(s), under exclusive license to Springer Nature Switzerland AG
About this paper
Cite this paper
Tuck, V.M. et al. (2024). SMT-Based Dynamic Multi-Robot Task Allocation. In: Benz, N., Gopinath, D., Shi, N. (eds) NASA Formal Methods. NFM 2024. Lecture Notes in Computer Science, vol 14627. Springer, Cham. https://doi.org/10.1007/978-3-031-60698-4_20
Download citation
DOI: https://doi.org/10.1007/978-3-031-60698-4_20
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-031-60697-7
Online ISBN: 978-3-031-60698-4
eBook Packages: Computer ScienceComputer Science (R0)