Scheduling of Missions with Constrained Tasks for Heterogeneous Robot Systems

TL;DR

This paper introduces KANOA, a formal approach for task allocation and scheduling in multi-robot missions with constraints like task order and joint tasks, using logic and probabilistic models.

Contribution

It presents a novel formal framework combining Alloy and PRISM tools for planning complex multi-robot missions with specific task constraints.

Findings

Effective task allocation and scheduling demonstrated in a hospital maintenance case study.

Formal methods improve planning accuracy for heterogeneous robot teams.

Separation of allocation and scheduling simplifies complex mission planning.

Abstract

We present a formal tasK AllocatioN and scheduling apprOAch for multi-robot missions (KANOA). KANOA supports two important types of task constraints: task ordering, which requires the execution of several tasks in a specified order; and joint tasks, which indicates tasks that must be performed by more than one robot. To mitigate the complexity of robotic mission planning, KANOA handles the allocation of the mission tasks to robots, and the scheduling of the allocated tasks separately. To that end, the task allocation problem is formalised in first-order logic and resolved using the Alloy model analyzer, and the task scheduling problem is encoded as a Markov decision process and resolved using the PRISM probabilistic model checker. We illustrate the application of KANOA through a case study in which a heterogeneous robotic team is assigned a hospital maintenance mission.