模型检测是近二十几年来最成功的自动验证技术之一,一直以来主要用于检测时态逻辑,人们很少注意空间逻辑的模型检测问题,而在分布式系统领域,为了能够描述系统的空间结构性质,已经广泛地采用空间逻辑来描述.　　 本论文主要探讨了基于传值CCS的带谓词μ演算的空间逻辑的模型检测和基于分布式异步П演算的空间逻辑的模型检测。研究内容包括:　　 1.基于传值CCS的带谓词μ演算的空间逻辑的模型检测。给出了带谓词μ演算的空间逻辑的语法语义。引用了[1]中的嵌套谓词等式系,针对于本文的逻辑系统,提出了相应的模态图的表示方法。给出了带赋值的符号迁移图和模态图的OBDD数据结构表示,并给出了逻辑公式和进程公式转换为OBDD的步骤规则。给出了模型检测算法。　　 2.基于分布式异步П演算的空间逻辑的模型检测。区别于异步П演算,分布式异步П演算主要增加了goto l.R算子,并引进了型和域的概念。其相应的空间逻辑中含有了k[u!]算子,用于刻画域中的动作。给出了模型检测算法,并证明了算法的正确性。