Research On Behavioral Theory For Mobile Ambients

Mobile computation has been more and more important. Mobile Ambients is an important process calculi system which aims to describe mobile computation. Process calculi is one of important research topics in concurrency theories. A central concern for process calculi is to establish processes'behavioral theories; especially, how to develop an effective semantics theory for Mobile Ambients has been a long-standing open problem. JACM published M.Merro and F.Zappa Nardelli's paper titled"Behavioral Theory for Mobile Ambients"[1] in 2005. This master thesis is based on Merro and Nardelli's work. It is about behavioral theories of Mobile Ambients based on strong bisimulation. The main content includes:(1) Two important mistakes of Merro and Nardelli's work are pointed out. One concerns the completeness of late bisimilarity≈in terms of ? S. It leads the completeness proofs fail. The other is about Up-To proof techniques of weak bisimulation. These mistakes have been confirmed by Merro and Nardelli, but they haven't solved these problems till now.(2) Discuss basic properties of corresponding concepts under strong bisimulation, including reduction barbed congruence over system S , late strong bisimilarity～l, and early strong bisimilarity～e.(3) The soundness (in terms of S ) of late strong bisimilarity～l and early strong bisimilarity～e are proved respectively. We also discuss some Up-To proof techniques of late strong bisimulation.(4) The completeness (in terms of S ) of early strong bisimilarity～e is proved.