# Towards the Verification of Strategic Properties in Multi-Agent Systems with Imperfect Information

arXiv: https://arxiv.org/abs/2112.13621 · HTML: https://mlsanity.com/paper/2112.13621/

## Key facts

- Cited by 2 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 27 Dec 2021.

## Built on by (most cited first, 2 of 2)

- [Model Checking Strategic Abilities in Information-sharing Systems](https://mlsanity.com/paper/2204.08896/) (2022)
- [Probabilistic Strategy Logic with Degrees of Observability](https://mlsanity.com/paper/2412.15135/) (2024)

## Abstract (arXiv)

In logics for the strategic reasoning the main challenge is represented by their verification in contexts of imperfect information and perfect recall. In this work, we show a technique to approximate the verification of Alternating-time Temporal Logic (ATL*) under imperfect information and perfect recall, which is known to be undecidable. Given a model M and a formula varphi, we propose a verification procedure that generates sub-models of M in which each sub-model M' satisfies a sub-formula varphi' of varphi and the verification of varphi' in M' is decidable. Then, we use CTL* model checking to provide a verification result of varphi on M. We prove that our procedure is in the same class of complexity of ATL* model checking under perfect information and perfect recall, we present a tool that implements our procedure, and provide experimental results.