In the last two decades, Alternating-time Temporal Logic (ATL) has been proved to be very useful in modeling strategic reasoning for Multi-Agent Systems (MAS). However, this logic struggles to capture the bounded rationality inherent in human decision-making processes. To overcome these limitations, Natural Alternating-time Temporal Logic (NatATL) has been recently introduced. As an extension of ATL, NatATL incorporates bounded memory constraints into agents' strategies, which allows to resemble human cognitive limitations. In this paper, we present a model checker tool for NatATL specifications - both for memoryless strategies and strategies with recall - integrated into VITAMIN, an open-source model checker designed specifically for MAS verification. By embedding NatATL into VITAMIN, we 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 NatATL's substantial potential.

翻译：在过去的二十年中，交替时序逻辑（ATL）已被证明在多智能体系统（MAS）的战略推理建模中非常有用。然而，该逻辑难以捕捉人类决策过程中固有的有限理性。为了克服这些局限性，自然交替时序逻辑（NatATL）最近被提出。作为ATL的扩展，NatATL将有限记忆约束纳入智能体的策略中，从而能够模拟人类的认知局限。本文提出了一种用于NatATL规约的模型检验工具——支持无记忆策略与有记忆策略——该工具已集成至VITAMIN中，VITAMIN是一个专为MAS验证设计的开源模型检验器。通过将NatATL嵌入VITAMIN，我们将理论进展转化为一个实用的验证框架，从而能够对复杂多智能体环境中的战略推理进行全面分析与验证。我们这一新颖的工具为可解释人工智能和人机协同系统等领域的应用铺平了道路，彰显了NatATL的巨大潜力。