Formal Aspects for Strategic Reasoning in Multi-Agent Systems with Natural Strategies

Multi-Agent Systems (MAS) provide a robust framework for modeling complex systems involving interacting agents, both human and artificial, in cooperative or adversarial settings. Strategic reasoning is fundamental to understanding agent behavior and designing systems with desirable properties. This thesis focuses on the formal aspects of strategic reasoning in MAS, introducing - for the first time - a verification tool for Natural Alternating-time Temporal Logic (NatATL). The research encompasses theoretical foundations, a critical analysis of existing verification tools, and the development of a scalable and extensible software solution. A key contribution is the introduction of the Strategies Generation Lemma, which proposes a novel approach to strategy generation. The implementation is evaluated through extensive experiments to assess scalability and performance. Additionally, practical applications and optimizations are explored to enhance the tool’s efficiency. By bridging a first gap between theory and implementation, this work advances formal verification in strategic reasoning, with direct implications for artificial intelligence and human-like strategies generation.