A Notation and Logic for Mobile Computing

Abstract. We de ne a concurrent mobile system as one where independently executing components may migrate through some space during the course of the computation, and where the pattern of connectivity among the components changes as they move in and out of proximity. The de nition is general enough to encompass a system of mobile hosts moving in physical space as well as a system of migrating software agents implemented on a set of possibly non-mobile hosts. In this paper, we present Mobile UNITY, a notation for expressing mobile computations and a logic for reasoning about their temporal properties. Our goal is to nd a minimalist model of mobile computation that will allow us to express mobile components in a modular fashion and to reason formally about the possible behaviors of a system composed from mobile components. A simpli ed serial communication protocol among components which can move in space serves as an illustration for the notation.

• Type: Journal
• Year: 2002
• Where: FMSD
• Authors: Gruia-Catalin Roman, Peter J. McCann
• Keywords: Computation, FMSD 2002, Mobile Components, Mobile Computation