1: \begin{abstract}

2: Multi-agent partially observable Markov decision processes (MPOMDPs) provide a framework to represent heterogeneous autonomous agents subject to uncertainty and partial observation. In this paper, given a nominal policy provided by a human operator or a conventional planning method, we propose a technique based on barrier functions to design a minimally interfering \emph{safety-shield} ensuring satisfaction of  high-level specifications in terms of linear distribution temporal logic (LDTL).  To this end, we use  sufficient and necessary conditions for the invariance of a given set based on discrete-time barrier functions (DTBFs) and formulate sufficient conditions for finite time DTBF to study finite time convergence to a set. We then show that different LDTL mission/safety specifications can be cast as a set of invariance or  finite time reachability problems. We demonstrate that the proposed method for safety-shield synthesis  can be implemented online by a sequence of one-step greedy algorithms. We demonstrate the efficacy of the proposed  method using experiments involving a team of~robots.

3: \end{abstract}

4: