  We consider the control design of stochastic discrete-time linear multi-agent
systems (MASs) under a global signal temporal logic (STL) specification to be
satisfied at a predefined probability. By decomposing the dynamics into
deterministic and error components, we construct a probabilistic reachable tube
(PRT) as the Cartesian product of reachable sets of the individual error
systems driven by disturbances lying in confidence regions (CRs) with a fixed
probability. By bounding the PRT probability with the specification
probability, we tighten all state constraints induced by the STL specification
by solving tractable optimization problems over segments of the PRT, and
convert the underlying stochastic problem into a deterministic one. This
approach reduces conservatism compared to tightening guided by the STL
structure. Additionally, we propose a recursively feasible algorithm to attack
the resulting problem by decomposing it into agent-level subproblems, which are
solved iteratively according to a scheduling policy. We demonstrate our method
on a ten-agent system, where existing approaches are impractical.
