In this paper, we present a spatial logic for distributed higher order π-calculus. In order to prove that the induced logical equivalence coincides with distributed context bisimulation, we present
some new bisimulations, and prove the equivalence between these new bisimulations and distributed context bisimulation. Furthermore,
we present a variant of this spatial logic and prove that it gives a logical characterisation of distributed bisimulations.
This work was supported by the National Natural Science Foundation of China under Grant 60473036.