A network-conscious π-calculus and its coalgebraic semantics

摘要

Traditional process calculi usually abstract away from network details, modeling only communication over shared channels. They, however, seem inadequate to describe new network architectures, such as Software Defined Networks, where programs are allowed to manipulate the infrastructure. In this paper we present the Network Conscious π-calculus (NCPi), a proper extension of the π-calculus with an explicit notion of network: network links and nodes are represented as names, in full analogy with ordinary π-calculus names, and observations are routing paths through which data is transported. However, restricted links do not appear in the observations, which thus can possibly be as abstract as in the π-calculus. Then we construct a presheaf-based coalgebraic semantics for NCPi along the lines of Turi-Plotkin's approach, by indexing processes with the network resources they use: we give a model for observational equivalence in this context, and we prove that it admits an equivalent nominal automaton (HD-automaton), suitable for verification. Finally, we give a concurrent semantics for NCPi where observations are multisets of routing paths. We show that bisimilarity for this semantics is a congruence, and this property holds also for the concurrent version of the π-calculus.