Optimizing Robotic Team Performance with Probabilistic Model Checking

We present an approach to analytically construct a robotic team, i.e., team members and deployment order, that achieves a specific task with quantified probability of success. We assume that each robot is Markovian, and that robots interact with each other via communication only. Our approach is based on probabilistic model checking (PMC). We first construct a set of Discrete Time Markov Chains (DTMCs) that each capture a specific “projection” of the behavior of an individual robot. Next, given a specific team, we construct the DTMC for its behavior by combining the projection DTMCs appropriately. Finally, we use PMC to evaluate the performance of the team. This procedure is repeated for multiple teams, the best one is selected. In practice, the projection DTMCs are constructed by observing the behavior of individual robots a finite number of times, which introduces an error in our results. We present an approach – based on sampling using the Dirichlet distribution – to quantify this error. We prove the correctness of our approach formally, and also validate it empirically on a mine detection task by a team of communicating Kilobots.