具有行为观察的移动界程演算空间逻辑  

Spatial Logic With Behavioral Observations for Ambient Calculus

作　　者：陈江[1] 林荣德[1] 

机构地区：[1]华侨大学网络信息中心,福建泉州362021

出　　处：《南京师范大学学报（工程技术版）》2011年第4期70-76,共7页Journal of Nanjing Normal University(Engineering and Technology Edition)

基　　金：华侨大学科研基金(11BS121)

摘　　要：界程逻辑中的并发模态副词是观察进程交互行为的关键因素之一,但引入并发模态副词又会导致模型检测的不可判定性.针对这一问题,提出了可判定的、描述移动界程演算进程的空间结构和行为性质的应用界程逻辑.该逻辑定义了空间模态词和行为模态词来直接观察移动进程的空间性质和潜在交互行为性质,并定义了不动点公式来刻画进程的递归性质.为了证明逻辑公式的指称语义的正确性,引入了性质集的概念并证明两者之间的一致性.最后给出了使用应用界程逻辑公式来描述一个资源传输系统在时间和空间上的行为性质的实例.A decidable ambient based spatial logic, named Applied Ambient Logic is proposed, which consists of spatial modal connectives and behavioral modal connectives. In traditional ambient logic, the composition adjunct is very ex- pressive, which makes it possible to observe behavioral properties of processes. However, it is proved that model-chec- king of logics with composition adjunct is not decidable. In Applied Ambient Logic, both spatial modal connectives and behavioral modal connectives are added which can specify spatial and behavioral properties of processes directly, and fix- point modals are also added for properties of recursive processes. A concept of property sets is adopted to describe the features of denotational semantics for logic formulas, and soundness between property-set and denotational semantics is proved. Finally, examples of Applied-Ambient Logic formulas are given which are applied to describe spatial-temporal behavioral properties of a resource transformation system model.

关 键 词：移动界程演算 界程逻辑 空间和行为观察 模型检测 

分 类 号：TP311[自动化与计算机技术—计算机软件与理论]