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

In logics for strategic reasoning the main challenge is represented by their verification in contexts of imperfect information and perfect recall strategies. 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 φ, we propose a verification procedure that generates sub-models of M in which each sub-model M' satisfies a sub-formula φ' of φ and the verification of φ' in M' is decidable. Then, we use CTL∗ model checking to provide a verification result of φ on M. We prove that our procedure is sound and in the same complexity class of ATL∗ model checking under perfect information and perfect recall. Moreover, we present a tool that uses our procedure and provide experimental results.