Equivalence relations of distributed systems with module passing

This paper presents a formal model of distributed systems that consist of a number of sites and the sites communicates each other. We consider distributed systems such that a site (a client site) sends a request message to the other site (a server site) and downloads a program module to execute. We introduce new equivalence relations on the set of sites that regard two sites as equivalent servers if they return semantically equivalent program modules for the same request message. The model introduced here is based on linear logic. Processes, messages, definitions and modules are represented as logical formulas of linear logic. Each site is a multiset of formulas and a system is a collection of multisets. Sending/receiving of messages, unfolding of process calls and downloading of modules are represented as logical inferences of linear logic. As a site is an open-ended system that communicates with the other sites, then the operational semantics of sites is defined as a labeled transition system. We define standard bisimulation equivalences of sites based on the labeled transition system at first. Then new equivalence relations for server sites are defined using the bisimulation equivalences.