An Intuitionistic Version of Alternating-Time Temporal Logic

Multi-Agent Systems (MAS) are essential for modelling strategic interactions between multiple agents, often involving partial information. Managing this partial information is crucial for accurate decision-making and strategy optimization. However, partial information combined with perfect recall strategies renders verifying strategic properties undecidable. Intuitionism, a form of partial information which has not yet been explored in the context of MAS, introduces a novel perspective. In this paper, we propose Intuitionistic Alternating Time Temporal Logic (IATL), an extension of ATL that incorporates intuitionistic logic, providing a specialized representation of imperfect information. We define its syntax, semantics, and key structural properties. Additionally, we propose a PTIME-complete algorithm for IATL model checking, supported by benchmarks demonstrating its efficiency.