Dormancy and Spatial Logic of Mobile Ambients

Ambient logic presented a schematic spatial logic for specifying and reasoning about spatial properties of mobile processes. However, in some scenarios, spatial properties of processes should be specified and analyzed in finegrained. In this paper, dormancy of mobile processes is analyzed, and their existence states can be described as dormant or active. Based on this, an extension of ambient logic, united spatial-state logic, is presented. This logic can express dormancy of processes, thus spatial properties of processes can be specified in fine-grained. And satisfiability of the logic is decidable. Furthermore, formal interpretation over mobile ambients and inference rules of dormant spatial formulas are given.