A Model Checker for Natural Strategic Ability

TL;DR

This paper introduces a new model checker for NatATL, an extension of ATL that models bounded rationality in multi-agent systems, enabling practical verification of strategic reasoning with cognitive constraints.

Contribution

We developed a model checker for NatATL integrated into VITAMIN, making the theoretical logic applicable for real-world multi-agent system verification.

Findings

Supports both memoryless and recall strategies

Enables analysis of human-like decision-making in MAS

Facilitates applications in explainable AI and human-in-the-loop systems

Abstract

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.