We develop a probabilistic control algorithm, $\texttt{GTLProCo}$, for swarms of agents with heterogeneous dynamics and objectives, subject to high-level task specifications. The resulting algorithm not only achieves decentralized control of the swarm but also significantly improves scalability over state-of-the-art existing algorithms. Specifically, we study a setting in which the agents move along the nodes of a graph, and the high-level task specifications for the swarm are expressed in a recently-proposed language called graph temporal logic (GTL). By constraining the distribution of the swarm over the nodes of the graph, GTL can specify a wide range of properties, including safety, progress, and response. $\texttt{GTLProCo}$, agnostic to the number of agents comprising the swarm, controls the density distribution of the swarm in a decentralized and probabilistic manner. To this end, it synthesizes a time-varying Markov chain modeling the time evolution of the density distribution under the GTL constraints. We first identify a subset of GTL, namely reach-avoid specifications, for which we can reduce the synthesis of such a Markov chain to either linear or semi-definite programs. Then, in the general case, we formulate the synthesis of the Markov chain as a mixed-integer nonlinear program (MINLP). We exploit the structure of the problem to provide an efficient sequential mixed-integer linear programming scheme with trust regions to solve the MINLP. We empirically demonstrate that our sequential scheme is at least three orders of magnitude faster than off-the-shelf MINLP solvers and illustrate the effectiveness of $\texttt{GTLProCo}$ in several swarm scenarios.
翻译:我们开发了一种概率控制算法, $\ textt{ GTLProCo} $\ ptrent{ GTL}, 用于具有不同动态和目标的代理商群群, 但须服从高层次任务规格。 由此产生的算法不仅能实现群体的分散控制, 而且还能显著改善现有最先进的算法的伸缩性。 具体地说, 我们研究一种环境, 使代理商沿着图表节点移动, 以及群体的高级任务规格, 以最近提出的语言表达, 称为图形时间流时间逻辑( GTL) 。 通过限制图表节点的群群分布, GTL 能够指定一系列广泛的属性, 包括安全性、 进步和反应。 $ltrenttt{ GTLProco} $, 与构成群落的代理商数量, 以分散性和不稳定性的方式控制着暖气的密度分布。 为此, 它综合了一个时间流的Mark- snent marve Mark 链 模型, 在GTL 节点上, 我们以最低水平的平流的立算程序 展示了一种直流 。