Formal verification of strategic abilities is a hard problem. We propose to use the methodology of assume-guarantee reasoning in order to facilitate model checking of alternating-time temporal logic with imperfect information and imperfect recall.

翻译：战略能力的正式验证是一个难题。我们提出采用假设-保证推理方法，以促进对具有不完全信息和不完全记忆的交替时态逻辑的模型检验。