The authors consider a simplified swarming scenario, in which the agents move along the nodes of a graph. The specification is given as a formula in a logic called graph temporal logic (GTL), which constrains the distribution of the swarm over the nodes of the graph. The authors propose an algorithm to control the density distribution of the swarm, which is based on a time-varying Markov chain modeling the time evolution of the density distribution of the swarm. GTL and the Markov-chain modeling have been published before. The main contributions of this paper are to (1) synthesize such a Markov chain as a mixed-integer nonlinear program (MINLP), and (2) relax the MINLP to a mixed integer linear program (MILP). My main concern with the paper is whether the contributions described above are enough to make this a RSS paper. My second major concerns is the simplicity of the examples throughout the paper. The running example us too simplistic, and the authors to not make any effort to connect this example to a robotic scenario. In the second example at the end of the paper, which is supposed to be more realistic, it is not cleat what the dynamics of the robot are. Aside from these, the paper is well written and, as far as I followed, technically correct. However, the related work misses three important and closely related works. First, there is no clear comparison with the plethora of papers on consensus. In the second paragraph of the Introduction, the author(s) say that "as the number of agents comprising the swarm increases, the computational cost for assigning the targets of each agent and generating all the optimal trajectories one by one becomes prohibitively high. As a result, these techniques suffer from scalability issues." This is not the case for consensus-type papers, in which simple, identical local rules lead to guaranteed global behavior. Second, there are some papers on controlling the statistics of a swarm, e.g., (1) Calin Belta and Vijay Kumar, Abstraction and control for groups of robots, IEEE Transactions on Robotics, vol.20, no.5, pp.865-875, 2004, (2) P. Yang, R. A. Freeman and K. M. Lynch, "Multi-Agent Coordination by Decentralized Estimation and Control," in IEEE Transactions on Automatic Control, vol. 53, no. 11, pp. 2480-2496, Dec. 2008, which are not mentioned and discussed. Third, there exist spatial temporal logics, that seem to be related to the GTL logic proposed here, e.g., (1) L. Nenzi, L. Bortolussi, V. Ciancia, M. Loreti, M. Massink, Qualitative and Quantitative Monitoring of Spatio-Temporal Properties with SSTL, Logical Methods in Computer Science, vol. 14(4) (2018), (2) Iman Haghighi, Sadra Sadraddini, Calin Belta, Robotic Swarm Control from Spatio-Temporal Specifications, 55th IEEE Conference on Decision and Control, Las Vegas, NV, 2016 (3) Iman Haghighi, Austin Jones, Zhaodan Kong, Ezio Bartocci, Radu Grosu and Calin Belta, SpaTeL: A Novel Spatial-Temporal Logic and Its Applications to Networked Systems, Hybrid Systems: Computation and Control (HSCC) 2015

This paper addresses the important problem of efficiently synthesizing a decentralized controllers for a large number agents, i.e. a swarm, such that together, they satisfy some high-level specification, here in the form of a graph temporal logic sentence. Such systems have a large number of applications, and by no means is this a solved problem. The prose and general outline of the paper is easy enough to follow, although illustrations of the examples and theorems would have been greatly appreciated. The high level approach taken in this paper is 4 fold: 1. The swarm is ultimately abstracted as a graph where the nodes represent locations and densities (#agents/#total number of agents). 2. The decentralized controller is abstracted as a time varying markov chain describing how densities evolve on this graph over time. 3. The synthesis of this controller subject to the specification and dynamics is cast as a feasibility query in a Mixed Integer Non-linear Program (MINLP). 4. Once synthesized, an online low-level controller implements this strategy in the work space this graph represents. This approach improves over prior work by either: * Modeling densities rather than agents directly to improve scaling w.r.t. swarm size. or * Synthesizing swarm strategies that satisfy bounded graph temporal logic specifications. The primary technical contribution of this work seems to be the handling of the complexity of the MINLP - being potentially much harder than MILPs which are already NP-hard. This is done by first observing that in the special case of a complete graph, the constraints on densities can be used to determine a feasible swarm strategy, resulting in a Mixed Integer *Linear* Program. While the proof seems straight forward, an interpretation would have been appreciated. For example, physically, I understand this to be the result of agents being able to always "keep up" with required densities at each time step since they are always one step away from there they need to be. A general solution is then proposed which alternates between solving two relaxations of the MINLP. The key insight is that once the swarm strategy (markov chain) or densities are set, the complexity of the MINLP reduces substantially. Thus at a high level, this algorithm alternates between estimating these to quantities. The paper then empirically demonstrates substantial improvements this proposed solution has over using off-the-shelf MINLP solvers as well we a few interesting case studies. While I believe this approach to be well-founded and the experiments convincing, I am left with a two questions: 1. While improving scalability, there doesn't seem any constraints ensuring that the Markov Chain densities can be realized - since in the actual swarm the densities cannot take on all real numbers. Is there a guarantee that the results will still hold with high probability? 2. Because the solutions need only be feasible, is it possible to leverage an SMT solver rather than optimization engine? The non-linearities in the MINLP seem fairly tame, and the proposed algorithm reminds the reviewer of Counter Example Guided Inductive Synthesis based on SMT solvers. Similar works in synthesizing controllers from Signal Temporal Logic have shown that combining SMT solvers with MILPs can also lead to dramatic increases in performance.