An Improved Full Abstraction Approach to Analyzing Locality Semantics

Concurrency semantics plays an important role in both concurrency theory and software engineering. Although many results on various concurrency semantics have been proposed, there is still room for improvement. This paper focuses on the locality semantics, an important non-interleaving semantics, based on studying the relationship between the located CCS and the π-calculus. We present a practical full abstraction result for the locality semantics, and reduce the location bisimulation of the located CCS to the observation bisimulation of the π-calculus. The full abstraction result respects process finiteness, i.e., finite processes of the located CCS are mapped onto finite π-processes. As a result, the location bisimulation on finite processes of the located CCS can be proved by an existing proof system on finite π-processes, which is not achieved in [31].