随着计算机和网络技术的高速发展,以并发性、分布性和实时性为主要特征的并发与分布式系统已成为计算机的主流研究方向。从C.A. Petri提出Petri网以来,各种从不同侧面反映并发本质的模型被相继提出。在这些模型中,进程代数因概念简洁,可用的数学工具丰富,得到了广泛的研究。在传统的进程代数中,进程间是否能够通信与它们之间的距离无关。而在现实世界中,通信距离受限的现象相当普遍。例如在无线传感器网络中,节点之间的距离直接影响其通信的质量,如果距离超过一定范围,则节点间通信完全不可行;在生物学中,某些细胞之间的信息交换只有在它们的距离小于一定值时才会发生。本文提出了一种进程代数系统,侧重考虑了进程间距离对进程间通信以及观测等效性的影响,并讨论了该系统的行为理论及模态逻辑特征。研究内容主要包括:(1)在CCS的基础上引入位置、距离等概念给出CCS~θ系统的语法,并给出了归约语义和LTS语义用以描述系统的行为。(2)提出了L-互模拟和B-互模拟两种刻画进程等价的概念。L-互模拟表现了在某个位置L的观测者所观测到的进程等价性;B-互模拟反映了观测者的位置以及交互能力对判定进程等价与否的影响。研究了L-互模拟和B-互模拟的基本性质。(3)建立了B-强互模拟的模态逻辑特征及分层B-强互模拟的模态逻辑特征。