移动计算在人们的日常生活中扮演着日益重要的角色,Mobile Ambients是一种重要的刻画移动计算的进程演算系统。进程演算是描述并发系统的重要模型之一。进程演算的一个核心问题是行为理论的研究,而如何构建Mobile Ambients的有效行为理论一直是一个公开问题。2005年,M.Merro和F.Zappa Nardelli在国际著名期刊JACM上发表了论文“Behavioral Theory for Mobile Ambients”[1]。本文主要基于Merro和Nardelli的工作展开,探讨Mobile Ambients在强互模拟下的行为理论,研究内容包括:(1)指出了Merro和Nardelli工作中的两处重要证明漏洞:其一涉及弱互模拟≈相对于归约barbed同余? S的完备性,它使得该完备性结果的证明失效;另外一个涉及弱互模拟下的Up-To技术。Merro和Nardelli确认了这些漏洞,但至今为止尚未能给出补救方法。(2)讨论了强互模拟下相关概念的基本性质,包括系统上的归约barbed同余关系S ,迟强互模拟～l和早强互模拟～e等。(3)分别证明了迟强互模拟～l和早强互模拟～e相对于归约barbed同余S的可靠性;讨论了迟强互模拟～l下的Up-To证明技术。(4)证明了早强互模拟～e相对于归约barbed同余S的完备性定理。