A concurrent calculus with geographical constraints

Process algebras with name passing have been proposed for concurrent mobile processes. They can be suitable to describe dynamical changes of connections among processes. To describe mobile communication or mobile computing systemshoweverit is necessary to consider locations at which processes run. We propose a description method to design mobile communication systems using a concurrent calculus in this paper. The concept of a field is introduced to model locality of communication. An extension of TT-calculus with a field is proposed. The extension does not include locality represented by a field while most related works treat locality within their languages. A field is given when behavior of a target system is verified in a particular environment. The aim of the extension is to verify and to test connectivity between processes under various geographical constraints. This method could be design-oriented in this context. Equivalence relations with/without location in this calculus are also discussed.