Reducing Higher Order Pi-Calculus to Spatial Logics

TL;DR

This paper introduces a spatial logic framework for higher order pi-calculus, enabling logical descriptions of process relations, and extends it with mu-operator and weak semantics to enhance expressiveness.

Contribution

It proposes a new spatial logic for higher order pi-calculus, proves its soundness and completeness, and extends it with mu-operator and weak semantics.

Findings

Logical relations describe process structure and transitions.

Bisimulations extended to logical formulae.

Replication expressed in muSL logic.

Abstract

In this paper, we show that theory of processes can be reduced to the theory of spatial logic. Firstly, we propose a spatial logic SL for higher order pi-calculus, and give an inference system of SL. The soundness and incompleteness of SL are proved. Furthermore, we show that the structure congruence relation and one-step transition relation can be described as the logical relation of SL formulae. We also extend bisimulations for processes to that for SL formulae. Then we extend all definitions and results of SL to a weak semantics version of SL, called WL. At last, we add mu-operator to SL. This new logic is named muSL. We show that WL is a sublogic of muSL and replication operator can be expressed in muSL.