  In this paper, we study the problem of controlling a two-dimensional robotic
swarm with the purpose of achieving high level and complex spatio-temporal
patterns. We use a rich spatio-temporal logic that is capable of describing a
wide range of time varying and complex spatial configurations, and develop a
method to encode such formal specifications as a set of mixed integer linear
constraints, which are incorporated into a mixed integer linear programming
problem. We plan trajectories for each individual robot such that the whole
swarm satisfies the spatio-temporal requirements, while optimizing total robot
movement and/or a metric that shows how strongly the swarm trajectory resembles
given spatio-temporal behaviors. An illustrative case study is included.
