Model Checking Properties of Multi-agent Systems with Imperfect Information and Imperfect Recall

摘要

The problem of practical model checking Alternating-time Temporal Logic (ATL) formulae under imperfect information and imperfect recall is considered. This is done by synthesis and subsequent verification of strategies, until a good one is found. To reduce the complexity of the problem we define an equivalence relation on strategies. Then an algorithm for model checking a class of modal properties with a single coalitional modality is presented, which utilises the observation that there is no need to verify more than one strategy from an equivalence class. The experimental results of the approach are also discussed.