Designing and verifying planning algorithms for multi-agent systems (MAS) is significantly more complex than single-agent systems due to the added burden of communication, coordination, and cooperation required between agents. In a decentralized MAS, agents rely on their own sensors coupled with communication with other agents to perceive the environment. Maintaining a consistent global estimate of the environment state may thus incur significant communication cost. Agents may operate in congested environments where coordinating their planned motion is crucial to ensure that agents do not collide or prevent each other from accomplishing their tasks. Task objectives for agents may be different, agents may be homogeneous or heterogeneous, and task objectives could be simple sequences of reach-avoid tasks or more complicated long-horizon temporal tasks. In order to reason about such diverse considerations, it is crucial to develop logical formalisms that can unambiguously express MAS specifications and develop planning algorithms that guarantee logical specifications. In this talk, we examine some existing and new MAS formalisms, and discuss algorithms to perform monitoring of such MAS. We will also look at an overarching framework to design safe control strategies for MAS subject to individual and collective specifications using the framework of potential games. We will present some recent results on monitoring and control synthesis for multi-agent UAV environments based on the presented techniques.