Multi-agent systems (MAS) are pervasive with applications in various areas such as computer networks, robotics, and power grids. For example, multi-robot systems play a critical role in our society, including industrial robots in car assembly lines, hundreds of drones in a light show, and many vehicles in future autonomous ride-sharing services. Sequential decision-making is crucial to construct functional, intelligent MAS that can meet our needs. Multi-agent reinforcement learning is an approach that facilitates machine learning through feedback that reinforces the desired behavior. However, this approach requires a quantitative reward function that is oftentimes unavailable or hard to design. Formal methods (FM), by nature, can accurately specify and verify software and hardware systems. This project aims to combine the two approaches in order to construct multi-agent systems that are more scalable, easier to understand, and safer. The investigators will also disseminate research findings, integrate them in teaching, and train graduate and undergraduate students. Specifically, this project has the following three research objectives. Objective A develops novel specification-guided Multi-agent Reinforcement Learning (MARL) approaches that optimally decompose the specification and assign the resulting parts to agents. The principled and interpretable methods can learn a “correct by construction” scheduler to decompose signal temporal logic specifications optimally, corres