Development of Natural Strategies in Strategic Logics

In the last two decades, both Alternating-time Temporal Logic (ATL) and Strategy Logic (SL) has been proved to be very useful in modeling strategic reasoning for Multi-Agent Systems (MAS). However, these logics struggle to capture the bounded rationality inherent in human decision-making processes. To overcome these limitations, Natural Alternating-time Temporal Logic (NatATL) and Natural Strategy Logic (NatSL) have been recently introduced. As respectively extensions of ATL and SL, these natural variants incorporate bounded memory constraints into agents’ strategies, which allows to resemble human cognitive limitations. In this paper, we discuss a novel verification implementation for NatATL and NatSL specifications, both for memoryless strategies and strategies with recall. This research project aims to transform theoretical advancements into a practical verification framework, enabling comprehensive analysis and validation of strategic reasoning in complex multi-agent environments. Our novel tool paves the way for applications in areas such as explainable AI and human-in-the-loop systems, highlighting both NatATL and NatSL substantial potential.