SMT-Based Dynamic Multi-Robot Task Allocation

Victoria Marie Tuck, Pei-Wei Chen, Georgios Fainekos, Bardh Hoxha, Hideki Okamoto, S. Shankar Sastry, and Sanjit A. Seshia. SMT-Based Dynamic Multi-Robot Task Allocation. In NASA Formal Methods - 16th International Symposium (NFM), pp. 331–351, Lecture Notes in Computer Science 14627, Springer, 2024.

Download

[pdf] 

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, keeping 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.

BibTeX

@inproceedings{tuck-nfm24,
  author       = {Victoria Marie Tuck and
                  Pei{-}Wei Chen and
                  Georgios Fainekos and
                  Bardh Hoxha and
                  Hideki Okamoto and
                  S. Shankar Sastry and
                  Sanjit A. Seshia},
  editor       = {Nathaniel Benz and
                  Divya Gopinath and
                  Nija Shi},
  title        = {{SMT}-Based Dynamic Multi-Robot Task Allocation},
  booktitle    = {{NASA} Formal Methods - 16th International Symposium (NFM)},
  series       = {Lecture Notes in Computer Science},
  volume       = {14627},
  pages        = {331--351},
  publisher    = {Springer},
  year         = {2024},
  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, keeping 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.},
}