Mobile Ambients行为理论的研究

摘要

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