Abstract: With the fast development of computer technology and network communication technology,process algebra,Petri net and other formal analysis methods were proposed for concurrent distributed systems.Due to the emergence and rapid development of the mobile internet in recent years,pi calculus is developed by adding mobility to process algebra,and at the same time,Petri nets field also uses predicate/transition net and color net to model the mobile system.But there still exist some weakness of them.Based on all previous works,A.Asperti and N.Busi proposed mobile net.Mobile net is obtained by adding mobility to Petri net and combining with the strengths of process algebra.It is suitable for the description of mobile computing system.However,no corresponding analysis method of mobile net has been developed now.Hence,this paper studied the analysis method for mobile net.The construct algorithm of the reachability tree of mobile net was proposed,and the reachability analysis method based on its reachability tree was provided.In addition,an example of the mobile vehicle telephone communication system was illustrated to demonstrate the effectiveness of this method.

Key words: Mobile net,Mobile system,Reachability tree,Algorithm