As the deployment of autonomous robots in real-world environments becomes increasingly prevalent, the need for these robots to operate safely and efficiently alongside human actors and other robots grows. Ensuring that robots adhere to their intended tasks and safety constraints as specified is of utmost importance, particularly when considering interactions between different robots and humans. To address this challenge, formal methods-based strategy synthesis techniques have emerged as a promising approach, offering rigorous specification languages and algorithms that generate correct-by-design strategies.

This doctoral thesis focuses on the design and development of decentralized strategy synthesis algorithms to handle multi-agent systems consisting of multiple robots, or robots and humans. By considering task planning in a shared environment, the research seeks to achieve guarantees regarding specification satisfaction while considering interactions between computational agents and human actors.

Several key considerations are addressed in this work. Scalability is a major concern in strategy synthesis methods, given their high computational costs. We avoid constructing a global, centralized model of the system to mitigate the state explosion problem. Instead, we focus on decentralized methods that ensure global integrity through communication of necessary, but minimal assumptions as least-limiting advisers.

Another challenge lies in effectively modeling human agents in the system. Human behavior is influenced by context and preferences, making it difficult to provide explicit models. We avoid explicitly modelling the human and instead propose an assume-guarantee approach, where the robot conveys only necessary advice to the human.This advice, if followed by the human, enables us to provide conditional guarantees on the satisfaction of the task specification.

Lastly, while temporal logics are a rich and expressive specification language, it can be difficult to correctly capture desired tasks and constraints. We present a specification language for object-oriented tasks that leverages spatial relations to intuitively specify desired spatial and temporal relations between objects. We show that this language can be used for monitoring and planning in various scenarios.We also demonstrate how it can be used to enable a robot to request help from a human assistant through structured language.

Overall, this doctoral thesis aims to bring the benefits of formal methods-based strategy synthesis to multi-agent systems with human actors, providing a unified methodology to compute and convey least-limiting advice in interactions between robots and between robots and humans.