Model Checking for Mobile Ambients

Mobile ambients is a model tool that describes distributed moving calculation. It consists of processes and nested sub-mobiles, and it has strong ability of expressing space. Ambients logic can describe the processs evolvement in time and space. Model-checking of ambients logic is a hotspot field of model-checking today. The authors study the model-checking of finite-control mobile ambients against formulas of predicate ambient logic with recursion. Before now, Lin H M concluded that this problem is able to be judged and proposed a detailed algorithm for it, but not considered much on the efficiency of the algorithm. In this paper, a local model-checking algorithm is developed by applying the nested predicate equations. To the knowledge of the authors, this is the first algorithm whose time complexity increases exponentially with the alternation depth in formula, and this is the second model-checking algorithm for predicate ambient logic with recursion after Lin H M’working. This papers contributions are: ①studying the semantic consistency between the ambient logic formula and nested predicate, proving the equivalence between them, and getting a detailed algorithm for converting the ambient logic formula into nested predicate equations; ②studying the model checking for ambient logic, getting a general local algorithm and analyzing the complicacy of it.