在多Agent系统中，为了尽可能细致的刻画Agent合理的行为能力，学者提出了合作逻辑这类理论。所谓合作是指，多Agent系统中Agent个体保持和团体完全相同的价值取向。多Agent合作逻辑是多Agent系统研究中一个新兴方向,而用多Agent系统来阐述分布式系统是一个新领域。ATL用于表达在分布式系统中Agent之间的合作关系，具体来说，ATL是CTL的扩展，其中用合作模态词代替路径算子，使得Agent集合能合作实现某些动作，体现了系统的智能化。　　 目前模型检测多Agent 系统用时序逻辑和认知逻辑比较多，但是两者的结合还不多。　　 本文主要是对ATL 系统在知识和思维状态方面作了一些研究，主要包括：　　 首先，我们介绍了ATEL。该逻辑在ATL的基础上加入了描述Agent 知识的算子，具有刻画单个Agent 知识的能力。我们讨论了ATEL的公理系统及其可靠性，并且具体刻画了一个安全协议的模型，用模型检测的工具进行了验证。　　 其次，我们以ATEL 为基础，建立了ATEPL。目的是为了描述和刻画系统中的不确定性，其中重点是知识的不确定性。然后我们给出了该系统的公理和模型检测算法，并把它应用到具体的协议中，最后简单说明了该系统的总体设计。　　 最后，为了详尽的描述Agent的思维状态，我们在ATL基础上加入了BDI算子，形成了新逻辑ATML。ATML 不仅可以描述Agent 之间的合作，还能刻画Agent的认知状态，使得该系统更加智能化。然后我们列举了ATML的公理系统，并给出了ATML的模型检测算法和实例。最后我们把ATML在概率信念下进行推广，给出了模型检测算法和实例。