[1]陈江,林荣德.具有行为观察的移动界程演算空间逻辑[J].南京师范大学学报(工程技术版),2011,11(04):070-76.
　Chen Jiang,Lin Rongde.Spatial Logic With Behavioral Observations for Ambient Calculus[J].Journal of Nanjing Normal University(Engineering and Technology),2011,11(04):070-76.
点击复制

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

南京师范大学学报（工程技术版）[ISSN:1006-6977/CN:61-1281/TN]

卷:
11卷
期数:
2011年04期
页码:
070-76
栏目:
出版日期:
2011-12-31

文章信息/Info

Title:
Spatial Logic With Behavioral Observations for Ambient Calculus
作者:
陈江; 林荣德
华侨大学网络信息中心，福建泉州362021
Author(s):
Chen Jiang; Lin Rongde
Computer Network and Information Center,Huaqiao University,Quanzhou 362021,China
关键词:
移动界程演算; 界程逻辑; 空间和行为观察; 模型检测
Keywords:
ambient calculus; ambient based logic; spatial and behavioral observations; model checking
分类号:
TP301
摘要:
界程逻辑中的并发模态副词是观察进程交互行为的关键因素之一,但引入并发模态副词又会导致模型检测的不可判定性.针对这一问题,提出了可判定的、描述移动界程演算进程的空间结构和行为性质的应用界程逻辑.该逻辑定义了空间模态词和行为模态词来直接观察移动进程的空间性质和潜在交互行为性质,并定义了不动点公式来刻画进程的递归性质.为了证明逻辑公式的指称语义的正确性,引入了性质集的概念并证明两者之间的一致性.最后给出了使用应用界程逻辑公式来描述一个资源传输系统在时间和空间上的行为性质的实例.
Abstract:
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 expressive， which makes it possible to observe behavioral properties of processes． However，it is proved that model-checking 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 fixpoint 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．

参考文献/References:

［1］Cardelli L，Gordon A D． Anytime，anywhere: Modal logics for mobile ambients［C］/ / POLP 2000． Virginia Gold: ACM Press， 2000: 365-377．
［2］Cardelli L，Gordon A D． Mobile ambients［J］． Foundations of Software Science and Computation Structures( LNCS) ，1998， 1378: 140-155．
［3］Hirschkoff D，Lozes ，Sangiorgi D． On the expressiveness of the ambient logic［J］． Logical Methods in Computer Science， 2006，2 ( 2) : 1-35．
［4］Sangiorgi D． Extensionality and intensionality of the ambient logics［J］． ACM SIGPLAN Notices，2001， 36( 3) : 4-13．
［5］Charatonik W． The complexity of model checking mobile ambients［C］/ / Proceedings of the 4th International Conference on Foundations of Software Science and Computation Structures ( FoSSaCS 2001) ，LNCS 2030． Berlin: Springer-Verlag，2001: 152-167．
［6］Charatonik W，Talbot J M． The decidability of model checking mobile ambients［C］/ / Proceedings of the 15th Annual Conference of the European Association for Computer Science Logic． Berlin: Springer，2001: 339-354．
［7］颜锋，陈韬略，韩婷婷，等． 空间逻辑的一个定义框架及其可判定性［J］． 计算机科学，2006， 33( 6) : 7-10． Yan Feng，Chen Taolue，Han Tingting，et al． A definition framework of spatial logic and decedability［J］． Computer Science， 2006， 33( 6) : 7-10． ( in Chinese)
［8］Fu Y． Fair ambients［J］． Acta Informatica，2007，43( 8) : 535-594．
［9］Charatonik W，Gordon A D，Talbot J M． Finite-control mobile ambients［C］/ / 11th European Symposium on Programming ( ESOP 2002) ，LNCS2305． Berlin: Springer，2002: 295-313．
［10］林荣德． 移动界程演算及模型检测应用的关键问题研究［D］． 广州: 华南理工大学计算机科学与工程学院，2010． Lin Rongde． Research on key issues of mobile ambients and model checking applications［D］． Guangzhou: College of Computer Science and Engineering，South China University of Technology，2010． ( in Chinese)
［11］Caires L． Behavioral and spatial observations in a logic for the π-calculus［J］． Foundations of Software Science and Computation Structures( LNCS) ，2004，2987: 72-89．
［12］Lin H． A predicate spatial logic for mobile processes［J］． Science in China Serise F: Information Sciences，2004，47( 3) : 394-408．
［13］Lin H． A predicate mu-calculus for mobile ambients［J］． Journal of Computer Science and Technology，2005，20( 2) : 95- 104．

备注/Memo

备注/Memo:
基金项目: 华侨大学科研基金( 11BS121) ．
通讯联系人: 陈江，讲师，研究方向: 网络计算、形式化建模等． E-mail: chenj@ hqu． edu． Cn
更新日期/Last Update: 2013-03-21