  This paper addresses the control synthesis of heterogeneous stochastic linear
multi-agent systems with real-time allocation of signal temporal logic (STL)
specifications. Based on previous work, we decompose specifications into
sub-specifications on the individual agent level. To leverage the efficiency of
task allocation, a heuristic filter evaluates potential task allocation based
on STL robustness. Subsequently, an auctioning algorithm determines the
definite allocation of specifications. Finally, a control strategy is
synthesized for each agent-specification pair using tube-based Model Predictive
Control (MPC), ensuring provable probabilistic satisfaction. We demonstrate the
efficacy of the proposed methods using a multi-bus scenario that highlights a
promising extension to autonomous driving applications like crossing an
intersection.
