模型检测作为一种有限状态系统的自动化验证技术已得到广泛应用，最近该技术在规划和多智能体系统(MAS)等人工智能领域的应用也越来越受到重视，MAS领域强调智能体的自治性和推理力，采用模态逻辑刻画智能体心智状态(包括智能体的知识，信念，愿望和意图)的演变过程。由于这些模态词的语义解释与标准时态算子不同，因此不能直接将当前的LTL或CTL时态逻辑模型检测工具应用到多智能体系统中。 本文重点研究多智能体系统的规范表示及其模型检测方法。根据智能体知识，信念，愿望和意图的表示和建模需求，提出新的Kripke语义模型，并在这一新的语义模型基础上研究多智能体系统的时态认知逻辑模型检测算法。这里提出的时态认知逻辑是在分支时态逻辑CTL~*语言中加入表示智能体知识，信念，愿望或意图的认知模态词后得到的。该时态认知逻辑有丰富的时态和认知表达能力，用户可以方便地检测智能体认知状态的演变过程。因此，本文研究成果在时态和认知两方面扩展并丰富了当前的多智能体系统模型检测技术。 另一方面，为了大幅缓解模型检测的状态爆炸问题，我们分别采用有序二叉判定图(OBDD)和可满足性(SAT)两种符号计算技术设计本文的符号模型检测算法，使得可验证问题的规模大大增加。 根据本文提出的理论，我们已实现两个高效的符号模型检测工具MCTK和MCKBDI，其中MCTK用于检测智能体的知识，而MCKBDI主要用于检测智能体的信念，愿望和意图。本文的研究成果主要体现在以下几方面： · 提出一个时态逻辑CTL~*的符号模型检测算法。该算法通过tableau构造方法和基于OBDD的不动点计算来判定一个有限状态系统是否满足CTL~*