Model Checking For Mobile Ambients

In the concurrent system, many tasks run at the same time. The main theory researches for the concurrent system are process algebra, and mode logic, etc. The representative theories are CCS process calculus theory proposed by Robin Milner and their variations, including pure CCS, value-passing CCS,π-calculus, and mobile ambients, etc.Model checking is an automatic technique for analyzing and verifying finite state concurrent systems whose basic idea is state exploration. Ensuring the terminating of the exploration for state space depends on the finite state mode converted from the system. Model checking's advantage is completely automatic and can give counterexample when terminating exploration if the property can't be satisfied, which can help the designer to improve the system. The main challenge in model checking is dealing with state space explosion problem.Model checking algorithms generally fall into two categories, local and global. Local procedures are designed for proving that a specific state of the transition system satisfies the given formula and global procedures are designed for finding all states of the transition system satisfies the given formula.The research work of this paper includes three aspects:1. In the area of the process calculus, because in, out, open operations in MAhave no limitation and the ambient has no management authority to its own boundary, and because both processes cannot communicate except in the same ambient in MA, open operation isnecessary for communicating in different ambients. But in the same ambient both processes can not only communicate but also perform other interactive operations. At the same time, because of using open operations, some processes might be forced to expose in the state of no ambient. Inorder to avoid this shortages, in, out, open operations, the permission of in, out, open operations, are added to SA to strengthen the management of the ambient boundary. Basedon SA, SAP adds the password to in, out, open, in, out, open operations. Only mastering the password's process can execute the in, out, open operations. open operation is canceled in BA, and provided the operation primitives among ambients and their sub-ambients communications instead. SA, SAP and BA are partial improvements for MA calculus. SA and SAP can't avoid the side effect from open operation and BA cannot control crossing the ambient boundary freely with in and out operation. At the same time, because BA has no open operation, once the ambient establishes will it stay in the system forever, which will occupy a large quantity of system resources, and doesn't match the actual case of process. To overcome the shortages of SA, SAP and BA, we put forward the Boxed Safe Ambients with Password (BSAP).Compared to MA, BSAP has the following advantages: (1) cancels open operation in MA and adds the communication operation primitive between ambients and sub-ambients; (2) adds in,out operation and adds password to in,out, in, outoperations; (3) adds the operation primitive del of ambient reclamation.2. In the area of mu-calculus model checking, because of fixpoint operators nesting,according to Tarski's theorem, a global algorithm may require O(n^k) iterations to evaluate a formula, where n is the number of states in the transition system and k is the depth of nesting of the fixpoints. Based on the function monotonicity in theμ-calculus formula, Long,Browne, Clarde, Jha and Marrero presented a global algorithm whose time complexity is O(n^d/2) and space complexity is an exponential. Our algorithm is an improvement for the work of Long, Browne Clarde, Jha and Marrero whose time complexity is O((2n + 1)^{(?)(d+3)/4(?)+(?)(d+2)/4(?)})andspace complexity is O(dn). It is the first known algorithm whose space complexity is O(dn) and the exponent part of time complexity is d /2 for a global model-checking algorithm in the fullμ-calculus formula at present. It has the best capability in the known fullμ-calculus global model checking algorithms at present. Because of theimproved capability of the algorithm, it can solve theμ- calculus formula whosefixpoints operator is deep alternating nesting, which is significant in the model checking.3. In the area of model checking, based on the work of Academician Lin Huimin, we study the model-checking of finite-control mobile ambients against formulas of predicate ambient logic with recursion. By applying the nested predicate equations, a local model-checking algorithm is developed. To our knowledge, it is the first algorithm whose time complexity is increased exponentially with the alternation depth in formula. It is the first predicate mobile ambients logic model checking algorithm which has the definite time complexity, and is the second known model-checking algorithm for predicate ambient logic with recursion. The contributions are: (1) studying the semantic consistency between the ambient logic formula and nested predicate equations, and getting the method for converting the ambient logic formula into the nested predicate equations; (2) studying the model checking for ambient logic with no alternation in formula, and getting a specific algorithm for this case; (3) studying the ambient logic model checking in which the fixpoint operators is alternation, and getting a general local algorithm for it.