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

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.