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.
翻译:在战略推理的逻辑中,主要挑战是在信息不完善和完全召回的情况下进行核查。在这项工作中,我们展示了一种技术,在不完善的信息和完全召回(众所周知是不可变的)的情况下,以不完善的信息和完全召回(这是不可变的)对交替时间时间逻辑(ATL* )的核查进行估计。考虑到模型M和公式$\varphie$,我们提议了一个产生亚模M的核查程序的核查程序,在这种模式中,每个子模型M都满足了一个次级公式$\varphi$的核查,而M的美元是可分数的。然后,我们使用CTL* 模式检查来提供M $\varphie$的核查结果。我们证明,我们的程序与ATL* 模型在完全的信息和完美回忆下进行检查的复杂程度相同,我们提出了一个工具来实施我们的程序,并提供实验结果。