一句话：为不完美信息 ATL 建立基于历史的交替互模拟与共同知识语义之间的完整 Hennessy-Milner 定理，并证明相关互模拟不可判定。
本文研究不完美信息下交替时间时序逻辑（ATL）与交替互模拟之间的关系。作者提出带不完美信息的、基于历史的交替互模拟变体，并证明它能与采用共同知识语义的不完美信息 ATL 建立完整的 Hennessy-Milner 定理：两个模型在该互模拟下等价当且仅当它们满足相同的 ATL 公式。共同知识语义要求联盟实现目标所用的统一策略在联盟内部是共同知识。作者指出其他不完美信息 ATL 语义变体不能容纳该定理，并进一步证明两个有限不完美信息并发博弈结构（iCGS）之间存在基于历史的交替互模拟这一问题不可判定。
We show that a history-based variant of alternating bisimulation with imperfect information allows it to be related to a variant of Alternating-time Temporal Logic (ATL) with imperfect information by a full Hennessy-Milner theorem. The variant of ATL we consider has a common knowledge semantics, which requires that the uniform strategy available for a coalition to accomplish some goal must be common knowledge inside the coalition, while other semantic variants of ATL with imperfect information do not accomodate a Hennessy-Milner theorem. We also show that the existence of a history-based alternating bisimulation between two finite Concurrent Game Structures with imperfect information (iCGS) is undecidable.