Research On Process Calculus With Distance-Limited Communication

With the rapid development of computer and network technology, concurrent and distributed systems, characterized by concurrency, distribution and real time, have a central branch of research in computer science. Since Petri nets were invented by C.A. Petri, many concurrent computation models have been established. Among these models, process algebra is widely studied because of its concise concepts and numerous mathematical tools.In traditional process algebra, communication between processes has nothing to do with the distance between them. However, distance limited communication is widespread in the real world. For example, in wireless sensor networks, the quality of communications is affected by the distance between sensors. Two sensors can't communicate if the distance between them is beyond a certain range. In biology, some cells can communicate only if the distance between them is in a certain range. In this paper, we propose a process calculus focusing on the impact of distance between processes on processes communication and on observation equivalence. Behavior theory and modal logical characterization of the calculus are discussed. The contributions of this paper include the following:(1) Based on CCS, we established a calculus CCSθwith the notions,'location'and'distance'. In order to describe the behavior of our system, the operational semantics is given both in terms of a Reduction Semantics and in terms of a Labeled Transition Semantics.(2) Two concepts, L-bisimulation and B-bisimulation, are introduced to characterize process equivalence. L-bisimulation represents the process equivalence which is observed by an observer in location L. B-bisimulation shows how the locations and abilites of the observer affect process equivalence. Some properties of L-bisimulation and B-bisimulation are studied.(3) Modal logic characterization of B-strong bisimulation and layered B-strong bisimulation are established.